From 943e182dd2063786e0523e9f0e35ce8376435edb Mon Sep 17 00:00:00 2001 From: Lasse Blaauwbroek Date: Tue, 17 Oct 2023 18:30:27 +0200 Subject: [PATCH 1/2] Package coq-tactician.8.18.dev --- .../coq-tactician/coq-tactician.8.18.dev/opam | 69 +++++++++++++++++++ 1 file changed, 69 insertions(+) create mode 100644 extra-dev/packages/coq-tactician/coq-tactician.8.18.dev/opam 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 new file mode 100644 index 000000000..6c486c538 --- /dev/null +++ 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 "] +authors: ["Lasse Blaauwbroek "] +homepage: "https://coq-tactician.github.io" +bug-reports: "https://github.com/coq-tactician/coq-tactician/issues" +license: "MIT" +depends: [ + "dune" {>= "3.5"} + "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" +} From dd5b6c968c9ce003589a9edb7d171b22b1073d7e Mon Sep 17 00:00:00 2001 From: Lasse Blaauwbroek Date: Tue, 17 Oct 2023 21:28:19 +0200 Subject: [PATCH 2/2] Dune >= 3.8 is not supported for coq-tactician due to ocaml/dune#8958 --- .../coq-tactician-dummy/coq-tactician-dummy.8.17.dev/opam | 2 +- extra-dev/packages/coq-tactician/coq-tactician.8.17.dev/opam | 2 +- extra-dev/packages/coq-tactician/coq-tactician.8.18.dev/opam | 2 +- extra-dev/packages/coq-tactician/coq-tactician.dev/opam | 2 +- 4 files changed, 4 insertions(+), 4 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 index f73593d8b..f085c5edc 100644 --- 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 index d9fedb862..d2d1c601e 100644 --- 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 index 6c486c538..2197b403d 100644 --- a/extra-dev/packages/coq-tactician/coq-tactician.8.18.dev/opam +++ b/extra-dev/packages/coq-tactician/coq-tactician.8.18.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.dev/opam b/extra-dev/packages/coq-tactician/coq-tactician.dev/opam index 66c96c16b..0e2b1e93e 100644 --- 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"}