From 7294813394e1871caf5833f079cc659d0f691614 Mon Sep 17 00:00:00 2001 From: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com> Date: Fri, 20 Dec 2024 09:27:57 +0100 Subject: [PATCH 1/3] Pick 8.20~2025.01: - updated coq-mathcomp-real-closed to version 2.0.2 and enabled it - updated coq-coqeal to version 2.0.3 and enabled it - updated coq-mathcomp-analysis to version 1.8.0 (the above two updates depend on this) --- package_picks/package-pick-8.20~2025.01.sh | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/package_picks/package-pick-8.20~2025.01.sh b/package_picks/package-pick-8.20~2025.01.sh index b5b99ea537..c117bb57e1 100644 --- a/package_picks/package-pick-8.20~2025.01.sh +++ b/package_picks/package-pick-8.20~2025.01.sh @@ -87,7 +87,7 @@ 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" @@ -140,12 +140,12 @@ 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-coqeal.2.0.3" PACKAGES="${PACKAGES} coq-libhyps.2.0.8" 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" From f9fa36b0717626e7f6b13e5915722023e5343ecf Mon Sep 17 00:00:00 2001 From: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com> Date: Fri, 20 Dec 2024 10:11:59 +0100 Subject: [PATCH 2/3] Pick 8.20~2025.01: - updated coq-coqprime to version 1.6.0 - updated coq-libhyps to version 3.0.1 - enabled coq-reglang.1.2.1 (depended on mathcomp-analysis fix) - enabled coq-extructures (depended on mathcomp-analysis fix) --- package_picks/package-pick-8.20~2025.01.sh | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/package_picks/package-pick-8.20~2025.01.sh b/package_picks/package-pick-8.20~2025.01.sh index c117bb57e1..e69c150435 100644 --- a/package_picks/package-pick-8.20~2025.01.sh +++ b/package_picks/package-pick-8.20~2025.01.sh @@ -93,7 +93,7 @@ then 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 @@ -141,7 +141,7 @@ then fi PACKAGES="${PACKAGES} coq-paramcoq.1.1.3+coq8.20" PACKAGES="${PACKAGES} coq-coqeal.2.0.3" - PACKAGES="${PACKAGES} coq-libhyps.2.0.8" + PACKAGES="${PACKAGES} coq-libhyps.3.0.1" PACKAGES="${PACKAGES} coq-itauto.8.20.0" # General mathematics (which requires one of the above tools) @@ -150,7 +150,7 @@ then 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" From 6b2090f196da6f94ba275d0ff4462003b566e8cf Mon Sep 17 00:00:00 2001 From: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com> Date: Fri, 20 Dec 2024 14:44:16 +0100 Subject: [PATCH 3/3] Legacy picks: updated z3_tptp to version 4.13.0 in all legacy picks using older versions (8.14..8.18) since the older version no longer build on Ubuntu 24 --- package_picks/package-pick-8.14~2022.01.sh | 2 +- package_picks/package-pick-8.14~2022.04.sh | 2 +- package_picks/package-pick-8.15~2022.04.sh | 2 +- package_picks/package-pick-8.15~2022.09.sh | 2 +- package_picks/package-pick-8.16~2022.09.sh | 2 +- package_picks/package-pick-8.16~2023.08.sh | 2 +- package_picks/package-pick-8.17~2023.08.sh | 2 +- package_picks/package-pick-8.18~2023.11.sh | 2 +- package_picks/package-pick-8.18~mc2.sh | 2 +- 9 files changed, 9 insertions(+), 9 deletions(-) diff --git a/package_picks/package-pick-8.14~2022.01.sh b/package_picks/package-pick-8.14~2022.01.sh index a0b7ee85fa..b53c67d033 100644 --- 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 index f5808c3c6d..8f13f20598 100644 --- 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 index 397d8d7c16..b0f6cf1660 100644 --- 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 index a607db1ca8..c064bd1b70 100644 --- 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 index ea84c472e6..573a299d10 100644 --- 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 index 4b1bab2836..a697900b6b 100644 --- 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 index 890832178c..338eddbb6a 100644 --- 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 index 05620d0437..8864f5fb2a 100644 --- 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 index 18fa0566fa..1bc53f1b97 100644 --- 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"