diff options
Diffstat (limited to 'dev/doc')
| -rw-r--r-- | dev/doc/build-system.dune.md | 34 |
1 files changed, 27 insertions, 7 deletions
diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index 37c6e2f619..cd35064b18 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -108,24 +108,44 @@ automatically. You can use `ocamldebug` with Dune; after a build, do: ``` -dune exec -- dev/dune-dbg /path/to/foo.v +dune exec -- dev/dune-dbg coqc foo.v (ocd) source dune_db ``` -or +to start `coqc.byte foo.v`, other targets are `{checker,coqide,coqtop}`: ``` -dune exec -- dev/dune-dbg checker Foo +dune exec -- dev/dune-dbg checker foo.vo (ocd) source dune_db ``` -for the checker. Unfortunately, dependency handling here is not fully -refined, so you need to build enough of Coq once to use this target -[it will then correctly compute the deps and rebuild if you call the -script again] This will be fixed in the future. +Unfortunately, dependency handling here is not fully refined, so you +need to build enough of Coq once to use this target [it will then +correctly compute the deps and rebuild if you call the script again] +This will be fixed in the future. For running in emacs, use `coqdev-ocamldebug` from `coqdev.el`. +**Note**: If you are using OCaml >= 4.08 you need to use + +``` +(ocd) source dune_db_408 +``` + +or + +``` +(ocd) source dune_db_409 +``` + +depending on your OCaml version. This is due to several factors: + +- OCaml >= 4.08 doesn't allow doubly-linking modules, however `source` + is not re entrant and seems to doubly-load in the default setup, see + https://github.com/coq/coq/issues/8952 +- OCaml >= 4.09 comes with `dynlink` already linked in so we need to + modify the list of modules loaded. + ## Dropping from coqtop: After doing `make -f Makefile.dune voboot`, the following commands should work: |