Emilio Jesús Gallego Arias edited this page Nov 9, 2018 · 2 revisions

Dune information for Coq developers

The main readme is at https://github.com/coq/coq/blob/master/dev/doc/build-system.dune.md


How to use dune-built Coq?

A complete Coq build is at _build/install/default. It usually suffices to call the binary, however dune exec may help with PATH and such.

How to install with dune (without opam)

Use dune-install or any tool that understand .install files.

dune complains about "File foo is both generated by a rule and present in the source tree."

This is generally caused by having used the make-based build system in the past. dune expects to have control over generated files (which it mostly puts in _build except for a few like .merlin), but the make-based system does not respect this assumption.

make distclean should resolve the issue. Occasionally this won't be enough (generally version A generated foo.ml, then version B stopped using it, and make distclean doesn't know that some arbitrary ml file was generated by a previous version) in which case git clean -xfd will keep only your git tracked files (make sure that you have no untracked files that you want to keep).

dune and manual ./configure

Before coq_dune passed the -coqlib flag using ./configure manually could break the dune build. Nowadays I think the error is delayed to when you try to use the dune-built Coq (unconfirmed).

Clone this wiki locally
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.
Press h to open a hovercard with more details.