Fix CI

PrincetonUniversity · Nov 23, 2021 · 842d6ae · 842d6ae
1 parent 3d03042
commit 842d6ae
Show file tree

Hide file tree

Showing 3 changed files with 14 additions and 13 deletions.
diff --git a/.github/workflows/coq-action.yml b/.github/workflows/coq-action.yml
@@ -25,9 +25,10 @@ jobs:
           - coq-vst
           - coq-vst-32
     steps:
-      - uses: actions/checkout@v2
-      - name: Checkout submodules
-        uses: textbook/[email protected]
+      - name: Checkout
+        uses: actions/checkout@v2
+        with:
+          submodules: recursive
       - uses: coq-community/docker-coq-action@v1
         with:
           opam_file: ${{ matrix.opam_name }}.opam

diff --git a/coq-vst-32.opam b/coq-vst-32.opam
@@ -17,16 +17,16 @@ dev-repo: "git+https://github.com/PrincetonUniversity/VST.git"
 bug-reports: "https://github.com/PrincetonUniversity/VST/issues"
 license: "https://raw.githubusercontent.com/PrincetonUniversity/VST/master/LICENSE"
 build: [
-  [make "BITSIZE=32" "depend"]
-  [make "BITSIZE=32" "-j%{jobs}%" "msl" "sepcomp" "veric" "floyd"]
+  [make "COMPCERT=bundled" "BITSIZE=32" "depend"]
+  [make "COMPCERT=bundled" "BITSIZE=32" "-j%{jobs}%" "msl" "sepcomp" "veric" "floyd"]
 ]
-run-test: [make "BITSIZE=32" "-j%{jobs}%" "progs" "sha-hmac" "mailbox"]
+run-test: [make "COMPCERT=bundled" "BITSIZE=32" "-j%{jobs}%" "progs" "sha-hmac" "mailbox"]
 install: [
-	make "BITSIZE=32" "install"
+        make "COMPCERT=bundled" "BITSIZE=32" "install"
 	]
 depends: [
   "coq" {>= "8.11.0"}
-  "coq-compcert-32" {= "3.9"}
+  "coq-flocq" {>= "3.1.0" & < "4.0.0"} | "coq-flocq3" { = "dev"}
 ]
 synopsis: "Verified Software Toolchain"
 description:

diff --git a/coq-vst.opam b/coq-vst.opam
@@ -17,16 +17,16 @@ dev-repo: "git+https://github.com/PrincetonUniversity/VST.git"
 bug-reports: "https://github.com/PrincetonUniversity/VST/issues"
 license: "https://raw.githubusercontent.com/PrincetonUniversity/VST/master/LICENSE"
 build: [
-  [make "BITSIZE=64" "depend"]
-  [make "BITSIZE=64" "-j%{jobs}%" "msl" "sepcomp" "veric" "floyd"]
+  [make "COMPCERT=bundled" "BITSIZE=64" "depend"]
+  [make "COMPCERT=bundled" "BITSIZE=64" "-j%{jobs}%" "msl" "sepcomp" "veric" "floyd"]
 ]
-run-test: [make "BITSIZE=64" "-j%{jobs}%" "progs"]
+run-test: [make "COMPCERT=bundled" "BITSIZE=64" "-j%{jobs}%" "progs"]
 install: [
-	make "BITSIZE=64" "install"
+        make "COMPCERT=bundled" "BITSIZE=64" "install"
 	]
 depends: [
   "coq" {>= "8.11.0"}
-  "coq-compcert" {= "3.9"}
+  "coq-flocq" {>= "3.1.0" & < "4.0.0"} | "coq-flocq3" { = "dev"}
 ]
 synopsis: "Verified Software Toolchain"
 description: