Merge pull request #2887 from palmskog/add-itauto-8.19

add coq-itauto.8.19.0 to extra-dev

extra-dev/packages/coq-itauto/coq-itauto.8.19.0/opam

@@ -0,0 +1,47 @@
+opam-version: "2.0"
+maintainer: "[email protected]"
+homepage: "https://gitlab.inria.fr/fbesson/itauto"
+dev-repo: "git+https://gitlab.inria.fr/fbesson/itauto.git"
+authors: ["Frédéric Besson"]
+bug-reports: ["[email protected]" "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.
+"""
+
+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"
+  ]
+}