Skip to content

Commit

Permalink
[CI] Remove coq-bignums before CI
Browse files Browse the repository at this point in the history
Otherwise the test are run with the bignums already in the Docker
image rather than the one just built by the CI.
  • Loading branch information
proux01 committed Feb 13, 2024
1 parent 3885b1a commit 83c83b9
Showing 1 changed file with 20 additions and 3 deletions.
23 changes: 20 additions & 3 deletions .github/workflows/docker-action.yml
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
# Beware not to destroy this file when regenerating it from meta.yml

name: Docker CI

on:
Expand Down Expand Up @@ -25,9 +27,24 @@ jobs:
with:
opam_file: 'coq-bignums.opam'
custom_image: ${{ matrix.image }}
export: 'OPAMWITHTEST'
env:
OPAMWITHTEST: 'true'
custom_script: |
startGroup Print opam config
opam config list; opam repo list; opam list
echo NJOBS=${NJOBS}
endGroup
startGroup Build coq-bignums
opam remove -y coq-bignums # remove coq-bignums already in image
opam pin add -n -y -k path coq-bignums .
opam install -y -v -j ${NJOBS}
opam list
endGroup
startGroup Test coq-bignums
git clean -dxf .
make -j ${NJOBS} -C tests
endGroup
startGroup Uninstallation test
opam remove -y coq-bignums
endGroup
# See also:
# https://github.com/coq-community/docker-coq-action#readme
Expand Down

0 comments on commit 83c83b9

Please sign in to comment.