diff options
Diffstat (limited to 'dev/doc')
| -rw-r--r-- | dev/doc/build-system.dune.md | 57 | ||||
| -rw-r--r-- | dev/doc/profiling.txt | 2 | ||||
| -rw-r--r-- | dev/doc/release-process.md | 30 |
3 files changed, 68 insertions, 21 deletions
diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index 85aaf317ef..7349360be8 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -3,29 +3,45 @@ 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. -Dune -==== +About 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. +Coq can now be built using [Dune](https://github.com/ocaml/dune). + +## Quick Start + +You need Dune >= 1.2.1 ; just type `dune build` to build the base Coq +libraries. No call to `./configure` 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 some help. + +Dune places build artifacts in a separate directory `_build`; it will +also generate an `.install` file so files can be properly installed by +package managers. + +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 +including library management, merlin files, and linking 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. +## Per-User Custom Settings -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. +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_)`. ## Targets @@ -36,8 +52,10 @@ 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. +$PACKAGE.install`. + +Dune also provides targets for documentation, testing, and release +builds, please see below. ## Developer shell @@ -66,7 +84,8 @@ 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. +version of Coq libs, and use a "release" profile that for example +enables stronger compiler optimizations. ## Stanzas diff --git a/dev/doc/profiling.txt b/dev/doc/profiling.txt index 45766293c7..29e87df6b8 100644 --- a/dev/doc/profiling.txt +++ b/dev/doc/profiling.txt @@ -7,7 +7,7 @@ want to profile time or memory consumption. AFAIK, this only works for Linux. In Coq source folder: -opam switch 4.02.3+fp +opam switch 4.05.0+trunk+fp ./configure -local -debug make perf record -g bin/coqtop -compile file.v diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md index 1821a181f1..b33a1cbd73 100644 --- a/dev/doc/release-process.md +++ b/dev/doc/release-process.md @@ -6,6 +6,35 @@ the present checklist. - [ ] Change the version name to the next major version and the magic numbers (see [#7008](https://github.com/coq/coq/pull/7008/files)). +- [ ] Update the compatibility infrastructure, which consists of doing + the following steps. Note that all but the final step can be + performed automatically by + [`dev/tools/update-compat.py`](/dev/tools/update-compat.py) so + long as you have already updated `coq_version` in + [`configure.ml`](/configure.ml). + + [ ] Add a file `theories/Compat/CoqXX.v` which contains just the header + from [`dev/header.ml`](/dev/header.ml) + + [ ] Add the line `Require Export Coq.Compat.CoqXX.` at the top of + `theories/Compat/CoqYY.v`, where Y.Y is the version prior to X.X. + + [ ] Delete the file `theories/Compat/CoqWW.v`, where W.W is three versions + prior to X.X. + + [ ] Update + [`doc/stdlib/index-list.html.template`](/doc/stdlib/index-list.html.template) + with the deleted/added files. + + [ ] Remove any notations in the standard library which have `compat "W.W"`. + + [ ] Update the type `compat_version` in [`lib/flags.ml`](/lib/flags.ml) by + bumping all the version numbers by one, and update the interpretations + of those flags in [`toplevel/coqargs.ml`](/toplevel/coqargs.ml) and + [`vernac/g_vernac.mlg`](/vernac/g_vernac.mlg). + + [ ] Update the files + [`test-suite/success/CompatCurrentFlag.v`](/test-suite/success/CompatCurrentFlag.v), + [`test-suite/success/CompatPreviousFlag.v`](/test-suite/success/CompatPreviousFlag.v), + and + [`test-suite/success/CompatOldFlag.v`](/test-suite/success/CompatOldFlag.v) + by bumping all version numbers by 1. + + [ ] Decide what to do about all test-suite files which mention `-compat + W.W` or `Coq.Comapt.CoqWW` (which is no longer valid, since we only + keep compatibility against the two previous versions) - [ ] Put the corresponding alpha tag using `git tag -s`. The `VX.X+alpha` tag marks the first commit to be in `master` and not in the branch of the previous version. @@ -57,7 +86,6 @@ ## Before the beta release date ## - [ ] Ensure the Credits chapter has been updated. -- [ ] Ensure an empty `CompatXX.v` file has been created. - [ ] Ensure that an appropriate version of the plugins we will distribute with Coq has been tagged. - [ ] Have some people test the recently auto-generated Windows and MacOS |