Merge pull request #2773 from LasseBlaauwbroek/coq-tactician-8.18.dev

Package coq-tactician.8.18.dev
coq · Oct 18, 2023 · 6eb2e53 · 6eb2e53
2 parents f9b8705 + dd5b6c9
commit 6eb2e53
Show file tree

Hide file tree

Showing 4 changed files with 72 additions and 3 deletions.
diff --git a/extra-dev/packages/coq-tactician-dummy/coq-tactician-dummy.8.17.dev/opam b/extra-dev/packages/coq-tactician-dummy/coq-tactician-dummy.8.17.dev/opam
@@ -16,7 +16,7 @@ homepage: "https://coq-tactician.github.io"
 bug-reports: "https://github.com/coq-tactician/coq-tactician-dummy/issues"
 license: "MIT"
 depends: [
-  "dune" {>= "3.5"}
+  "dune" {>= "3.5" & < "3.8~"}
   "coq-core"
   "odoc" {with-doc}
 ]

diff --git a/extra-dev/packages/coq-tactician/coq-tactician.8.17.dev/opam b/extra-dev/packages/coq-tactician/coq-tactician.8.17.dev/opam
@@ -16,7 +16,7 @@ homepage: "https://coq-tactician.github.io"
 bug-reports: "https://github.com/coq-tactician/coq-tactician/issues"
 license: "MIT"
 depends: [
-  "dune" {>= "3.5"}
+  "dune" {>= "3.5" & < "3.8~"}
   "ocaml" {>= "4.08"}
   "dune-site" {>= "2.9.1"}
   "opam-client" {>= "2.1.0"}

diff --git a/extra-dev/packages/coq-tactician/coq-tactician.8.18.dev/opam b/extra-dev/packages/coq-tactician/coq-tactician.8.18.dev/opam
@@ -0,0 +1,69 @@
+opam-version: "2.0"
+synopsis:
+  "Tactician: A Seamless, Interactive Tactic Learner and Prover for Coq"
+description: """
+Tactician is a tactic learner and prover for the Coq Proof Assistant.
+The system will help users make tactical proof decisions while they retain
+control over the general proof strategy. To this end, Tactician will learn
+from previously written tactic scripts, and either gives the user suggestions
+about the next tactic to be executed or altogether takes over the burden of
+proof synthesis. Tactician's goal is to provide the user with a seamless,
+interactive, and intuitive experience together with strong, adaptive proof
+automation."""
+maintainer: ["Lasse Blaauwbroek <lasse@blaauwbroek.eu>"]
+authors: ["Lasse Blaauwbroek <lasse@blaauwbroek.eu>"]
+homepage: "https://coq-tactician.github.io"
+bug-reports: "https://github.com/coq-tactician/coq-tactician/issues"
+license: "MIT"
+depends: [
+  "dune" {>= "3.5" & < "3.8~"}
+  "ocaml" {>= "4.08"}
+  "dune-site" {>= "2.9.1"}
+  "opam-client" {>= "2.1.0"}
+  "cmdliner" {>= "1.1.0"}
+  "coq-core" {>= "8.18" & < "8.19~"}
+  "coq-stdlib" {with-test}
+  "conf-git"
+  "bos" {>= "0.2.1"}
+  "coq-tactician-dummy" {= "8.17.dev" & with-test}
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "--promote-install-files=false"
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+  ["dune" "install" "-p" name "--create-install-files" name]
+]
+dev-repo: "git+https://github.com/coq-tactician/coq-tactician.git"
+post-messages: ["
+--- Tactician was successfully installed ---
+
+In order to enable Tactician, you should run
+
+tactician enable
+" {success}]
+tags: [
+  "keyword:tactic-learning"
+  "keyword:machine-learning"
+  "keyword:automation"
+  "keyword:proof-synthesis"
+  "category:Miscellaneous/Coq Extensions"
+  "logpath:Tactician"
+]
+substs: [
+  "coq-shim/tactician-patch"
+  "coq-shim/tactician.ml"
+]
+url {
+  src: "git+https://github.com/coq-tactician/coq-tactician.git#coq8.18"
+}
diff --git a/extra-dev/packages/coq-tactician/coq-tactician.dev/opam b/extra-dev/packages/coq-tactician/coq-tactician.dev/opam
@@ -16,7 +16,7 @@ homepage: "https://coq-tactician.github.io"
 bug-reports: "https://github.com/coq-tactician/coq-tactician/issues"
 license: "MIT"
 depends: [
-  "dune" {>= "3.5"}
+  "dune" {>= "3.5" & < "3.8~"}
   "ocaml" {>= "4.08"}
   "dune-site" {>= "2.9.1"}
   "opam-client" {>= "2.1.0"}