Merge pull request #82 from coq-community/pull-if-missing

Don't pull `$COQ_IMAGE` if it exists locally
coq-community · Nov 24, 2022 · 56a68e2 · 56a68e2
2 parents a5d9d3b + cae2de1
commit 56a68e2
Show file tree

Hide file tree

Showing 3 changed files with 72 additions and 2 deletions.
diff --git a/.github/workflows/gha-rt.yml b/.github/workflows/gha-rt.yml
@@ -9,7 +9,10 @@ on:
       - "**"  # forall submitted Pull Requests
 jobs:
 
+  # The following job tests the use of single quotes in before_script.
+
   issue-40:
+    name: test / script with quotes / custom_image / opam
     # interpolated scripts couldn't contain single-quotes
     runs-on: ubuntu-latest
     steps:
@@ -30,3 +33,39 @@ jobs:
             opam repo list
             opam repo add --all-switches --set-default coq-extra-dev 'https://coq.inria.fr/opam/extra-dev'
             opam repo list
+
+  # The following job illustrates the use of two successive docker-coq-action calls.
+  issue-80:
+    name: test / multi-call / custom_image / custom_script
+    runs-on: ubuntu-latest
+    steps:
+      ################################################################
+      # Begin GHA_TEST_ENV # You should remove this GHA_TEST_ENV block
+      #                    # if you copy this demo workflow elsewhere!
+      - uses: actions/checkout@v3
+        with:
+          path: 'docker-coq-action'
+      - uses: './docker-coq-action'
+        # End GHA_TEST_ENV
+        ##################
+        # - uses: actions/checkout@v3
+        # - uses: coq-community/docker-coq-action@v1
+        name: Run docker-coq-action, SHOULD FAIL
+        continue-on-error: true
+        with:
+          custom_image: mock-image # non-existing image
+          custom_script: |
+            cat /etc/os-release
+      - name: Pull mock image
+        run: |
+          docker pull ubuntu:latest
+          docker tag ubuntu:latest mock-image
+      - uses: './docker-coq-action'
+        ##################
+        # - uses: actions/checkout@v3
+        # - uses: coq-community/docker-coq-action@v1
+        name: Run docker-coq-action, SHOULD SUCCEED
+        with:
+          custom_image: mock-image # non-existing image
+          custom_script: |
+            cat /etc/os-release
diff --git a/.github/workflows/python-demo.yml b/.github/workflows/python-demo.yml
@@ -54,3 +54,34 @@ jobs:
             endGroup
         # in case there is a permission mismatch issue at GHA cleanup time,
         # see https://github.com/coq-community/docker-coq-action#permissions
+
+  # ######################################################################
+  # This job illustrates how to run a docker command before the entrypoint
+  # ######################################################################
+  entrypoint-demo:
+    name: entrypoint / custom_image / python:3
+    runs-on: ubuntu-latest
+    env:
+      REGISTRY: docker.io
+      IMAGE_NAME: python
+      IMAGE_TAG: 3
+    steps:
+      ################################################################
+      # Begin GHA_TEST_ENV # You should remove this GHA_TEST_ENV block
+      #                    # if you copy this demo workflow elsewhere!
+      - uses: actions/checkout@v2
+        with:
+          path: 'docker-coq-action'
+      - uses: './docker-coq-action'
+        # End GHA_TEST_ENV
+        ##################
+        # - uses: actions/checkout@v2
+        # - uses: coq-community/docker-coq-action@v1
+        with:
+          entrypoint: /bin/sh
+          # see also https://github.com/coq-community/docker-coq-action/issues/80#issuecomment-1321272915
+          # args: -c "/bin/echo \"${{ secrets.GITHUB_TOKEN }}\" | docker login ${{ env.REGISTRY }} -u ${{ github.actor }} --password-stdin && exec /app/entrypoint.sh \"$@\"" sh
+          args: -c "docker pull ${{ env.REGISTRY }}/${{ env.IMAGE_NAME }}:${{ env.IMAGE_TAG }} && exec /app/entrypoint.sh \"$@\"" sh
+          custom_image: ${{ env.REGISTRY }}/${{ env.IMAGE_NAME }}:${{ env.IMAGE_TAG }}
+          custom_script: |
+            python --version
diff --git a/entrypoint.sh b/entrypoint.sh
@@ -195,13 +195,13 @@ fi
 startGroup "Pull docker image"
 
 echo COQ_IMAGE="$COQ_IMAGE"
-docker pull "$COQ_IMAGE"
+docker image inspect "$COQ_IMAGE" --format="Reusing existing local image." || docker pull "$COQ_IMAGE"
 
 endGroup
 
 ## Note to docker-coq-action maintainers: Run ./helper.sh gen & Copy min.sh
 # shellcheck disable=SC2046,SC2086
-docker run -i --init --rm --name=COQ $( [ -n "$INPUT_EXPORT" ] && printf -- "-e %s " $INPUT_EXPORT ) -e WORKDIR="$WORKDIR" -e PACKAGE="$PACKAGE" \
+docker run --pull=never -i --init --rm --name=COQ $( [ -n "$INPUT_EXPORT" ] && printf -- "-e %s " $INPUT_EXPORT ) -e WORKDIR="$WORKDIR" -e PACKAGE="$PACKAGE" \
        -v "$HOST_WORKSPACE_REPO:$PWD" -w "$PWD" \
        "$COQ_IMAGE" /bin/bash --login -c "
 exec 2>&1 ; endGroup () {  {  init_opts=\"\$-\"; set +x ; } 2> /dev/null; if [ -n \"\$startTime\" ]; then endTime=\$(date -u +%s); echo \"::endgroup::\"; printf \"↳ \"; date -u -d \"@\$((endTime - startTime))\" '+%-Hh %-Mm %-Ss'; echo; unset startTime; else echo 'Error: missing startGroup command.'; case \"\$init_opts\" in  *x*) set -x ;; esac; return 1; fi; case \"\$init_opts\" in  *x*) set -x ;; esac; } ; startGroup () {  {  init_opts=\"\$-\"; set +x ; } 2> /dev/null; if [ -n \"\$startTime\" ]; then endGroup; fi; if [ \$# -ge 1 ]; then groupTitle=\"\$*\"; else groupTitle=\"Unnamed group\"; fi; echo; echo \"::group::\$groupTitle\"; startTime=\$(date -u +%s); case \"\$init_opts\" in  *x*) set -x ;; esac; } # generated from helper.sh