Skip to content

Commit

Permalink
Test install target on CI
Browse files Browse the repository at this point in the history
We match the fiat-crypto-with-bedrock opam install targets.

Fixes #1732
  • Loading branch information
JasonGross committed Nov 15, 2023
1 parent 5450a10 commit 0028ed1
Show file tree
Hide file tree
Showing 5 changed files with 66 additions and 0 deletions.
9 changes: 9 additions & 0 deletions .github/workflows/coq-alpine.yml
Original file line number Diff line number Diff line change
Expand Up @@ -91,6 +91,15 @@ jobs:
- name: only-test-amd64-files-lite
shell: alpine.sh {0}
run: make TIMED=1 TIMING=1 -j2 only-test-amd64-files-lite SLOWEST_FIRST=1
- name: install
shell: alpine.sh {0}
run: sudo make EXTERNAL_DEPENDENCIES=1 SKIP_COQSCRIPTS_INCLUDE=1 install install-standalone-ocaml
- name: install-without-bedrock2
shell: alpine.sh {0}
run: sudo make EXTERNAL_DEPENDENCIES=1 SKIP_BEDROCK2=1 install-without-bedrock2 install-standalone-ocaml
- name: install-dev
shell: alpine.sh {0}
run: sudo make EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1 install install-standalone-ocaml
- name: display timing info
run: cat time-of-build-pretty.log || true
- name: display per-line timing info
Expand Down
9 changes: 9 additions & 0 deletions .github/workflows/coq-debian.yml
Original file line number Diff line number Diff line change
Expand Up @@ -83,6 +83,15 @@ jobs:
- name: only-test-amd64-files-lite
shell: in-debian-chroot.sh {0}
run: etc/ci/github-actions-make.sh -j2 only-test-amd64-files-lite SLOWEST_FIRST=1
- name: install
shell: in-debian-chroot.sh {0}
run: sudo etc/ci/github-actions-make.sh EXTERNAL_DEPENDENCIES=1 SKIP_COQSCRIPTS_INCLUDE=1 install install-standalone-ocaml
- name: install-without-bedrock2
shell: in-debian-chroot.sh {0}
run: sudo etc/ci/github-actions-make.sh EXTERNAL_DEPENDENCIES=1 SKIP_BEDROCK2=1 install-without-bedrock2 install-standalone-ocaml
- name: install-dev
shell: in-debian-chroot.sh {0}
run: sudo etc/ci/github-actions-make.sh EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1 install install-standalone-ocaml
- name: display timing info
run: cat time-of-build-pretty.log
- name: display per-line timing info
Expand Down
24 changes: 24 additions & 0 deletions .github/workflows/coq-docker.yml
Original file line number Diff line number Diff line change
Expand Up @@ -89,6 +89,30 @@ 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: |
etc/ci/github-actions-docker-make.sh ${EXTRA_GH_REPORTIFY} EXTERNAL_DEPENDENCIES=1 SKIP_COQSCRIPTS_INCLUDE=1 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} EXTERNAL_DEPENDENCIES=1 SKIP_BEDROCK2=1 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} EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1 install install-standalone-ocaml
- name: display timing info
run: cat time-of-build-pretty.log
- name: display per-line timing info
Expand Down
12 changes: 12 additions & 0 deletions .github/workflows/coq-macos.yml
Original file line number Diff line number Diff line change
Expand Up @@ -85,6 +85,18 @@ jobs:
with:
name: standalone-macos
path: dist/fiat_crypto
- name: install
run: |
eval $(opam env)
etc/ci/github-actions-make.sh EXTERNAL_DEPENDENCIES=1 SKIP_COQSCRIPTS_INCLUDE=1 install install-standalone-ocaml
- name: install-without-bedrock2
run: |
eval $(opam env)
etc/ci/github-actions-make.sh EXTERNAL_DEPENDENCIES=1 SKIP_BEDROCK2=1 install-without-bedrock2 install-standalone-ocaml
- name: install-dev
run: |
eval $(opam env)
etc/ci/github-actions-make.sh EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1 install install-standalone-ocaml
- name: display timing info
run: cat time-of-build-pretty.log
- name: display per-line timing info
Expand Down
12 changes: 12 additions & 0 deletions .github/workflows/coq-windows.yml
Original file line number Diff line number Diff line change
Expand Up @@ -102,6 +102,18 @@ jobs:
with:
name: standalone-windows
path: dist/fiat_crypto.exe
- name: install
run: |
%CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- etc/ci/github-actions-make.sh EXTERNAL_DEPENDENCIES=1 SKIP_COQSCRIPTS_INCLUDE=1 install install-standalone-ocaml'
shell: cmd
- name: install-without-bedrock2
run: |
%CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- etc/ci/github-actions-make.sh EXTERNAL_DEPENDENCIES=1 SKIP_BEDROCK2=1 install-without-bedrock2 install-standalone-ocaml'
shell: cmd
- name: install-dev
run: |
%CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- etc/ci/github-actions-make.sh EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1 install install-standalone-ocaml'
shell: cmd
- name: display timing info
run: type time-of-build-pretty.log
shell: cmd
Expand Down

0 comments on commit 0028ed1

Please sign in to comment.