Package updates

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 ;;

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'