diff options
Diffstat (limited to 'dev/doc')
| -rw-r--r-- | dev/doc/COMPATIBILITY | 201 | ||||
| -rw-r--r-- | dev/doc/build-system.dev.txt | 2 | ||||
| -rw-r--r-- | dev/doc/build-system.txt | 8 | ||||
| -rw-r--r-- | dev/doc/changes.md | 37 | ||||
| -rw-r--r-- | dev/doc/coq-src-description.txt | 2 | ||||
| -rw-r--r-- | dev/doc/debugging.md | 27 | ||||
| -rw-r--r-- | dev/doc/setup.txt | 34 |
7 files changed, 268 insertions, 43 deletions
diff --git a/dev/doc/COMPATIBILITY b/dev/doc/COMPATIBILITY new file mode 100644 index 0000000000..a81afca32d --- /dev/null +++ b/dev/doc/COMPATIBILITY @@ -0,0 +1,201 @@ +Note: this file isn't used anymore. Incompatibilities are documented +as part of CHANGES. + +Potential sources of incompatibilities between Coq V8.6 and V8.7 +---------------------------------------------------------------- + +- Extra superfluous names in introduction patterns may now raise an + error rather than a warning when the superfluous name is already in + use. The easy fix is to remove the superfluous name. + +Potential sources of incompatibilities between Coq V8.5 and V8.6 +---------------------------------------------------------------- + +Symptom: An obligation generated by Program or an abstracted subproof +has different arguments. +Cause: Set Shrink Abstract and Set Shrink Obligations are on by default +and the subproof does not use the argument. +Remedy: +- Adapt the script. +- Write an explicit lemma to prove the obligation/subproof and use it + instead (compatible with 8.4). +- Unset the option for the program/proof the obligation/subproof originates + from. + +Symptom: In a goal, order of hypotheses, or absence of an equality of +the form "x = t" or "t = x", or no unfolding of a local definition. +Cause: This might be connected to a number of fixes in the tactic +"subst". The former behavior can be reactivated by issuing "Unset +Regular Subst Tactic". + +Potential sources of incompatibilities between Coq V8.4 and V8.5 +---------------------------------------------------------------- + +* List of typical changes to be done to adapt files from Coq 8.4 * +* to Coq 8.5 when not using compatibility option "-compat 8.4". * + +Symptom: "The reference omega was not found in the current environment". +Cause: "Require Omega" does not import the tactic "omega" any more +Possible solutions: +- use "Require Import OmegaTactic" (not compatible with 8.4) +- use "Require Import Omega" (compatible with 8.4) +- add definition "Ltac omega := Coq.omega.Omega.omega." + +Symptom: "intuition" cannot solve a goal (not working anymore on non standard connective) +Cause: "intuition" had an accidental non uniform behavior fixed on non standard connectives +Possible solutions: +- use "dintuition" instead; it is stronger than "intuition" and works + uniformly on non standard connectives, such as n-ary conjunctions or disjunctions + (not compatible with 8.4) +- do the script differently + +Symptom: The constructor foo (in type bar) expects n arguments. +Cause: parameters must now be given in patterns +Possible solutions: +- use option "Set Asymmetric Patterns" (compatible with 8.4) +- add "_" for the parameters (not compatible with 8.4) +- turn the parameters into implicit arguments (compatible with 8.4) + +Symptom: "NPeano.Nat.foo" not existing anymore +Possible solutions: +- use "Nat.foo" instead + +Symptom: typing problems with proj1_sig or similar +Cause: coercion from sig to sigT and similar coercions have been + removed so as to make the initial state easier to understand for + beginners +Solution: change proj1_sig into projT1 and similarly (compatible with 8.4) + +* Other detailed changes * + +(see also file CHANGES) + +- options for *coq* compilation (see below for ocaml). + +** [-I foo] is now deprecated and will not add directory foo to the + coq load path (only for ocaml, see below). Just replace [-I foo] by + [-Q foo ""] in your project file and re-generate makefile. Or + perform the same operation directly in your makefile if you edit it + by hand. + +** Option -R Foo bar is the same in v8.5 than in v8.4 concerning coq + load path. + +** Option [-I foo -as bar] is unchanged but discouraged unless you + compile ocaml code. Use -Q foo bar instead. + + for more details: file CHANGES or section "Customization at launch + time" of the reference manual. + +- Command line options for ocaml Compilation of ocaml code (plugins) + +** [-I foo] is *not* deprecated to add foo to the ocaml load path. + +** [-I foo -as bar] adds foo to the ocaml load path *and* adds foo to + the coq load path with logical name bar (shortcut for -I foo -Q foo + bar). + + for more details: file CHANGES or section "Customization at launch + time" of the reference manual. + +- Universe Polymorphism. + +- Refinement, unification and tactics are now aware of universes, + resulting in more localized errors. Universe inconsistencies + should no more get raised at Qed time but during the proof. + Unification *always* produces well-typed substitutions, hence + some rare cases of unifications that succeeded while producing + ill-typed terms before will now fail. + +- The [change p with c] tactic semantics changed, now typechecking + [c] at each matching occurrence [t] of the pattern [p], and + converting [t] with [c]. + +- Template polymorphic inductive types: the partial application + of a template polymorphic type (e.g. list) is not polymorphic. + An explicit parameter application (e.g [fun A => list A]) or + [apply (list _)] will result in a polymorphic instance. + +- The type inference algorithm now takes opacity of constants into + account. This may have effects on tactics using type inference + (e.g. induction). Extra "Transparent" might have to be added to + revert opacity of constants. + +Type classes. + +- When writing an Instance foo : Class A := {| proj := t |} (note the + vertical bars), support for typechecking the projections using the + type information and switching to proof mode is no longer available. + Use { } (without the vertical bars) instead. + +Tactic abstract. + +- Auxiliary lemmas generated by the abstract tactic are removed from + the global environment and inlined in the proof term when a proof + is ended with Qed. The behavior of 8.4 can be obtained by ending + proofs with "Qed exporting" or "Qed exporting ident, .., ident". + +Potential sources of incompatibilities between Coq V8.3 and V8.4 +---------------------------------------------------------------- + +(see also file CHANGES) + +The main known incompatibilities between 8.3 and 8.4 are consequences +of the following changes: + +- The reorganization of the library of numbers: + + Several definitions have new names or are defined in modules of + different names, but a special care has been taken to have this + renaming transparent for the user thanks to compatibility notations. + + However some definitions have changed, what might require some + adaptations. The most noticeable examples are: + - The "?=" notation which now bind to Pos.compare rather than former + Pcompare (now Pos.compare_cont). + - Changes in names may induce different automatically generated + names in proof scripts (e.g. when issuing "destruct Z_le_gt_dec"). + - Z.add has a new definition, hence, applying "simpl" on subterms of + its body might give different results than before. + - BigN.shiftl and BigN.shiftr have reversed arguments order, the + power function in BigN now takes two BigN. + +- Other changes in libraries: + + - The definition of functions over "vectors" (list of fixed length) + have changed. + - TheoryList.v has been removed. + +- Slight changes in tactics: + + - Less unfolding of fixpoints when applying destruct or inversion on + a fixpoint hiding an inductive type (add an extra call to simpl to + preserve compatibility). + - Less unexpected local definitions when applying "destruct" + (incompatibilities solvable by adapting name hypotheses). + - Tactic "apply" might succeed more often, e.g. by now solving + pattern-matching of the form ?f x y = g(x,y) (compatibility + ensured by using "Unset Tactic Pattern Unification"), but also + because it supports (full) betaiota (using "simple apply" might + then help). + - Tactic autorewrite does no longer instantiate pre-existing + existential variables. + - Tactic "info" is now available only for auto, eauto and trivial. + +- Miscellaneous changes: + + - The command "Load" is now atomic for backtracking (use "Unset + Atomic Load" for compatibility). + + +Incompatibilities beyond 8.4... + +- Syntax: "x -> y" has now lower priority than "<->" "A -> B <-> C" is + now "A -> (B <-> C)" + +- Tactics: tauto and intuition no longer accidentally destruct binary + connectives or records other than and, or, prod, sum, iff. In most + of cases, dtauto or dintuition, though stronger than 8.3 tauto and + 8.3 intuition will provide compatibility. + +- "Solve Obligations using" is now "Solve Obligations with". diff --git a/dev/doc/build-system.dev.txt b/dev/doc/build-system.dev.txt index f3fc13e969..abba13428f 100644 --- a/dev/doc/build-system.dev.txt +++ b/dev/doc/build-system.dev.txt @@ -46,7 +46,7 @@ see build-system.txt . .ml4 files ---------- -.ml4 are converted to .ml by camlp4. By default, they are produced +.ml4 are converted to .ml by camlp5. By default, they are produced in the binary ast format understood by ocamlc/ocamlopt/ocamldep. Pros: - faster than parsing clear-text source file. diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt index 873adc1b22..fd3101613a 100644 --- a/dev/doc/build-system.txt +++ b/dev/doc/build-system.txt @@ -88,7 +88,7 @@ bootstrapped. The dependencies of a file FOO are in FOO.d . This enables partial recalculation of dependencies (only the dependencies of changed files are recomputed). -If you add a dependency to a Coq camlp4 extension (grammar.cma or +If you add a dependency to a Coq camlp5 extension (grammar.cma or q_constr.cmo), then see sections ".ml4 files" and "new files". Cleaning Targets @@ -127,7 +127,7 @@ of a grammar extension via a line of the form: The use of (*i camlp4use: ... i*) to mention uses of standard extension such as IFDEF has also been discontinued, the Makefile now -always calls camlp4 with pa_macros.cmo and a few others by default. +always calls camlp5 with pa_macros.cmo and a few others by default. For debugging a Coq grammar extension, it could be interesting to use the READABLE_ML4=1 option, otherwise the generated .ml are @@ -143,7 +143,9 @@ file list(s): These files are also used by the experimental ocamlbuild plugin, which is quite touchy about them : be careful with order, duplicated entries, whitespace errors, and do not mention .mli there. - - For .v, in the corresponding vo.itarget (e.g theories/Init/vo.itarget) + If module B depends on module A, then B should be after A in the .mllib + file. +- For .v, in the corresponding vo.itarget (e.g theories/Init/vo.itarget) - The definitions in Makefile.common might have to be adapted too. - If your file needs a specific rule, add it to Makefile.build diff --git a/dev/doc/changes.md b/dev/doc/changes.md index f6fbb69424..ab78b0956f 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -12,16 +12,6 @@ All the bugs with a number below 1154 had to be renumbered, you can find a correspondence table [here](/dev/bugzilla2github_stripped.csv). All the other bugs kept their number. -### Plugin API - -Coq 8.8 offers a new module overlay containing a proposed plugin API -in `API/API.ml`; this overlay is enabled by adding the `-open API` -flag to the OCaml compiler; this happens automatically for -developments in the `plugin` folder and `coq_makefile`. - -However, `coq_makefile` can be instructed not to enable this flag by -passing `-bypass-API`. - ### ML API General deprecation @@ -30,6 +20,14 @@ General deprecation removed. Please, make sure your plugin is warning-free in 8.7 before trying to port it over 8.8. +Proof engine + + Due to the introduction of `EConstr` in 8.7, it is not necessary to + track "goal evar normal form status" anymore, thus the type `'a + Proofview.Goal.t` loses its ghost argument. This may introduce some + minor incompatibilities at the typing level. Code-wise, things + should remain the same. + We removed the following functions: - `Universes.unsafe_constr_of_global`: use `Global.constr_of_global_in_context` @@ -51,6 +49,14 @@ We changed the type of the following functions: a functional way. The old style of passing `evar_map`s as references is not supported anymore. +Changes in the abstract syntax tree: + +- The practical totality of the AST has been nodified using + `CAst.t`. This means that all objects coming from parsing will be + indeed wrapped in a `CAst.t`. `Loc.located` is on its way to + deprecation. Some minor interfaces changes have resulted from + this. + We have changed the representation of the following types: - `Lib.object_prefix` is now a record instead of a nested tuple. @@ -68,6 +74,17 @@ Declaration of printers for arguments used only in vernac command happen. An alternative is to register the corresponding argument as a value, using "Geninterp.register_val0 wit None". +### STM API + +The STM API has seen a general overhaul. The main change is the +introduction of a "Coq document" type, which all operations now take +as a parameter. This effectively functionalize the STM API and will +allow in the future to handle several documents simultaneously. + +The main remarkable point is that key implicit global parameters such +as load-paths and required modules are now arguments to the document +creation function. This helps enforcing some key invariants. + ### XML IDE Protocol - Before 8.8, `Query` only executed the first command present in the diff --git a/dev/doc/coq-src-description.txt b/dev/doc/coq-src-description.txt index 2dbd132da7..b3d49b7e56 100644 --- a/dev/doc/coq-src-description.txt +++ b/dev/doc/coq-src-description.txt @@ -25,7 +25,7 @@ intf : grammar : - Camlp4 syntax extensions. The file grammar/grammar.cma is used + Camlp5 syntax extensions. The file grammar/grammar.cma is used to pre-process .ml4 files containing EXTEND constructions, either TACTIC EXTEND, ARGUMENTS EXTEND or VERNAC ... EXTEND. This grammar.cma incorporates many files from other directories diff --git a/dev/doc/debugging.md b/dev/doc/debugging.md index fa145d498a..fd3cbd1bc3 100644 --- a/dev/doc/debugging.md +++ b/dev/doc/debugging.md @@ -22,8 +22,8 @@ Debugging from Coq toplevel using Caml trace mechanism printers too. -Debugging from Caml debugger -============================ +Debugging with ocamldebug from Emacs +==================================== Requires [Tuareg mode](https://github.com/ocaml/tuareg) in Emacs.\ Coq must be configured with `-local` (`./configure -local`) and the @@ -59,6 +59,29 @@ Debugging from Caml debugger from the debugger. If this happens, unset the variable, re-start Emacs, and run the debugger again. +Debugging with ocamldebug from the command line +=============================================== + +In the `coq` directory: +1. (on Cygwin/Windows) Pass the `-no-custom` option to the `configure` script before building Coq. +2. Run `make` (to compile the .v files) +3. Run `make byte` +4. (on Cygwin/Windows) Add the full pathname of the directory `.../kernel/byterun` to your bash PATH. + Alternatively, copy the file `kernel/byterun/dllcoqrun.dll` to a directory that is in the PATH. (The + CAML_LD_LIBRARY_PATH mechanism described at the end of INSTALL isn't working.) +5. Run `dev/ocamldebug-coq bin/coqtop.byte` (on Cygwin/Windows, use `... bin/coqtop.byte.exe`) +6. Enter `source db` to load printers +7. Enter `set arguments -coqlib .` so Coq can find plugins, theories, etc. +8. See the ocamldebug manual for more information. A few points: + - use `break @ Printer 501` to set a breakpoint on line 501 in the Printer module (printer.ml). + `break` can be abbreviated as `b`. + - `backtrace` or `bt` to see the call stack + - `step` or `s` goes into called functions; `next` or `n` skips over them + - `list` or `li` shows the code just before and after the current stack frame + - `print <var>` or `p <var>` to see the value of a variable +Note that `make byte` doesn't recompile .v files. `make` recompiles all of them if there +are changes in any .ml file--safer but much slower. + Global gprof-based profiling ============================ diff --git a/dev/doc/setup.txt b/dev/doc/setup.txt index 26f3d0ddc7..c48c2d5d16 100644 --- a/dev/doc/setup.txt +++ b/dev/doc/setup.txt @@ -41,15 +41,15 @@ Building coqtop: cd ~/git/coq git checkout trunk make distclean - ./configure -annotate -local + ./configure -profile devel make clean make -j4 coqide printers -The "-annotate" option is essential when one wants to use Merlin. +The "-profile devel" enables all options recommended for developers (like +warnings, support for Merlin, etc). Moreover Coq is configured so that +it can be run without installing it (i.e. from the current directory). -The "-local" option is useful if one wants to run the coqtop and coqide binaries without running make install - -Then check if +Once the compilation is over check if - bin/coqtop - bin/coqide behave as expected. @@ -58,30 +58,12 @@ behave as expected. A note about rlwrap ------------------- -Running "coqtop" under "rlwrap" is possible, but (on Debian) there is a catch. If you try: - - cd ~/git/coq - rlwrap bin/coqtop - -you will get an error: +When using "rlwrap coqtop" make sure the version of rlwrap is at least +0.42, otherwise you will get rlwrap: error: Couldn't read completions from /usr/share/rlwrap/completions/coqtop: No such file or directory -This is a known issue: - - https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=779692 - -It was fixed upstream in version 0.42, and in a Debian package that, at the time of writing, is not part of Debian stable/testing/sid archives but only of Debian experimental. - - https://packages.debian.org/experimental/rlwrap - -The quick solution is to grab it from there, since it installs fine on Debian stable (jessie). - - cd /tmp - wget http://ftp.us.debian.org/debian/pool/main/r/rlwrap/rlwrap_0.42-1_amd64.deb - sudo dpkg -i rlwrap_0.42-1_amd64.deb - -After that, "rlwrap" works fine with "coqtop". +If this happens either update or use an alternate readline wrapper like "ledit". How to install and configure Merlin (for Emacs) |