Skip to content

build-system.dune.md

Latest commit

 

History

History
337 lines (248 loc) · 12.8 KB

build-system.dune.md

File metadata and controls

337 lines (248 loc) · 12.8 KB

This file documents what a Rocq developer needs to know about the Dune-based build system.

About Dune

Rocq uses the Dune build system.

Quick Start

Usually, using the latest version of Dune is recommended, see the first line of the dune-project file for the minimum required version.

It is strongly recommended that you use the helper targets available in Makefile, make will display help. Note that dune will call configure for you if needed, so no need to call ./configure in the regular development workflow, unless you want to tweak options.

2 common operations are:

  • make check : build all ml targets as fast as possible
  • make world : build a complete Rocq distribution

For more targeted builds, you can also call dune directly. First, call make dunestrap to generate necessary build files (the make targets above do it automatically). Then you can use:

  • dune exec -- rocq <args...>: build and launch rocq (does not build the worker and Prelude.vo). with arguments of your choice
  • dune build $target: where $target can refer to the build directory or the source directory [but will be placed under _build]

You need to run make dunestrap again if the dependencies between the core library .v files have changed.

dune build @install will build all the public Rocq artifacts; dune build builds the @default alias, defined in the top level dune file.

Dune puts build artifacts in a separate directory _build/$context; usual context is default; dune also produces an "install" layout under _build/install/$context/. Depending on whether you want refer to the source layout or to the install layout, you may refer to targets in one or the other directory. It will also generate an .install file so files can be properly installed by package managers.

Dune doesn't allow leftovers of object files it may generate in-tree [as to avoid conflicts], so please be sure your tree is clean from objects files generated by the make-based system or from manual compilation.

Contrary to other systems, Dune doesn't use a global Makefile but local build files named dune which are later composed to form a global build, for example plugins/ltac/dune or kernel/dune.

As a developer, Dune should take care of all OCaml-related build tasks including library management, merlin setup, linking order, etc... You should not have to modify dune files in regular workflow unless you are adding a new binary, library, or plugin, or want to tweak some low-level option.

The bootstrap process / rule generation

Dune is able to build all the OCaml parts of Rocq in a pretty standard way, using its built-in rule generation for OCaml. Public tools written in OCaml are distributed in the rocq-runtime package.

The set of public .v files present in this repository, usually referred as the "Rocq prelude" are distributed in the rocq-core package. As of June 2022, Dune has a set of built-in rules for .v files which is capable of building Rocq's core library.

However, in order to have a bit more control, we generate ourselves a set of custom rules using the tools/dune_rule_gen binary, which are then stored in the theories/dune file. This allows us to have a finer control over the build rules without having to bump the Dune version. The generation of the theories/dune and user-contrib/*/dune files is known as "bootstrap".

The rule generation code in tools/dune_rule_gen is mostly derived from Dune's built-in rules, and it works in an straightforward way: it will scan a directory with .v files in it, and output the corresponding build rule. The script will look at some configuration values such as whether native is enabled or not and adapt rule generation accordingly.

In the case of native, the script supports two modes, coqc -native-compiler on and coqnative. The default is the first, as currently coqnative incurs a 33% build time overhead on a powerful 16-core machine.

There are several modes for the rule generation script to work, depending on the parameter passed. As of today, it support -async.

-async will pass -async-proofs on to coqc.

Per-User Custom Settings

Dune will read the file ~/.config/dune/config; see man dune-config. Among others, you can set in this file the custom number of build threads (jobs N) and display options (display _mode_).

Running binaries (rocq compile, rocq top)

You should generally run make world before running rocq so that the corelib is built and placed in _build/install.

If building the corelib produces an error outside the prelude, make world will still result in a usable state (of course you won't be able to Require any failed files).

For errors inside the prelude, invoke rocq with -boot -noinit -R _build/default/theories/Corelib Corelib. For instance if you get an error in Datatypes,

dune exec -- rocq compile -boot -noinit -R _build/default/theories/Corelib Corelib _build/default/theories/Corelib/Init/Datatypes.v

should reproduce it.

dune exec -- rocq compile -boot -noinit -R _build/default/theories/Corelib Corelib -R theories/Corelib Corelib theories/Corelib/Init/Datatypes.v

should be equivalent.

Giving -boot -R _build/default/theories/Corelib Corelib to an IDE while visiting a file in theories/Corelib/Init should combine with theories/Corelib/Init/_CoqProject to produce the above result, eg

dune exec -- rocqide -boot -R _build/default/theories/Corelib Corelib theories/Corelib/Init/Datatypes.v

should work to reproduce the error interactively.

Building custom toplevels

You can build custom toplevels by tweaking the toplevel/dune files, for example, to add plugins to be linked statically using the (libraries ...) field.

Note that Rocq relies on a hidden Dune hack, which will add -linkall to binaries if they depend on the findlib.dynload library. As of today, rocq-runtime.vernac uses findlib.dynload, so if your toplevel hooks at the rocq-runtime.vernac or above level, you should be OK, otherwise add -linkall to Dune's (link_flags ...) field for your binary.

Targets

The default dune target is dune build (or dune build @install), which will scan all sources in the Rocq tree and then build the whole project, creating an "install" overlay in _build/install/default.

You can build some other target by doing dune build $TARGET, where $TARGET can be a .cmxa, a binary, a file that Dune considers a target, an alias, etc...

In order to build a single package, you can do dune build $PACKAGE.install.

A very useful target is dune build @check, that will compile all the ml files in quick mode.

Dune also provides targets for documentation, testing, and release builds, please see below.

Testing and documentation targets

There are two ways to run the test suite using Dune:

  • After building Rocq with make world, you can run the test-suite in place, generating output files in the source tree by running make -C test-suite from the top directory of the source tree (equivalent to running make test-suite from the test-suite directory). This permits incremental usage since output files will be preserved.

  • You can also run the test suite in a hygienic way using make test-suite or dune runtest. This is convenient for full runs from scratch, for instance in CI.

    Since dune still invokes the test-suite makefile, the environment variable NJOBS is used to set the -j option that is passed to make (for example, with the command NJOBS=8 dune runtest). This use of NJOBS will be removed when the test suite is fully ported to Dune.

There is preliminary support to build the API documentation and reference manual in HTML format, use dune build {@doc,@refman-html} to generate them.

So far these targets will build the documentation artifacts, however no install rules are generated yet.

Developer shell

You can create a developer shell with dune utop $library, where $library can be any directory in the current workspace. For example, dune utop engine or dune utop plugins/ltac will launch utop with the right libraries already loaded.

ocamldebug

You can use ocamldebug with Dune; after a build, do:

dune exec -- dev/dune-dbg coqc foo.v
(ocd) source db

to start coqc.byte foo.v, other targets are {checker,rocqide,coqtop}:

dune exec -- dev/dune-dbg checker foo.vo
(ocd) source db

More info in the wiki.

Unfortunately, dependency handling is not fully refined / automated, you may find the occasional hiccup due to libraries being renamed, etc... Please report any issue.

For running in emacs, use coqdev-ocamldebug from coqdev.el.

Debugging hints

  • To debug a failure/error/anomaly, add a breakpoint in Vernacinterp.interp_gen (in vernac/vernacinterp.ml) at the with clause of the "try ... with ..." block, then go "back" a few steps to find where the failure/error/anomaly has been raised

  • Alternatively, for an error or an anomaly, add breakpoints where it was raised (eg in user_err or anomaly in lib/cErrors.ml, or the functions in pretyping/pretype_errors.ml, or other raises depending on the error)

  • If there is a linking error (eg from "source db"), do a "dune build rocq-runtime.install" and try again.

Dropping from coqtop:

The following should work:

dune exec -- rocq repl-with-drop
> Drop.

Compositionality, developer and release modes.

By default [in "developer mode"], Dune will compose all the packages present in the tree and perform a global build. That means that for example you could drop the ltac2 folder under plugins and get a build using ltac2, that will use the current Rocq version.

This is very useful to develop plugins and Rocq libraries as your plugin will correctly track dependencies and rebuild incrementally as needed.

However, it is not always desirable to go this way. For example, the current Rocq source tree contains two packages [Rocq and RocqIDE], and in the OPAM RocqIDE package we don't want to build RocqIDE against the local copy of Rocq. For this purpose, Dune supports the -p option, so dune build -p rocqide will build RocqIDE against the system-installed version of Rocq libs, and use a "release" profile that for example enables stronger compiler optimizations.

OPAM file generation

.opam files will be automatically generated by Dune from the package descriptions in the dune-project file; see Dune's manual for more details. For now we have disabled this due to some bugs.

Stanzas

dune files contain the so-called "stanzas", that may declare:

  • libraries,
  • executables,
  • documentation, arbitrary blobs.

The concrete options for each stanza can be seen in the Dune manual, but usually the default setup will work well with the current Rocq sources. Note that declaring a library or an executable won't make it installed by default, for that, you need to provide a "public name".

Workspaces and Profiles

Dune provides support for tree workspaces so the developer can set global options --- such as flags --- on all packages, or build Rocq with different OPAM switches simultaneously [for example to test compatibility]; for more information, please refer to the Dune manual.

Inlining reports

The ireport profile will produce standard OCaml inlining reports. These are to be found under _build/default/$lib/$lib.objs/$module.$round.inlining.org and are in Emacs org-mode format.

Note that due to ocaml/dune#1401 , we must perform a full rebuild each time as otherwise Dune will remove the files. We hope to solve this in the future.

Planned and Advanced features

Dune supports or will support extra functionality that may result very useful to Rocq, some examples are:

  • Cross-compilation.
  • Automatic Generation of OPAM files.
  • Multi-directory libraries.

FAQ

  • I get "Error: Dynlink error: Interface mismatch":

    You are likely running a partial build which doesn't include implicitly loaded plugins / vo files. See the "Running binaries [coqtop / rocqide]" section above as to how to correctly call Rocq's binaries.

Dune cheat sheet

  • dune build build all targets in the current workspace
  • dune build @check build all ML targets as fast as possible, setup merlin
  • dune utop $dir open a shell for libraries in $dir
  • dune exec -- $file build and execute binary $file, can be in path or be an specific name
  • dune build _build/$context/$foo build target $foo$ in $context, with build dir layout
  • dune build _build/install/$context/foo build target $foo$ in $context, with install dir layout

packaging:

  • dune subst generate metadata for a package to be installed / distributed, necessary for opam
  • dune build -p $pkg build a package in release mode