diff options
Diffstat (limited to 'dev/doc')
| -rw-r--r-- | dev/doc/INSTALL.make.md | 258 | ||||
| -rw-r--r-- | dev/doc/MERGING.md | 177 | ||||
| -rw-r--r-- | dev/doc/README.md | 4 | ||||
| -rw-r--r-- | dev/doc/changes.md | 10 | ||||
| -rw-r--r-- | dev/doc/critical-bugs | 12 | ||||
| -rw-r--r-- | dev/doc/shield-icon.png | bin | 0 -> 2512 bytes |
6 files changed, 284 insertions, 177 deletions
diff --git a/dev/doc/INSTALL.make.md b/dev/doc/INSTALL.make.md new file mode 100644 index 0000000000..3db5d0b14f --- /dev/null +++ b/dev/doc/INSTALL.make.md @@ -0,0 +1,258 @@ +Quick Installation Procedure using Make. +---------------------------------------- + + $ ./configure + $ make + $ make install (you may need superuser rights) + +Detailed Installation Procedure. +-------------------------------- + +1. Check that you have the OCaml compiler installed on your + computer and that `ocamlc` (or, better, its native code version + `ocamlc.opt`) is in a directory which is present in your $PATH + environment variable. At the time of writing this document, all + versions of Objective Caml later or equal to 4.05.0 are + supported. + + To get Coq in native-code, (which runs 4 to 10 times faster than + bytecode, but it takes more time to get compiled and the binary is + bigger), you will also need the `ocamlopt` (or its native code version + `ocamlopt.opt`) command. + +2. The uncompression and un-tarring of the distribution file gave birth + to a directory named "coq-8.xx". You can rename this directory and put + it wherever you want. Just keep in mind that you will need some spare + space during the compilation (reckon on about 300 Mb of disk space + for the whole system in native-code compilation). Once installed, the + binaries take about 30 Mb, and the library about 200 Mb. + +3. First you need to configure the system. It is done automatically with + the command: + + ./configure <options> + + The `configure` script will ask you for directories where to put + the Coq binaries, standard library, man pages, etc. It will propose + default values. + + For a list of options accepted by the `configure` script, run + `./configure -help`. The main options accepted are: + + * `-prefix <dir>` + Binaries, library, and man pages will be respectively + installed in `<dir>/bin`, `<dir>/lib/coq`, and `<dir>/man` + + * `-bindir <dir>` (default: `/usr/local/bin`) + Directory where the binaries will be installed + + * `-libdir <dir>` (default: `/usr/local/lib/coq`) + Directory where the Coq standard library will be installed + + * `-mandir <dir>` (default: `/usr/local/share/man`) + Directory where the Coq manual pages will be installed + + * `-arch <value>` (default is the result of the command `arch`) + An arbitrary architecture name for your machine (useful when + compiling Coq on two different architectures for which the + result of "arch" is the same, e.g. Sun OS and Solaris) + + * `-local` + Compile Coq to run in its source directory. The installation (step 6) + is not necessary in that case. + + * `-browser <command>` + Use <command> to open an URL in a browser. %s must appear in <command>, + and will be replaced by the URL. + + * `-flambda-opts <flags>` + This experimental option will pass specific user flags to the + OCaml optimizing compiler. In most cases, this option is used + to tweak the flambda backend; for maximum performance we + recommend using: + + -flambda-opts `-O3 -unbox-closures` + + but of course you are free to try with a different combination + of flags. You can read more at + https://caml.inria.fr/pub/docs/manual-ocaml/flambda.html + + There is a known problem with certain OCaml versions and + `native_compute`, that will make compilation to require + a large amount of RAM (>= 10GiB) in some particular files. + + We recommend disabling native compilation (`-native-compiler no`) + with flambda unless you use OCaml >= 4.07.0. + + c.f. https://caml.inria.fr/mantis/view.php?id=7630 + + If you want your build to be reproducible, ensure that the + SOURCE_DATE_EPOCH environment variable is set as documented in + https://reproducible-builds.org/specs/source-date-epoch/ + +4. Still in the root directory, do + + make + + to compile Coq in the best OCaml mode available (native-code if supported, + bytecode otherwise). + + This will compile the entire system. This phase can take more or less time, + depending on your architecture and is fairly verbose. On a multi-core machine, + it is recommended to compile in parallel, via make -jN where N is your number + of cores. + +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 + + umask 022 + make install + + Of course, you may need superuser rights to do that. + +6. Optionally, you could build the bytecode version of Coq via: + + make byte + + and install it via + + make install-byte + + This version is much slower than the native code version of Coq, but could + be helpful for debugging purposes. In particular, coqtop.byte embeds an OCaml + toplevel accessible via the Drop command. + +7. You can now clean all the sources. (You can even erase them.) + + make clean + +Installation Procedure For Plugin Developers. +--------------------------------------------- + +If you wish to write plugins you *must* keep the Coq sources, without +cleaning them. Therefore, to avoid a duplication of binaries and library, +it is not necessary to do the installation step (6- above). You just have +to tell it at configuration step (4- above) with the option -local : + + ./configure -local <other options> + +Then compile the sources as described in step 5 above. The resulting +binaries will reside in the subdirectory bin/. + +Unless you pass the -nodebug option to ./configure, the -g option of the +OCaml compiler will be used during compilation to allow debugging. +See the debugging file in dev/doc and the chapter 15 of the Coq Reference +Manual for details about how to use the OCaml debugger with Coq. + + +The Available Commands. +----------------------- + +There are two Coq commands: + + coqtop The Coq toplevel + coqc The Coq compiler + +Under architecture where ocamlopt is available, coqtop is the native code +version of Coq. On such architecture, you could additionally request +the build of the bytecode version of Coq via 'make byte' and install it via +'make install-byte'. This will create an extra binary named coqtop.byte, +that could be used for debugging purpose. If native code isn't available, +coqtop.byte is directly built by 'make', and coqtop is a link to coqtop.byte. +coqc also invokes the fastest version of Coq. Options -opt and -byte to coqtop +and coqc selects a particular binary. + +* `coqtop` launches Coq in the interactive mode. By default it loads + basic logical definitions and tactics from the Init directory. + +* `coqc` allows compilation of Coq files directly from the command line. + To compile a file foo.v, do: + + coqc foo.v + + It will produce a file `foo.vo`, that you can now load through the Coq + command `Require`. + + A detailed description of these commands and of their options is given + in the Reference Manual (which you can get in the doc/ + directory, or read online on http://coq.inria.fr/doc/) + and in the corresponding manual pages. + +Compiling For Different Architectures. +-------------------------------------- + +This section explains how to compile Coq for several architecture, sharing +the same sources. The important fact is that some files are architecture +dependent (`.cmx`, `.o` and executable files for instance) but others are not +(`.cmo` and `.vo`). Consequently, you can : + +- save some time during compilation by not cleaning the architecture + independent files; + +- save some space during installation by sharing the Coq standard + library (which is fully architecture independent). + +So, in order to compile Coq for a new architecture, proceed as follows: + +* Omit step 7 above and clean only the architecture dependent files: + it is done automatically with the command + + make archclean + +* Configure the system for the new architecture: + + ./configure <options> + + You can specify the same directory for the standard library but you + MUST specify a different directory for the binaries (of course). + +* Compile and install the system as described in steps 5 and 6 above. + +Moving Binaries Or Library. +--------------------------- + +If you move both the binaries and the library in a consistent way, +Coq should be able to still run. Otherwise, Coq may be "lost", +running "coqtop" would then return an error message of the kind: + + Error during initialization : + Error: cannot guess a path for Coq libraries; please use -coqlib option + +You can then indicate the new places to Coq, using the options -coqlib : + + coqtop -coqlib <new directory> + +See also next section. + +Dynamically Loaded Libraries For Bytecode Executables. +------------------------------------------------------ + +Some bytecode executables of Coq use the OCaml runtime, which dynamically +loads a shared library (.so or .dll). When it is not installed properly, you +can get an error message of this kind: + + Fatal error: cannot load shared library dllcoqrun + Reason: dllcoqrun.so: cannot open shared object file: No such file or directory + +In this case, you need either: + +- to set the `CAML_LD_LIBRARY_PATH` environment variable to point to the + directory where dllcoqrun.so is; this is suitable when you want to run + the command a limited number of times in a controlled environment (e.g. + during compilation of binary packages); +- install dllcoqrun.so in a location listed in the file ld.conf that is in + the directory of the standard library of OCaml; +- recompile your bytecode executables after reconfiguring the location + of the shared library: + + ./configure -vmbyteflags "-dllib,-lcoqrun,-dllpath,<path>" ... + + where `<path>` is the directory where the dllcoqrun.so is installed; +- (not recommended) compile bytecode executables with a custom OCaml + runtime by using: + + ./configure -custom ... + + be aware that stripping executables generated this way, or performing + other executable-specific operations, will make them useless. 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/README.md b/dev/doc/README.md index bc281e0d94..ba53605b0e 100644 --- a/dev/doc/README.md +++ b/dev/doc/README.md @@ -43,8 +43,12 @@ To learn how to run the test suite, you can read ## Development environment + tooling + - [`Merlin`](https://github.com/ocaml/merlin) for autocomplete. - [Wiki pages on tooling containing `emacs`, `vim`, and `git` information](https://github.com/coq/coq/wiki/DevelSetup) +- [`ocamlformat`](https://github.com/ocaml-ppx/ocamlformat) provides + support for automatic formatting of OCaml code. To use it please run + `dune build @fmt`, see `ocamlformat`'s documentation for more help. ## A note about rlwrap diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 7d394c3401..04b20c6889 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -1,5 +1,15 @@ ## Changes between Coq 8.11 and Coq 8.12 +### ML API + +Printers: + +- Functions such as Printer.pr_lconstr_goal_style_env have been + removed, use instead functions such as pr_lconstr with label + `goal_concl_style:true`. Functions such as + Constrextern.extern_constr which were taking a boolean argument for + the goal style now take instead a label. + ## 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..2d187f7bae 100644 --- a/dev/doc/critical-bugs +++ b/dev/doc/critical-bugs @@ -255,6 +255,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/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 |
