1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
|
# Beginner's guide to hacking Coq
## Getting dependencies
See the first section of [`INSTALL.md`](../../INSTALL.md). Developers are
recommended to use a recent OCaml version, which they can get through
opam or Nix, in particular.
## Configuring Dune caching and default verbosity
There are several configuration settings that you can control globally
by creating a Dune configuration file (see `man dune-config` to learn
more). This file is generally located in `~/.config/dune/config` (this
is system-dependent). It should start with the version of the Dune
language used (by the configuration file---which can be different from
the one used in the Coq repository), e.g.:
```
(lang dune 2.0)
```
- You will get faster rebuilds if you enable Dune caching. This is
true in all cases, but even more so when using the targets in
`Makefile.dune` (see below).
To set up Dune caching, you should append the following line to your
Dune configuration file:
```
(cache enabled)
```
Note that by default, Dune caching will use up to 10GB of disk size.
See the [official documentation](https://dune.readthedocs.io/en/stable/caching.html#on-disk-size)
to learn how to change the default.
- Dune is not very verbose by default. If you want to change the
behavior to a more verbose one, you may append the following line to
your Dune configuration file:
```
(display short)
```
## Building `coqtop` / `coqc` binaries
We recommend that you use the targets in `Makefile.dune`. See
[`build-system.dune.md`](build-system.dune.md) to learn more about
them. In the example below, you may omit `-f Makefile.dune` by
setting `COQ_USE_DUNE=1`.
```
$ git clone https://github.com/coq/coq.git
$ cd coq
$ make -f Makefile.dune
# to get an idea of the available targets
$ make -f Makefile.dune check
# build all OCaml files as fast as possible
$ dune exec -- dev/shim/coqc-prelude test.v
# update coqc and the prelude and compile file test.v
$ make -f Makefile.dune world
# build coq and the complete stdlib and setup it for use under _build/install/default
# In particular, you may run, e.g., coq_makefile from _build/install/default
# to build some test project
```
When running the commands above, you may set `DUNEOPT=--display=short`
for a more verbose build (not required if you have already set the
default verbosity globally as described in the previous section).
Alternatively, you can use the legacy build system (which is now
a hybrid since it relies on Dune for the OCaml parts). If you haven't
set `COQ_USE_DUNE=1`, then you don't need `-f Makefile.make`.
```
$ ./configure -profile devel
# add -warn-error no if you don't want to fail on warnings while building the stlib
$ make -f Makefile.make -j $JOBS
# Make once for `merlin` (autocompletion tool)
<hack>
$ make -f Makefile.make -j $JOBS states
# builds just enough to run coqtop
$ bin/coqc <test_file_name.v>
<goto hack until stuff works>
```
When running the commands above, you may set `_DDISPLAY=short` for a
more verbose build.
To learn how to run the test suite, you can read
[`test-suite/README.md`](../../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`](https://github.com/ocaml/merlin) for autocomplete.
- [Wiki pages on tooling containing `emacs`, `vim`, and `git` information](https://github.com/coq/coq/wiki/DevelSetup)
- [`ocamlformat`](https://github.com/ocaml-ppx/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`.
|
