README.md

Beginner's guide to hacking Coq

Getting dependencies

See the first section of INSTALL. Developers are recommended to use a recent OCaml version, which they can get through opam or Nix, in particular.

Building coqtop

The general workflow is to first setup a development environment with the correct configure settings, then hacking on Coq, make-ing, and testing.

This document will use $JOBS to refer to the number of parallel jobs one is willing to have with make.

$ git clone git clone https://github.com/coq/coq.git
$ cd coq
$ ./configure -profile devel
$ make -j $JOBS # Make once for `merlin`(autocompletion tool)

<hack>

$ make -j $JOBS states # builds just enough to run coqtop
$ bin/coqtop -compile <test_file_name.v>
<goto hack until stuff works>

<run test-suite>

To learn how to run the test suite, you can read test-suite/README.md.

Coq functions of interest

• Coqtop.start: This function is the main entry point of coqtop.
• Coqtop.parse_args : This function is responsible for parsing command-line arguments.
• Coqloop.loop: This function implements the read-eval-print loop.
• Vernacentries.interp: This function is called to execute the Vernacular command user have typed. It dispatches the control to specific functions handling different Vernacular command.
• Vernacentries.vernac_check_may_eval: This function handles the Check ... command.

Development environment + tooling

• Merlin for autocomplete.
• Wiki pages on tooling containing emacs, vim, and git information
• ocamlformat provides support for automatic formatting of OCaml code. To use it please run dune build @fmt, see ocamlformat's documentation for more help.

A note about rlwrap

When using rlwrap coqtop make sure the version of rlwrap is at least 0.42, otherwise you will get

rlwrap: error: Couldn't read completions from /usr/share/rlwrap/completions/coqtop: No such file or directory

If this happens either update or use an alternate readline wrapper like ledit.