diff options
Diffstat (limited to 'dev/doc')
| -rw-r--r-- | dev/doc/build-system.dune.md | 38 | ||||
| -rw-r--r-- | dev/doc/critical-bugs | 22 | ||||
| -rw-r--r-- | dev/doc/release-process.md | 16 |
3 files changed, 64 insertions, 12 deletions
diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index de3d5a3d15..8ebd6b5073 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -10,17 +10,23 @@ Coq can now be built using [Dune](https://github.com/ocaml/dune). ## Quick Start -Usually, using the latest version of Dune is recommended, see -`dune-project` for the minimum required version; type `dune build` to -build the base Coq libraries. No call to `./configure` is needed. +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.dune`, `make -f Makefile.dune` will display help. Note +that dune will call configure for you if needed, so no need to call +`./configure` in the regular development workflow. + +`dune build @install` will build all the public Coq artifacts; `dune +build` will build all the targets in the workspace, including tests +and documentations. 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. -More helper targets are available 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. @@ -84,7 +90,11 @@ builds, please see below. ## Documentation and testing targets -Coq's test-suite can be run with `dune runtest`. +Coq's test-suite can be run with `dune runtest`; given that `dune` +still invokes the test-suite makefile, the environment variable +`NJOBS` will control the value of the `-j` option that is passed to +make; common call `NJOBS=8 dune runtest`. This will be resolved in the +future once the test suite is ported to Dune rules. There is preliminary support to build the API documentation and reference manual in HTML format, use `dune build {@doc,@refman-html}` @@ -229,3 +239,17 @@ useful to Coq, some examples are: implicitly loaded plugins / vo files. See the "Running binaries [coqtop / coqide]" section above as to how to correctly call Coq'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 diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs index 79c2155823..5c8b8944a7 100644 --- a/dev/doc/critical-bugs +++ b/dev/doc/critical-bugs @@ -332,6 +332,28 @@ Conversion machines GH issue number: ocaml/ocaml#6385, #11170 risk: unlikely to be activated by chance, might happen for autogenerated code + component: "virtual machine" (compilation to bytecode ran by a C-interpreter) + summary: buffer overflow, arbitrary code execution on floating-point operations + introduced: 8.13 + impacted released versions: 8.13.0 + impacted coqchk versions: none (no virtual machine in coqchk) + fixed in: 8.13.1 + found by: Melquiond + GH issue number: #13867 + risk: none, unless using floating-point operations; high otherwise; + noticeable if activated by chance, since it usually breaks + control-flow integrity + + component: "virtual machine" (compilation to bytecode ran by a C-interpreter) + summary: arbitrary code execution on irreducible PArray.set + introduced: 8.13 + impacted released versions: 8.13.0, 8.13.1 + impacted coqchk versions: none (no virtual machine in coqchk) + fixed in: 8.13.2 + found by: Melquiond + GH issue number: #13998 + risk: none, unless using primitive array operations; systematic otherwise + Side-effects component: side-effects diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md index e450cd2b8b..1697a19668 100644 --- a/dev/doc/release-process.md +++ b/dev/doc/release-process.md @@ -114,6 +114,11 @@ list of contributors between Coq revisions. Typically used with `VX.X+alpha..vX.X` to check the contributors of version `VX.X`. + Note that this script relies on `.mailmap` to merge multiple + identities. If you notice anything incorrect while using it, use + the opportunity to fix the `.mailmap` file. Same thing if you want + to have the full name of a contributor shown instead of a pseudonym. + ## For each release (preview, final, patch-level) ## - [ ] Ensure that there exists a milestone for the following version. @@ -153,11 +158,10 @@ - [ ] Publish a release on GitHub with the PDF version of the reference manual attached. -## Once the final release is published ## - -Ping `@Zimmi48` to: +## For each non-preview release ## -- [ ] Switch the default version of the reference manual on the website. +- [ ] Ping `@Zimmi48` to switch the default version of the reference + manual on the website. This is done by logging into the server (`vps697916.ovh.net`), editing two `ProxyPass` lines (one for the refman and one for the @@ -168,7 +172,9 @@ Ping `@Zimmi48` to: repository. See [coq/www#111](https://github.com/coq/www/issues/111) and [coq/www#131](https://github.com/coq/www/issues/131). -- [ ] Publish a new version on Zenodo (only once per major version). +## Only for the final release of each major version ## + +- [ ] Ping `@Zimmi48` to publish a new version on Zenodo. *TODO:* automate this with coqbot. |