Skip to content

Commit

Permalink
Test install target on CI (docker only)
Browse files Browse the repository at this point in the history
We match the various opam install targets.

The non-docker targets are being done separately, since I'm less
confident about how to get docker working.

Fixes #1732

Use COQBIN

Work around mit-plv/coqutil#104

Comment out install-dev test
  • Loading branch information
JasonGross committed Nov 19, 2023
1 parent 2f79c57 commit 2a94a62
Showing 1 changed file with 32 additions and 0 deletions.
32 changes: 32 additions & 0 deletions .github/workflows/coq-docker.yml
Original file line number Diff line number Diff line change
Expand Up @@ -89,6 +89,38 @@ jobs:
name: ExtractionHaskell-${{ matrix.env.COQ_VERSION }}
path: src/ExtractionHaskell
if: always ()
- name: install
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: |
# dry run first to run coqdep, etc, since sudo can't find coqdep, but non-sudo can't install
etc/ci/github-actions-docker-make.sh ${EXTRA_GH_REPORTIFY} --dry-run EXTERNAL_DEPENDENCIES=1 SKIP_COQSCRIPTS_INCLUDE=1 install install-standalone-ocaml
sudo git config --global --add safe.directory "*"
sudo make EXTERNAL_DEPENDENCIES=1 SKIP_COQSCRIPTS_INCLUDE=1 COQBIN="$(dirname "$(which coqc)")/" install install-standalone-ocaml
- name: install-without-bedrock2
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} --dry-run EXTERNAL_DEPENDENCIES=1 SKIP_BEDROCK2=1 install-without-bedrock2 install-standalone-ocaml
sudo git config --global --add safe.directory "*"
sudo make EXTERNAL_DEPENDENCIES=1 SKIP_BEDROCK2=1 COQBIN="$(dirname "$(which coqc)")/" install-without-bedrock2 install-standalone-ocaml
# blocking on https://github.com/mit-plv/bedrock2/issues/388
# - name: install-dev
# 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} --dry-run EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1 install install-standalone-ocaml || true # no idea why make fails even with --dry-run here but succeeds above
# sudo git config --global --add safe.directory "*"
# sudo make EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1 COQBIN="$(dirname "$(which coqc)")/" install install-standalone-ocaml
- name: display timing info
run: cat time-of-build-pretty.log
- name: display per-line timing info
Expand Down

0 comments on commit 2a94a62

Please sign in to comment.