Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

2025.01 prep 6 #454

Merged
merged 3 commits into from
Dec 20, 2024
Merged

2025.01 prep 6 #454

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
7294813
Pick 8.20~2025.01:
MSoegtropIMC Dec 20, 2024
f9fa36b
Pick 8.20~2025.01:
MSoegtropIMC Dec 20, 2024
6b2090f
Legacy picks: updated z3_tptp to version 4.13.0 in all legacy picks u…
MSoegtropIMC Dec 20, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion package_picks/package-pick-8.14~2022.01.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion package_picks/package-pick-8.14~2022.04.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down
2 changes: 1 addition & 1 deletion package_picks/package-pick-8.15~2022.04.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down
2 changes: 1 addition & 1 deletion package_picks/package-pick-8.15~2022.09.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down
2 changes: 1 addition & 1 deletion package_picks/package-pick-8.16~2022.09.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down
2 changes: 1 addition & 1 deletion package_picks/package-pick-8.16~2023.08.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down
2 changes: 1 addition & 1 deletion package_picks/package-pick-8.17~2023.08.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down
2 changes: 1 addition & 1 deletion package_picks/package-pick-8.18~2023.11.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down
2 changes: 1 addition & 1 deletion package_picks/package-pick-8.18~mc2.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down
14 changes: 7 additions & 7 deletions package_picks/package-pick-8.20~2025.01.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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"
Expand Down Expand Up @@ -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"
Expand Down
Loading