Tactician beta2 for Coq 8.11 and 8.17

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 <[email protected]>"]
+authors: ["Lasse Blaauwbroek <[email protected]>"]
+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"
+}

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 <[email protected]>"]
+authors: ["Lasse Blaauwbroek <[email protected]>"]
+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"
+}

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 <[email protected]>"
+authors: "Lasse Blaauwbroek <[email protected]"
+license: "MIT"
+messages: [
+  "*** WARNING ***"
+  "This package will overwrite Coq's standard library files."
+  "A backup of the original files will be placed under Coq's"
+  "library directory at user-contrib/tactician-stdlib-backup/"
+  "and they will be restored when you remove this package."
+  "After installation of this package, all other Coq packages"
+  "also need to be recompiled. Running the 'tactician recompile'"
+  "command-line utility will help with this process."
+]
+post-messages: ["
+--- The standard library was successfully recompiled ---
+
+In order to finish the process, you should run
+
+tactician recompile
+" {success}]
+depends: [
+  "coq" {>= "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"
+}

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 <[email protected]>"]
+authors: ["Lasse Blaauwbroek <[email protected]>"]
+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"
+}

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 <[email protected]>"]
+authors: ["Lasse Blaauwbroek <[email protected]>"]
+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"
+}