From 7214977e3783ce47bdd92264dd60d9b1025a3e7d Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 15 Nov 2023 10:17:34 -0800 Subject: [PATCH 1/3] Test install target on CI (docker only) 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 https://github.com/mit-plv/coqutil/issues/104 --- .github/workflows/coq-docker.yml | 31 +++++++++++++++++++++++++++++++ 1 file changed, 31 insertions(+) diff --git a/.github/workflows/coq-docker.yml b/.github/workflows/coq-docker.yml index 21427763eb..4acd5c10c8 100644 --- a/.github/workflows/coq-docker.yml +++ b/.github/workflows/coq-docker.yml @@ -89,6 +89,37 @@ 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 + - 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 + 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 From 20a60868f251cff3c7ca0aac8d3e6c83819d5f40 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 19 Nov 2023 07:21:15 -0800 Subject: [PATCH 2/3] Update coq-docker.yml --- .github/workflows/coq-docker.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/coq-docker.yml b/.github/workflows/coq-docker.yml index 4acd5c10c8..0a70121d54 100644 --- a/.github/workflows/coq-docker.yml +++ b/.github/workflows/coq-docker.yml @@ -117,7 +117,7 @@ jobs: 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 + 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 From 4f167c83add8cfad8fe1a7dd88559e4a8e0cffb6 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 19 Nov 2023 12:29:36 -0800 Subject: [PATCH 3/3] Comment out install-dev test --- .github/workflows/coq-docker.yml | 21 +++++++++++---------- 1 file changed, 11 insertions(+), 10 deletions(-) diff --git a/.github/workflows/coq-docker.yml b/.github/workflows/coq-docker.yml index 0a70121d54..c8fcda1934 100644 --- a/.github/workflows/coq-docker.yml +++ b/.github/workflows/coq-docker.yml @@ -110,16 +110,17 @@ jobs: 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 - - 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 +# 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