Meant to be used with ProofDB, a natural language Coq theorem search engine.
Currently we support Coq 8.16. Good support for newer versions is pending some issues12.
This software is of prototype quality. Expect sharp edges and inconveniences, and let us know what breaks!
$ opam switch create proofdb --packages="coq.8.16.1,ocaml.4.14.1" --repos="default" # add coq-released if you want.
$ git clone https://github.com/tom-p-reichel/proofdb-webui-client.git
$ cd proofdb-webui-client
$ opam install .We try to provide an instance of proofdb at https://proofdb.tompreichel.com. This is the one that is configured by default. We don't guarantee perfect uptime.
If you want to host your own server and use it with this client, you can issue the command ProofDB Endpoint Is "...". to change the API endpoint used.
In a Coq session, one should be able to simply:
Load ProofDB.Note that we can't "Require Import" it, because we're working around a Coq import bug1.
Then, natural language searches can be sent using the NLSearch command.
NLSearch "list reverse".One can also add additional search items (non-natural-language filters) similar to the built-in search command.
NLSearch "list reverse" list. (* results must contain the term `list` *)All search results must be embedded on the server side. If the server was just set up, it has no cache. It might take minutes to run searches if they're over thousands of theorems that have never been searched before! After that, searches should be much faster.
There is also a client side cache. First searches of a session will be somewhat slower before this is populated.
If you want to decrease delays associated with populating caches, just add additional filters to searches as in the usage section above. This will result in fewer theorems being considered for embedding.