From 00a4b8ea16d0764b72a27adfb5d1e8821494c666 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Sun, 19 Nov 2023 20:45:57 -0800
Subject: [PATCH] Test install target on CI (docker only) (#1733)

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
---
 .github/workflows/coq-docker.yml | 32 ++++++++++++++++++++++++++++++++
 1 file changed, 32 insertions(+)

diff --git a/.github/workflows/coq-docker.yml b/.github/workflows/coq-docker.yml
index 73fb0dae30..9b0856b096 100644
--- a/.github/workflows/coq-docker.yml
+++ b/.github/workflows/coq-docker.yml
@@ -126,6 +126,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