Package update 8.19

opam/opam-coq-archive/released/packages/coq-itauto/coq-itauto.8.19.0/files/0001-Remove-root-on-dune-calls-does-not-work-on-Windows-M.patch

@@ -0,0 +1,25 @@
+From 828e973c631eeb4875ca94fb1a4d1bfb7ebc7866 Mon Sep 17 00:00:00 2001
+From: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com>
+Date: Fri, 24 Nov 2023 17:57:28 +0100
+Subject: [PATCH] Remove --root on dune calls - does not work on Windows MinGW
+ cygwin cross
+
+---
+ src/patch/Makefile | 4 ++--
+ 1 file changed, 2 insertions(+), 2 deletions(-)
+
+diff --git a/src/patch/Makefile b/src/patch/Makefile
+index 6b347bd..d3ba762 100644
+--- a/src/patch/Makefile
++++ b/src/patch/Makefile
+@@ -1,5 +1,5 @@
+ mlpatch : lexer.mll parser.mly patch.ml mlpatch.ml
+-	dune build --root $(CURDIR)
++	dune build
+
+ clean :
+-	dune clean --root $(CURDIR)
++	dune clean
+-- 
+2.37.3
+

opam/opam-coq-archive/released/packages/coq-itauto/coq-itauto.8.19.0/opam

@@ -0,0 +1,50 @@
+opam-version: "2.0"
+maintainer: "frederic.besson@inria.fr"
+homepage: "https://gitlab.inria.fr/fbesson/itauto"
+dev-repo: "git+https://gitlab.inria.fr/fbesson/itauto.git"
+authors: ["Frédéric Besson"]
+bug-reports: ["frederic.besson@inria.fr" "https://gitlab.inria.fr/fbesson/itauto/-/issues"]
+license: "MIT"
+synopsis: "Reflexive SAT solver with Nelson-Oppen support, parameterised by a leaf tactic inside Coq"
+description: """
+itauto is a reflexive intuitionistic SAT solver parameterised by a theory module.
+When run inside Coq, the theory module wraps an arbitrary Coq tactic, e.g., the lia
+solver for linear arithmetic or the congruence solver for uninterpreted function symbols
+and constructors. Using a black-box Nelson-Oppen scheme for combination of theories,
+itauto also provides an SMT-like tactic for propositional reasoning modulo the solvers for
+both arithmetic and function symbols.
+"""
+
+patches: [
+  "0001-Remove-root-on-dune-calls-does-not-work-on-Windows-M.patch"
+]
+build: [
+  [make "-j%{jobs}%"]
+ ]
+install: [make "install"]
+depends: [
+  "ocaml" {>= "4.9~"}
+  "coq" {>= "8.19" & < "8.20"}
+  "dune" {>= "2.9"}
+]
+depopts: [ "ocamlformat" {build} ]
+
+tags: [
+  "category:Miscellaneous/Coq Extensions"
+  "category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures"
+  "keyword:integers"
+  "keyword:SAT"
+  "keyword:SMT"
+  "keyword:Nelson-Oppen"
+  "keyword:automation"
+  "logpath:Cdcl"
+  "date:2024-01-03"
+]
+
+url {
+  src: "https://gitlab.inria.fr/fbesson/itauto/-/archive/8.19.0/itauto-8.19.0.tar.gz"
+  checksum: [
+    "md5=95c1617377a2a60f0db72f9893e7149c"
+    "sha512=9a5f92dde1cadd7ef70022b5289462d0beadd451e92a42a390dd460e4851f0c85204c97209a3dc0b93cbdfea48131444f3673df34d2021787d807e51cad1d434"
+  ]
+}

opam/opam-repository/packages/z3_tptp/z3_tptp.4.13.0/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.0" & < "4.13.1~" }
+  "conf-g++" {build}
+]
+synopsis: "TPTP front end for Z3 solver"
+url {
+  src: "https://github.com/Z3Prover/z3/archive/refs/tags/z3-4.13.0.tar.gz"
+  checksum: [
+    "sha256=01bcc61c8362e37bb89fd2430f7e3385e86df7915019bd2ce45de9d9bd934502"
+    "sha512=8503787fe0b18592b5a131bcec2cacfa5f5096d76386a1c4fda7a836e472924b154433306d27600ff0d0758ddb710c965901fbfc2e5605919b624b9d4d1bc4fd"
+  ]
+}

package_picks/package-pick-8.19~2024.01+beta1.sh

@@ -69,7 +69,7 @@ then
   # Standard library extensions
   PACKAGES="${PACKAGES} coq-bignums.9.0.0+coq8.19"
   PACKAGES="${PACKAGES} coq-ext-lib.0.12.1"
-  #PACKAGES="${PACKAGES} coq-stdpp.1.9.0" #does not build
+  PACKAGES="${PACKAGES} coq-stdpp.1.10.0"
 
   # General mathematics
   PACKAGES="${PACKAGES} coq-mathcomp-ssreflect.2.2.0"
@@ -96,8 +96,8 @@ then
   PACKAGES="${PACKAGES} gappa.1.4.1"
 
   # Constructive mathematics
-  #PACKAGES="${PACKAGES} coq-math-classes.8.18.0" #DOES NOT BUILD
-  #PACKAGES="${PACKAGES} coq-corn.8.18.0" #DOES NOT BUILD
+  PACKAGES="${PACKAGES} coq-math-classes.8.19.0"
+  PACKAGES="${PACKAGES} coq-corn.8.19.0"
 
   # Homotopy Type Theory (HoTT)
   PACKAGES="${PACKAGES} coq-hott.8.19"
@@ -120,23 +120,29 @@ then
   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.18" #DOES NOT BUILD
-  #PACKAGES="${PACKAGES} coq-mtac2.1.4+8.18" #DOES NOT BUILD, DEPENDS ON UNICOQ
+  PACKAGES="${PACKAGES} coq-unicoq.1.6+8.19"
+  if [[ "$OSTYPE" != cygwin ]]
+  then
+    PACKAGES="${PACKAGES} coq-mtac2.1.4+8.19" # build issues on Windows
+  fi
   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.2" #DOES NOT BUILD ON WINDOWS
-  #PACKAGES="${PACKAGES} coq-hammer-tactics.1.3.2+8.18" # DOES NOT BUILD
+  if [[ "$OSTYPE" != cygwin ]]
+  then
+    PACKAGES="${PACKAGES} coq-quickchick.2.0.3" # build issues on Windows
+  fi
+  PACKAGES="${PACKAGES} coq-hammer-tactics.1.3.2+8.19"
   if [[ "$OSTYPE" != cygwin ]]
   then
     # coq-hammer does not work on Windows because it heavily relies on fork
-    #PACKAGES="${PACKAGES} coq-hammer.1.3.2+8.18" # DEPENDS ON COQ-HAMMER-TACTICS
-    PACKAGES="${PACKAGES} eprover.3.0"
-    PACKAGES="${PACKAGES} z3_tptp.4.11.2"  # 4.12.2-1 has build issues on ARM macOS
+    PACKAGES="${PACKAGES} coq-hammer.1.3.2+8.19"
+    PACKAGES="${PACKAGES} eprover.3.1"
+    PACKAGES="${PACKAGES} z3_tptp.4.13.0"
   fi
   PACKAGES="${PACKAGES} coq-paramcoq.1.1.3+coq8.19"
   PACKAGES="${PACKAGES} coq-coqeal.2.0.2"
-  #PACKAGES="${PACKAGES} coq-libhyps.2.0.8" #DOES NOT BUILD
-  #PACKAGES="${PACKAGES} coq-itauto.8.19.0" #DOES NOT BUILD ON WINDOWS
+  PACKAGES="${PACKAGES} coq-libhyps.2.0.8"
+  PACKAGES="${PACKAGES} coq-itauto.8.19.0" #DOES NOT BUILD ON WINDOWS
 
   # General mathematics (which requires one of the above tools)
   PACKAGES="${PACKAGES} coq-mathcomp-analysis.1.1.0"
@@ -145,13 +151,13 @@ then
 
   # Formal languages, compilers and code verification
   PACKAGES="${PACKAGES} coq-reglang.1.2.1"
-  #PACKAGES="${PACKAGES} coq-iris.4.1.0" #DEPENDS ON coq-stdpp
-  #PACKAGES="${PACKAGES} coq-iris-heap-lang.4.1.0" #DEPENDS on coq-iris
+  PACKAGES="${PACKAGES} coq-iris.4.2.0"
+  PACKAGES="${PACKAGES} coq-iris-heap-lang.4.2.0"
   if [[ "$OSTYPE" != cygwin ]]
   then
     # Windows: some issues with executable extensions (ott.opt instead of ott.exe)
     # Note: 0.32 does work on Windows!
-    #PACKAGES="${PACKAGES} coq-ott.0.33" #DOES NOT BUILD
+    PACKAGES="${PACKAGES} coq-ott.0.33"
     PACKAGES="${PACKAGES} ott.0.33"
   fi
   PACKAGES="${PACKAGES} coq-mathcomp-word.3.0"