Test install target on CI (no docker) (#1734)

We match the various opam install targets. Skipping docker for now due to sudo problems, that's coming in another PR. Fixes #1732
mit-plv · Nov 16, 2023 · fa68a25 · fa68a25
1 parent 60b5d0e
commit fa68a25
Show file tree

Hide file tree

Showing 4 changed files with 43 additions and 1 deletion.
diff --git a/.github/workflows/coq-alpine.yml b/.github/workflows/coq-alpine.yml
@@ -36,7 +36,7 @@ jobs:
       with:
         branch: ${{ matrix.alpine }}
         extra-repositories: https://dl-cdn.alpinelinux.org/alpine/edge/testing
-        packages: git make jq gcc musl-dev python3 ocaml ocaml-findlib ghc cabal coq ocaml-zarith bash
+        packages: git make jq gcc musl-dev python3 ocaml ocaml-findlib ghc cabal coq ocaml-zarith bash sudo
     - name: work around coq issue 15663
       shell: alpine.sh --root {0}
       run: |
@@ -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

diff --git a/.github/workflows/coq-debian.yml b/.github/workflows/coq-debian.yml
@@ -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

diff --git a/.github/workflows/coq-macos.yml b/.github/workflows/coq-macos.yml
@@ -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

diff --git a/.github/workflows/coq-windows.yml b/.github/workflows/coq-windows.yml
@@ -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