package coq-tactician-api
An API exposing Coq's web of formal knowledge to external agents
Install
Dune Dependency
Authors
Maintainers
Sources
v15.0-8.11.tar.gz
sha512=a42d446726f4cb7a54213f7b546c86165eb3f3901890ad198661424798a4ec676fe22b2e8091683a025da9be834519d73bc518cd405ce0b5fe5c1af47bdea19a
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.
Published: 11 Jan 2024
Dependencies (15)
-
lwt
<= "5.1.1" -
ocaml
< "4.12~" -
ocaml
>= "4.12~" -
dune
>= "2.9" - xxhash
- ocamlgraph
- ppx_deriving
-
capnp
>= "3.4.0" - capnp-rpc-lwt
- capnp-rpc-unix
- fmt
- logs
-
coq-tactician
= "1.0~beta2~neural+8.11" -
coq
>= "8.11" & < "8.12~" - ocamlfind
Dev Dependencies (1)
-
odoc
with-doc
Used by (2)
Conflicts
None
On This Page