Document how to ensure a single Coq version is used across multiple invocations of the action
Closed this issue · 6 comments
Fiat Crypto has a workflow where we invoke the action multiple times, as in
- name: deps
uses: coq-community/docker-coq-action@v1
with:
coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }}
ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }}
export: CI ALLOW_DIFF COQCHKEXTRAFLAGS
custom_script: etc/ci/github-actions-docker-make.sh -j2 deps
- name: all-except-generated
uses: coq-community/docker-coq-action@v1
with:
coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }}
ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }}
export: CI ALLOW_DIFF COQCHKEXTRAFLAGS
custom_script: etc/ci/github-actions-docker-make.sh ${EXTRA_GH_REPORTIFY} -j2 all-except-generated
- name: generated-files
run: etc/ci/github-actions-make.sh ${EXTRA_GH_REPORTIFY} -f Makefile.examples -j2 generated-files
if: github.event_name == 'pull_request' || ${{ matrix.env.COQ_VERSION }} != 'master'
- run: tar -czvf generated-files.tgz fiat-*/
if: ${{ failure() }}
- name: upload generated files
uses: actions/upload-artifact@v3
with:
name: generated-files-${{ matrix.env.COQ_VERSION }}
path: generated-files.tgz
- name: standalone-haskell
run: etc/ci/github-actions-make.sh -f Makefile.standalone -j1 standalone-haskell GHCFLAGS='+RTS -M6G -RTS'
- name: validate
uses: coq-community/docker-coq-action@v1
with:
coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }}
ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }}
export: CI ALLOW_DIFF COQCHKEXTRAFLAGS
custom_script: etc/ci/github-actions-docker-make.sh TIMED=1 validate COQCHKFLAGS="-o ${COQCHKEXTRAFLAGS}"
if: env.SKIP_VALIDATE == '' && github.event_name != 'pull_request'
This has a couple advantages:
- we can order steps the way we want, which is not possible if we can only invoke the docker action once (unless I want to figure out how to hand-code a replacement for actions/upload-artifact from inside docker, which I don't)
- we can make use of other actions, like installing Haskell and uploading artifacts
- we get more readable logs because we can make separate steps
However, there's a big downside, which is that sometimes "coq.dev" changes meaning between one step and the next, and this causes our CI to do duplicative work or fail outright.
I'd like to be able to somehow record the particular commit of Coq or docker image or something in a file or GitHub environment variable (I think one step can persistently modify the environment for subsequent steps by writing to a file), but I'm not sure how to get the relevant information from inside docker, nor how to tell the next step to use the same version. How can I set up my script to do this?
Hi @JasonGross! (sorry I didn't see the notification of this issue earlier), thanks for your input 👍
I hope to be able to dedicate a slot on docker-coq/docker-keeper/docker-coq-action evolutions soon. Meanwhile, here is some feedback:
unless I want to figure out how to hand-code a replacement for actions/upload-artifact from inside docker, which I don't.
curl is available from within the docker-coq-action container shell, but as documented in this §, the natural way to upload artifacts after a docker-coq-action run is to use actions/upload-artifact@v2 afterwards.
So my first question is: are you sure you need to use docker-coq-action twice?
If yes, I agree that if the underlying coqorg/coq:dev-* image changes between the two runs, you have an issue ✅
However, I think this behavior is easy to change, given the underlying architecture of GHA+docker-coq-action:
I would just replace this command:
docker-coq-action/entrypoint.sh
Line 198 in a5d9d3b
with
docker image inspect "$COQ_IMAGE" --format="Reusing existing local image." || docker pull "$COQ_IMAGE"
If you're interested, I could push one such variant of docker-coq-action in a branch, so you could test in production… and @Zimmi48 and I would then decide whether this behavior must be standard, or triggered by a boolean option. WDYT?
Otherwise, you said:
I'd like to be able to somehow record the particular commit of Coq
This is easy by printing the pin list using opam.
or docker image
I don't think the $COQ_IMAGE variable is available from within the container shell. But I could export it if you want.
But of course, if ever the image changed, one cannot pull the old one anew.
as documented in this §, the natural way to upload artifacts after a docker-coq-action run is to use
actions/upload-artifact@v2afterwards.
Note also that the seemingly Travis/GitLab-inspired keywords in docker-coq-action (before_install:, install: etc.) specifically came from our intent to encourage users writing their whole test script this way, wrapped in a docker-coq-action call (which, BTW, is a portable bash environment, that can just as well be run outside GHA; except of course the GHA-specific tasks such as uploading artifacts or create a release).
Finally on a related topic, note that it is already possible to override the docker environment just before the docker pull mentioned above is done, e.g., docker-coq-action happens to be able to pull images from a private Docker registry.
Proof-of-concept code (that I have recently tested; but not publicly documented up to now!):
(…)
env:
REGISTRY: ghcr.io
IMAGE_NAME: orga-name/repo-name
IMAGE_TAG: latest
jobs:
test:
permissions:
contents: read
packages: read
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v2
- uses: coq-community/docker-coq-action@v1
with:
# override entrypoint to login to GH container registry beforehand
# to allow docker-coq-action to pull a private image from ghcr.io.
entrypoint: /bin/sh
args: -c "/bin/echo \"${{ secrets.GITHUB_TOKEN }}\" | docker login ${{ env.REGISTRY }} -u ${{ github.actor }} --password-stdin && exec /app/entrypoint.sh \"$@\"" sh
custom_image: ${{ env.REGISTRY }}/${{ env.IMAGE_NAME }}:${{ env.IMAGE_TAG }}
custom_script: |
(…)So my first question is: are you sure you need to use docker-coq-action twice?
Need, no. Want to, very much yes. I want control over grouping of logs (GH is very bad at loading grouping of long logs within a single high-level step), I want to see at a glance what failed and not have to go digging for it, I want to be able to tell which steps failed for knowing which future steps to run, I want to be able to see at a glance how long the various steps took, and I want to be able to interleave Coq steps with steps that are very painful to run in the docker action, like testing the build of extracted Haskell files in various versions of Haskell
If you're interested, I could push one such variant of docker-coq-action in a branch, so you could test in production… and @Zimmi48 and I would then decide whether this behavior must be standard, or triggered by a boolean option. WDYT?
This would be very nice! Am I understanding correctly that this would then pin the image version to whatever it was when the first step was run? I can't imagine an action wanting a different behavior...
I don't think the
$COQ_IMAGEvariable is available from within the container shell. But I could export it if you want.But of course, if ever the image changed, one cannot pull the old one anew.
It sounds like there's no way to force the second step to reuse the image from the first step with this scheme, then? (If I'm right, then it's no use to me to have this exported.)
This would be very nice! Am I understanding correctly that this would then pin the image version to whatever it was when the first step was run? I can't imagine an action wanting a different behavior...
That's also as I understand it, and if that's correct, then I agree this should probably be the default behavior.
Hi @Zimmi48 OK, thanks!
@JasonGross Just opened PR #82; feel free to test it if you can/want:
- uses: coq-community/docker-coq-action@pull-if-missingI'll do a release tonight-or-tomorrow-Tuesday-morning.