Merge pull request #454 from MSoegtropIMC/2025.01-prep-6

2025.01 prep 6
coq · Dec 20, 2024 · 972dbc8 · 972dbc8
2 parents cfaa14b + 6b2090f
commit 972dbc8
Show file tree

Hide file tree

Showing 10 changed files with 16 additions and 16 deletions.
diff --git a/package_picks/package-pick-8.14~2022.01.sh b/package_picks/package-pick-8.14~2022.01.sh
@@ -134,7 +134,7 @@ then
     # coq-hammer does not work on Windows because it heavily relies on fork
     PACKAGES="${PACKAGES} coq-hammer.1.3.2+8.14"        # pick confirmed https://github.com/lukaszcz/coqhammer/issues/110
     PACKAGES="${PACKAGES} eprover.2.6"                  # ATP for coq-hammer (latest version)
-    PACKAGES="${PACKAGES} z3_tptp.4.8.13"               # ATP for coq-hammer (latest version)
+    PACKAGES="${PACKAGES} z3_tptp.4.13.0"               # ATP for coq-hammer (latest version)
   fi
   PACKAGES="${PACKAGES} coq-paramcoq.1.1.3+coq8.14"   # pick confirmed https://github.com/coq-community/paramcoq/issues/82
   PACKAGES="${PACKAGES} coq-coqeal.1.1.0"             # Pick confirmed https://github.com/coq-community/coqeal/issues/51

diff --git a/package_picks/package-pick-8.14~2022.04.sh b/package_picks/package-pick-8.14~2022.04.sh
@@ -135,7 +135,7 @@ then
     # coq-hammer does not work on Windows because it heavily relies on fork
     PACKAGES="${PACKAGES} coq-hammer.1.3.2+8.14"
     PACKAGES="${PACKAGES} eprover.2.6"
-    PACKAGES="${PACKAGES} z3_tptp.4.8.14"
+    PACKAGES="${PACKAGES} z3_tptp.4.13.0"
   fi
   PACKAGES="${PACKAGES} coq-paramcoq.1.1.3+coq8.14"
   PACKAGES="${PACKAGES} coq-coqeal.1.1.0"

diff --git a/package_picks/package-pick-8.15~2022.04.sh b/package_picks/package-pick-8.15~2022.04.sh
@@ -131,7 +131,7 @@ then
     # coq-hammer does not work on Windows because it heavily relies on fork
     PACKAGES="${PACKAGES} coq-hammer.1.3.2+8.15"
     PACKAGES="${PACKAGES} eprover.2.6"
-    PACKAGES="${PACKAGES} z3_tptp.4.8.14"
+    PACKAGES="${PACKAGES} z3_tptp.4.13.0"
   fi
   PACKAGES="${PACKAGES} coq-paramcoq.1.1.3+coq8.15"
   PACKAGES="${PACKAGES} coq-coqeal.1.1.0"

diff --git a/package_picks/package-pick-8.15~2022.09.sh b/package_picks/package-pick-8.15~2022.09.sh
@@ -136,7 +136,7 @@ then
     # coq-hammer does not work on Windows because it heavily relies on fork
     PACKAGES="${PACKAGES} coq-hammer.1.3.2+8.15"
     PACKAGES="${PACKAGES} eprover.2.6"
-    PACKAGES="${PACKAGES} z3_tptp.4.11.0"
+    PACKAGES="${PACKAGES} z3_tptp.4.13.0"
   fi
   PACKAGES="${PACKAGES} coq-paramcoq.1.1.3+coq8.15"
   PACKAGES="${PACKAGES} coq-coqeal.1.1.1"

diff --git a/package_picks/package-pick-8.16~2022.09.sh b/package_picks/package-pick-8.16~2022.09.sh
@@ -136,7 +136,7 @@ then
     # coq-hammer does not work on Windows because it heavily relies on fork
     PACKAGES="${PACKAGES} coq-hammer.1.3.2+8.16"
     PACKAGES="${PACKAGES} eprover.2.6"
-    PACKAGES="${PACKAGES} z3_tptp.4.11.0"
+    PACKAGES="${PACKAGES} z3_tptp.4.13.0"
   fi
   PACKAGES="${PACKAGES} coq-paramcoq.1.1.3+coq8.16"
   PACKAGES="${PACKAGES} coq-coqeal.1.1.1"

diff --git a/package_picks/package-pick-8.16~2023.08.sh b/package_picks/package-pick-8.16~2023.08.sh
@@ -137,7 +137,7 @@ then
     # coq-hammer does not work on Windows because it heavily relies on fork
     PACKAGES="${PACKAGES} coq-hammer.1.3.2+8.16"
     PACKAGES="${PACKAGES} eprover.2.6"
-    PACKAGES="${PACKAGES} z3_tptp.4.11.2"
+    PACKAGES="${PACKAGES} z3_tptp.4.13.0"
   fi
   PACKAGES="${PACKAGES} coq-paramcoq.1.1.3+coq8.16"
   PACKAGES="${PACKAGES} coq-coqeal.1.1.3"

diff --git a/package_picks/package-pick-8.17~2023.08.sh b/package_picks/package-pick-8.17~2023.08.sh
@@ -132,7 +132,7 @@ then
     # coq-hammer does not work on Windows because it heavily relies on fork
     PACKAGES="${PACKAGES} coq-hammer.1.3.2+8.17"
     PACKAGES="${PACKAGES} eprover.2.6"
-    PACKAGES="${PACKAGES} z3_tptp.4.11.2"
+    PACKAGES="${PACKAGES} z3_tptp.4.13.0"
   fi
   PACKAGES="${PACKAGES} coq-paramcoq.1.1.3+coq8.17"
   PACKAGES="${PACKAGES} coq-coqeal.1.1.3"

diff --git a/package_picks/package-pick-8.18~2023.11.sh b/package_picks/package-pick-8.18~2023.11.sh
@@ -131,7 +131,7 @@ then
     # coq-hammer does not work on Windows because it heavily relies on fork
     PACKAGES="${PACKAGES} coq-hammer.1.3.2+8.18"
     PACKAGES="${PACKAGES} eprover.3.0"
-    PACKAGES="${PACKAGES} z3_tptp.4.11.2"  # 4.12.2-1 has build issues on ARM macOS
+    PACKAGES="${PACKAGES} z3_tptp.4.13.0"
   fi
   PACKAGES="${PACKAGES} coq-paramcoq.1.1.3+coq8.18"
   PACKAGES="${PACKAGES} coq-coqeal.1.1.3"

diff --git a/package_picks/package-pick-8.18~mc2.sh b/package_picks/package-pick-8.18~mc2.sh
@@ -132,7 +132,7 @@ then
     # coq-hammer does not work on Windows because it heavily relies on fork
     PACKAGES="${PACKAGES} coq-hammer.1.3.2+8.18"
     PACKAGES="${PACKAGES} eprover.3.0"
-    PACKAGES="${PACKAGES} z3_tptp.4.11.2"  # 4.12.2-1 has build issues on ARM macOS
+    PACKAGES="${PACKAGES} z3_tptp.4.13.0"
   fi
   PACKAGES="${PACKAGES} coq-paramcoq.1.1.3+coq8.18"
   PACKAGES="${PACKAGES} coq-coqeal.2.0.0"

diff --git a/package_picks/package-pick-8.20~2025.01.sh b/package_picks/package-pick-8.20~2025.01.sh
@@ -87,13 +87,13 @@ then
   PACKAGES="${PACKAGES} coq-mathcomp-character.2.3.0"
   PACKAGES="${PACKAGES} coq-mathcomp-bigenough.1.0.1"
   PACKAGES="${PACKAGES} coq-mathcomp-finmap.2.1.0"
-# PACKAGES="${PACKAGES} coq-mathcomp-real-closed.2.0.1" # ToDo requires downgrade coq-mathcomp-ssreflect 2.3.0 to 2.2.0, fails with version restriction relaxation
+  PACKAGES="${PACKAGES} coq-mathcomp-real-closed.2.0.2"
   PACKAGES="${PACKAGES} coq-mathcomp-zify.1.5.0+2.0+8.16"
   PACKAGES="${PACKAGES} coq-mathcomp-multinomials.2.3.0"
   PACKAGES="${PACKAGES} coq-coquelicot.3.4.2"
 
   # Number theory
-  PACKAGES="${PACKAGES} coq-coqprime.1.5.0"
+  PACKAGES="${PACKAGES} coq-coqprime.1.6.0"
   PACKAGES="${PACKAGES} coq-coqprime-generator.1.1.1" #TODO: this points to https://github.com/thery/coqprime/archive/v8.14.1.tar.gz
 
   # Numerical mathematics
@@ -140,17 +140,17 @@ then
     PACKAGES="${PACKAGES} z3_tptp.4.13.0" # ToDo Check
   fi
   PACKAGES="${PACKAGES} coq-paramcoq.1.1.3+coq8.20"
-  # PACKAGES="${PACKAGES} coq-coqeal.2.0.2" # ToDo: requires downgrade coq-mathcomp-ssreflect 2.3.0 to 2.2.0, depends on packages which fail with version relaxation
-  PACKAGES="${PACKAGES} coq-libhyps.2.0.8"
+  PACKAGES="${PACKAGES} coq-coqeal.2.0.3"
+  PACKAGES="${PACKAGES} coq-libhyps.3.0.1"
   PACKAGES="${PACKAGES} coq-itauto.8.20.0"
 
   # General mathematics (which requires one of the above tools)
-  PACKAGES="${PACKAGES} coq-mathcomp-analysis.1.7.0"
+  PACKAGES="${PACKAGES} coq-mathcomp-analysis.1.8.0"
   PACKAGES="${PACKAGES} coq-mathcomp-algebra-tactics.1.2.3" # Works with version relaxation
   PACKAGES="${PACKAGES} coq-relation-algebra.1.7.11"
 
   # Formal languages, compilers and code verification
-# PACKAGES="${PACKAGES} coq-reglang.1.2.1" # ToDo: requires downgrade coq-mathcomp-ssreflect 2.3.0 to 2.2.0, fails with version restriction relaxation 
+  PACKAGES="${PACKAGES} coq-reglang.1.2.1"
   PACKAGES="${PACKAGES} coq-iris.4.3.0"
   PACKAGES="${PACKAGES} coq-iris-heap-lang.4.3.0"
   PACKAGES="${PACKAGES} coq-ott.0.33"
@@ -188,7 +188,7 @@ then
   fi
 
   # General mathematics
-# PACKAGES="${PACKAGES} coq-extructures.0.4.0" # ToDo: fails to build
+ PACKAGES="${PACKAGES} coq-extructures.0.5.0"
 
   # Gallina extensions
   PACKAGES="${PACKAGES} coq-reduction-effects.0.1.5"