Compilation mode

All three major modes, train, verify and export, are implemented internally by a fourth mode called compile. Ocasionally it may be useful to access this mode. These circumstances are listed below:

See the verification queries being generated

TODO

Export a specification without generating a proof cache

TODO