Enable usage of GHA environment-files commands (#90)

This allows the use of `>> $GITHUB_ENV`, `>> $GITHUB_OUTPUT`, and `>> $GITHUB_STEP_SUMMARY` to pass information to subsequent steps. Co-authored-by: Jason Gross <[email protected]> Co-authored-by: Erik Martin-Dorel <[email protected]>
coq-community · May 12, 2024 · 7c98410 · 7c98410
1 parent 89cff67
commit 7c98410
Show file tree

Hide file tree

Showing 3 changed files with 95 additions and 1 deletion.
diff --git a/.github/workflows/coq-demo.yml b/.github/workflows/coq-demo.yml
@@ -374,3 +374,60 @@ jobs:
           path: artifacts/
           if-no-files-found: error  # 'warn' or 'ignore' are also available, defaults to `warn`
           retention-days: 8
+
+
+  # The following job illustrates the upload of github environment files.
+
+  demo-9:
+    name: custom_image / docker-mathcomp / opam / env+GITHUB_ENV
+    runs-on: ubuntu-latest
+    strategy:
+      matrix:
+        image:
+          - 'mathcomp/mathcomp:latest-coq-8.19'
+      fail-fast: false  # don't stop jobs if one fails
+    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:
+          repository: 'erikmd/docker-coq-github-action-demo'
+          ref: 'master'
+      - 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
+        id: docker-coq-action
+        env:
+          # Pass string data to docker-coq-action
+          after_ok: 'Test successful!'
+        with:
+          export: 'COQ_IMAGE after_ok'
+          custom_image: ${{ matrix.image }}
+          opam_file: 'coq-demo.opam'
+          before_script: |
+            # Pass step outputs (Docker image name) to next step
+            echo "docker_image=$COQ_IMAGE" >> "$GITHUB_OUTPUT"
+          after_script: |
+            # Pass env vars (Coq version string...) to next step
+            echo "coq_version=$(opam var coq:version)" >> "$GITHUB_ENV"
+            echo "some_variable=expected_value" >> "$GITHUB_ENV"
+            # Display Markdown summary
+            [ -n "$after_ok" ]
+            echo "### $after_ok :rocket:" >> "$GITHUB_STEP_SUMMARY"
+      - name: Next step
+        env:
+          docker_image: ${{ steps.docker-coq-action.outputs.docker_image}}
+        run: |
+          : Summary
+          echo "Previous step pulled Docker image: $docker_image"
+          [ -n "$docker_image" ]
+          echo "Previous step used: coq_version=$coq_version"
+          [ -n "$coq_version" ]
+          echo "some_variable=$some_variable"
+          [ "$some_variable" = "expected_value" ]
diff --git a/README.md b/README.md
@@ -385,6 +385,9 @@ steps:
       custom_image: ${{ matrix.image }}
 ```
 
+If ever you want to retrieve the Docker image name within the CI script, you can 
+use the [`export`](#export) keyword to expose the `COQ_IMAGE` internal variable.
+
 #### `export`
 
 *Optional*
@@ -644,6 +647,20 @@ strategy:
           retention-days: 8
 ```
 
+### GitHub Actions environment files
+
+Recall that `docker-coq-action` runs your CI script in a Docker container,
+the filesystem of which being isolated from the GitHub runner.
+
+Still, `docker-coq-action` bind-mounts some special paths for
+[GitHub Actions environment files](https://docs.github.com/en/actions/using-workflows/workflow-commands-for-github-actions#environment-files),
+so that `"$GITHUB_ENV"`, `"$GITHUB_OUTPUT"`, and `"$GITHUB_STEP_SUMMARY"` can be used
+in (parts of) the [`custom_script`](#custom_script) in order to pass environment
+variables or step outputs to the following steps, or set a Markdown summary.
+
+Conversely, the [`export`](#export) keyword can be used to pass variables
+from the previous step to `docker-coq-action`.
+
 ### Install Debian packages
 
 If you use `docker-coq-action` with a

diff --git a/entrypoint.sh b/entrypoint.sh
@@ -25,6 +25,18 @@ echo "GITHUB_REPOSITORY=$GITHUB_REPOSITORY"
 echo "RUNNER_OS=$RUNNER_OS"
 echo "RUNNER_TEMP=$RUNNER_TEMP"
 echo "RUNNER_WORKSPACE=$RUNNER_WORKSPACE"
+
+# We want to bind-mount the dirname of $GITHUB_ENV.
+# $GITHUB_ENV is typically /home/runner/work/_temp/_runner_file_commands/set_env_87406d6e-4979-4d42-98e1-3dab1f48b13a
+# so $(dirname "$GITHUB_ENV") is typically /home/runner/work/_temp/_runner_file_commands on the host.
+# We also notice that $RUNNER_WORKSPACE is typically /home/runner/work/${GITHUB_REPOSITORY%/*} (e.g. /home/runner/work/docker-coq-action).
+# Hence this hardcoded yet as-general-as-possible path:
+HOST_GITHUB_RUNNER_FILE_COMMANDS="${RUNNER_WORKSPACE%/*}/_temp/_runner_file_commands"
+# Another hardcoded path:
+DIR_FILE_COMMANDS="/github/file_commands"
+echo "HOST_GITHUB_RUNNER_FILE_COMMANDS=$HOST_GITHUB_RUNNER_FILE_COMMANDS"
+echo "DIR_FILE_COMMANDS=$DIR_FILE_COMMANDS"
+
 # Assuming you used https://github.com/actions/checkout,
 # the GITHUB_WORKSPACE variable corresponds to the following host dir:
 # ${RUNNER_WORKSPACE}/${GITHUB_REPOSITORY#*/}, see also
@@ -192,6 +204,13 @@ if test -z "$INPUT_CUSTOM_SCRIPT_EXPANDED"; then
     exit 1
 fi
 
+startGroup "Set permissions for GHA environment files in $DIR_FILE_COMMANDS"
+# a.k.a. $HOST_GITHUB_RUNNER_FILE_COMMANDS on the host.
+
+chmod -R a+rw "$DIR_FILE_COMMANDS"
+
+endGroup
+
 startGroup "Pull docker image"
 
 echo COQ_IMAGE="$COQ_IMAGE"
@@ -203,8 +222,9 @@ export COQ_IMAGE
 
 ## Note to docker-coq-action maintainers: Run ./helper.sh gen & Copy min.sh
 # shellcheck disable=SC2046,SC2086
-docker run --pull=never -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 GITHUB_ENV -e GITHUB_OUTPUT -e GITHUB_STEP_SUMMARY -e WORKDIR="$WORKDIR" -e PACKAGE="$PACKAGE" \
        -v "$HOST_WORKSPACE_REPO:$PWD" -w "$PWD" \
+       -v "$HOST_GITHUB_RUNNER_FILE_COMMANDS:$DIR_FILE_COMMANDS" \
        "$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
 export PS4='+ \e[33;1m(\$0 @ line \$LINENO) \$\e[0m '; set -ex