diff --git a/released/packages/coq-tactician-dummy/coq-tactician-dummy.1.0~beta2+8.11/opam b/released/packages/coq-tactician-dummy/coq-tactician-dummy.1.0~beta2+8.11/opam new file mode 100644 index 000000000..9d722c49e --- /dev/null +++ b/released/packages/coq-tactician-dummy/coq-tactician-dummy.1.0~beta2+8.11/opam @@ -0,0 +1,48 @@ +opam-version: "2.0" +synopsis: "A dummy implementation of Tactician" +description: """ +This package acts as a stand-in for the Tactician plugin (`coq-tactician`). +It provides short files that replicate Tactician's tactics without actually +doing much. This is useful when you have a development that uses Tactician +that you want to package up. In most situations, it is not a good idea to +have your package directly depend on `coq-tactician`. Instead you should load +Tactician through your `coqrc` file. In order for your package to be compilable +by others, your package can depend on this package. Just add +`From Tactician Require Import Ltac1Dummy` in your development and you are good +to go.""" +maintainer: ["Lasse Blaauwbroek "] +authors: ["Lasse Blaauwbroek "] +license: "MIT" +homepage: "https://coq-tactician.github.io" +bug-reports: "https://github.com/coq-tactician/coq-tactician-dummy/issues" +depends: [ + "dune" {>= "2.5"} + "coq" {>= "8.6.1" & < "8.17~"} +] +build: [ + ["dune" "subst"] {pinned} + [ + "dune" + "build" + "-p" + name + "-j" + jobs + "@install" + "@runtest" {with-test} + "@doc" {with-doc} + ] +] +dev-repo: "git+https://github.com/coq-tactician/coq-tactician-dummy.git" +tags: [ + "keyword:tactic-learning" + "keyword:machine-learning" + "keyword:automation" + "keyword:proof-synthesis" + "category:Miscellaneous/Coq Extensions" + "logpath:Tactician" +] +url { + src: "https://github.com/coq-tactician/coq-tactician-dummy/archive/1.0-beta2-8.11.tar.gz" + checksum: "sha512=89aa13aff38e7ff3d53c00c0a604771ee1b3d0fadb3dab21161b28e25ab9fa14bd834a445472c05140c881ba7b7205ed81ca20b479002573051f42660428e9bb" +} diff --git a/released/packages/coq-tactician-dummy/coq-tactician-dummy.1.0~beta2+8.17/opam b/released/packages/coq-tactician-dummy/coq-tactician-dummy.1.0~beta2+8.17/opam new file mode 100644 index 000000000..c33ee2e63 --- /dev/null +++ b/released/packages/coq-tactician-dummy/coq-tactician-dummy.1.0~beta2+8.17/opam @@ -0,0 +1,49 @@ +opam-version: "2.0" +synopsis: "A dummy implementation of Tactician" +description: """ +This package acts as a stand-in for the Tactician plugin (`coq-tactician`). +It provides short files that replicate Tactician's tactics without actually +doing much. This is useful when you have a development that uses Tactician +that you want to package up. In most situations, it is not a good idea to +have your package directly depend on `coq-tactician`. Instead you should load +Tactician through your `coqrc` file. In order for your package to be compilable +by others, your package can depend on this package. Just add +`From Tactician Require Import Ltac1Dummy` in your development and you are good +to go.""" +maintainer: ["Lasse Blaauwbroek "] +authors: ["Lasse Blaauwbroek "] +license: "MIT" +homepage: "https://coq-tactician.github.io" +bug-reports: "https://github.com/coq-tactician/coq-tactician-dummy/issues" +depends: [ + "coq-core" + "dune" {>= "3.5" & < "3.8~"} + "odoc" {with-doc} +] +build: [ + ["dune" "subst"] {dev} + [ + "dune" + "build" + "-p" + name + "-j" + jobs + "@install" + "@runtest" {with-test} + "@doc" {with-doc} + ] +] +dev-repo: "git+https://github.com/coq-tactician/coq-tactician-dummy.git" +tags: [ + "keyword:tactic-learning" + "keyword:machine-learning" + "keyword:automation" + "keyword:proof-synthesis" + "category:Miscellaneous/Coq Extensions" + "logpath:Tactician" +] +url { + src: "https://github.com/coq-tactician/coq-tactician-dummy/archive/1.0-beta2-8.17.tar.gz" + checksum: "sha512=301266149d28b93bb8a747e170b6bdf5bca47ae5b21e9f31d652916c35d749f651ea2b472079db40e02d90a1b1e8137c3e956f9922f9d421a4751f20f0f5e364" +} diff --git a/released/packages/coq-tactician-stdlib/coq-tactician-stdlib.1.0~beta2+8.11/opam b/released/packages/coq-tactician-stdlib/coq-tactician-stdlib.1.0~beta2+8.11/opam new file mode 100644 index 000000000..21f271387 --- /dev/null +++ b/released/packages/coq-tactician-stdlib/coq-tactician-stdlib.1.0~beta2+8.11/opam @@ -0,0 +1,64 @@ +opam-version: "2.0" +name: "coq-tactician-stdlib" +synopsis: "Recompiles Coq's standard libary with Tactician's instrumentation loaded" +description: """ + *** WARNING *** This package will overwrite Coq's standard library files. + + This package recompiles Coq's standard library with Tactician's (`coq-tactician`) + instrumentation loaded such that Tactician can learn from the library. When you + install this package, the current `.vo` files of the standard library are backed + in the folder `user-contrib/Tactician/stdlib-backup`. The new `.vo` files are + equivalent to the originals, except that they also contain Tactician's tactic + databases. After installation of this package, all other Coq developments that + are installed will also need to be recompiled. The 'tactician recompile' command + line utility can help with this. + Upon removal of this package, the original files will be placed back. +""" +homepage: "https://coq-tactician.github.io" +dev-repo: "git+https://github.com/coq-tactician/coq-tactician-stdlib" +bug-reports: "https://github.com/coq-tactician/coq-tactician-stdlib/issues" +maintainer: "Lasse Blaauwbroek " +authors: "Lasse Blaauwbroek = "8.11" & < "8.12~"} + "coq-tactician" +] +build: [ + [make "-j%{jobs}%"] +] +install: [ + [make "install"] +] +remove: [ + [make "restore"] +] +tags: [ + "keyword:tactic-learning" + "keyword:machine-learning" + "keyword:automation" + "keyword:proof-synthesis" + "category:Miscellaneous/Coq Extensions" + "logpath:Tactician" +] +url { + src: "https://github.com/coq-tactician/coq-tactician-stdlib/archive/1.0-beta2-8.11.tar.gz" + checksum: "sha512=a19b9eb3710f89fbc26cae581d20f914530042993990bf203522aaa2e7bfcc07b5220050e703bd84981dfed376e76c700944074f58885d1b4fbd87f275e4f44f" +} diff --git a/released/packages/coq-tactician/coq-tactician.1.0~beta2+8.11/opam b/released/packages/coq-tactician/coq-tactician.1.0~beta2+8.11/opam new file mode 100644 index 000000000..84993ede8 --- /dev/null +++ b/released/packages/coq-tactician/coq-tactician.1.0~beta2+8.11/opam @@ -0,0 +1,67 @@ +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 "] +license: "MIT" +homepage: "https://coq-tactician.github.io" +bug-reports: "https://github.com/coq-tactician/coq-tactician/issues" +depends: [ + "ocaml" {>= "4.08"} + "dune" {>= "2.8"} + "dune-site" {>= "2.9.1"} + "opam-client" {>= "2.1.0"} + "cmdliner" {>= "1.1.0"} + "coq" {>= "8.11.0" & < "8.12~"} + "conf-git" + "bos" {>= "0.2.1"} + "coq-tactician-dummy" {= "1.0~beta2+8.11" & with-test} + "odoc" {with-doc} +] +build: [ + ["dune" "subst"] {dev} + [ + "dune" + "build" + "-p" + name + "-j" + jobs + "@install" + "@runtest" {with-test} + "@doc" {with-doc} + ] +] +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: "https://github.com/coq-tactician/coq-tactician/archive/1.0-beta2-8.11.tar.gz" + checksum: "sha512=cfc3750e2d8a22ea2e9c9445f6475c1d9f6357627d315530b3b58cf4e4b0cc330981dab61854b00f59a23a1e8605a2991cb1e96ab0a66105d2fc6aedce3328a6" +} diff --git a/released/packages/coq-tactician/coq-tactician.1.0~beta2+8.17/opam b/released/packages/coq-tactician/coq-tactician.1.0~beta2+8.17/opam new file mode 100644 index 000000000..5619e4430 --- /dev/null +++ b/released/packages/coq-tactician/coq-tactician.1.0~beta2+8.17/opam @@ -0,0 +1,70 @@ +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 "] +license: "MIT" +homepage: "https://coq-tactician.github.io" +bug-reports: "https://github.com/coq-tactician/coq-tactician/issues" +depends: [ + "ocaml" {>= "4.08"} + "dune" {>= "3.5" & < "3.8~"} + "dune-site" {>= "2.9.1"} + "opam-client" {>= "2.1.0"} + "cmdliner" {>= "1.1.0"} + "coq-core" {>= "8.17" & < "8.18~"} + "coq-stdlib" {with-test} + "conf-git" + "bos" {>= "0.2.1"} + "coq-tactician-dummy" {= "1.0~beta2+8.17" & 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: "https://github.com/coq-tactician/coq-tactician/archive/1.0-beta2-8.17.tar.gz" + checksum: "sha512=278ba081341b1ed455bec972fedab9278005915dd9c96eab70f0ec9a3bd356158474dbf16e4bb0190d811a2aa1393d8db27a8e9b59916211f4028f97340c4837" +}