Tips on Developing Coq

Setup

  1. sudo apt install opam (OCaml package manager)
  2. opam init && opam switch create ocaml-base-compiler (OCaml compiler)
  3. opam install num ocamlfind ounit merlin user-setup (OCaml libraries needed for compilation and development)
  4. opam user-setup install (configuring Merlin)
  5. For VSCode, use the OCaml and Reason IDE by Darin Morrison

Debugging

Building

  1. ./configure -profile devel (use -warn-error no to turn off errorfying warnings)
  2. make coqbinaries (native code) or make byte (bytecode) to build toplevel
  3. make coqlib to build libraries; make theories/<path>/<file>.vo for specific library

Using coqtop

  1. bin/coqtop or bin/coqtop.byte
  2. Drop.
  3. #use “base_include”;; for basic printing or #use “include”;; for pretty-printing
  4. #trace Module.function;;
  5. go();;
  6. Run your Coq code in the prompt; CTRL-D to exit

Useful functions

Helpers for printing out Pp.t and constr with a prefixed message:

let print_pp msg ppt =
  let open Format in
  let open Pp in
  pp_with std_formatter @@ str msg ++ spc () ++ ppt ++ fnl ()

let print_constr msg cstr =
  print_pp msg (debug_print cstr)

Using ocamldebug

  1. make && make byte
  2. dev/ocamldebug-coq bin/coqtop.byte
  3. source db to load printers (optional)
  4. break @ Module 123 to set breakpoint at line 123 of module.ml
  5. run, then run your Coq code in the prompt
  6. Useful commands (more here):
    • s to step into a function
    • n to go to the next function
    • p var to print the variable var
    • li to print the surrounding lines of the current breakpoint

Unit testing

Running tests

  1. make bin/coqtop to compile to native code; make bin/coqide to compile CoqIDE if needed
  2. In test-suite, run make unit-tests/<dir>/*.ml.log to run the unit tests in test-suite/unit-tests/<dir> (or make unit-tests/**/*.ml.log to run all)
  3. make summary to see test files run; make report PRINT_LOGS=1 to see test failures

Test template

open Utest

let log_out_ch = open_log_out_ch __FILE__

let test1 = mk_{eq,bool}_test "name" "description" ...
...
let testn = ...
let tests = [test1;...;testn]

let _ = run_tests __FILE__ log_out_ch tests

Plugins

Use the plugin example_plugin with the command Declare ML Module “example_plugin”. Rerun ./configure so that .cma files will be created during make byte. In Makefile.common, add to PLUGINDIRS and PLUGINSCMO so that .cmo files will be created during make pluginsopt.

In example.mlg:

{

open Example
...

}

DECLARE PLUGIN "example_plugin"

VERNAC COMMAND EXTEND CommandName CLASSIFIED AS SIDEFF
| [ "Set" "Flag" ] -> { set_flag true }
END

VERNAC COMMAND EXTEND CommandName CLASSIFIED AS QUERY
| [ "Print" "Stuff" ] -> { print_stuff () }
END

In example.ml:

let set_flag b = ...
let print_stuff () = ...

In example.mli:

val set_flag b : bool -> unit
val print_stuff : unit -> unit

In example_plugin.mlpack:

Example
G_example

Type inference

Important types and functions

Constr

  • constr: Main AST of the Coq kernel (“constructions”)
  • mk*, is*, dest*: Functions for creating, testing membership, and destroying (extracting data from) constr
  • compare_head_gen_leq_with: Tests for subtyping on types and alpha equivalence on terms, with optional collection of stage constraints
  • constr_ord_int: Comparison function for total ordering with alpha equivalence (nothing to do with subtyping)

Typeops

  • execute: Main inference algorithm
  • infer*: Entry points to inference algorithm
  • check_cast: Entry point to subtyping (i.e. conv rule)

CClosure

  • fconstr: Frozen version of Constr.constr for closure

Reduction

  • eqappr: Tests for subtyping on fterm, similar to compare_head_gen_leq_with (probably)

Term

Contains functions for decomposing and recomposing lambdas, products, and arities.

Pretyping

  • search_guard: Guard-checking entry point for fixpoints. Used by other functions to “guess” the recursive indices of fixpoints.

Other

  • If the dependencies of kernel/declarations.ml are changed, e.g. adding a new field to a variant in Constr.constr, changes may be needed in checker/values.ml, e.g. in Values.v_constr. Failure to make the necessary changes may result in mysterious segfaults.
  • Changes to Constr.constr need to be reflected in the hashing functions in Constr.