Merge pull request #2895 from LasseBlaauwbroek/tatician-agents

Packages coq-tactician-api, coq-graph2tac and coq-text2tac

released/packages/coq-graph2tac/coq-graph2tac.1.0.anon/files/Graph2TacConfig.v.in

@@ -0,0 +1 @@
+Set Tactician Neural Executable "g2t-server --arch tfgnn --model %{share}%/%{name}%/model --log_level=critical --tf_log_level=critical --tactic_expand_bound=256 --search_expand_bound=256 --update_new_definitions".

released/packages/coq-graph2tac/coq-graph2tac.1.0.anon/files/injection-flags

@@ -0,0 +1 @@
+-l Graph2TacConfig.v

released/packages/coq-graph2tac/coq-graph2tac.1.0.anon/opam

@@ -0,0 +1,50 @@
+opam-version: "2.0"
+synopsis: "Graph neural network that predicts tactics for Tactician"
+description:
+  "Graph2Tac is a novel neural network architecture for predicting appropriate
+  tactics for proof states. The crucial innovation of Graph2Tac is that it can
+  build an understanding of the math concepts in an entire Coq development and
+  all of its dependencies on-the-fly. That is, it analyzes the structure of
+  definitions and lemmas and builds an internal representation of each object
+  in the global context. Then, when presented with a proof state that
+  references these mathematical concepts, Graph2Tac can leverage its deep
+  knowledge to predict tactics and arguments."
+maintainer: ["Lasse Blaauwbroek <[email protected]>"]
+authors: [
+  "Jason Rute"
+  "Mirek Olsak"
+  "Lasse Blaauwbroek"
+  "Fidel I. Schaposnik Massolo"
+  "Jelle Piepenbrock"
+  "Vasily Pestun"
+]
+license: "https://zenodo.org/records/10410474/files/LICENSE.md"
+homepage: "https://coq-tactician.github.io/api/graph2tac"
+bug-reports:
+    "https://github.com/IBM/graph2tac/issues"
+conflict-class: ["tactician-neural-model"]
+build: [
+  [ "tar" "-xzf" "model.tar.gz" "--one-top-level" "--strip-components" "1" ]
+]
+install: [
+  [ "mkdir" "-p" "%{share}%/%{name}%/" ]
+  [ "cp" "-r" "model/" "%{share}%/%{name}%/" ]
+
+  [ "cp" "Graph2TacConfig.v" "%{lib}%/coq/user-contrib/Tactician/Graph2TacConfig.v" ]
+
+  # We have to make sure that our injection flags get loaded after the injection flags of coq-tactician-api.
+  # We do this by using a name that is guaranteed to sort after coq-tactician-api.
+  [ "mkdir" "-p" "%{share}%/coq-tactician/plugins/coq-tactician-api-%{name}%/" ]
+  [ "cp" "injection-flags" "%{share}%/coq-tactician/plugins/coq-tactician-api-%{name}%/" ]
+]
+dev-repo: "git+https://github.com/IBM/graph2tac.git"
+depends: [
+  "coq-tactician-api" {= "15.0+8.11"}
+]
+  extra-source "model.tar.gz" {
+  src: "https://zenodo.org/records/10410474/files/graph2tac-anon.tar.gz"
+       checksum: "md5=7ad3473b25bc515fead4353264263cce"
+}
+substs: [
+  "Graph2TacConfig.v"
+]

released/packages/coq-tactician-api/coq-tactician-api.15.0+8.11/opam

@@ -0,0 +1,59 @@
+opam-version: "2.0"
+synopsis: "An API exposing Coq's web of formal knowledge to external agents"
+description: """
+   Tactician's API provides external machine learning agents with the data
+   collected by Tactician from the Coq Proof Assistant. It is able to extract
+   large-scale datasets from a wide variety of Coq packages for the purpose of
+   offline machine learning. Additionally, it allows agents to interact with
+   Coq. Proving servers can be connected to Tactician's `synth` tactic and prove
+   theorems for Coq users. Additionally, servers can do proof exploration
+   through the `Tactician Explore` command."""
+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-api/issues"
+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-api.git"
+depends: [
+  "ocamlfind"
+  "coq" {>= "8.11" & < "8.12~"}
+  "coq-tactician" {= "1.0~beta2~neural+8.11"}
+  "logs"
+  "fmt"
+  "capnp-rpc-unix"
+  "capnp-rpc-lwt"
+  "capnp" {>= "3.4.0"}
+  "ppx_deriving"
+  "ocamlgraph"
+  "xxhash"
+  "dune" {>= "2.9"}
+  "odoc" {with-doc}
+  # These constraints are to work around
+  # https://github.com/ocsigen/lwt/issues/764 and
+  # https://github.com/ocaml/ocaml/pull/9914
+  "ocaml" {>= "4.12~"} | ("ocaml" {< "4.12~"} & "lwt" {<= "5.1.1"})
+]
+substs: [
+  "src/graph_generator_learner.ml"
+  "theories/injection-flags-loader"
+]
+url {
+  src: "https://github.com/coq-tactician/coq-tactician-api/archive/refs/tags/v15.0-8.11.tar.gz"
+  checksum: "sha512=a42d446726f4cb7a54213f7b546c86165eb3f3901890ad198661424798a4ec676fe22b2e8091683a025da9be834519d73bc518cd405ce0b5fe5c1af47bdea19a"
+}

released/packages/coq-tactician/coq-tactician.1.0~beta2~neural+8.11/opam

@@ -0,0 +1,72 @@
+opam-version: "2.0"
+synopsis:
+  "Tactician: A Seamless, Interactive Tactic Learner and Prover for Coq"
+description: """
+This version of Tactician is specifically meant to be used with the 'graph2tac'
+and 'text2tac' for neural-based proof synthesis. Avoid this version for other
+purposes.
+
+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"
+flags: [avoid-version]
+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/refs/tags/1.0-beta2.1-8.11-neural.tar.gz"
+  checksum: "sha512=c3bcc342dc0d1bfa53640f50ab9bdf96de43d0493f594d52e8d6570532afb0edfba1ac828123f516a4d66c6d4ba0947fad5a6d77eb5407c5a4d7aa5ca3c09d13"
+}

released/packages/coq-text2tac/coq-text2tac.1.0/files/Text2TacConfig.v.in

@@ -0,0 +1,2 @@
+Set Tactician Neural Textmode.
+Set Tactician Neural Executable "text2tac-server --dev cpu --pt_threads 1 --temp 1.0 --truncate_side left --model %{share}%/%{name}%/model/pytorch_model.bin --tokenizer=%{share}%/%{name}%/model/ --beam_width=20".

released/packages/coq-text2tac/coq-text2tac.1.0/files/injection-flags

@@ -0,0 +1 @@
+-l Text2TacConfig.v

released/packages/coq-text2tac/coq-text2tac.1.0/opam

@@ -0,0 +1,38 @@
+opam-version: "2.0"
+synopsis: "Language model that predicts tactics for Tactician"
+description:
+  "Text2Tac is a language model for synthesizing tactics. It receives the
+  current proof state as a human-readable prompt and “completes” this prompt
+  by synthesizing a tactic."
+maintainer: ["Jelle Piepenbrock"]
+authors: ["Jelle Piepenbrock"]
+license: "https://zenodo.org/records/10410474/files/LICENSE.md"
+homepage: "https://coq-tactician.github.io/api/text2tac"
+bug-reports:
+    "https://github.com/JellePiepenbrock/text2tac/tree/text2tac/issues"
+conflict-class: ["tactician-neural-model"]
+build: [
+  [ "tar" "-xzf" "model.tar.gz" "--one-top-level" "--strip-components" "1" ]
+]
+install: [
+  [ "mkdir" "--parents" "%{share}%/%{name}%/" ]
+  [ "cp" "-r" "model/" "%{share}%/%{name}%/" ]
+
+  [ "cp" "Text2TacConfig.v" "%{lib}%/coq/user-contrib/Tactician/Text2TacConfig.v" ]
+
+  # We have to make sure that our injection flags get loaded after the injection flags of coq-tactician-api.
+  # We do this by using a name that is guaranteed to sort after coq-tactician-api.
+  [ "mkdir" "-p" "%{share}%/coq-tactician/plugins/coq-tactician-api-%{name}%/" ]
+  [ "cp" "injection-flags" "%{share}%/coq-tactician/plugins/coq-tactician-api-%{name}%/" ]
+]
+dev-repo: "git+https://github.com/JellePiepenbrock/text2tac.git"
+depends: [
+  "coq-tactician-api" {= "15.0+8.11"}
+]
+extra-source "model.tar.gz" {
+  src: "https://zenodo.org/records/10410474/files/text2tac.tar.gz"
+  checksum: "md5=50d688940a24796867fbfc48f085bc4f"
+}
+substs: [
+  "Text2TacConfig.v"
+]