Tips on Developing Rocq

15 May 2021 • Computer Touching

N.B. These notes date back to before the name change to Rocq.

The following is a grab bag of tips on developing Rocq itself, from writing plugins for it to modifying the trusted kernel.

Further references:

Setup

For writing OCaml in VSCode, use the OCaml and Reason IDE plugin by Darin Morrison.

$ sudo apt install opam                                 # OCaml package manager
$ opam init && opam switch create ocaml-base-compiler   # OCaml compiler
$ opam install ocamlfind zarith ounit merlin user-setup # OCaml libraries
$ opam user-setup install                               # configuring Merlin
$ ./configure -profile devel -warn-error no             # local binaries, disable errorfying warnings
$ make coqbinaries                # make native code toplevel
$ make byte                       # make bytecode toplevel
$ make coqocaml                   # make all OCaml code
$ make init                       # make Init libraries
$ make coqlib                     # make all Coq libraries
$ make theories/<PATH>/<FILE>.vo  # make a specific library

Debugging

Printing

let open Format in
let open Pp in
let msg : string = ... in
let cstr : Constr.constr = ... in
(* See Pp.mli for more handy dandy pretty printers *)
let prs : Pp.t list = [str msg; spc (); Constr.debug_print cstr; fnl ()] in

(* Print to file *)
let oc = open_out_gen [Open_append; Open_creat] 0o666 "out.txt" in
let fmt = formatter_of_out_channel oc in
pp_with fmt @@ seq prs;
pp_print_flush fmt ();
close_out oc;

(* Print to stdout *)
pp_with std_formatter @@ seq prs;

From toplevel

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

Using ocamldebug

  1. dev/ocamldebug-coq bin/coqtop.byte
  2. source db (optionally load printers)
  3. break @ Module 123 to set breakpoint at line 123 in module.ml
  4. run, then run Coq code in prompt
  5. Useful commands (see OCaml manual for more):
    • s: Step into function
    • n: Next function
    • p var: Print variable var
    • li: Print surrounding lines

Unit tests

Test template

open Utest

let log_out_ch = open_log_out_ch __FILE__

let test1 = mk_{eq, bool}_test "<NAME>" "<DESC>" ...
...
let testn = ...
let tests = [test1;...;testn]

let _ = run_tests __FILE__ log_out_ch tests

Running tests

$ make bin/coqtop bin/coqide
$ cd test-suite
$ make unit-tests/<DIR>/*.ml.log  # run tests in `unit-tests/<DIR>`
$ make unit-tests/**/*.ml.log     # run all unit tests
$ make summary                    # print list of tests that were run
$ make report PRINT_LOGS=1        # print test failures

Plugins

$ ./configure -profile devel           # make sure *.cma files will be built
$ make byte
$ bin/coqtop.byte
> Declare ML Module "example_plugin".  # load plugin

plugins/example/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

plugins/example/example.ml(i)

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

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

plugins/example/example_plugin.mlpack

Example
G_example

Relevant modules for typing

Constr

  • constr: Main AST of Coq core (“constructions”)
  • mk*, is*, dest*: Create/test membership/destruct constr
  • compare_head_gen_leq_with: Subtyping and alpha equivalence of terms
  • constr_ord_int: Total ordering with alpha equivalence (unrelated to subtyping)

Typeops

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

CClosure

  • fconstr: Frozen version of Constr.constr for closures

Reduction

  • eqappr: Subtyping on fterm, similar to Constr.compare_head_gen_leq_with (probably)

Other modules

  • Term: Contains functions for making and decomposing lambdas, products, arities
  • Term_typing: Main caller of Typeops functions
  • Univ: Type universes
  • uGraph: Specialization of acyclic graphs to universe levels for constraint solving

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 also need to be reflected in Constr.hash*.
 proof assistants  Coq  Rocq