2.1.9 Coq with coq and SerAPI

2.1.10 Coq Module Organization

The ‘coq’ module is split into two layers. The lower layer, implemented in ‘serapi-io.lisp’, is strictly responsible for serialization of Coq abstract syntax trees (ASTs). This is done with Coq SerAPI https://github.com/ejgallego/coq-serapi, specifically ‘sertop’, which allows for querying of Coq documents and serializes ASTs to S-expressions.

The ‘coq’ and ‘coq-project’ software objects, implemented in ‘coq.lisp’ and ‘coq-project.lisp’, respectively, are higher-level abstractions built on ‘serapi-io’. Ideally, clients should only have to construct software objects anduse API functions provided by ‘coq.lisp’ or ‘coq-project.lisp’ without having to worry about the lower-level functions.

2.1.11 Setting up SerAPI

In order to construct a Coq software object, coq-serapi must be installed. Refer to its GitHub project page for instructions. The variables ‘*sertop-path*’ and ‘*sertop-args*’ must then be set. This can be done either with ‘setf’ or by setting the environment variables ‘SERAPI’ and ‘COQLIB’ and invoking ‘set-serapi-paths’ to update the Lisp variables. ‘SERAPI’ and ‘*sertop-path*’ should point to the sertop executable.

If you intend to use the Coq standard library, you will need to ensure that sertop is started with the ‘–coqlib’ flag pointing to the coq/lib directory. This can be done either by setting the environment variable ‘COQLIB’ to that path or by setting ‘*sertop-args*’ to (list ``--coqlib=/path/to/coq/lib/''). Other sertop parameters may also be added to ‘*sertop-args*’.

2.1.12 Coq Module Organization

The ‘coq’ module is split into two layers. The lower layer, implemented in ‘serapi-io.lisp’, is strictly responsible for serialization of Coq abstract syntax trees (ASTs) and is described in-depth in its own section.

The ‘coq’ and ‘coq-project’ software objects, implemented in ‘coq.lisp’ and ‘coq-project.lisp’, respectively, are higher-level abstractions built on ‘serapi-io’. Ideally, clients should only have to construct software objects and use API functions provided by ‘coq.lisp’ or ‘coq-project.lisp’ without having to worry about the lower-level functions.

2.1.13 Creating Coq Objects

Coq software objects have the following fields:

• project-file path to _CoqProject file
• file-source path to the Coq source file this object represents
• imports list of ASTs representing load or require statements
• genome list of ASTs representing the Coq source, excluding imports
• ast-ids list of AST IDs assigned to ASTs in the genome
• fitness fitness of the object last time it was evaluated

The recommended way to create a Coq software object is using ‘from-file’:

    (with-serapi ()
      (from-file (make-instance 'coq :project-file "/path/to/_CoqProject")
                 "/path/to/Foo.v"))

If you don’t have a _CoqProject file, you may omit the ‘:project-file’ keyword.

Since many API functions require interactions with SerAPI, a ‘with-serapi’ macro is provided to automatically create a sertop process. This works by binding the dynamic variable ‘*serapi-process*’ to an interactive sertop process. This is important to be aware of if you intend to use multiple threads: each thread _must_ have its own separate sertop process (in bordeaux-threads this may be accomplished by creating thread-local copies with ‘*default-special-bindings*’).

Each ‘-I’ or ‘-R’ line in _CoqProject will be automatically added to the Coq loadpath in the sertop process. If a new sertop process is created, you must ensure that these load paths are reset and any imports are reloaded. You can do this with either ‘set-load-paths’ (which only sets the load paths) or ‘reset-and-load-imports’ (which in addition to setting load paths also executes import statements).

2.1.14 Usage of Coq Objects

The ASTs of a Coq genome are lists whose elements are lists, symbols, and strings. A ‘type-safe-swap’ mutation selects two subtrees that have the same “tag” (i.e., the first symbol in that list) and swaps them. Favoring this mutation helps to cut down on type errors that would result from swapping arbitrary subtrees.

Additional mutations are forthcoming.

In the AST representations provided by Coq, many statements include location information tying AST nodes to locations in the source file. To help reduce the size of the AST, ‘from-file’ replaces the full location information with the list ‘(:loc nil)’. This ensures that it’s clear where the location information was without overly cluttering the AST. The implementation of ‘lookup-source-strings’ ensures that these are removed prior to sending the ASTs to sertop to look up source strings. The default implementations of ‘pick-bad’ and ‘pick-good’ for Coq objects exclude “located” statements.

Since sertop maintains a stateful representation of definitions that have been loaded and Coq prevents redefinition, it is sometimes necessary to reset the state of sertop to an earlier state. The easiest way to do this is to use ‘insert-reset-point’ to indicate that you may later want to restore sertop to the current state, and ‘reset-serapi-process’ to reset to a previously saved state. Both ‘from-file’ and ‘reset-and-load-imports’ insert a reset point before returning.