pytact
PyTactician
This is the API documentation of the PyTactician library that assists in
interfacing with Tactician's API to the Coq proof assistant from Python. The
main entry-point for the API is pytact.data_reader, which contains functions
for loading and exploring dataset as well as abstractions around the
communication protocol with Coq.
PyTactician also provides several command-line programs such as a dataset
sanity checker, a visualization webserver, and several proving servers. Their
implementations may be instructive examples on the usage of pytact.data_reader.
Implementations for each program can be found here:
pytact-server:pytact.fake_python_serveris a minimal example for a proving serverpytact-oracle:pytact.oracle_serveris a good example both of a proving server and getting data from a datasetpytact-visualize:pytact.graph_visualize_browsefor the visualization logic andpytact.visualisation_webserverfor the serverpytact-check:pytact.graph_sanity_check(mostly low-level access to the dataset, not idiomatic high-level code)
In addition to these programs, there are some code snippets in pytact.scripts
that may be instructive.
1"""# PyTactician 2 3This is the API documentation of the PyTactician library that assists in 4interfacing with Tactician's API to the Coq proof assistant from Python. The 5main entry-point for the API is `pytact.data_reader`, which contains functions 6for loading and exploring dataset as well as abstractions around the 7communication protocol with Coq. 8 9PyTactician also provides several command-line programs such as a dataset 10sanity checker, a visualization webserver, and several proving servers. Their 11implementations may be instructive examples on the usage of `pytact.data_reader`. 12Implementations for each program can be found here: 13 14- `pytact-server`: `pytact.fake_python_server` is a minimal example for a proving server 15- `pytact-oracle`: `pytact.oracle_server` is a good example both of a proving server 16 and getting data from a dataset 17- `pytact-visualize`: `pytact.graph_visualize_browse` for the visualization logic 18 and `pytact.visualisation_webserver` for the server 19- `pytact-check`: `pytact.graph_sanity_check` (mostly low-level access to the 20 dataset, not idiomatic high-level code) 21 22In addition to these programs, there are some code snippets in `pytact.scripts` 23that may be instructive. 24 25"""