Local opam package

1 files changed, 44 insertions, 0 deletions

diff --git a/coq-smtcoq.opam b/coq-smtcoq.opam
new file mode 100644
index 0000000..e597b1e
--- /dev/null
+++ b/coq-smtcoq.opam
@@ -0,0 +1,44 @@
+opam-version: "2.0"
+maintainer: "matthieu.sozeau@inria.fr"
+homepage: "https://smtcoq.github.io/"
+dev-repo: "git+https://github.com/smtcoq/smtcoq.git"
+bug-reports: "https://github.com/smtcoq/smtcoq/issues"
+license: "CECILL-C"
+build: [
+  [make "-j%{jobs}%"]
+]
+install: [
+  [make "install"]
+]
+depends: [
+  "ocaml" {>= "4.07.1" }
+  "coq" {>= "8.13~" & < "8.14~"}
+  "coq-trakt"
+]
+pin-depends: [
+  [ "coq-trakt.dev" "git+https://github.com/ecranceMERCE/trakt.git" ]
+]
+tags: [ 
+  "category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures"
+  "category:Miscellaneous/Coq Extensions"
+  "keyword: SMT"
+  "keyword: SAT"
+  "keyword: automation"
+]
+authors: [ 
+ "Michaël Armand"
+ "Valentin Blot"
+ "Amina Bousalem"
+ "Quentin Garchery"
+ "Benjamin Grégoire"
+ "Chantal Keller"
+ "Burak Ekici"
+ "Alain Mebsout"
+]
+synopsis: "A Coq plugin that checks proof witnesses coming from external SAT and SMT solvers"
+description: """
+- a certified checker for proof witnesses coming from the SAT solver ZChaff and the SMT solvers veriT and CVC4. This checker increases the confidence in these tools by checking their answers a posteriori and allows to import new theroems proved by these solvers in Coq;
+- decision procedures through new tactics that discharge some Coq goals to ZChaff, veriT, CVC4, and their combination"""
+url {
+  src: "git+https://github.com/smtcoq/smtcoq.git#itp22"
+}