diff options
Diffstat (limited to 'dev/doc')
| -rw-r--r-- | dev/doc/MERGING.md | 2 | ||||
| -rw-r--r-- | dev/doc/profiling.txt | 6 | ||||
| -rw-r--r-- | dev/doc/release-process.md | 58 | ||||
| -rw-r--r-- | dev/doc/versions-history.tex | 2 |
4 files changed, 32 insertions, 36 deletions
diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md index 56fdab0c26..5705857d76 100644 --- a/dev/doc/MERGING.md +++ b/dev/doc/MERGING.md @@ -93,7 +93,7 @@ put the approriate label. Otherwise, they are expected to merge the PR using the When CI has a few failures which look spurious, restarting the corresponding jobs is a good way of ensuring this was indeed the case. -To restart a job on Travis or on AppVeyor, you should connect using your GitHub +To restart a job on AppVeyor, you should connect using your GitHub account; being part of the Coq organization on GitHub should give you the permission to do so. To restart a job on GitLab CI, you should sign into GitLab (this can be done diff --git a/dev/doc/profiling.txt b/dev/doc/profiling.txt index 29e87df6b8..8455d13377 100644 --- a/dev/doc/profiling.txt +++ b/dev/doc/profiling.txt @@ -10,7 +10,7 @@ In Coq source folder: opam switch 4.05.0+trunk+fp ./configure -local -debug make -perf record -g bin/coqtop -compile file.v +perf record -g bin/coqc file.v perf report -g fractal,callee --no-children To profile only part of a file, first load it using @@ -96,7 +96,7 @@ https://github.com/mshinwell/opam-repo-dev ### For memory dump: -CAMLRUNPARAM=T,mj bin/coqtop -compile file.v +CAMLRUNPARAM=T,mj bin/coqc file.v In another terminal: @@ -112,7 +112,7 @@ number of objects and third is the place where the objects where allocated. ### For complete memory graph: -CAMLRUNPARAM=T,gr bin/coqtop -compile file.v +CAMLRUNPARAM=T,gr bin/coqc file.v In another terminal: diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md index b1c111685b..d05b6c8eef 100644 --- a/dev/doc/release-process.md +++ b/dev/doc/release-process.md @@ -4,37 +4,20 @@ - [ ] Create a new issue to track the release process where you can copy-paste 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) +- [ ] Change the version name to the next major version and the magic + numbers (see [#7008](https://github.com/coq/coq/pull/7008/files)). + + Additionally, in the same commit, update the compatibility + infrastructure, which consists of invoking + [`dev/tools/update-compat.py`](../tools/update-compat.py) with the + `--master` flag. + + Note that the `update-compat.py` script must be run twice: once + *immediately after* branching with the `--master` flag (which sets + up Coq to support four `-compat` flag arguments), *in the same + commit* as the one that updates `coq_version` in + [`configure.ml`](../../configure.ml), and once again later on before + the next branch point with the `--release` flag (see next section). - [ ] 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. @@ -43,6 +26,19 @@ release date) and put this information in the milestone (using the description and due date fields). +## Anytime after the previous version is branched off master ## + +- [ ] Update the compatibility infrastructure to the next release, + which consists of invoking + [`dev/tools/update-compat.py`](../tools/update-compat.py) with the + `--release` flag; this sets up Coq to support three `-compat` flag + arguments. To ensure that CI passes, you will have to decide what + to do about all test-suite files which mention `-compat U.U` or + `Coq.Comapt.CoqUU` (which is no longer valid, since we only keep + compatibility against the two previous versions on releases), and + you may have to prepare overlays for projects using the + compatibility flags. + ## About one month before the beta ## - [ ] Create the `X.X.0` milestone and set its due date. diff --git a/dev/doc/versions-history.tex b/dev/doc/versions-history.tex index 8f9c3171da..1c4913d201 100644 --- a/dev/doc/versions-history.tex +++ b/dev/doc/versions-history.tex @@ -271,7 +271,7 @@ Coq ``V7'' archive & August 1999 & new cvs archive based on J.-C. Filliâtre's \ & & \feature{kernel-centric} architecture \\ & & more care for outside readers\\ & & (indentation, ocaml warning protection)\\ -Coq V7.0beta& released 27 December 2000 & \feature{${\cal L}_{\mathit{tac}}$} \\ +Coq V7.0beta& released 27 December 2000 & \feature{${\mathcal{L}}_{\mathit{tac}}$} \\ Coq V7.0beta2& released 2 February 2001\\ Coq V7.0& released 25 April 2001 & \feature{extraction} (version 2) [6-2-2001] \\ |