diff options
Diffstat (limited to 'dev/doc')
| -rw-r--r-- | dev/doc/INSTALL.make.md | 8 | ||||
| -rw-r--r-- | dev/doc/MERGING.md | 177 | ||||
| -rw-r--r-- | dev/doc/build-system.dune.md | 62 | ||||
| -rw-r--r-- | dev/doc/changes.md | 38 | ||||
| -rw-r--r-- | dev/doc/critical-bugs | 27 | ||||
| -rw-r--r-- | dev/doc/release-process.md | 16 | ||||
| -rw-r--r-- | dev/doc/shield-icon.png | bin | 0 -> 2512 bytes | |||
| -rw-r--r-- | dev/doc/xml-protocol.md | 5 |
8 files changed, 131 insertions, 202 deletions
diff --git a/dev/doc/INSTALL.make.md b/dev/doc/INSTALL.make.md index 3db5d0b14f..f81630c55d 100644 --- a/dev/doc/INSTALL.make.md +++ b/dev/doc/INSTALL.make.md @@ -102,6 +102,14 @@ Detailed Installation Procedure. it is recommended to compile in parallel, via make -jN where N is your number of cores. + If you wish to create timing logs for the standard library, you can + pass `TIMING=1` (for per-line timing files) or `TIMED=1` (for + per-file timing on stdout). Further variables and targets are + available for more detailed timing analysis; see the section of the + reference manual on `coq_makefile`. If there is any timing target + or variable supported by `coq_makefile`-made Makefiles which is not + supported by Coq's own Makefile, please report that as a bug. + 5. You can now install the Coq system. Executables, libraries, and manual pages are copied in some standard places of your system, defined at configuration time (step 3). Just do diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md deleted file mode 100644 index 66f5a96802..0000000000 --- a/dev/doc/MERGING.md +++ /dev/null @@ -1,177 +0,0 @@ -# Merging changes in Coq - -This document describes how patches, submitted as pull requests (PRs) on the -`master` branch, should be merged into the main repository -(https://github.com/coq/coq). - -## Code owners - -The [CODEOWNERS](../../.github/CODEOWNERS) file defines owners for each part of -the code. Sometime there is one principal maintainer and one or several -secondary maintainer(s). Sometimes, it is a team of code owners and all of its -members act as principal maintainers for the component. - -When a PR is submitted, GitHub will automatically ask the principal -maintainer (or the code owner team) for a review. If the PR touches several -parts, all the corresponding owners will be asked for a review. - -Maintainers are never assigned as reviewer on their own PRs. - -If a principal maintainer submits a PR or is a co-author of a PR that is -submitted and this PR changes the component they own, they must request a -review from a secondary maintainer. They can also delegate the review if they -know they are not available to do it. - -## Reviewing - -When maintainers receive a review request, they are expected to: - -* Put their name in the assignee field, if they are in charge of the component - that is the main target of the patch (or if they are the only maintainer asked - to review the PR). -* Review the PR, approve it or request changes. -* If they are the assignee, check if all reviewers approved the PR. If not, - regularly ping the author (if changes should be implemented) or the reviewers - (if reviews are missing). The assignee ensures that any requests for more - discussion have been granted. When the discussion has converged and ALL - REVIEWERS(*) have approved the PR, the assignee is expected to follow the merging - process described below. - -To know what files you are a code owner of in a large PR, you can run -`dev/tools/check-owners-pr.sh xxxx`. Results are unfortunately imperfect. - -When a PR received lots of comments or if the PR has not been opened for long -and the assignee thinks that some other developers might want to comment, -it is recommended that they announce their intention to merge and wait a full -working day (or more if deemed useful) before the actual merge, as a sort of -last call for comments. - -In all cases, maintainers can delegate reviews to the other maintainers, -except if it would lead to a maintainer reviewing their own patch. - -A maintainer is expected to be reasonably reactive, but no specific timeframe is -given for reviewing. - -When none of the maintainers have commented nor self-assigned a PR in a delay -of five working days, any maintainer of another component who feels comfortable -reviewing the PR can assign it to themselves. To prevent misunderstandings, -maintainers should not hesitate to announce in advance when they shall be -unavailable for more than five working days. - -(*) In case a component is touched in a trivial way (adding/removing one file in -a `Makefile`, etc), or by applying a systematic refactoring process (global -renaming for instance) that has been reviewed globally, the assignee can -say in a comment they think a review is not required from every code owner and -proceed with the merge. - -### Breaking changes - -If the PR breaks compatibility of some external projects in CI, then fixes to -those external projects should have been prepared (cf. the relevant sub-section -in the [CI README](../ci/README.md#Breaking-changes) and the PR can be tested -with these fixes thanks to ["overlays"](../ci/user-overlays/README.md). - -Moreover the PR author *must* add an entry to the [unreleased -changelog](../../doc/changelog/README.md) or to the -[`dev/doc/changes.md`](changes.md) file. - -If overlays are missing, ask the author to prepare them and label the PR with -the [needs: overlay](https://github.com/coq/coq/labels/needs%3A%20overlay) label. - -When fixes are ready, there are two cases to consider: - -- For patches that are backward compatible (best scenario), you should get the - external project maintainers to integrate them before merging the PR. -- For patches that are not backward compatible (which is often the case when - patching plugins after an update to the Coq API), you can proceed to merge - the PR and then notify the external project maintainers they can merge the - patch. - -## Merging - -Once all reviewers approved the PR, the assignee is expected to check that CI -completed without relevant failures, and that the PR comes with appropriate -documentation and test cases. If not, they should leave a comment on the PR and -put the appropriate label. Otherwise, they are expected to merge the PR using the -[merge script](../tools/merge-pr.sh). - -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 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 -using a GitHub account); if you are part of the -[Coq organization on GitLab](https://gitlab.com/coq), you should see a "Retry" -button; otherwise, send a request to join the organization. - -When the PR has conflicts, the assignee can either: -- ask the author to rebase the branch, fixing the conflicts -- warn the author that they are going to rebase the branch, and push to the - branch directly - -In both cases, CI should be run again. - -In some rare cases (e.g. the conflicts are in the `CHANGES.md` file and the PR -is not a candidate for backporting), it is ok to fix -the conflicts in the merge commit (following the same steps as below), and push -to `master` directly. DON'T USE the GitHub interface to fix these conflicts. - -To merge the PR proceed in the following way -``` -$ git checkout master -$ git pull -$ dev/tools/merge-pr.sh XXXX -$ git push upstream -``` -where `XXXX` is the number of the PR to be merged and `upstream` is the name -of your remote pointing to `git@github.com:coq/coq.git`. -Note that you are only supposed to merge PRs into `master`. PRs should rarely -target the stable branch, but when it is the case they are the responsibility -of the release manager. - -This script conducts various checks before proceeding to merge. Don't bypass them -without a good reason to, and in that case, write a comment in the PR thread to -explain the reason. - -Maintainers MUST NOT merge their own patches. - -DON'T USE the GitHub interface for merging, since it will prevent the automated -backport script from operating properly, generates bad commit messages, and a -messy history when there are conflicts. - -### Merge script dependencies - -The merge script passes option `-S` to `git merge` to ensure merge commits -are signed. Consequently, it depends on the GnuPG command utility being -installed and a GPG key being available. Here is a short documentation on -how to use GPG, git & GitHub: https://help.github.com/articles/signing-commits-with-gpg/. - -The script depends on a few other utilities. If you are a Nix user, the -simplest way of getting them is to run `nix-shell` first. - -**Note for homebrew (MacOS) users:** it has been reported that installing GnuPG -is not out of the box. Installing explicitly "pinentry-mac" seems important for -typing of passphrase to work correctly (see also this -[Stack Overflow Q-and-A](https://stackoverflow.com/questions/39494631/gpg-failed-to-sign-the-data-fatal-failed-to-write-commit-object-git-2-10-0)). - -## Addendum for organization admins - -### Adding a new code owner individual - -If someone is added to the [`CODEOWNERS`](../../.github/CODEOWNERS) file and -they did not have merging rights before, they should also be added to the -**@coq/pushers** team. You may do so using -[this link](https://github.com/orgs/coq/teams/pushers/members?add=true). - -Before adding someone to the **@coq/pushers** team, you should ensure that they -have read the present merging documentation, and explicitly tell them not to -use the merging button on the GitHub web interface. - -### Adding a new code owner team - -Go to [that page](https://github.com/orgs/coq/teams/pushers/teams) and click on -the green "Add a team" button. Use a "-maintainer" suffix for the name of your -team. You may then add new members to this team (you don't need to add them to -the **@coq/pushers** team first as this will be done automatically because the -team you created is a sub-team of **@coq/pushers**). diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index 37c6e2f619..0506216541 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -46,21 +46,27 @@ of build threads `(jobs N)` and display options `(display _mode_)`. ## Running binaries [coqtop / coqide] -There are two special targets `states` and `quickide` that will -generate "shims" for running `coqtop` and `coqide` in a fast build. In -order to use them, do: +Running `coqtop` directly with `dune exec -- coqtop` won't in general +work well unless you are using `dune exec -- coqtop -noinit`. The +`coqtop` binary doesn't depend itself on Coq's prelude, so plugins / +vo files may go stale if you rebuild only `coqtop`. + +Instead, you should use the provided "shims" for running `coqtop` and +`coqide` in a fast build. In order to use them, do: ``` $ make -f Makefile.dune voboot # Only once per session $ dune exec -- dev/shim/coqtop-prelude ``` -or `quickide` / `dev/shim/coqide-prelude` for CoqIDE. These targets -enjoy quick incremental compilation thanks to `-opaque` so they tend -to be very fast while developing. +or `quickide` / `dev/shim/coqide-prelude` for CoqIDE, etc.... See +`dev/shim/dune` for a complete list of targets. These targets enjoy +quick incremental compilation thanks to `-opaque` so they tend to be +very fast while developing. Note that for a fast developer build of ML files, the `check` target -will be faster. +is faster, as it doesn't link the binaries and uses the non-optimizing +compiler. ## Targets @@ -108,24 +114,43 @@ automatically. You can use `ocamldebug` with Dune; after a build, do: ``` -dune exec -- dev/dune-dbg /path/to/foo.v +dune exec -- dev/dune-dbg coqc foo.v (ocd) source dune_db ``` -or +to start `coqc.byte foo.v`, other targets are `{checker,coqide,coqtop}`: ``` -dune exec -- dev/dune-dbg checker Foo +dune exec -- dev/dune-dbg checker foo.vo (ocd) source dune_db ``` -for the checker. Unfortunately, dependency handling here is not fully -refined, so you need to build enough of Coq once to use this target -[it will then correctly compute the deps and rebuild if you call the -script again] This will be fixed in the future. +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`. +**Note**: If you are using OCaml >= 4.08 you need to use + +``` +(ocd) source dune_db_408 +``` + +or + +``` +(ocd) source dune_db_409 +``` + +depending on your OCaml version. This is due to several factors: + +- OCaml >= 4.08 doesn't allow doubly-linking modules, however `source` + is not re entrant and seems to doubly-load in the default setup, see + https://github.com/coq/coq/issues/8952 +- OCaml >= 4.09 comes with `dynlink` already linked in so we need to + modify the list of modules loaded. + ## Dropping from coqtop: After doing `make -f Makefile.dune voboot`, the following commands should work: @@ -194,3 +219,12 @@ useful to Coq, 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 / coqide]" section above as to how to correctly call Coq's + binaries. diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 04b20c6889..eac8d86b0a 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -1,7 +1,40 @@ ## Changes between Coq 8.11 and Coq 8.12 +### Code formatting + +- The automatic code formatting tool `ocamlformat` is enabled now for + the micromega codebase. Version 0.13.0 is required. See + `ocalmformat`'s documentation for more details on integration with + your editor. + ### ML API +Notations: + +- Most operators on numerals have moved to file numTok.ml. + +- Types `precedence`, `parenRelation`, `tolerability` in + `notgram_ops.ml` have been reworked. See `entry_level` and + `entry_relative_level` in `constrexpr.ml`. + +Exception handling: + +- Coq's custom `Backtrace` module has been removed in favor of OCaml's + native backtrace implementation. Please use the functions in + `Exninfo.capture` and `iraise` when re-raising inside an exception + handler. + +- Registration of exception printers now follows more closely OCaml's + API, thus: + + + printers are of type `exn -> Pp.t option` [`None` == not handled] + + it is forbidden for exception printers to raise. + +- Refiner.catchable_exception is deprecated, use instead + CErrors.noncritical in try-with block. Note that nothing is needed in + tclORELSE block since the exceptions there are supposed to be + non-critical by construction. + Printers: - Functions such as Printer.pr_lconstr_goal_style_env have been @@ -10,6 +43,11 @@ Printers: Constrextern.extern_constr which were taking a boolean argument for the goal style now take instead a label. +Implicit arguments: + +- The type `Impargs.implicit_kind` was removed in favor of + `Glob_term.binding_kind`. + ## Changes between Coq 8.10 and Coq 8.11 ### ML API diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs index 67becb251a..3260040248 100644 --- a/dev/doc/critical-bugs +++ b/dev/doc/critical-bugs @@ -158,7 +158,7 @@ Universes component: universe polymorphism, asynchronous proofs summary: universe constraints erroneously discarded when forcing an asynchronous proof containing delayed monomorphic constraints inside a universe polymorphic section introduced: between 8.4 and 8.5 by merging the asynchronous proofs feature branch and universe polymorphism one - impacted released: V8.5-V8.10 + impacted released versions: V8.5-V8.10 impacted development branches: none impacted coqchk versions: immune fixed in: PR#10664 @@ -167,6 +167,19 @@ Universes GH issue number: none risk: unlikely to be triggered in interactive mode, not present in batch mode (i.e. coqc) + component: algebraic universes + summary: Set+2 was incorrectly simplified to Set+1 + introduced: V8.10 (with the SProp commit 75508769762372043387c67a9abe94e8f940e80a) + impacted released versions: V8.10.0 V8.10.1 V8.10.2 + impacted coqchk versions: same + fixed in: PR#11422 + found by: Gilbert + exploit: see PR (custom application of Hurkens to get around the refreshing at elaboration) + GH issue number: see PR + risk: unlikely to be triggered through the vernacular (the system "refreshes" algebraic + universes such that +2 increments do not appear), mild risk from plugins which manipulate + algebraic universes. + Primitive projections component: primitive projections, guard condition @@ -255,6 +268,18 @@ Conversion machines GH issue number: #9925 risk: + component: "virtual machine" (compilation to bytecode ran by a C-interpreter) + summary: broken long multiplication primitive integer emulation layer on 32 bits + introduced: e43b176 + impacted released versions: 8.10.0, 8.10.1, 8.10.2 + impacted development branches: 8.11 + impacted coqchk versions: none (no virtual machine in coqchk) + fixed in: 4e176a7 + found by: Soegtrop, Melquiond + exploit: test-suite/bugs/closed/bug_11321.v + GH issue number: #11321 + risk: critical, as any BigN computation on 32-bit architectures is wrong + component: "native" conversion machine (translation to OCaml which compiles to native code) summary: translation of identifier from Coq to OCaml was not bijective, leading to identify True and False introduced: V8.5 diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md index 1c486b024d..58c2fcc68a 100644 --- a/dev/doc/release-process.md +++ b/dev/doc/release-process.md @@ -75,7 +75,8 @@ in time. - [ ] Pin the versions of libraries and plugins in `dev/ci/ci-basic-overlays.sh` to use commit hashes or tag (or, if it exists, a branch dedicated to compatibility with the corresponding - Coq branch). + Coq branch). You can use the `dev/tools/pin-ci.sh` script to do this + semi-automatically. - [ ] Remove all remaining unmerged feature PRs from the beta milestone. - [ ] Start a new project to track PR backporting. The project should have a "Request X.X+beta1 inclusion" column for the PRs that were @@ -126,11 +127,11 @@ in time. - [ ] Send an e-mail on Coqdev announcing that the tag has been put so that package managers can start preparing package updates (including a `coq-bignums` compatible version). -- [ ] Ping **@erikmd** to update the Docker images in `coqorg/coq` - (requires `coq-bignums` in `extra-dev` for a beta / in `released` - for a final release). +- [ ] When opening the corresponding PR for `coq` in the opam repository ([`coq/opam-coq-archive`](https://github.com/coq/opam-coq-archive) or [`ocaml/opam-repository`](https://github.com/ocaml/opam-repository)), + the package managers can Cc `@erikmd` to request that he prepare the necessary configuration for the Docker release in [`coqorg/coq`](https://hub.docker.com/r/coqorg/coq) + (namely, he'll need to make sure a `coq-bignums` opam package is available in [`extra-dev`](https://github.com/coq/opam-coq-archive/tree/master/extra-dev), respectively [`released`](https://github.com/coq/opam-coq-archive/tree/master/released), so the Docker image gathering `coq` and `coq-bignums` can be built). - [ ] Draft a release on GitHub. -- [ ] Get **@maximedenes** to sign the Windows and MacOS packages and +- [ ] Get `@maximedenes` to sign the Windows and MacOS packages and upload them on GitHub. - [ ] Prepare a page of news on the website with the link to the GitHub release (see [coq/www#63](https://github.com/coq/www/pull/63)). @@ -138,8 +139,6 @@ in time. *TODO: setup some continuous deployment for this.* - [ ] Merge the website update, publish the release and send announcement e-mails. -- [ ] Ping **@Zimmi48** to publish a new version on Zenodo. - *TODO: automate this.* - [ ] Close the milestone ## At the final release time ## @@ -159,7 +158,10 @@ in time. Repeat the generic process documented above for all releases. +Ping `@Zimmi48` to: + - [ ] Switch the default version of the reference manual on the website. +- [ ] Publish a new version on Zenodo. ## At the patch-level release time ## diff --git a/dev/doc/shield-icon.png b/dev/doc/shield-icon.png Binary files differnew file mode 100644 index 0000000000..629e51a819 --- /dev/null +++ b/dev/doc/shield-icon.png diff --git a/dev/doc/xml-protocol.md b/dev/doc/xml-protocol.md index 0fc0a413ba..fca7b77fc2 100644 --- a/dev/doc/xml-protocol.md +++ b/dev/doc/xml-protocol.md @@ -1,12 +1,11 @@ # Coq XML Protocol This document is based on documentation originally written by CJ Bell -for his [vscoq](https://github.com/siegebell/vscoq/) project. +for his [vscoq](https://github.com/coq-community/vscoq/) project. Here, the aim is to provide a "hands on" description of the XML protocol that coqtop and IDEs use to communicate. The protocol first appeared -with Coq 8.5, and is used by CoqIDE. It will also be used in upcoming -versions of Proof General. +with Coq 8.5, and is used by CoqIDE, [vscoq](https://github.com/coq-community/vscoq/), and other user interfaces. A somewhat out-of-date description of the async state machine is [documented here](https://github.com/ejgallego/jscoq/blob/v8.10/etc/notes/coq-notes.md). |
