diff options
Diffstat (limited to 'dev/doc')
| -rw-r--r-- | dev/doc/build-system.dev.txt | 40 | ||||
| -rw-r--r-- | dev/doc/build-system.dune.md | 120 | ||||
| -rw-r--r-- | dev/doc/changes.md | 11 | ||||
| -rw-r--r-- | dev/doc/critical-bugs | 10 | ||||
| -rw-r--r-- | dev/doc/profiling.txt | 52 |
5 files changed, 225 insertions, 8 deletions
diff --git a/dev/doc/build-system.dev.txt b/dev/doc/build-system.dev.txt index abba13428f..b0a2b04121 100644 --- a/dev/doc/build-system.dev.txt +++ b/dev/doc/build-system.dev.txt @@ -1,5 +1,3 @@ - - HISTORY: ------- @@ -35,13 +33,41 @@ HISTORY: grammar.cma (and q_constr.cmo) directly, no need for a separate subcall to make nor awkward include-failed-and-retry. - ---------------------------------------------------------------------------- +* February - September 2018 (Emilio Jesús Gallego Arias) + + Dune support added. + + The build setup is mostly vanilla for the OCaml part, however the + `.v` to `.vo` compilation relies on `coq_dune` a `coqdep` wrapper + that will generate the necessary `dune` files. + + As a developer, you should not have to deal with Dune configuration + files on a regular basis unless adding a new library or plugin. + The vanilla setup declares all the Coq libraries and binaries [we + must respect proper containment/module implementation rules as to + allow packing], and we build custom preprocessors (based on `camlp5` + and `coqpp`) that will process the `ml4`/`mlg` files. + + This suffices to build `coqtop` and `coqide`, all that remains to + handle is `.vo` compilation. + + To teach Dune about the `.vo`, we use a small utility `coq_dune`, + that will generate a `dune` file for each directory in `plugins` and + `theories`. The code is pretty straightforward and declares build + and install rules for each `.v` straight out of `coqdep`. Thus, our + build strategy looks like this: + + 1. Use `dune` to build `coqdep` and `coq_dune`. + 2. Use `coq_dune` to generate `dune` files for each directory with `.v` files. + 3. ? + 4. Profit! [Seriously, at this point Dune has all the information to build Coq] + +--------------------------------------------------------------------------- -This file documents internals of the implementation of the build -system. For what a Coq developer needs to know about the build system, -see build-system.txt . +This file documents internals of the implementation of the make-based +build system. For what a Coq developer needs to know about the build +system, see build-system.txt and build-system.dune.md . .ml4 files ---------- diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md new file mode 100644 index 0000000000..36d5e5841b --- /dev/null +++ b/dev/doc/build-system.dune.md @@ -0,0 +1,120 @@ +This file documents what a Coq developer needs to know about the +Dune-based build system. If you want to enhance the build system +itself (or are curious about its implementation details), see +build-system.dev.txt, and in particular its initial HISTORY section. + +Quick Start +=========== + +You need Dune >= 1.2.1 ; just type `dune build` to build the base Coq +libraries. No `./configure` step is needed. + +Dune will get confused if it finds leftovers of in-tree compilation, +so please be sure your tree is clean from objects files generated by +the make-based system. + +If you want to build the standard libraries and plugins you should +call `make -f Makefile.dune voboot`. It is usually enough to do that +once per-session. + +More helper targets are availabe in `Makefile.dune`, `make -f +Makefile.dune` will display help. + +Dune +==== + +Coq can now be built using +[Dune](https://github.com/ocaml/dune). Contrary to other systems, +Dune, doesn't use a global`makefile` but local build files named +`dune` that are later composed to form a global build. + +As a developer, Dune should take care of all OCaml-related build tasks +including library management, merlin files, and link order. You are +are not supposed to modify the `dune` files unless you are adding a +new binary, library, or plugin. + +The current Dune setup also doesn't require a call to `configure`. The +auto-generated configuration files are properly included in the +dependency graph so it will be automatically generated by Dune with +reasonable developer defaults. You can still override the defaults by +manually calling `./configure`, but note that some configure options +such as install paths are not used by Dune. + +Dune uses a separate directory `_build` to store build artifacts; it +will generate an `.install` file so artifacts in the build can be +properly installed by package managers. + +## Targets + +The default dune target is `dune build` (or `dune build @install`), +which will scan all sources in the Coq 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`. + +In order to build a single package, you can do `dune build +$PACKAGE.install`. Dune also provides targets for documentation and +testing, see below. + +## 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. + +Note that you must invoke the `#rectypes;;` toplevel flag in order to +use Coq libraries. The provided `.ocamlinit` file does this +automatically. + +## 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 Coq version. + +This is very useful to develop plugins and Coq 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 Coq source tree contains two packages [Coq and CoqIDE], and in +the OPAM CoqIDE package we don't want to build CoqIDE against the +local copy of Coq. For this purpose, Dune supports the `-p` option, so +`dune build -p coqide` will build CoqIDE against the system-installed +version of Coq libs. + +## 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 Coq +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 Coq +with different OPAM switches simultaneously [for example to test +compatibility]; for more information, please refer to the Dune manual. + +## Documentation and test targets + +The documentation and test suite targets for Coq are still not +implemented in Dune. + +## Planned and Advanced features + +Dune supports or will support extra functionality that may result very +useful to Coq, some examples are: + +- Cross-compilation. +- Automatic Generation of OPAM files. +- Multi-directory libraries. diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 1eea2443fe..fdeb0abed4 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -1,3 +1,12 @@ +## Changes between Coq 8.9 and Coq 8.10 + +### ML API + +Termops: + +- Internal printing functions have been placed under the + `Termops.Internal` namespace. + ## Changes between Coq 8.8 and Coq 8.9 ### ML API @@ -219,7 +228,7 @@ General deprecation Proof engine - Due to the introduction of `EConstr` in 8.7, it is not necessary to +- Due to the introduction of `EConstr` in 8.7, it is not necessary to track "goal evar normal form status" anymore, thus the type `'a Proofview.Goal.t` loses its ghost argument. This may introduce some minor incompatibilities at the typing level. Code-wise, things diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs index 6166d24b70..8d78559c0d 100644 --- a/dev/doc/critical-bugs +++ b/dev/doc/critical-bugs @@ -109,6 +109,16 @@ Universes GH issue number: none risk: unlikely to be activated by chance + component: universe polymorphism + summary: universe polymorphism can capture global universes + impacted released versions: V8.5 to V8.8 + impacted coqchk versions: V8.5 to current (NOT FIXED) + fixed in: 2385b5c1ef + found by: Gaëtan Gilbert + exploit: test-suite/misc/poly-capture-global-univs + GH issue number: #8341 + risk: unlikely to be activated by chance (requires a plugin) + Primitive projections component: primitive projections, guard condition diff --git a/dev/doc/profiling.txt b/dev/doc/profiling.txt index b5dd8445db..45766293c7 100644 --- a/dev/doc/profiling.txt +++ b/dev/doc/profiling.txt @@ -21,6 +21,58 @@ and plug into the process perf record -g -p PID +### Per-component [flame graphs](https://github.com/brendangregg/FlameGraph) + +I (Andres Erbsen) have found it useful to look at library-wide flame graphs of +coq time consumption. As the Ltac interpreter stack is reflected in the OCaml +stack, calls to the same primitive can appear on top of multiple essentially +equivalent stacks. To make the profiles more readable, one could either try to +edit the stack trace to merge "equivalent" frames, or simply look at the +aggregate profile on a component-by-component basis. Here is how to do the +second for the standard library ([example output](https://cdn.rawgit.com/andres-erbsen/b29b29cb6480dfc6a662062e4fcd0ae3/raw/304fc3fea9630c8e453929aa7920ca8a2a570d0b/stdlib_categorized_outermost.svg)). + +~~~~~ +#!/bin/bash +make -f Makefile.dune clean +make -f Makefile.dune states +perf record -F99 `# ~1GB of data` --call-graph=dwarf -- make -f Makefile.dune world +perf script --time '0%-100%' | + stackcollapse-perf.pl | + grep Coqtop__compile | + sed -rf <(cat <<'EOF' + s/;caml/;/g + s/_[0-9]*;/;/g + s/Logic_monad__fun;//g + s/_apply[0-9];//g + s/;System/@&@/ + s/;Hashcons/@&@/ + s/;Grammar/@&@/ + s/;Declaremods/@&@/ + s/;Tactics/@&@/ + s/;Pretyping/@&@/ + s/;Typeops/@&@/ + s/;Reduction/@&@/ + s/;Unification/@&@/ + s/;Evarutil/@&@/ + s/;Evd/@&@/ + s/;EConstr/@&@/ + s/;Constr/@&@/ + s/;Univ/@&@/ + s/;Ugraph/@&@/ + s/;UState/@&@/ + s/;Micromega/@&@/ + s/;Omega/@&@/ + s/;Auto/@&@/ + s/;Ltac_plugin__Tacinterp/@&@/ + s/;Ltac_plugin__Rewrite/@&@/ + s/[^@]*@;([^@]*)@/\1;\1/ + s/@//g + :a; s/;([^;]+);\1;/;\1;/g;ta +EOF + ) | + flamegraph.pl +~~~~~ + ## Memory You first need a few commits atop trunk for this to work. |