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