From 7c98410bb26905e003d5b5ed964d91e6c87c35ae Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 12 May 2024 07:57:40 -0700 Subject: [PATCH] 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 Co-authored-by: Erik Martin-Dorel --- .github/workflows/coq-demo.yml | 57 ++++++++++++++++++++++++++++++++++ README.md | 17 ++++++++++ entrypoint.sh | 22 ++++++++++++- 3 files changed, 95 insertions(+), 1 deletion(-) diff --git a/.github/workflows/coq-demo.yml b/.github/workflows/coq-demo.yml index 187fb75..78e0284 100644 --- 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 index 74441d4..0f9acf0 100644 --- 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 index 966f516..c3c5024 100755 --- 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