Merge pull request #411 from rtetley/package-updates

Package updates
coq · Oct 11, 2024 · 8ea5c21 · 8ea5c21
2 parents 1d85bf0 + 5e54c91
commit 8ea5c21
Show file tree

Hide file tree

Showing 9 changed files with 10 additions and 312 deletions.
diff --git a/opam/opam-coq-archive/released/packages/coq-corn/coq-corn.8.18.0/opam b/opam/opam-coq-archive/released/packages/coq-corn/coq-corn.8.18.0/opam
diff --git a/opam/opam-coq-archive/released/packages/coq-dpdgraph/coq-dpdgraph.1.0+8.18/opam b/opam/opam-coq-archive/released/packages/coq-dpdgraph/coq-dpdgraph.1.0+8.18/opam
diff --git a/opam/opam-coq-archive/released/packages/coq-hott/coq-hott.8.18/opam b/opam/opam-coq-archive/released/packages/coq-hott/coq-hott.8.18/opam
diff --git a/opam/opam-coq-archive/released/packages/coq-interval/coq-interval.4.10.0/opam b/opam/opam-coq-archive/released/packages/coq-interval/coq-interval.4.10.0/opam
diff --git a/opam/opam-coq-archive/released/packages/coq-mathcomp-word/coq-mathcomp-word.3.0/opam b/opam/opam-coq-archive/released/packages/coq-mathcomp-word/coq-mathcomp-word.3.0/opam
diff --git a/.../opam-coq-archive/released/packages/coq-relation-algebra/coq-relation-algebra.1.7.10/opam b/.../opam-coq-archive/released/packages/coq-relation-algebra/coq-relation-algebra.1.7.10/opam
diff --git a/opam/opam-coq-archive/released/packages/coq-vst-zlist/coq-vst-zlist.2.13/opam b/opam/opam-coq-archive/released/packages/coq-vst-zlist/coq-vst-zlist.2.13/opam
diff --git a/package_picks/package-pick-8.19~2024.01+beta1.sh b/package_picks/package-pick-8.19~2024.01+beta1.sh
@@ -119,17 +119,17 @@ then
   fi 
 
   # Code extraction
-  PACKAGES="${PACKAGES} coq-simple-io.1.8.0"
+  PACKAGES="${PACKAGES} coq-simple-io.1.9.0"
 
   # Proof automation / generation / helpers
   PACKAGES="${PACKAGES} coq-menhirlib.20231231 menhir.20231231"
   PACKAGES="${PACKAGES} coq-equations.1.3+8.19"
   PACKAGES="${PACKAGES} coq-aac-tactics.8.19.0"
   PACKAGES="${PACKAGES} coq-unicoq.1.6+8.19"
-  PACKAGES="${PACKAGES} coq-mtac2.1.4+8.19" # build issues on Windows
+  PACKAGES="${PACKAGES} coq-mtac2.1.4+8.19"
   PACKAGES="${PACKAGES} elpi.1.18.2 coq-elpi.2.1.0"
   PACKAGES="${PACKAGES} coq-hierarchy-builder.1.7.0"
-  PACKAGES="${PACKAGES} coq-quickchick.2.0.3" # build issues on Windows
+  PACKAGES="${PACKAGES} coq-quickchick.2.0.3"
   PACKAGES="${PACKAGES} coq-hammer-tactics.1.3.2+8.19"
   if [[ "$OSTYPE" != cygwin ]]
   then
@@ -154,7 +154,7 @@ then
   PACKAGES="${PACKAGES} coq-iris-heap-lang.4.2.0"
   PACKAGES="${PACKAGES} coq-ott.0.33"
   PACKAGES="${PACKAGES} ott.0.33"
-  PACKAGES="${PACKAGES} coq-mathcomp-word.3.0"
+  PACKAGES="${PACKAGES} coq-mathcomp-word.3.1"
 
   case "$COQ_PLATFORM_COMPCERT" in
     [yY]) PACKAGES="${PACKAGES} coq-compcert.3.13.1" ;;
@@ -201,13 +201,13 @@ then
   then
     case "$COQ_PLATFORM_FIATCRYPTO" in
       [yY])
-        PACKAGES="${PACKAGES} coq-coqutil.0.0.5"
+        PACKAGES="${PACKAGES} coq-coqutil.0.0.6"
         PACKAGES="${PACKAGES} coq-rewriter.0.0.11"
         PACKAGES="${PACKAGES} coq-riscv.0.0.5"
-        PACKAGES="${PACKAGES} coq-bedrock2.0.0.7"
-        PACKAGES="${PACKAGES} coq-bedrock2-compiler.0.0.7"
-        PACKAGES="${PACKAGES} coq-rupicola.0.0.9"
-        PACKAGES="${PACKAGES} coq-fiat-crypto.0.1.2"
+        PACKAGES="${PACKAGES} coq-bedrock2.0.0.8"
+        PACKAGES="${PACKAGES} coq-bedrock2-compiler.0.0.8"
+        PACKAGES="${PACKAGES} coq-rupicola.0.0.10"
+        PACKAGES="${PACKAGES} coq-fiat-crypto.0.1.3"
         ;;
       [nN]) true ;;
       *) echo "Illegal value for COQ_PLATFORM_FIATCRYPTO - aborting"; false ;;

diff --git a/shell_scripts/create_smoke_test_kit.sh b/shell_scripts/create_smoke_test_kit.sh
@@ -154,6 +154,7 @@ TEST_FILES[coq-rupicola]='src/Rupicola/Examples/Uppercase.v'
 TEST_FILES[coq-serapi]='../../test_files/coq-serapi/serapi_example'
 TEST_CMDS[coq-serapi]="sertop < serapi_example"
 TEST_FILES[coq-simple-io]='test/Example.v test/TestExtraction.v'
+TEST_FILES[coq-simple-io~8.19~2024.01+beta1]='test/example/main.v test/extraction/main.v'
 TEST_FILES[coq-stdpp]='tests/sets.v'
 TEST_FILES[coq-unicoq]='test-suite/microtests.v'
 TEST_FILES[coq-unimath]='UniMath/Foundations/Tests.v'