From 292afcdbb987cddfe8946af070eb2a17fadfdc26 Mon Sep 17 00:00:00 2001 From: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com> Date: Fri, 6 Dec 2024 17:09:14 +0100 Subject: [PATCH 1/3] Pick 8.20~2025.01: update/enable coq-rewriter from 0.0.100 to 0.0.12 and enable coq-fiat-crypto.0.1.3 --- .../packages/z3_tptp/z3_tptp.4.13.3/opam | 37 +++++++++++++++++++ package_picks/package-pick-8.20~2025.01.sh | 4 +- 2 files changed, 39 insertions(+), 2 deletions(-) create mode 100644 opam/opam-repository/packages/z3_tptp/z3_tptp.4.13.3/opam diff --git a/opam/opam-repository/packages/z3_tptp/z3_tptp.4.13.3/opam b/opam/opam-repository/packages/z3_tptp/z3_tptp.4.13.3/opam new file mode 100644 index 0000000000..ff1dd47fbc --- /dev/null +++ b/opam/opam-repository/packages/z3_tptp/z3_tptp.4.13.3/opam @@ -0,0 +1,37 @@ +opam-version: "2.0" +maintainer: "7895506+MSoegtropIMC@users.noreply.github.com" +authors: "MSR" +homepage: "https://github.com/Z3prover/z3" +bug-reports: "https://github.com/Z3prover/z3/issues" +license: "MIT" +dev-repo: "git+https://github.com/Z3prover/z3.git" +# OK, this is really ugly, but it is quite hard to do this via z3's make system +# using an already installed opam z3. +# Also this should be quite robust with just source 2 files and opam knowns the +# library folder better than any configure script. +build: [ + [ "g++" + "-I./src/api/c++" + "-I./src/api" + "-std=c++11" + "-L%{lib}%/stublibs" + "-o" "z3_tptp" + "examples/tptp/tptp5.cpp" "examples/tptp/tptp5.lex.cpp" + "-lz3" + "-Wl,-rpath" + "-Wl,%{lib}%/stublibs" + ] +] +install: [ "cp" "z3_tptp" "%{bin}%/z3_tptp" ] +depends: [ + "z3" { >= "4.13.3" & < "4.13.4~" } + "conf-g++" {build} +] +synopsis: "TPTP front end for Z3 solver" +url { + src: "https://github.com/Z3Prover/z3/archive/refs/tags/z3-4.13.3.tar.gz" + checksum: [ + "sha256=f59c9cf600ea57fb64ffeffbffd0f2d2b896854f339e846f48f069d23bc14ba0" + "sha512=c899f57d8cb5450801463b07cd651869d766a920e41a4beedc96c4978e940bfadff9af2fbbb5ba10f94f6742bb33f7abaca0a351f3e1803d778e84d735d6829e" + ] +} diff --git a/package_picks/package-pick-8.20~2025.01.sh b/package_picks/package-pick-8.20~2025.01.sh index 01a320be9b..b742b51ecd 100644 --- a/package_picks/package-pick-8.20~2025.01.sh +++ b/package_picks/package-pick-8.20~2025.01.sh @@ -203,12 +203,12 @@ then case "$COQ_PLATFORM_FIATCRYPTO" in [yY]) PACKAGES="${PACKAGES} coq-coqutil.0.0.6" -# PACKAGES="${PACKAGES} coq-rewriter.0.0.11" # ToDo: fails to build + PACKAGES="${PACKAGES} coq-rewriter.0.0.12" PACKAGES="${PACKAGES} coq-riscv.0.0.5" 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" # ToDo: there is a 0.1.4 version in git but not in opam, ToDo: requires coq-rewriter + PACKAGES="${PACKAGES} coq-fiat-crypto.0.1.3" ;; [nN]) true ;; *) echo "Illegal value for COQ_PLATFORM_FIATCRYPTO - aborting"; false ;; From ea30cf85b747348ccb83cb00ce71bd058b16a571 Mon Sep 17 00:00:00 2001 From: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com> Date: Fri, 6 Dec 2024 17:14:59 +0100 Subject: [PATCH 2/3] Pick 8.20~2025.01: updated coq-ext-lib from 0.12.2 to 0.13.0 --- package_picks/package-pick-8.20~2025.01.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/package_picks/package-pick-8.20~2025.01.sh b/package_picks/package-pick-8.20~2025.01.sh index b742b51ecd..57da245d3d 100644 --- a/package_picks/package-pick-8.20~2025.01.sh +++ b/package_picks/package-pick-8.20~2025.01.sh @@ -73,7 +73,7 @@ then # Standard library extensions PACKAGES="${PACKAGES} coq-bignums.9.0.0+coq8.20" - PACKAGES="${PACKAGES} coq-ext-lib.0.12.2" + PACKAGES="${PACKAGES} coq-ext-lib.0.13.0" PACKAGES="${PACKAGES} coq-stdpp.1.11.0" # General mathematics From 115eac7278bd2ecf6ac91210a79c15bc1b9b3876 Mon Sep 17 00:00:00 2001 From: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com> Date: Mon, 9 Dec 2024 10:06:35 +0100 Subject: [PATCH 3/3] Pick 8.20~2025.01: updated elpi to 2.0.5, coq-elpi to 2.3.0 and coq-hierarchy-builder to 1.7.1 --- 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 57da245d3d..72567949af 100644 --- a/package_picks/package-pick-8.20~2025.01.sh +++ b/package_picks/package-pick-8.20~2025.01.sh @@ -77,9 +77,9 @@ then PACKAGES="${PACKAGES} coq-stdpp.1.11.0" # General mathematics - PACKAGES="${PACKAGES} elpi.1.19.6 coq-elpi.2.2.3" # required by coq-hierarchy-builder - PACKAGES="${PACKAGES} coq-hierarchy-builder.1.7.0" - PACKAGES="${PACKAGES} coq-mathcomp-ssreflect.2.3.0" # Todo: move elpi and hierarchy builder before this + PACKAGES="${PACKAGES} elpi.2.0.5 coq-elpi.2.3.0" # This would belong into the "Proof automation" section, but it is required by coq-hierarchy-builder + PACKAGES="${PACKAGES} coq-hierarchy-builder.1.7.1" + PACKAGES="${PACKAGES} coq-mathcomp-ssreflect.2.3.0" PACKAGES="${PACKAGES} coq-mathcomp-fingroup.2.3.0" PACKAGES="${PACKAGES} coq-mathcomp-algebra.2.3.0" PACKAGES="${PACKAGES} coq-mathcomp-solvable.2.3.0"