The package coq-tactician-api makes some commands available in addition to the usual commands listed in the manual. You should install this package when you wish to build your own external agent. (Both Graph2Tac and Text2Tac depend on this package.)

Graph Visualizations

These commands will create a graph of some object, and write it to graph.pdf (if graphviz is available).

The following commands are always available:

[Shared] Graph [Depth <n>] Ident identifier.
[Shared] Graph [Depth <n>] Term term.

The normal commands print a fully transitive graph. Adding Depth i limits the traversal to visiting at most i nested definitions.

Additionally, in proof mode, these commands are available:

[Shared] Graph [Depth <n>] Proof.

Options that modify the graphs generated by the commands above are

[Set | Unset] Tactician Neural Visualize Ordered.
[Set | Unset] Tactician Neural Visualize Labels.
[Set | Unset] Tactician Neural Visualize Hashes.

Interaction with synth

In order to connect Tactician’s synth tactic to a external tactic prediction server like the dummy pytact-server described provided by PyTactician, the plugin makes a number of commands and settings available in Coq. In order to load the plugin, Coq needs to be started appropriately. This can be done by prefixing every invocation of a command that uses Coq, like coqc, coqide, a make command or an editor like emacs with tactician exec:

tactician exec -- coqc ...
tactician exec -- coqide ...
tactician exec -- make ...
tactician exec -- dune build ...
tactician exec -- emacs ...

To make the synth command available, your Coq file will have to start with

From Tactician Require Import Ltac1.

The following settings govern the data that Coq will send to the server:

• Set Tactician Neural Textmode determines wether Coq is communicating with a graph-based server or a text-based server (graph-based by default).
• Set Tactician Neural Metadata adds text-based metadata to when communicating in graph-mode, such as hypothesis names, textual representation of proof states and textual representations of definition. This will slow down the communication protocol, and should only be enabled for debugging, or when otherwise needed.

To let Coq take care of starting and stopping the server, use the command

Set Tactician Neural Executable "external-server-executable --argument1 --argument2".

If you have a prediction server already running somewhere over TCP, you can make Coq connect to it using

Set Tactician Neural Server "<address>:<port>".

At this point, you have the following commands available which will interact with the server:

• Tactician Neural Alignment will ask the which tactics and definitions currently in scope are unknown to it. This is meant as a sanity check.
• Suggest and Debug Suggest will ask the server for predictions for the current proof state.
• synth and debug synth will perform a proof search by repeatedly asking the server for predictions.
• Tactician Neural Cache will preemptively send a lot of required data to the prediction server and keeps that information cached. This will make the commands above run much faster. This command can be issued multiple times in a document, creating multiple nested caches.
• Set Tactician Autocache will automatically execute Tactician Neural Cache on each command. This is an experimental option, and there may be some overhead associated with this.

Client-based proof exploration

Finally, the command Tactician Explore. will initiate a proof exploration session. An example of this is available in TestReinforceStdin.v. To do this, you need to have a python client running. An example is available in the pytact-prover executable. To see how it works, run pytact-prover --pdfsequence --pdfname test This will execute a dummy proof through the proof exploration interface. Visualizations of each proof state are available in test<n>.pdf. optionally --file option to point to a source Coq .v file. Also with --interactive option the interactive shell appears where you can manually interact with the environment. Whenever a tactic is executed, the resulting proof state if visualized in the file python_graph.pdf.