diff options
Diffstat (limited to 'dev/doc')
| -rw-r--r-- | dev/doc/INSTALL.make.md | 258 | ||||
| -rw-r--r-- | dev/doc/README.md | 4 | ||||
| -rw-r--r-- | dev/doc/changes.md | 14 | ||||
| -rw-r--r-- | dev/doc/critical-bugs | 44 | ||||
| -rw-r--r-- | dev/doc/xml-protocol.md | 43 |
5 files changed, 359 insertions, 4 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/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 ab9df12766..04b20c6889 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -1,7 +1,21 @@ +## 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 +- Function UnivGen.global_of_constr has been removed. + - Functions and types deprecated in 8.10 have been removed in Coq 8.11. diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs index 6d90ced12d..2d187f7bae 100644 --- a/dev/doc/critical-bugs +++ b/dev/doc/critical-bugs @@ -112,15 +112,25 @@ Universes component: universe polymorphism summary: universe polymorphism can capture global universes impacted released versions: V8.5 to V8.8 - impacted coqchk versions: V8.5 to current (NOT FIXED) - fixed in: 2385b5c1ef + impacted coqchk versions: V8.5 to V8.9 + fixed in: ec4aa4971f (58e1d0f200 for the checker) found by: Gaëtan Gilbert exploit: test-suite/misc/poly-capture-global-univs GH issue number: #8341 risk: unlikely to be activated by chance (requires a plugin) component: template polymorphism - summary: template polymorphism not collecting side constrains on the universe level of a parameter; this is a general form of the previous issue about template polymorphism exploiting other ways to generate untracked constraints introduced: morally at the introduction of template polymorphism, 23 May 2006, 9c2d70b, r8845, Herbelin impacted released versions: at least V8.4-V8.4pl6, V8.5-V8.5pl3, V8.6-V8.6pl2, V8.7.0-V8.7.1, V8.8.0-V8.8.1, V8.9.0-V8.9.1, in theory also V8.1-V8.1pl4, V8.2-V8.2pl2, V8.3-V8.3pl2 but not exploit found there yet (an exploit using a plugin to force sharing of universe level is in principle possible though) + summary: template polymorphism not collecting side constrains on the + universe level of a parameter; this is a general form of the + previous issue about template polymorphism exploiting other ways to + generate untracked constraints + introduced: morally at the introduction of template polymorphism, 23 + May 2006, 9c2d70b, r8845, Herbelin + impacted released versions: at least V8.4-V8.4pl6, V8.5-V8.5pl3, + V8.6-V8.6pl2, V8.7.0-V8.7.1, V8.8.0-V8.8.1, V8.9.0-V8.9.1, in theory + also V8.1-V8.1pl4, V8.2-V8.2pl2, V8.3-V8.3pl2 but not exploit found + there yet (an exploit using a plugin to force sharing of universe + level is in principle possible though) impacted development branches: all from 8.4 to 8.9 at the time of writing and suspectingly also all from 8.1 to 8.4 if a way to create untracked constraints can be found impacted coqchk versions: a priori all (tested with V8.4 and V8.9 which accept the exploit) fixed in: soon in master and V8.10.0 (PR #9918, Aug 2019, Dénès and Sozeau) @@ -129,6 +139,22 @@ Universes GH issue number: #9294 risk: moderate risk to be activated by chance + component: template polymorphism + summary: using the same universe in the parameters and the + constructor arguments of a template polymorphic inductive (using + named universes in modern Coq, or unification tricks in older Coq) + produces implicit equality constraints not caught by the previous + template polymorphism fix. + introduced: same as the previous template polymorphism bug, morally + from V8.1, first verified impacted version V8.5 (the universe + unification is sufficiently different in V8.4 to prevent our trick + from working) + fixed in: expected in 8.10.2, 8.11+beta, master (#11128, Nov 2019, Gilbert) + found by: Gilbert + exploit: test-suite/bugs/closed/bug_11039.v + GH issue number: #11039 + risk: moderate risk (found by investigating #10504) + 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 @@ -229,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/xml-protocol.md b/dev/doc/xml-protocol.md index a3e1a4e90b..0fc0a413ba 100644 --- a/dev/doc/xml-protocol.md +++ b/dev/doc/xml-protocol.md @@ -9,7 +9,7 @@ with Coq 8.5, and is used by CoqIDE. It will also be used in upcoming versions of Proof General. A somewhat out-of-date description of the async state machine is -[documented here](https://github.com/ejgallego/jscoq/blob/master/etc/notes/coq-notes.md). +[documented here](https://github.com/ejgallego/jscoq/blob/v8.10/etc/notes/coq-notes.md). OCaml types for the protocol can be found in the [`ide/protocol/interface.ml` file](/ide/protocol/interface.ml). Changes to the XML protocol are documented as part of [`dev/doc/changes.md`](/dev/doc/changes.md). @@ -45,6 +45,7 @@ Changes to the XML protocol are documented as part of [`dev/doc/changes.md`](/de - [File Loaded](#feedback-fileloaded) - [Message](#feedback-message) - [Custom](#feedback-custom) +* [Highlighting Text](#highlighting) Sentences: each command sent to Coqtop is a "sentence"; they are typically terminated by ".\s" (followed by whitespace or EOF). Examples: "Lemma a: True.", "(* asdf *) Qed.", "auto; reflexivity." @@ -753,3 +754,43 @@ Ex: `status = "Idle"` or `status = "proof: myLemmaName"` or `status = "Dead"` </feedback> ``` +## <a name="highlighting">Highlighting Text</a> + +[Proof diffs](https://coq.inria.fr/distrib/current/refman/proof-engine/proof-handling.html#showing-differences-between-proof-steps) +highlight differences between the current and previous proof states in the displayed output. +These are represented by tags embedded in output fields of the XML document. + +There are 4 tags that indicate how the enclosed text should be highlighted: +- diff.added - added text +- diff.removed - removed text +- diff.added.bg - unchanged text in a line that has additions ("bg" for "background") +- diff.removed.bg - unchanged text in a line that has removals + +CoqIDE, Proof General and coqtop currently use 2 shades of green and 2 shades of red +as the background color for highlights. Coqtop and CoqIDE also apply underlining and/or +strikeout highlighting for the sake of the color blind. + +For example, `<diff.added>ABC</diff.added>` indicates that "ABC" should be highlighted +as added text. Tags can be nested, such as: +`<diff.added.bg>A <diff.added> + 1</diff.added> + B</diff.added.bg>`. IDE code +displaying highlighted strings should maintain a stack for nested tags and the associated +highlight. Currently the diff code only nests at most 2 tags deep. +If an IDE uses other highlights such as text foreground color or italic text, it may +need to merge the background color with those other highlights to give the desired +(IDE dependent) behavior. + +The current implementations avoid highlighting white space at the beginning or the +end of a line. This gives a better appearance. + +There may be additional text that is marked with other tags in the output text. IDEs probably +should ignore and not display tags they don't recognize. + +Some internal details about generating tags within Coq (e.g. if you want to add +additional tags): + +Tagged output strings are generated from Pp.t's. Use Pp.tag to highlight a Pp.t using +one of the tags listed above. A span of tokens can be marked by using "start.<tag>" on +the first token and "end.<tag>" on the last token. (Span markers are needed because a span of +tokens in the output may not match nesting of layout boxes in the Pp.t.) +The conversion from the Pp.t to the XML-tagged string replaces the "start.\*" and "end.\*" +tags with the basic tags. |