From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- dev/doc/COMPATIBILITY | 201 ++++++ dev/doc/build-system.dev.txt | 22 +- dev/doc/build-system.txt | 8 +- dev/doc/changes.md | 1316 +++++++++++++++++++++++++++++++++++++++ dev/doc/changes.txt | 1095 -------------------------------- dev/doc/cic.dtd | 2 +- dev/doc/coq-src-description.txt | 7 +- dev/doc/debugging.md | 106 ++++ dev/doc/debugging.txt | 78 --- dev/doc/econstr.md | 129 ++++ dev/doc/naming-conventions.tex | 2 +- dev/doc/notes-on-conversion | 73 --- dev/doc/notes-on-conversion.v | 73 +++ dev/doc/primproj.md | 41 ++ dev/doc/profiling.txt | 2 +- dev/doc/proof-engine.md | 133 ++++ dev/doc/setup.txt | 40 +- dev/doc/style.txt | 215 ++++--- dev/doc/universes.md | 226 +++++++ dev/doc/universes.txt | 26 - dev/doc/univpoly.txt | 279 --------- dev/doc/versions-history.tex | 18 + dev/doc/xml-protocol.md | 755 ++++++++++++++++++++++ 23 files changed, 3169 insertions(+), 1678 deletions(-) create mode 100644 dev/doc/COMPATIBILITY create mode 100644 dev/doc/changes.md delete mode 100644 dev/doc/changes.txt create mode 100644 dev/doc/debugging.md delete mode 100644 dev/doc/debugging.txt create mode 100644 dev/doc/econstr.md delete mode 100644 dev/doc/notes-on-conversion create mode 100644 dev/doc/notes-on-conversion.v create mode 100644 dev/doc/primproj.md create mode 100644 dev/doc/proof-engine.md create mode 100644 dev/doc/universes.md delete mode 100644 dev/doc/universes.txt delete mode 100644 dev/doc/univpoly.txt create mode 100644 dev/doc/xml-protocol.md (limited to 'dev/doc') diff --git a/dev/doc/COMPATIBILITY b/dev/doc/COMPATIBILITY new file mode 100644 index 00000000..a81afca3 --- /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 fefcb093..abba1342 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. @@ -74,25 +74,25 @@ The Makefile is separated in several files : - Makefile.doc : specific rules for compiling the documentation. -FIND_VCS_CLAUSE +FIND_SKIP_DIRS --------------- -The recommended style of using FIND_VCS_CLAUSE is for example +The recommended style of using FIND_SKIP_DIRS is for example - find . $(FIND_VCS_CLAUSE) '(' -name '*.example' ')' -print - find . $(FIND_VCS_CLAUSE) '(' -name '*.example' -or -name '*.foo' ')' -print + find . $(FIND_SKIP_DIRS) '(' -name '*.example' ')' -print + find . $(FIND_SKIP_DIRS) '(' -name '*.example' -or -name '*.foo' ')' -print 1) The parentheses even in the one-criteria case is so that if one adds other conditions, e.g. change the first example to the second - find . $(FIND_VCS_CLAUSE) '(' -name '*.example' -and -not -name '*.bak.example' ')' -print + find . $(FIND_SKIP_DIRS) '(' -name '*.example' -and -not -name '*.bak.example' ')' -print one is not tempted to write - find . $(FIND_VCS_CLAUSE) -name '*.example' -and -not -name '*.bak.example' -print + find . $(FIND_SKIP_DIRS) -name '*.example' -and -not -name '*.bak.example' -print -because this will not necessarily work as expected; $(FIND_VCS_CLAUSE) +because this will not necessarily work as expected; $(FIND_SKIP_DIRS) ends with an -or, and how it combines with what comes later depends on operator precedence and all that. Much safer to override it with parentheses. @@ -105,13 +105,13 @@ As to the -print at the end, yes it is necessary. Here's why. You are used to write: find . -name '*.example' and it works fine. But the following will not: - find . $(FIND_VCS_CLAUSE) -name '*.example' -it will also list things directly matched by FIND_VCS_CLAUSE + find . $(FIND_SKIP_DIRS) -name '*.example' +it will also list things directly matched by FIND_SKIP_DIRS (directories we want to prune, in which we don't want to find anything). C'est subtil... Il y a effectivement un -print implicite à la fin, qui fait que la commande habituelle sans print fonctionne bien, mais dès que l'on introduit d'autres commandes dans le lot (le --prune de FIND_VCS_CLAUSE), ça se corse à cause d'histoires de +-prune de FIND_SKIP_DIRS), ça se corse à cause d'histoires de parenthèses du -print implicite par rapport au parenthésage dans la forme recommandée d'utilisation: diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt index 873adc1b..fd310161 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 new file mode 100644 index 00000000..ab78b095 --- /dev/null +++ b/dev/doc/changes.md @@ -0,0 +1,1316 @@ +## Changes between Coq 8.7 and Coq 8.8 + +### Bug tracker + +As of 18/10/2017, Coq uses [GitHub issues](https://github.com/coq/coq/issues) +as bug tracker. +Old bug reports were migrated from Bugzilla to GitHub issues using +[this migration script](https://gist.github.com/Zimmi48/d923e52f64fe17c72852d9c148bfcdc6#file-bugzilla2github) +as detailed in [this blog post](https://www.theozimmermann.net/2017/10/bugzilla-to-github/). + +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. + +### ML API + +General deprecation + +- All functions marked [@@ocaml.deprecated] in 8.7 have been + 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` + instead. The returned term contains De Bruijn universe variables. If you don't + depend on universes being instantiated, simply drop the context. + +- `Universes.unsafe_type_of_global`: same as above with + `Global.type_of_global_in_context` + +We changed the type of the following functions: + +- `Global.body_of_constant_body`: now also returns the abstract universe context. + The returned term contains De Bruijn universe variables. + +- `Global.body_of_constant`: same as above. + +- `Constrinterp.*` generally, many functions that used to take an + `evar_map ref` have been now switched to functions that will work in + 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. + +Some tactics and related functions now support static configurability, e.g.: + +- injectable, dEq, etc. takes an argument ~keep_proofs which, + - if None, tells to behave as told with the flag Keep Proof Equalities + - if Some b, tells to keep proof equalities iff b is true + +Declaration of printers for arguments used only in vernac command + +- It should now use "declare_extra_vernac_genarg_pprule" rather than + "declare_extra_genarg_pprule", otherwise, a failure at runtime might + 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 + `query` string; starting with 8.8, the caller may include several + statements. This is useful for instance for temporarily setting an + option and then executing a command. + +## Changes between Coq 8.6 and Coq 8.7 + +### Ocaml + +Coq is compiled with `-safe-string` enabled and requires plugins to do +the same. This means that code using `String` in an imperative way +will fail to compile now. They should switch to `Bytes.t` + +Configure supports passing flambda options, use `-flambda-opts OPTS` +with a flambda-enabled Ocaml to tweak the compilation to your taste. + +### ML API + +- Added two functions for declaring hooks to be executed in reduction +functions when some given constants are traversed: + + * `declare_reduction_effect`: to declare a hook to be applied when some + constant are visited during the execution of some reduction functions + (primarily cbv). + + * `set_reduction_effect`: to declare a constant on which a given effect + hook should be called. + +- We renamed the following functions: + + ``` + Context.Rel.Declaration.fold -> Context.Rel.Declaration.fold_constr + Context.Named.Declaration.fold -> Context.Named.Declaration.fold_constr + Printer.pr_var_list_decl -> Printer.pr_compacted_decl + Printer.pr_var_decl -> Printer.pr_named_decl + Nameops.lift_subscript -> Nameops.increment_subscript + ``` + +- We removed the following functions: + + * `Termops.compact_named_context_reverse`: practical substitute is `Termops.compact_named_context`. + * `Namegen.to_avoid`: equivalent substitute is `Names.Id.List.mem`. + +- We renamed the following modules: + + * `Context.ListNamed` -> `Context.Compacted` + +- The following type aliases where removed + + * `Context.section_context`: it was just an alias for `Context.Named.t` which is still available. + +- The module `Constrarg` was merged into `Stdarg`. + +- The following types have been moved and modified: + + * `local_binder` -> `local_binder_expr` + * `glob_binder` merged with `glob_decl` + +- The following constructors have been renamed: + + ``` + LocalRawDef -> CLocalDef + LocalRawAssum -> CLocalAssum + LocalPattern -> CLocalPattern + ``` + +- In `Constrexpr_ops`: + + Deprecating `abstract_constr_expr` in favor of `mkCLambdaN`, and + `prod_constr_expr` in favor of `mkCProdN`. Note: the first ones were + interpreting `(x y z:_)` as `(x:_) (y:_) (z:_)` while the second + ones were preserving the original sharing of the type. + +- In `Nameops`: + + The API has been made more uniform. New combinators added in the + `Name` space name. Function `out_name` now fails with `IsAnonymous` + rather than with `Failure "Nameops.out_name"`. + +- Location handling and AST attributes: + + Location handling has been reworked. First, `Loc.ghost` has been + removed in favor of an option type, all objects carrying an optional + source code location have been switched to use `Loc.t option`. + + Storage of location information has been also refactored. The main + datatypes representing Coq AST (`constrexpr`, `glob_expr`) have been + switched to a generic "node with attributes" representation `'a + CAst.ast`, which is a record of the form: + + ```ocaml + type 'a ast = private { + v : 'a; + loc : Loc.t option; + ... + } + ``` + consumers of AST nodes are recommended to use accessor-based pattern + matching `{ v; loc }` to destruct `ast` object. Creation is done + with `CAst.make ?loc obj`, where the attributes are optional. Some + convenient combinators are provided in the module. A typical match: + + ```ocaml + | CCase(loc, a1) -> CCase(loc, f a1) + ``` + + is now done as: + ```ocaml + | { v = CCase(a1); loc } -> CAst.make ?loc @@ CCase(f a1) + + ``` + or even better, if plan to preserve the attributes you can wrap your + top-level function in `CAst.map` to have: + + ```ocaml + | CCase(a1) -> CCase(f a1) + ``` + + This scheme based on records enables easy extensibility of the AST + node type without breaking compatibility. + + Not all objects carrying a location have been converted to the + generic node representation, some of them may be converted in the + future, for some others the abstraction is not just worth it. + + Thus, we still maintain a `'a Loc.located == Loc.t option * a'`, + tuple type which should be treated as private datatype (ok to match + against, but forbidden to manually build), and it is mandatory to + use it for objects that carry a location. This policy has been + implemented in the whole code base. Matching a located object hasn't + changed, however, `Loc.tag ?loc obj` must be used to build one. + +- In `GOption`: + + Support for non-synchronous options has been removed. Now all + options are handled as a piece of normal document state, and thus + passed to workers, etc... As a consequence, the field + `Goptions.optsync` has been removed. + +- In `Coqlib` / reference location: + + We have removed from Coqlib functions returning `constr` from + names. Now it is only possible to obtain references, that must be + processed wrt the particular needs of the client. + We have changed in constrintern the functions returnin `constr` as + well to return global references instead. + + Users of `coq_constant/gen_constant` can do + `Universes.constr_of_global (find_reference dir r)` _however_ note + the warnings in the `Universes.constr_of_global` in the + documentation. It is very likely that you were previously suffering + from problems with polymorphic universes due to using + `Coqlib.coq_constant` that used to do this. You must rather use + `pf_constr_of_global` in tactics and `Evarutil.new_global` variants + when constructing terms in ML (see univpoly.txt for more information). + +### Tactic API + +- `pf_constr_of_global` now returns a tactic instead of taking a continuation. + Thus it only generates one instance of the global reference, and it is the + caller's responsibility to perform a focus on the goal. + +- `pf_global`, `construct_reference`, `global_reference`, + `global_reference_in_absolute_module` now return a `global_reference` + instead of a `constr`. + +- The `tclWEAK_PROGRESS` and `tclNOTSAMEGOAL` tacticals were removed. Their usecase + was very specific. Use `tclPROGRESS` instead. + +- New (internal) tactical `tclINDEPENDENTL` that combined with enter_one allows + to iterate a non-unit tactic on all goals and access their returned values. + +- The unsafe flag of the `Refine.refine` function and its variants has been + renamed and dualized into typecheck and has been made mandatory. + +### Ltac API + +Many Ltac specific API has been moved in its own ltac/ folder. Amongst other +important things: + +- `Pcoq.Tactic` -> `Pltac` +- `Constrarg.wit_tactic` -> `Tacarg.wit_tactic` +- `Constrarg.wit_ltac` -> `Tacarg.wit_ltac` +- API below `ltac/` that accepted a *`_tactic_expr` now accept a *`_generic_argument` + instead +- Some printing functions were moved from `Pptactic` to `Pputils` +- A part of `Tacexpr` has been moved to `Tactypes` +- The `TacFun` tactic expression constructor now takes a `Name.t list` for the + variable list rather than an `Id.t option list`. + +The folder itself has been turned into a plugin. This does not change much, +but because it is a packed plugin, it may wreak havoc for third-party plugins +depending on any module defined in the `ltac/` directory. Namely, even if +everything looks OK at compile time, a plugin can fail to load at link time +because it mistakenly looks for a module `Foo` instead of `Ltac_plugin.Foo`, with +an error of the form: + +``` +Error: while loading myplugin.cmxs, no implementation available for Foo. +``` + +In particular, most `EXTEND` macros will trigger this problem even if they +seemingly do not use any Ltac module, as their expansion do. + +The solution is simple, and consists in adding a statement `open Ltac_plugin` +in each file using a Ltac module, before such a module is actually called. An +alternative solution would be to fully qualify Ltac modules, e.g. turning any +call to Tacinterp into `Ltac_plugin.Tacinterp`. Note that this solution does not +work for `EXTEND` macros though. + +### Additional changes in tactic extensions + +Entry `constr_with_bindings` has been renamed into +`open_constr_with_bindings`. New entry `constr_with_bindings` now +uses type classes and rejects terms with unresolved holes. + +### Error handling + +- All error functions now take an optional parameter `?loc:Loc.t`. For + functions that used to carry a suffix `_loc`, such suffix has been + dropped. + +- `errorlabstrm` and `error` has been removed in favor of `user_err`. + +- The header parameter to `user_err` has been made optional. + +### Pretty printing + +Some functions have been removed, see pretty printing below for more +details. + +#### Pretty Printing and XML protocol + +The type `std_cmdpps` has been reworked and made the canonical "Coq rich +document type". This allows for a more uniform handling of printing +(specially in IDEs). The main consequences are: + + - Richpp has been confined to IDE use. Most of previous uses of the + `richpp` type should be replaced now by `Pp.std_cmdpps`. Main API + has been updated. + + - The XML protocol will send a new message type of `pp`, which should + be rendered client-wise. + + - `Set Printing Width` is deprecated, now width is controlled + client-side. + + - `Pp_control` has removed. The new module `Topfmt` implements + console control for the toplevel. + + - The impure tag system in `Pp` has been removed. This also does away + with the printer signatures and functors. Now printers tag + unconditionally. + + - The following functions have been removed from `Pp`: + + ```ocaml + val stras : int * string -> std_ppcmds + val tbrk : int * int -> std_ppcmds + val tab : unit -> std_ppcmds + val pifb : unit -> std_ppcmds + val comment : int -> std_ppcmds + val comments : ((int * int) * string) list ref + val eval_ppcmds : std_ppcmds -> std_ppcmds + val is_empty : std_ppcmds -> bool + val t : std_ppcmds -> std_ppcmds + val hb : int -> std_ppcmds + val vb : int -> std_ppcmds + val hvb : int -> std_ppcmds + val hovb : int -> std_ppcmds + val tb : unit -> std_ppcmds + val close : unit -> std_ppcmds + val tclose : unit -> std_ppcmds + val open_tag : Tag.t -> std_ppcmds + val close_tag : unit -> std_ppcmds + val msg_with : ... + + module Tag + ``` + +### Stm API + +- We have streamlined the `Stm` API, now `add` and `query` take a + `coq_parsable` instead a `string` so clients can have more control + over their input stream. As a consequence, their types have been + modified. + +- The main parsing entry point has also been moved to the + `Stm`. Parsing is considered a synchronous operation so it will + either succeed or raise an exception. + +- `Feedback` is now only emitted for asynchronous operations. As a + consequence, it always carries a valid stateid and the type has + changed to accommodate that. + +- A few unused hooks were removed due to cleanups, no clients known. + +### Toplevel and Vernacular API + +- The components related to vernacular interpretation have been moved + to their own folder `vernac/` whereas toplevel now contains the + proper toplevel shell and compiler. + +- Coq's toplevel has been ported to directly use the common `Stm` + API. The signature of a few functions has changed as a result. + +### XML Protocol + +- The legacy `Interp` call has been turned into a noop. + +- The `query` call has been modified, now it carries a mandatory + `route_id` integer parameter, that associated the result of such + query with its generated feedback. + +## Changes between Coq 8.5 and Coq 8.6 + +### Parsing + +`Pcoq.parsable` now takes an extra optional filename argument so as to +bind locations to a file name when relevant. + +### Files + +To avoid clashes with OCaml's compiler libs, the following files were renamed: + +``` +kernel/closure.ml{,i} -> kernel/cClosure.ml{,i} +lib/errors.ml{,i} -> lib/cErrors.ml{,i} +toplevel/cerror.ml{,i} -> toplevel/explainErr.mli{,i} +``` + +All IDE-specific files, including the XML protocol have been moved to `ide/` + +### Reduction functions + +In `closure.ml`, we introduced the more precise reduction flags `fMATCH`, `fFIX`, +`fCOFIX`. + +We renamed the following functions: + +``` +Closure.betadeltaiota -> Closure.all +Closure.betadeltaiotanolet -> Closure.allnolet +Reductionops.beta -> Closure.beta +Reductionops.zeta -> Closure.zeta +Reductionops.betaiota -> Closure.betaiota +Reductionops.betaiotazeta -> Closure.betaiotazeta +Reductionops.delta -> Closure.delta +Reductionops.betalet -> Closure.betazeta +Reductionops.betadelta -> Closure.betadeltazeta +Reductionops.betadeltaiota -> Closure.all +Reductionops.betadeltaiotanolet -> Closure.allnolet +Closure.no_red -> Closure.nored +Reductionops.nored -> Closure.nored +Reductionops.nf_betadeltaiota -> Reductionops.nf_all +Reductionops.whd_betadelta -> Reductionops.whd_betadeltazeta +Reductionops.whd_betadeltaiota -> Reductionops.whd_all +Reductionops.whd_betadeltaiota_nolet -> Reductionops.whd_allnolet +Reductionops.whd_betadelta_stack -> Reductionops.whd_betadeltazeta_stack +Reductionops.whd_betadeltaiota_stack -> Reductionops.whd_all_stack +Reductionops.whd_betadeltaiota_nolet_stack -> Reductionops.whd_allnolet_stack +Reductionops.whd_betadelta_state -> Reductionops.whd_betadeltazeta_state +Reductionops.whd_betadeltaiota_state -> Reductionops.whd_all_state +Reductionops.whd_betadeltaiota_nolet_state -> Reductionops.whd_allnolet_state +Reductionops.whd_eta -> Reductionops.shrink_eta +Tacmach.pf_whd_betadeltaiota -> Tacmach.pf_whd_all +Tacmach.New.pf_whd_betadeltaiota -> Tacmach.New.pf_whd_all +``` + +And removed the following ones: + +``` +Reductionops.whd_betaetalet +Reductionops.whd_betaetalet_stack +Reductionops.whd_betaetalet_state +Reductionops.whd_betadeltaeta_stack +Reductionops.whd_betadeltaeta_state +Reductionops.whd_betadeltaeta +Reductionops.whd_betadeltaiotaeta_stack +Reductionops.whd_betadeltaiotaeta_state +Reductionops.whd_betadeltaiotaeta +``` + +In `intf/genredexpr.mli`, `fIota` was replaced by `FMatch`, `FFix` and +`FCofix`. Similarly, `rIota` was replaced by `rMatch`, `rFix` and `rCofix`. + +### Notation_ops + +Use `Glob_ops.glob_constr_eq` instead of `Notation_ops.eq_glob_constr`. + +### Logging and Pretty Printing + +* Printing functions have been removed from `Pp.mli`, which is now a + purely pretty-printing interface. Functions affected are: + +```` ocaml +val pp : std_ppcmds -> unit +val ppnl : std_ppcmds -> unit +val pperr : std_ppcmds -> unit +val pperrnl : std_ppcmds -> unit +val pperr_flush : unit -> unit +val pp_flush : unit -> unit +val flush_all : unit -> unit +val msg : std_ppcmds -> unit +val msgnl : std_ppcmds -> unit +val msgerr : std_ppcmds -> unit +val msgerrnl : std_ppcmds -> unit +val message : string -> unit +```` + + which are no more available. Users of `Pp.pp msg` should now use the + proper `Feedback.msg_*` function. Clients also have no control over + flushing, the back end takes care of it. + + Also, the `msg_*` functions now take an optional `?loc` parameter + for relaying location to the client. + +* Feedback related functions and definitions have been moved to the + `Feedback` module. `message_level` has been renamed to + level. Functions moved from `Pp` to `Feedback` are: + +```` ocaml +val set_logger : logger -> unit +val std_logger : logger +val emacs_logger : logger +val feedback_logger : logger +```` + +* Changes in the Feedback format/Protocol. + +- The `Message` feedback type now carries an optional location, the main + payload is encoded using the richpp document format. + +- The `ErrorMsg` feedback type is thus unified now with `Message` at + level `Error`. + +* We now provide several loggers, `log_via_feedback` is removed in + favor of `set_logger feedback_logger`. Output functions are: + +```` ocaml +val with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b +val msg_error : ?loc:Loc.t -> Pp.std_ppcmds -> unit +val msg_warning : ?loc:Loc.t -> Pp.std_ppcmds -> unit +val msg_notice : ?loc:Loc.t -> Pp.std_ppcmds -> unit +val msg_info : ?loc:Loc.t -> Pp.std_ppcmds -> unit +val msg_debug : ?loc:Loc.t -> Pp.std_ppcmds -> unit +```` + + with the `msg_*` functions being just an alias for `logger $Level`. + +* The main feedback functions are: + +```` ocaml +val set_feeder : (feedback -> unit) -> unit +val feedback : ?id:edit_or_state_id -> ?route:route_id -> feedback_content -> unit +val set_id_for_feedback : ?route:route_id -> edit_or_state_id -> unit +```` + Note that `feedback` doesn't take two parameters anymore. After + refactoring the following function has been removed: + +```` ocaml +val get_id_for_feedback : unit -> edit_or_state_id * route_id +```` + +### Kernel API changes + +- The interface of the `Context` module was changed. + Related types and functions were put in separate submodules. + The mapping from old identifiers to new identifiers is the following: + + ``` + Context.named_declaration ---> Context.Named.Declaration.t + Context.named_list_declaration ---> Context.NamedList.Declaration.t + Context.rel_declaration ---> Context.Rel.Declaration.t + Context.map_named_declaration ---> Context.Named.Declaration.map_constr + Context.map_named_list_declaration ---> Context.NamedList.Declaration.map + Context.map_rel_declaration ---> Context.Rel.Declaration.map_constr + Context.fold_named_declaration ---> Context.Named.Declaration.fold + Context.fold_rel_declaration ---> Context.Rel.Declaration.fold + Context.exists_named_declaration ---> Context.Named.Declaration.exists + Context.exists_rel_declaration ---> Context.Rel.Declaration.exists + Context.for_all_named_declaration ---> Context.Named.Declaration.for_all + Context.for_all_rel_declaration ---> Context.Rel.Declaration.for_all + Context.eq_named_declaration ---> Context.Named.Declaration.equal + Context.eq_rel_declaration ---> Context.Rel.Declaration.equal + Context.named_context ---> Context.Named.t + Context.named_list_context ---> Context.NamedList.t + Context.rel_context ---> Context.Rel.t + Context.empty_named_context ---> Context.Named.empty + Context.add_named_decl ---> Context.Named.add + Context.vars_of_named_context ---> Context.Named.to_vars + Context.lookup_named ---> Context.Named.lookup + Context.named_context_length ---> Context.Named.length + Context.named_context_equal ---> Context.Named.equal + Context.fold_named_context ---> Context.Named.fold_outside + Context.fold_named_list_context ---> Context.NamedList.fold + Context.fold_named_context_reverse ---> Context.Named.fold_inside + Context.instance_from_named_context ---> Context.Named.to_instance + Context.extended_rel_list ---> Context.Rel.to_extended_list + Context.extended_rel_vect ---> Context.Rel.to_extended_vect + Context.fold_rel_context ---> Context.Rel.fold_outside + Context.fold_rel_context_reverse ---> Context.Rel.fold_inside + Context.map_rel_context ---> Context.Rel.map_constr + Context.map_named_context ---> Context.Named.map_constr + Context.iter_rel_context ---> Context.Rel.iter + Context.iter_named_context ---> Context.Named.iter + Context.empty_rel_context ---> Context.Rel.empty + Context.add_rel_decl ---> Context.Rel.add + Context.lookup_rel ---> Context.Rel.lookup + Context.rel_context_length ---> Context.Rel.length + Context.rel_context_nhyps ---> Context.Rel.nhyps + Context.rel_context_tags ---> Context.Rel.to_tags + ``` + +- Originally, rel-context was represented as: + + ```ocaml + type Context.rel_context = Names.Name.t * Constr.t option * Constr.t + ``` + + Now it is represented as: + + ```ocaml + type Context.Rel.Declaration.t = LocalAssum of Names.Name.t * Constr.t + | LocalDef of Names.Name.t * Constr.t * Constr.t + ``` + +- Originally, named-context was represented as: + + ```ocaml + type Context.named_context = Names.Id.t * Constr.t option * Constr.t + ``` + + Now it is represented as: + + ```ocaml + type Context.Named.Declaration.t = LocalAssum of Names.Id.t * Constr.t + | LocalDef of Names.Id.t * Constr.t * Constr.t + ``` + +- The various `EXTEND` macros do not handle specially the Coq-defined entries + anymore. Instead, they just output a name that have to exist in the scope + of the ML code. The parsing rules (`VERNAC`) `ARGUMENT EXTEND` will look for + variables `$name` of type `Gram.entry`, while the parsing rules of + (`VERNAC COMMAND` | `TACTIC`) `EXTEND`, as well as the various `TYPED AS` clauses will + look for variables `wit_$name` of type `Genarg.genarg_type`. The small DSL + for constructing compound entries still works over this scheme. Note that in + the case of (`VERNAC`) `ARGUMENT EXTEND`, the name of the argument entry is bound + in the parsing rules, so beware of recursive calls. + + For example, to get `wit_constr` you must `open Constrarg` at the top of the file. + +- `Evarutil` was split in two parts. The new `Evardefine` file exposes functions + `define_evar_`* mostly used internally in the unification engine. + +- The `Refine` module was moved out of `Proofview`. + + ``` + Proofview.Refine.* ---> Refine.* + ``` + +- A statically monotonic evarmap type was introduced in `Sigma`. Not all the API + has been converted, so that the user may want to use compatibility functions + `Sigma.to_evar_map` and `Sigma.Unsafe.of_evar_map` or `Sigma.Unsafe.of_pair` when + needed. Code can be straightforwardly adapted in the following way: + + ```ocaml + let (sigma, x1) = ... in + ... + let (sigma, xn) = ... in + (sigma, ans) + ``` + + should be turned into: + + ```ocaml + open Sigma.Notations + + let Sigma (x1, sigma, p1) = ... in + ... + let Sigma (xn, sigma, pn) = ... in + Sigma (ans, sigma, p1 +> ... +> pn) + ``` + + Examples of `Sigma.Unsafe.of_evar_map` include: + + ``` + Evarutil.new_evar env (Tacmach.project goal) ty ----> Evarutil.new_evar env (Sigma.Unsafe.of_evar_map (Tacmach.project goal)) ty + ``` + +- The `Proofview.Goal.`*`enter` family of functions now takes a polymorphic + continuation given as a record as an argument. + + ```ocaml + Proofview.Goal.enter begin fun gl -> ... end + ``` + + should be turned into + + ```ocaml + open Proofview.Notations + + Proofview.Goal.enter { enter = begin fun gl -> ... end } + ``` + +- `Tacexpr.TacDynamic(Loc.dummy_loc, Pretyping.constr_in c)` ---> `Tacinterp.Value.of_constr c` +- `Vernacexpr.HintsResolveEntry(priority, poly, hnf, path, atom)` ---> `Vernacexpr.HintsResolveEntry(Vernacexpr.({hint_priority = priority; hint_pattern = None}), poly, hnf, path, atom)` +- `Pretyping.Termops.mem_named_context` ---> `Engine.Termops.mem_named_context_val` +- `Global.named_context` ---> `Global.named_context_val` +- `Context.Named.lookup` ---> `Environ.lookup_named_val` + +### Search API + +The main search functions now take a function iterating over the +results. This allows for clients to use streaming or more economic +printing. + +### XML Protocol + +- In several places, flat text wrapped in `` tags now appears as structured text inside `` tags. + +- The "errormsg" feedback has been replaced by a "message" feedback which contains `` tag, with a message_level attribute of "error". + +## Changes between Coq 8.4 and Coq 8.5 + +### Refactoring : more mli interfaces and simpler grammar.cma + +- A new directory intf/ now contains mli-only interfaces : + + * `Constrexpr` : definition of `constr_expr`, was in `Topconstr` + * `Decl_kinds` : now contains `binding_kind = Explicit | Implicit` + * `Evar_kinds` : type `Evar_kinds.t` was previously `Evd.hole_kind` + * `Extend` : was `parsing/extend.mli` + * `Genredexpr` : regroup `Glob_term.red_expr_gen` and `Tacexpr.glob_red_flag` + * `Glob_term` : definition of `glob_constr` + * `Locus` : definition of occurrences and stuff about clauses + * `Misctypes` : `intro_pattern_expr`, `glob_sort`, `cast_type`, `or_var`, ... + * `Notation_term` : contains `notation_constr`, was `Topconstr.aconstr` + * `Pattern` : contains `constr_pattern` + * `Tacexpr` : was `tactics/tacexpr.ml` + * `Vernacexpr` : was `toplevel/vernacexpr.ml` + +- Many files have been divided : + + * vernacexpr: vernacexpr.mli + Locality + * decl_kinds: decl_kinds.mli + Kindops + * evd: evar_kinds.mli + evd + * tacexpr: tacexpr.mli + tacops + * glob_term: glob_term.mli + glob_ops + genredexpr.mli + redops + * topconstr: constrexpr.mli + constrexpr_ops + + notation_expr.mli + notation_ops + topconstr + * pattern: pattern.mli + patternops + * libnames: libnames (qualid, reference) + globnames (global_reference) + * egrammar: egramml + egramcoq + +- New utility files : miscops (cf. misctypes.mli) and + redops (cf genredexpr.mli). + +- Some other directory changes : + * grammar.cma and the source files specific to it are now in grammar/ + * pretty-printing files are now in printing/ + +- Inner-file changes : + + * aconstr is now notation_constr, all constructors for this type + now start with a N instead of a A (e.g. NApp instead of AApp), + and functions about aconstr may have been renamed (e.g. match_aconstr + is now match_notation_constr). + + * occurrences (now in Locus.mli) is now an algebraic type, with + - AllOccurrences instead of all_occurrences_expr = (false,[]) + - (AllOccurrencesBut l) instead of (all_occurrences_expr_but l) = (false,l) + - NoOccurrences instead of no_occurrences_expr = (true,[]) + - (OnlyOccurrences l) instead of (no_occurrences_expr_but l) = (true,l) + + * move_location (now in Misctypes) has two new constructors + MoveFirst and MoveLast replacing (MoveToEnd false) and (MoveToEnd true) + +- API of pretyping.ml and constrintern.ml has been made more uniform + * Parametrization of understand_* functions is now made using + "inference flags" + * Functions removed: + - interp_constr_judgment (inline its former body if really needed) + - interp_casted_constr, interp_type: use instead interp_constr with + expected_type set to OfType or to IsType + - interp_gen: use any of interp_constr, interp_casted_constr, interp_type + - interp_open_constr_patvar + - interp_context: use interp_context_evars (with a "evar_map ref") and + call solve_remaining_evars afterwards with a failing flag + (e.g. all_and_fail_flags) + - understand_type, understand_gen: use understand with appropriate + parameters + * Change of semantics: + - Functions interp_*_evars_impls have a different interface and do + not any longer check resolution of evars by default; use + check_evars_are_solved explicitly to check that evars are solved. + See also the corresponding commit log. + +- Tactics API: new_induct -> induction; new_destruct -> destruct; + letin_pat_tac do not accept a type anymore + +- New file find_subterm.ml for gathering former functions + `subst_closed_term_occ_modulo`, `subst_closed_term_occ_decl` (which now + take and outputs also an `evar_map`), and + `subst_closed_term_occ_modulo`, `subst_closed_term_occ_decl_modulo` (now + renamed into `replace_term_occ_modulo` and + `replace_term_occ_decl_modulo`). + +- API of Inductiveops made more uniform (see commit log or file itself). + +- API of intros_pattern style tactic changed; "s" is dropped in + "intros_pattern" and "intros_patterns" is not anymore behaving like + tactic "intros" on the empty list. + +- API of cut tactics changed: for instance, cut_intro should be replaced by + "assert_after Anonymous" + +- All functions taking an env and a sigma (or an evdref) now takes the + env first. + +## Changes between Coq 8.3 and Coq 8.4 + +- Functions in unification.ml have now the evar_map coming just after the env + +- Removal of Tacinterp.constr_of_id + +Use instead either global_reference or construct_reference in constrintern.ml. + +- Optimizing calls to Evd functions + +Evars are split into defined evars and undefined evars; for +efficiency, when an evar is known to be undefined, it is preferable to +use specific functions about undefined evars since these ones are +generally fewer than the defined ones. + +- Type changes in TACTIC EXTEND rules + +Arguments bound with tactic(_) in TACTIC EXTEND rules are now of type +glob_tactic_expr, instead of glob_tactic_expr * tactic. Only the first +component is kept, the second one can be obtained via +Tacinterp.eval_tactic. + +- ARGUMENT EXTEND + +It is now forbidden to use TYPED simultaneously with {RAW,GLOB}_TYPED +in ARGUMENT EXTEND statements. + +- Renaming of rawconstr to glob_constr + +The "rawconstr" type has been renamed to "glob_constr" for +consistency. The "raw" in everything related to former rawconstr has +been changed to "glob". For more details about the rationale and +scripts to migrate code using Coq's internals, see commits 13743, +13744, 13755, 13756, 13757, 13758, 13761 (by glondu, end of December +2010) in Subversion repository. Contribs have been fixed too, and +commit messages there might also be helpful for migrating. + +## Changes between Coq 8.2 and Coq 8.3 + +### Light cleaning in evaruil.ml + +whd_castappevar is now whd_head_evar +obsolete whd_ise disappears + +### Restructuration of the syntax of binders + +``` +binders_let -> binders +binders_let_fixannot -> binders_fixannot +binder_let -> closed_binder (and now covers only bracketed binders) +binder was already obsolete and has been removed +``` + +### Semantical change of h_induction_destruct + +Warning, the order of the isrec and evar_flag was inconsistent and has +been permuted. Tactic induction_destruct in tactics.ml is unchanged. + +### Internal tactics renamed + +There is no more difference between bindings and ebindings. The +following tactics are therefore renamed + +``` +apply_with_ebindings_gen -> apply_with_bindings_gen +left_with_ebindings -> left_with_bindings +right_with_ebindings -> right_with_bindings +split_with_ebindings -> split_with_bindings +``` + +and the following tactics are removed + + - apply_with_ebindings (use instead apply_with_bindings) + - eapply_with_ebindings (use instead eapply_with_bindings) + +### Obsolete functions in typing.ml + +For mtype_of, msort_of, mcheck, now use type_of, sort_of, check + +### Renaming functions renamed + +``` +concrete_name -> compute_displayed_name_in +concrete_let_name -> compute_displayed_let_name_in +rename_rename_bound_var -> rename_bound_vars_as_displayed +lookup_name_as_renamed -> lookup_name_as_displayed +next_global_ident_away true -> next_ident_away_in_goal +next_global_ident_away false -> next_global_ident_away +``` + +### Cleaning in commmand.ml + +Functions about starting/ending a lemma are in lemmas.ml +Functions about inductive schemes are in indschemes.ml + +Functions renamed: + +``` +declare_one_assumption -> declare_assumption +declare_assumption -> declare_assumptions +Command.syntax_definition -> Metasyntax.add_syntactic_definition +declare_interning_data merged with add_notation_interpretation +compute_interning_datas -> compute_full_internalization_env +implicits_env -> internalization_env +full_implicits_env -> full_internalization_env +build_mutual -> do_mutual_inductive +build_recursive -> do_fixpoint +build_corecursive -> do_cofixpoint +build_induction_scheme -> build_mutual_induction_scheme +build_indrec -> build_induction_scheme +instantiate_type_indrec_scheme -> weaken_sort_scheme +instantiate_indrec_scheme -> modify_sort_scheme +make_case_dep, make_case_nodep -> build_case_analysis_scheme +make_case_gen -> build_case_analysis_scheme_default +``` + +Types: + +decl_notation -> decl_notation option + +### Cleaning in libnames/nametab interfaces + +Functions: + +``` +dirpath_prefix -> pop_dirpath +extract_dirpath_prefix pop_dirpath_n +extend_dirpath -> add_dirpath_suffix +qualid_of_sp -> qualid_of_path +pr_sp -> pr_path +make_short_qualid -> qualid_of_ident +sp_of_syntactic_definition -> path_of_syntactic_definition +sp_of_global -> path_of_global +id_of_global -> basename_of_global +absolute_reference -> global_of_path +locate_syntactic_definition -> locate_syndef +path_of_syntactic_definition -> path_of_syndef +push_syntactic_definition -> push_syndef +``` + +Types: + +section_path -> full_path + +### Cleaning in parsing extensions (commit 12108) + +Many moves and renamings, one new file (Extrawit, that contains wit_tactic). + +### Cleaning in tactical.mli + +``` +tclLAST_HYP -> onLastHyp +tclLAST_DECL -> onLastDecl +tclLAST_NHYPS -> onNLastHypsId +tclNTH_DECL -> onNthDecl +tclNTH_HYP -> onNthHyp +onLastHyp -> onLastHypId +onNLastHyps -> onNLastDecls +onClauses -> onClause +allClauses -> allHypsAndConcl +``` + +and removal of various unused combinators on type "clause" + +## Changes between Coq 8.1 and Coq 8.2 + +### Datatypes + +List of occurrences moved from "int list" to "Termops.occurrences" (an + alias to "bool * int list") +ETIdent renamed to ETName + +### Functions + +``` +Eauto: e_resolve_constr, vernac_e_resolve_constr -> simplest_eapply +Tactics: apply_with_bindings -> apply_with_bindings_wo_evars +Eauto.simplest_apply -> Hiddentac.h_simplest_apply +Evarutil.define_evar_as_arrow -> define_evar_as_product +Old version of Tactics.assert_tac disappears +Tactics.true_cut renamed into Tactics.assert_tac +Constrintern.interp_constrpattern -> intern_constr_pattern +Hipattern.match_with_conjunction is a bit more restrictive +Hipattern.match_with_disjunction is a bit more restrictive +``` + +### Universe names (univ.mli) + + ```ocaml + base_univ -> type0_univ (* alias of Set is the Type hierarchy *) + prop_univ -> type1_univ (* the type of Set in the Type hierarchy *) + neutral_univ -> lower_univ (* semantic alias of Prop in the Type hierarchy *) + is_base_univ -> is_type1_univ + is_empty_univ -> is_lower_univ + ``` + +### Sort names (term.mli) + + ``` + mk_Set -> set_sort + mk_Prop -> prop_sort + type_0 -> type1_sort + ``` + +## Changes between Coq 8.0 and Coq 8.1 + +### Functions + +- Util: option_app -> option_map +- Term: substl_decl -> subst_named_decl +- Lib: library_part -> remove_section_part +- Printer: prterm -> pr_lconstr +- Printer: prterm_env -> pr_lconstr_env +- Ppconstr: pr_sort -> pr_rawsort +- Evd: in_dom, etc got standard ocaml names (i.e. mem, etc) +- Pretyping: + - understand_gen_tcc and understand_gen_ltac merged into understand_ltac + - type_constraints can now say typed by a sort (use OfType to get the + previous behavior) +- Library: import_library -> import_module + +### Constructors + + * Declarations: mind_consnrealargs -> mind_consnrealdecls + * NoRedun -> NoDup + * Cast and RCast have an extra argument: you can recover the previous + behavior by setting the extra argument to "CastConv DEFAULTcast" and + "DEFAULTcast" respectively + * Names: "kernel_name" is now "constant" when argument of Term.Const + * Tacexpr: TacTrueCut and TacForward(false,_,_) merged into new TacAssert + * Tacexpr: TacForward(true,_,_) branched to TacLetTac + +### Modules + + * module Decl_kinds: new interface + * module Bigint: new interface + * module Tacred spawned module Redexpr + * module Symbols -> Notation + * module Coqast, Ast, Esyntax, Termast, and all other modules related to old + syntax are removed + * module Instantiate: integrated to Evd + * module Pretyping now a functor: use Pretyping.Default instead + +### Internal names + +OBJDEF and OBJDEF1 -> CANONICAL-STRUCTURE + +### Tactic extensions + + * printers have an extra parameter which is a constr printer at high precedence + * the tactic printers have an extra arg which is the expected precedence + * level is now a precedence in declare_extra_tactic_pprule + * "interp" functions now of types the actual arg type, not its encapsulation + as a generic_argument + +## Changes between Coq 7.4 and Coq 8.0 + +See files in dev/syntax-v8 + + +## Main changes between Coq 7.4 and Coq 8.0 + +### Changes due to introduction of modules + +#### Kernel + + The module level has no effect on constr except for the structure of +section_path. The type of unique names for constructions (what +section_path served) is now called a kernel name and is defined by + +```ocaml +type uniq_ident = int * string * dir_path (* int may be enough *) +type module_path = + | MPfile of dir_path (* reference to physical module, e.g. file *) + | MPbound of uniq_ident (* reference to a module parameter in a functor *) + | MPself of uniq_ident (* reference to one of the containing module *) + | MPdot of module_path * label +type label = identifier +type kernel_name = module_path * dir_path * label + ^^^^^^^^^^^ ^^^^^^^^ ^^^^^ + | | \ + | | the base name + | \ + / the (true) section path + example: (non empty only inside open sections) + L = (* i.e. some file of logical name L *) + struct + module A = struct Def a = ... end + end + M = (* i.e. some file of logical name M *) + struct + Def t = ... + N = functor (X : sig module T = struct Def b = ... end end) -> struct + module O = struct + Def u = ... + end + Def x := ... .t ... .O.u ... X.T.b ... L.A.a +``` + + and are self-references, X is a bound reference and L is a +reference to a physical module. + + Notice that functor application is not part of a path: it must be +named by a "module M = F(A)" declaration to be used in a kernel +name. + + Notice that Jacek chose a practical approach, making directories not +modules. Another approach could have been to replace the constructor +MPfile by a constant constructor MProot representing the root of the +world. + + Other relevant informations are in kernel/entries.ml (type +module_expr) and kernel/declarations.ml (type module_body and +module_type_body). + +#### Library + +1. tables +[Summaries] - the only change is the special treatment of the +global environmet. + +2. objects +[Libobject] declares persistent objects, given with methods: + + * cache_function specifying how to add the object in the current + scope; + * load_function, specifying what to do when the module + containing the object is loaded; + * open_function, specifying what to do when the module + containing the object is opened (imported); + * classify_function, specyfying what to do with the object, + when the current module (containing the object) is ended. + * subst_function + * export_function, to signal end_section survival + +(Almost) Each of these methods is called with a parameter of type +object_name = section_path * kernel_name +where section_path is the full user name of the object (such as +Coq.Init.Datatypes.Fst) and kernel_name is its substitutive internal +version such as (MPself,[],"Fst") (see above) + + +#### What happens at the end of an interactive module ? + +(or when a file is stored and reloaded from disk) + +All summaries (except Global environment) are reverted to the state +from before the beginning of the module, and: + +1. the objects (again, since last Declaremods.start_module or + Library.start_library) are classified using the classify_function. + To simplify consider only those who returned Substitute _ or Keep _. + +2. If the module is not a functor, the subst_function for each object of + the first group is called with the substitution + [MPself "" |-> MPfile "Coq.Init.Datatypes"]. + Then the load_function is called for substituted objects and the + "keep" object. + (If the module is a library the substitution is done at reloading). + +3. The objects which returned substitute are stored in the modtab + together with the self ident of the module, and functor argument + names if the module was a functor. + + They will be used (substituted and loaded) when a command like + Module M := F(N) or + Module Z := N + is evaluated + + +#### The difference between "substitute" and "keep" objects + +1. The "keep" objects can _only_ reference other objects by section_paths +and qualids. They do not need the substitution function. + +They will work after end_module (or reloading a compiled library), +because these operations do not change section_path's + +They will obviously not work after Module Z:=N. + +These would typically be grammar rules, pretty printing rules etc. + + + +2. The "substitute" objects can _only_ reference objects by +kernel_names. They must have a valid subst_function. + +They will work after end_module _and_ after Module Z:=N or +Module Z:=F(M). + + + +Other kinds of objects: + +3. "Dispose" - objects which do not survive end_module + As a consequence, objects which reference other objects sometimes + by kernel_names and sometimes by section_path must be of this kind... + +4. "Anticipate" - objects which must be treated individually by + end_module (typically "REQUIRE" objects) + + + +#### Writing subst_thing functions + +The subst_thing shoud not copy the thing if it hasn't actually +changed. There are some cool emacs macros in dev/objects.el +to help writing subst functions this way quickly and without errors. +Also there are *_smartmap functions in Util. + +The subst_thing functions are already written for many types, +including constr (Term.subst_mps), +global_reference (Libnames.subst_global), +rawconstr (Rawterm.subst_raw) etc + +They are all (apart from constr, for now) written in the non-copying +way. + + +#### Nametab + +Nametab has been made more uniform. For every kind of thing there is +only one "push" function and one "locate" function. + + +#### Lib + +library_segment is now a list of object_name * library_item, where +object_name = section_path * kernel_name (see above) + +New items have been added for open modules and module types + + +#### Declaremods + +Functions to declare interactive and noninteractive modules and module +types. + + +#### Library + +Uses Declaremods to actually communicate with Global and to register +objects. + + +### Other changes + +Internal representation of tactics bindings has changed (see type +Rawterm.substitution). + +New parsing model for tactics and vernacular commands + + - Introduction of a dedicated type for tactic expressions + (Tacexpr.raw_tactic_expr) + - Introduction of a dedicated type for vernac expressions + (Vernacexpr.vernac_expr) + - Declaration of new vernacular parsing rules by a new camlp4 macro + GRAMMAR COMMAND EXTEND ... END to be used in ML files + - Declaration of new tactics parsing/printing rules by a new camlp4 macro + TACTIC EXTEND ... END to be used in ML files + +New organisation of THENS: + +- tclTHENS tac tacs : tacs is now an array +- tclTHENSFIRSTn tac1 tacs tac2 : + apply tac1 then, apply the array tacs on the first n subgoals and + tac2 on the remaining subgoals (previously tclTHENST) +- tclTHENSLASTn tac1 tac2 tacs : + apply tac1 then, apply tac2 on the first subgoals and apply the array + tacs on the last n subgoals +- tclTHENFIRSTn tac1 tacs = tclTHENSFIRSTn tac1 tacs tclIDTAC (prev. tclTHENSI) +- tclTHENLASTn tac1 tacs = tclTHENSLASTn tac1 tclIDTAC tacs +- tclTHENFIRST tac1 tac2 = tclTHENFIRSTn tac1 [|tac2|] +- tclTHENLAST tac1 tac2 = tclTHENLASTn tac1 [|tac2|] (previously tclTHENL) +- tclTHENS tac1 tacs = tclTHENSFIRSTn tac1 tacs (fun _ -> error "wrong number") +- tclTHENSV same as tclTHENS but with an array +- tclTHENSi : no longer available + +Proof_type: subproof field in type proof_tree glued with the ref field + +Tacmach: no more echo from functions of module Refiner + +Files plugins/*/g_*.ml4 take the place of files plugins/*/*.v. + +Files parsing/{vernac,tac}extend.ml{4,i} implements TACTIC EXTEND andd + VERNAC COMMAND EXTEND macros + +File syntax/PPTactic.v moved to parsing/pptactic.ml + +Tactics about False and not now in tactics/contradiction.ml + +Tactics depending on Init now tactics/*.ml4 (no longer in tactics/*.v) + +File tacinterp.ml moved from proofs to directory tactics + + +## Changes between Coq 7.1 and Coq 7.2 + +The core of Coq (kernel) has meen minimized with the following effects: + +- kernel/term.ml split into kernel/term.ml, pretyping/termops.ml +- kernel/reduction.ml split into kernel/reduction.ml, pretyping/reductionops.ml +- kernel/names.ml split into kernel/names.ml, library/nameops.ml +- kernel/inductive.ml split into kernel/inductive.ml, pretyping/inductiveops.ml + +the prefixes "Is" ans "IsMut" have been dropped from kind_of_term constructors, +e.g. IsRel is now Rel, IsMutCase is now Case, etc. diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt deleted file mode 100644 index 3de938d7..00000000 --- a/dev/doc/changes.txt +++ /dev/null @@ -1,1095 +0,0 @@ -========================================= -= CHANGES BETWEEN COQ V8.5 AND COQ V8.6 = -========================================= - -** Parsing ** - -Pcoq.parsable now takes an extra optional filename argument so as to -bind locations to a file name when relevant. - -** Files ** - -To avoid clashes with OCaml's compiler libs, the following files were renamed: -kernel/closure.ml{,i} -> kernel/cClosure.ml{,i} -lib/errors.ml{,i} -> lib/cErrors.ml{,i} -toplevel/cerror.ml{,i} -> toplevel/explainErr.mli{,i} - -All IDE-specific files, including the XML protocol have been moved to ide/ - -** Reduction functions ** - -In closure.ml, we introduced the more precise reduction flags fMATCH, fFIX, -fCOFIX. - -We renamed the following functions: - -Closure.betadeltaiota -> Closure.all -Closure.betadeltaiotanolet -> Closure.allnolet -Reductionops.beta -> Closure.beta -Reductionops.zeta -> Closure.zeta -Reductionops.betaiota -> Closure.betaiota -Reductionops.betaiotazeta -> Closure.betaiotazeta -Reductionops.delta -> Closure.delta -Reductionops.betalet -> Closure.betazeta -Reductionops.betadelta -> Closure.betadeltazeta -Reductionops.betadeltaiota -> Closure.all -Reductionops.betadeltaiotanolet -> Closure.allnolet -Closure.no_red -> Closure.nored -Reductionops.nored -> Closure.nored -Reductionops.nf_betadeltaiota -> Reductionops.nf_all -Reductionops.whd_betadelta -> Reductionops.whd_betadeltazeta -Reductionops.whd_betadeltaiota -> Reductionops.whd_all -Reductionops.whd_betadeltaiota_nolet -> Reductionops.whd_allnolet -Reductionops.whd_betadelta_stack -> Reductionops.whd_betadeltazeta_stack -Reductionops.whd_betadeltaiota_stack -> Reductionops.whd_all_stack -Reductionops.whd_betadeltaiota_nolet_stack -> Reductionops.whd_allnolet_stack -Reductionops.whd_betadelta_state -> Reductionops.whd_betadeltazeta_state -Reductionops.whd_betadeltaiota_state -> Reductionops.whd_all_state -Reductionops.whd_betadeltaiota_nolet_state -> Reductionops.whd_allnolet_state -Reductionops.whd_eta -> Reductionops.shrink_eta -Tacmach.pf_whd_betadeltaiota -> Tacmach.pf_whd_all -Tacmach.New.pf_whd_betadeltaiota -> Tacmach.New.pf_whd_all - -And removed the following ones: - -Reductionops.whd_betaetalet -Reductionops.whd_betaetalet_stack -Reductionops.whd_betaetalet_state -Reductionops.whd_betadeltaeta_stack -Reductionops.whd_betadeltaeta_state -Reductionops.whd_betadeltaeta -Reductionops.whd_betadeltaiotaeta_stack -Reductionops.whd_betadeltaiotaeta_state -Reductionops.whd_betadeltaiotaeta - -In intf/genredexpr.mli, fIota was replaced by FMatch, FFix and -FCofix. Similarly, rIota was replaced by rMatch, rFix and rCofix. - -** Notation_ops ** - -Use Glob_ops.glob_constr_eq instead of Notation_ops.eq_glob_constr. - -** Logging and Pretty Printing: ** - -* Printing functions have been removed from `Pp.mli`, which is now a - purely pretty-printing interface. Functions affected are: - -```` ocaml -val pp : std_ppcmds -> unit -val ppnl : std_ppcmds -> unit -val pperr : std_ppcmds -> unit -val pperrnl : std_ppcmds -> unit -val pperr_flush : unit -> unit -val pp_flush : unit -> unit -val flush_all : unit -> unit -val msg : std_ppcmds -> unit -val msgnl : std_ppcmds -> unit -val msgerr : std_ppcmds -> unit -val msgerrnl : std_ppcmds -> unit -val message : string -> unit -```` - - which are no more available. Users of `Pp.pp msg` should now use the - proper `Feedback.msg_*` function. Clients also have no control over - flushing, the back end takes care of it. - - Also, the `msg_*` functions now take an optional `?loc` parameter - for relaying location to the client. - -* Feedback related functions and definitions have been moved to the - `Feedback` module. `message_level` has been renamed to - level. Functions moved from Pp to Feedback are: - -```` ocaml -val set_logger : logger -> unit -val std_logger : logger -val emacs_logger : logger -val feedback_logger : logger -```` - -* Changes in the Feedback format/Protocol. - -- The `Message` feedback type now carries an optional location, the main - payload is encoded using the richpp document format. - -- The `ErrorMsg` feedback type is thus unified now with `Message` at - level `Error`. - -* We now provide several loggers, `log_via_feedback` is removed in - favor of `set_logger feedback_logger`. Output functions are: - -```` ocaml -val with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b -val msg_error : ?loc:Loc.t -> Pp.std_ppcmds -> unit -val msg_warning : ?loc:Loc.t -> Pp.std_ppcmds -> unit -val msg_notice : ?loc:Loc.t -> Pp.std_ppcmds -> unit -val msg_info : ?loc:Loc.t -> Pp.std_ppcmds -> unit -val msg_debug : ?loc:Loc.t -> Pp.std_ppcmds -> unit -```` - - with the `msg_*` functions being just an alias for `logger $Level`. - -* The main feedback functions are: - -```` ocaml -val set_feeder : (feedback -> unit) -> unit -val feedback : ?id:edit_or_state_id -> ?route:route_id -> feedback_content -> unit -val set_id_for_feedback : ?route:route_id -> edit_or_state_id -> unit -```` - Note that `feedback` doesn't take two parameters anymore. After - refactoring the following function has been removed: - -```` ocaml -val get_id_for_feedback : unit -> edit_or_state_id * route_id -```` - -** Kernel API changes ** - -- The interface of the Context module was changed. - Related types and functions were put in separate submodules. - The mapping from old identifiers to new identifiers is the following: - - Context.named_declaration ---> Context.Named.Declaration.t - Context.named_list_declaration ---> Context.NamedList.Declaration.t - Context.rel_declaration ---> Context.Rel.Declaration.t - Context.map_named_declaration ---> Context.Named.Declaration.map_constr - Context.map_named_list_declaration ---> Context.NamedList.Declaration.map - Context.map_rel_declaration ---> Context.Rel.Declaration.map_constr - Context.fold_named_declaration ---> Context.Named.Declaration.fold - Context.fold_rel_declaration ---> Context.Rel.Declaration.fold - Context.exists_named_declaration ---> Context.Named.Declaration.exists - Context.exists_rel_declaration ---> Context.Rel.Declaration.exists - Context.for_all_named_declaration ---> Context.Named.Declaration.for_all - Context.for_all_rel_declaration ---> Context.Rel.Declaration.for_all - Context.eq_named_declaration ---> Context.Named.Declaration.equal - Context.eq_rel_declaration ---> Context.Rel.Declaration.equal - Context.named_context ---> Context.Named.t - Context.named_list_context ---> Context.NamedList.t - Context.rel_context ---> Context.Rel.t - Context.empty_named_context ---> Context.Named.empty - Context.add_named_decl ---> Context.Named.add - Context.vars_of_named_context ---> Context.Named.to_vars - Context.lookup_named ---> Context.Named.lookup - Context.named_context_length ---> Context.Named.length - Context.named_context_equal ---> Context.Named.equal - Context.fold_named_context ---> Context.Named.fold_outside - Context.fold_named_list_context ---> Context.NamedList.fold - Context.fold_named_context_reverse ---> Context.Named.fold_inside - Context.instance_from_named_context ---> Context.Named.to_instance - Context.extended_rel_list ---> Context.Rel.to_extended_list - Context.extended_rel_vect ---> Context.Rel.to_extended_vect - Context.fold_rel_context ---> Context.Rel.fold_outside - Context.fold_rel_context_reverse ---> Context.Rel.fold_inside - Context.map_rel_context ---> Context.Rel.map_constr - Context.map_named_context ---> Context.Named.map_constr - Context.iter_rel_context ---> Context.Rel.iter - Context.iter_named_context ---> Context.Named.iter - Context.empty_rel_context ---> Context.Rel.empty - Context.add_rel_decl ---> Context.Rel.add - Context.lookup_rel ---> Context.Rel.lookup - Context.rel_context_length ---> Context.Rel.length - Context.rel_context_nhyps ---> Context.Rel.nhyps - Context.rel_context_tags ---> Context.Rel.to_tags - -- Originally, rel-context was represented as: - - Context.rel_context = Names.Name.t * Constr.t option * Constr.t - - Now it is represented as: - - Context.Rel.Declaration.t = LocalAssum of Names.Name.t * Constr.t - | LocalDef of Names.Name.t * Constr.t * Constr.t - -- Originally, named-context was represented as: - - Context.named_context = Names.Id.t * Constr.t option * Constr.t - - Now it is represented as: - - Context.Named.Declaration.t = LocalAssum of Names.Id.t * Constr.t - | LocalDef of Names.Id.t * Constr.t * Constr.t - -- The various EXTEND macros do not handle specially the Coq-defined entries - anymore. Instead, they just output a name that have to exist in the scope - of the ML code. The parsing rules (VERNAC) ARGUMENT EXTEND will look for - variables "$name" of type Gram.entry, while the parsing rules of - (VERNAC COMMAND | TACTIC) EXTEND, as well as the various TYPED AS clauses will - look for variables "wit_$name" of type Genarg.genarg_type. The small DSL - for constructing compound entries still works over this scheme. Note that in - the case of (VERNAC) ARGUMENT EXTEND, the name of the argument entry is bound - in the parsing rules, so beware of recursive calls. - - For example, to get "wit_constr" you must "open Constrarg" at the top of the file. - -- Evarutil was split in two parts. The new Evardefine file exposes functions -define_evar_* mostly used internally in the unification engine. - -- The Refine module was move out of Proofview. - - Proofview.Refine.* ---> Refine.* - -- A statically monotonous evarmap type was introduced in Sigma. Not all the API - has been converted, so that the user may want to use compatibility functions - Sigma.to_evar_map and Sigma.Unsafe.of_evar_map or Sigma.Unsafe.of_pair when - needed. Code can be straightforwardly adapted in the following way: - - let (sigma, x1) = ... in - ... - let (sigma, xn) = ... in - (sigma, ans) - - should be turned into: - - open Sigma.Notations - - let Sigma (x1, sigma, p1) = ... in - ... - let Sigma (xn, sigma, pn) = ... in - Sigma (ans, sigma, p1 +> ... +> pn) - - Examples of `Sigma.Unsafe.of_evar_map` include: - - Evarutil.new_evar env (Tacmach.project goal) ty ----> Evarutil.new_evar env (Sigma.Unsafe.of_evar_map (Tacmach.project goal)) ty - -- The Proofview.Goal.*enter family of functions now takes a polymorphic - continuation given as a record as an argument. - - Proofview.Goal.enter begin fun gl -> ... end - - should be turned into - - open Proofview.Notations - - Proofview.Goal.enter { enter = begin fun gl -> ... end } - -- `Tacexpr.TacDynamic(Loc.dummy_loc, Pretyping.constr_in c)` ---> `Tacinterp.Value.of_constr c` -- `Vernacexpr.HintsResolveEntry(priority, poly, hnf, path, atom)` ---> `Vernacexpr.HintsResolveEntry(Vernacexpr.({hint_priority = priority; hint_pattern = None}), poly, hnf, path, atom)` -- `Pretyping.Termops.mem_named_context` ---> `Engine.Termops.mem_named_context_val` - (`Global.named_context` ---> `Global.named_context_val`) - (`Context.Named.lookup` ---> `Environ.lookup_named_val`) - -** Search API ** - -The main search functions now take a function iterating over the -results. This allows for clients to use streaming or more economic -printing. - -========================================= -= CHANGES BETWEEN COQ V8.4 AND COQ V8.5 = -========================================= - -** Refactoring : more mli interfaces and simpler grammar.cma ** - -- A new directory intf/ now contains mli-only interfaces : - - Constrexpr : definition of constr_expr, was in Topconstr - Decl_kinds : now contains binding_kind = Explicit | Implicit - Evar_kinds : type Evar_kinds.t was previously Evd.hole_kind - Extend : was parsing/extend.mli - Genredexpr : regroup Glob_term.red_expr_gen and Tacexpr.glob_red_flag - Glob_term : definition of glob_constr - Locus : definition of occurrences and stuff about clauses - Misctypes : intro_pattern_expr, glob_sort, cast_type, or_var, ... - Notation_term : contains notation_constr, was Topconstr.aconstr - Pattern : contains constr_pattern - Tacexpr : was tactics/tacexpr.ml - Vernacexpr : was toplevel/vernacexpr.ml - -- Many files have been divided : - - vernacexpr: vernacexpr.mli + Locality - decl_kinds: decl_kinds.mli + Kindops - evd: evar_kinds.mli + evd - tacexpr: tacexpr.mli + tacops - glob_term: glob_term.mli + glob_ops + genredexpr.mli + redops - topconstr: constrexpr.mli + constrexpr_ops - + notation_expr.mli + notation_ops + topconstr - pattern: pattern.mli + patternops - libnames: libnames (qualid, reference) + globnames (global_reference) - egrammar: egramml + egramcoq - -- New utility files : miscops (cf. misctypes.mli) and - redops (cf genredexpr.mli). - -- Some other directory changes : - * grammar.cma and the source files specific to it are now in grammar/ - * pretty-printing files are now in printing/ - -- Inner-file changes : - - * aconstr is now notation_constr, all constructors for this type - now start with a N instead of a A (e.g. NApp instead of AApp), - and functions about aconstr may have been renamed (e.g. match_aconstr - is now match_notation_constr). - - * occurrences (now in Locus.mli) is now an algebraic type, with - - AllOccurrences instead of all_occurrences_expr = (false,[]) - - (AllOccurrencesBut l) instead of (all_occurrences_expr_but l) = (false,l) - - NoOccurrences instead of no_occurrences_expr = (true,[]) - - (OnlyOccurrences l) instead of (no_occurrences_expr_but l) = (true,l) - - * move_location (now in Misctypes) has two new constructors - MoveFirst and MoveLast replacing (MoveToEnd false) and (MoveToEnd true) - -- API of pretyping.ml and constrintern.ml has been made more uniform - * Parametrization of understand_* functions is now made using - "inference flags" - * Functions removed: - - interp_constr_judgment (inline its former body if really needed) - - interp_casted_constr, interp_type: use instead interp_constr with - expected_type set to OfType or to IsType - - interp_gen: use any of interp_constr, interp_casted_constr, interp_type - - interp_open_constr_patvar - - interp_context: use interp_context_evars (with a "evar_map ref") and - call solve_remaining_evars afterwards with a failing flag - (e.g. all_and_fail_flags) - - understand_type, understand_gen: use understand with appropriate - parameters - * Change of semantics: - - Functions interp_*_evars_impls have a different interface and do - not any longer check resolution of evars by default; use - check_evars_are_solved explicitly to check that evars are solved. - See also the corresponding commit log. - -- Tactics API: new_induct -> induction; new_destruct -> destruct; - letin_pat_tac do not accept a type anymore - -- New file find_subterm.ml for gathering former functions - subst_closed_term_occ_modulo, subst_closed_term_occ_decl (which now - take and outputs also an evar_map), and - subst_closed_term_occ_modulo, subst_closed_term_occ_decl_modulo (now - renamed into replace_term_occ_modulo and - replace_term_occ_decl_modulo). - -- API of Inductiveops made more uniform (see commit log or file itself). - -- API of intros_pattern style tactic changed; "s" is dropped in - "intros_pattern" and "intros_patterns" is not anymore behaving like - tactic "intros" on the empty list. - -- API of cut tactics changed: for instance, cut_intro should be replaced by - "assert_after Anonymous" - -- All functions taking an env and a sigma (or an evdref) now takes the - env first. - -========================================= -= CHANGES BETWEEN COQ V8.3 AND COQ V8.4 = -========================================= - -** Functions in unification.ml have now the evar_map coming just after the env - -** Removal of Tacinterp.constr_of_id ** - -Use instead either global_reference or construct_reference in constrintern.ml. - -** Optimizing calls to Evd functions ** - -Evars are split into defined evars and undefined evars; for -efficiency, when an evar is known to be undefined, it is preferable to -use specific functions about undefined evars since these ones are -generally fewer than the defined ones. - -** Type changes in TACTIC EXTEND rules ** - -Arguments bound with tactic(_) in TACTIC EXTEND rules are now of type -glob_tactic_expr, instead of glob_tactic_expr * tactic. Only the first -component is kept, the second one can be obtained via -Tacinterp.eval_tactic. - -** ARGUMENT EXTEND ** - -It is now forbidden to use TYPED simultaneously with {RAW,GLOB}_TYPED -in ARGUMENT EXTEND statements. - -** Renaming of rawconstr to glob_constr ** - -The "rawconstr" type has been renamed to "glob_constr" for -consistency. The "raw" in everything related to former rawconstr has -been changed to "glob". For more details about the rationale and -scripts to migrate code using Coq's internals, see commits 13743, -13744, 13755, 13756, 13757, 13758, 13761 (by glondu, end of December -2010) in Subversion repository. Contribs have been fixed too, and -commit messages there might also be helpful for migrating. - -========================================= -= CHANGES BETWEEN COQ V8.2 AND COQ V8.3 = -========================================= - -** Light cleaning in evarutil.ml ** - -whd_castappevar is now whd_head_evar -obsolete whd_ise disappears - -** Restructuration of the syntax of binders ** - -binders_let -> binders -binders_let_fixannot -> binders_fixannot -binder_let -> closed_binder (and now covers only bracketed binders) -binder was already obsolete and has been removed - -** Semantical change of h_induction_destruct ** - -Warning, the order of the isrec and evar_flag was inconsistent and has -been permuted. Tactic induction_destruct in tactics.ml is unchanged. - -** Internal tactics renamed - -There is no more difference between bindings and ebindings. The -following tactics are therefore renamed - -apply_with_ebindings_gen -> apply_with_bindings_gen -left_with_ebindings -> left_with_bindings -right_with_ebindings -> right_with_bindings -split_with_ebindings -> split_with_bindings - -and the following tactics are removed - -apply_with_ebindings (use instead apply_with_bindings) -eapply_with_ebindings (use instead eapply_with_bindings) - -** Obsolete functions in typing.ml - -For mtype_of, msort_of, mcheck, now use type_of, sort_of, check - -** Renaming functions renamed - -concrete_name -> compute_displayed_name_in -concrete_let_name -> compute_displayed_let_name_in -rename_rename_bound_var -> rename_bound_vars_as_displayed -lookup_name_as_renamed -> lookup_name_as_displayed -next_global_ident_away true -> next_ident_away_in_goal -next_global_ident_away false -> next_global_ident_away - -** Cleaning in commmand.ml - -Functions about starting/ending a lemma are in lemmas.ml -Functions about inductive schemes are in indschemes.ml - -Functions renamed: - -declare_one_assumption -> declare_assumption -declare_assumption -> declare_assumptions -Command.syntax_definition -> Metasyntax.add_syntactic_definition -declare_interning_data merged with add_notation_interpretation -compute_interning_datas -> compute_full_internalization_env -implicits_env -> internalization_env -full_implicits_env -> full_internalization_env -build_mutual -> do_mutual_inductive -build_recursive -> do_fixpoint -build_corecursive -> do_cofixpoint -build_induction_scheme -> build_mutual_induction_scheme -build_indrec -> build_induction_scheme -instantiate_type_indrec_scheme -> weaken_sort_scheme -instantiate_indrec_scheme -> modify_sort_scheme -make_case_dep, make_case_nodep -> build_case_analysis_scheme -make_case_gen -> build_case_analysis_scheme_default - -Types: - -decl_notation -> decl_notation option - -** Cleaning in libnames/nametab interfaces - -Functions: - -dirpath_prefix -> pop_dirpath -extract_dirpath_prefix pop_dirpath_n -extend_dirpath -> add_dirpath_suffix -qualid_of_sp -> qualid_of_path -pr_sp -> pr_path -make_short_qualid -> qualid_of_ident -sp_of_syntactic_definition -> path_of_syntactic_definition -sp_of_global -> path_of_global -id_of_global -> basename_of_global -absolute_reference -> global_of_path -locate_syntactic_definition -> locate_syndef -path_of_syntactic_definition -> path_of_syndef -push_syntactic_definition -> push_syndef - -Types: - -section_path -> full_path - -** Cleaning in parsing extensions (commit 12108) - -Many moves and renamings, one new file (Extrawit, that contains wit_tactic). - -** Cleaning in tactical.mli - -tclLAST_HYP -> onLastHyp -tclLAST_DECL -> onLastDecl -tclLAST_NHYPS -> onNLastHypsId -tclNTH_DECL -> onNthDecl -tclNTH_HYP -> onNthHyp -onLastHyp -> onLastHypId -onNLastHyps -> onNLastDecls -onClauses -> onClause -allClauses -> allHypsAndConcl - -+ removal of various unused combinators on type "clause" - -========================================= -= CHANGES BETWEEN COQ V8.1 AND COQ V8.2 = -========================================= - -A few differences in Coq ML interfaces between Coq V8.1 and V8.2 -================================================================ - -** Datatypes - -List of occurrences moved from "int list" to "Termops.occurrences" (an - alias to "bool * int list") -ETIdent renamed to ETName - -** Functions - -Eauto: e_resolve_constr, vernac_e_resolve_constr -> simplest_eapply -Tactics: apply_with_bindings -> apply_with_bindings_wo_evars -Eauto.simplest_apply -> Hiddentac.h_simplest_apply -Evarutil.define_evar_as_arrow -> define_evar_as_product -Old version of Tactics.assert_tac disappears -Tactics.true_cut renamed into Tactics.assert_tac -Constrintern.interp_constrpattern -> intern_constr_pattern -Hipattern.match_with_conjunction is a bit more restrictive -Hipattern.match_with_disjunction is a bit more restrictive - -** Universe names (univ.mli) - - base_univ -> type0_univ (* alias of Set is the Type hierarchy *) - prop_univ -> type1_univ (* the type of Set in the Type hierarchy *) - neutral_univ -> lower_univ (* semantic alias of Prop in the Type hierarchy *) - is_base_univ -> is_type1_univ - is_empty_univ -> is_lower_univ - -** Sort names (term.mli) - - mk_Set -> set_sort - mk_Prop -> prop_sort - type_0 -> type1_sort - -========================================= -= CHANGES BETWEEN COQ V8.0 AND COQ V8.1 = -========================================= - -A few differences in Coq ML interfaces between Coq V8.0 and V8.1 -================================================================ - -** Functions - -Util: option_app -> option_map -Term: substl_decl -> subst_named_decl -Lib: library_part -> remove_section_part -Printer: prterm -> pr_lconstr -Printer: prterm_env -> pr_lconstr_env -Ppconstr: pr_sort -> pr_rawsort -Evd: in_dom, etc got standard ocaml names (i.e. mem, etc) -Pretyping: - - understand_gen_tcc and understand_gen_ltac merged into understand_ltac - - type_constraints can now say typed by a sort (use OfType to get the - previous behavior) -Library: import_library -> import_module - -** Constructors - -Declarations: mind_consnrealargs -> mind_consnrealdecls -NoRedun -> NoDup -Cast and RCast have an extra argument: you can recover the previous - behavior by setting the extra argument to "CastConv DEFAULTcast" and - "DEFAULTcast" respectively -Names: "kernel_name" is now "constant" when argument of Term.Const -Tacexpr: TacTrueCut and TacForward(false,_,_) merged into new TacAssert -Tacexpr: TacForward(true,_,_) branched to TacLetTac - -** Modules - -module Decl_kinds: new interface -module Bigint: new interface -module Tacred spawned module Redexpr -module Symbols -> Notation -module Coqast, Ast, Esyntax, Termast, and all other modules related to old - syntax are removed -module Instantiate: integrated to Evd -module Pretyping now a functor: use Pretyping.Default instead - -** Internal names - -OBJDEF and OBJDEF1 -> CANONICAL-STRUCTURE - -** Tactic extensions - -- printers have an extra parameter which is a constr printer at high precedence -- the tactic printers have an extra arg which is the expected precedence -- level is now a precedence in declare_extra_tactic_pprule -- "interp" functions now of types the actual arg type, not its encapsulation - as a generic_argument - -========================================= -= CHANGES BETWEEN COQ V7.4 AND COQ V8.0 = -========================================= - -See files in dev/syntax-v8 - - -============================================== -= MAIN CHANGES BETWEEN COQ V7.3 AND COQ V7.4 = -============================================== - -CHANGES DUE TO INTRODUCTION OF MODULES -====================================== - -1.Kernel --------- - - The module level has no effect on constr except for the structure of -section_path. The type of unique names for constructions (what -section_path served) is now called a kernel name and is defined by - -type uniq_ident = int * string * dir_path (* int may be enough *) -type module_path = - | MPfile of dir_path (* reference to physical module, e.g. file *) - | MPbound of uniq_ident (* reference to a module parameter in a functor *) - | MPself of uniq_ident (* reference to one of the containing module *) - | MPdot of module_path * label -type label = identifier -type kernel_name = module_path * dir_path * label - ^^^^^^^^^^^ ^^^^^^^^ ^^^^^ - | | \ - | | the base name - | \ - / the (true) section path - example: (non empty only inside open sections) - L = (* i.e. some file of logical name L *) - struct - module A = struct Def a = ... end - end - M = (* i.e. some file of logical name M *) - struct - Def t = ... - N = functor (X : sig module T = struct Def b = ... end end) -> struct - module O = struct - Def u = ... - end - Def x := ... .t ... .O.u ... X.T.b ... L.A.a - - and are self-references, X is a bound reference and L is a -reference to a physical module. - - Notice that functor application is not part of a path: it must be -named by a "module M = F(A)" declaration to be used in a kernel -name. - - Notice that Jacek chose a practical approach, making directories not -modules. Another approach could have been to replace the constructor -MPfile by a constant constructor MProot representing the root of the -world. - - Other relevant informations are in kernel/entries.ml (type -module_expr) and kernel/declarations.ml (type module_body and -module_type_body). - -2. Library ----------- - -i) tables -[Summaries] - the only change is the special treatment of the -global environmet. - -ii) objects -[Libobject] declares persistent objects, given with methods: - - * cache_function specifying how to add the object in the current - scope; - * load_function, specifying what to do when the module - containing the object is loaded; - * open_function, specifying what to do when the module - containing the object is opened (imported); - * classify_function, specyfying what to do with the object, - when the current module (containing the object) is ended. - * subst_function - * export_function, to signal end_section survival - -(Almost) Each of these methods is called with a parameter of type -object_name = section_path * kernel_name -where section_path is the full user name of the object (such as -Coq.Init.Datatypes.Fst) and kernel_name is its substitutive internal -version such as (MPself,[],"Fst") (see above) - - -What happens at the end of an interactive module ? -================================================== -(or when a file is stored and reloaded from disk) - -All summaries (except Global environment) are reverted to the state -from before the beginning of the module, and: - -a) the objects (again, since last Declaremods.start_module or - Library.start_library) are classified using the classify_function. - To simplify consider only those who returned Substitute _ or Keep _. - -b) If the module is not a functor, the subst_function for each object of - the first group is called with the substitution - [MPself "" |-> MPfile "Coq.Init.Datatypes"]. - Then the load_function is called for substituted objects and the - "keep" object. - (If the module is a library the substitution is done at reloading). - -c) The objects which returned substitute are stored in the modtab - together with the self ident of the module, and functor argument - names if the module was a functor. - - They will be used (substituted and loaded) when a command like - Module M := F(N) or - Module Z := N - is evaluated - - -The difference between "substitute" and "keep" objects -======================================================== -i) The "keep" objects can _only_ reference other objects by section_paths -and qualids. They do not need the substitution function. - -They will work after end_module (or reloading a compiled library), -because these operations do not change section_path's - -They will obviously not work after Module Z:=N. - -These would typically be grammar rules, pretty printing rules etc. - - - -ii) The "substitute" objects can _only_ reference objects by -kernel_names. They must have a valid subst_function. - -They will work after end_module _and_ after Module Z:=N or -Module Z:=F(M). - - - -Other kinds of objects: -iii) "Dispose" - objects which do not survive end_module - As a consequence, objects which reference other objects sometimes - by kernel_names and sometimes by section_path must be of this kind... - -iv) "Anticipate" - objects which must be treated individually by - end_module (typically "REQUIRE" objects) - - - -Writing subst_thing functions -============================= -The subst_thing shoud not copy the thing if it hasn't actually -changed. There are some cool emacs macros in dev/objects.el -to help writing subst functions this way quickly and without errors. -Also there are *_smartmap functions in Util. - -The subst_thing functions are already written for many types, -including constr (Term.subst_mps), -global_reference (Libnames.subst_global), -rawconstr (Rawterm.subst_raw) etc - -They are all (apart from constr, for now) written in the non-copying -way. - - -Nametab -======= - -Nametab has been made more uniform. For every kind of thing there is -only one "push" function and one "locate" function. - - -Lib -=== - -library_segment is now a list of object_name * library_item, where -object_name = section_path * kernel_name (see above) - -New items have been added for open modules and module types - - -Declaremods -========== -Functions to declare interactive and noninteractive modules and module -types. - - -Library -======= -Uses Declaremods to actually communicate with Global and to register -objects. - - -OTHER CHANGES -============= - -Internal representation of tactics bindings has changed (see type -Rawterm.substitution). - -New parsing model for tactics and vernacular commands - - - Introduction of a dedicated type for tactic expressions - (Tacexpr.raw_tactic_expr) - - Introduction of a dedicated type for vernac expressions - (Vernacexpr.vernac_expr) - - Declaration of new vernacular parsing rules by a new camlp4 macro - GRAMMAR COMMAND EXTEND ... END to be used in ML files - - Declaration of new tactics parsing/printing rules by a new camlp4 macro - TACTIC EXTEND ... END to be used in ML files - -New organisation of THENS: -tclTHENS tac tacs : tacs is now an array -tclTHENSFIRSTn tac1 tacs tac2 : - apply tac1 then, apply the array tacs on the first n subgoals and - tac2 on the remaining subgoals (previously tclTHENST) -tclTHENSLASTn tac1 tac2 tacs : - apply tac1 then, apply tac2 on the first subgoals and apply the array - tacs on the last n subgoals -tclTHENFIRSTn tac1 tacs = tclTHENSFIRSTn tac1 tacs tclIDTAC (prev. tclTHENSI) -tclTHENLASTn tac1 tacs = tclTHENSLASTn tac1 tclIDTAC tacs -tclTHENFIRST tac1 tac2 = tclTHENFIRSTn tac1 [|tac2|] -tclTHENLAST tac1 tac2 = tclTHENLASTn tac1 [|tac2|] (previously tclTHENL) -tclTHENS tac1 tacs = tclTHENSFIRSTn tac1 tacs (fun _ -> error "wrong number") -tclTHENSV same as tclTHENS but with an array -tclTHENSi : no longer available - -Proof_type: subproof field in type proof_tree glued with the ref field - -Tacmach: no more echo from functions of module Refiner - -Files plugins/*/g_*.ml4 take the place of files plugins/*/*.v. -Files parsing/{vernac,tac}extend.ml{4,i} implements TACTIC EXTEND andd - VERNAC COMMAND EXTEND macros -File syntax/PPTactic.v moved to parsing/pptactic.ml -Tactics about False and not now in tactics/contradiction.ml -Tactics depending on Init now tactics/*.ml4 (no longer in tactics/*.v) -File tacinterp.ml moved from proofs to directory tactics - - -========================================== -= MAIN CHANGES FROM COQ V7.1 TO COQ V7.2 = -========================================== - -The core of Coq (kernel) has meen minimized with the following effects: - -kernel/term.ml split into kernel/term.ml, pretyping/termops.ml -kernel/reduction.ml split into kernel/reduction.ml, pretyping/reductionops.ml -kernel/names.ml split into kernel/names.ml, library/nameops.ml -kernel/inductive.ml split into kernel/inductive.ml, pretyping/inductiveops.ml - -the prefixes "Is" ans "IsMut" have been dropped from kind_of_term constructors, -e.g. IsRel is now Rel, IsMutCase is now Case, etc. - - -======================================================= -= PRINCIPAUX CHANGEMENTS ENTRE COQ V6.3.1 ET COQ V7.0 = -======================================================= - -Changements d'organisation / modules : --------------------------------------- - - Std, More_util -> lib/util.ml - - Names -> kernel/names.ml et kernel/sign.ml - (les parties noms et signatures ont été séparées) - - Avm,Mavm,Fmavm,Mhm -> utiliser plutôt Map (et freeze alors gratuit) - Mhb -> Bij - - Generic est intégré à Term (et un petit peu à Closure) - -Changements dans les types de données : ---------------------------------------- - dans Generic: free_rels : constr -> int Listset.t - devient : constr -> Intset.t - - type_judgement -> typed_type - environment -> context - context -> typed_type signature - - -ATTENTION: ----------- - - Il y a maintenant d'autres exceptions que UserError (TypeError, - RefinerError, etc.) - - Il ne faut donc plus se contenter (pour rattraper) de faire - - try . .. with UserError _ -> ... - - mais écrire à la place - - try ... with e when Logic.catchable_exception e -> ... - - -Changements dans les fonctions : --------------------------------- - - Vectops. - it_vect -> Array.fold_left - vect_it -> Array.fold_right - exists_vect -> Util.array_exists - for_all2eq_vect -> Util.array_for_all2 - tabulate_vect -> Array.init - hd_vect -> Util.array_hd - tl_vect -> Util.array_tl - last_vect -> Util.array_last - it_vect_from -> array_fold_left_from - vect_it_from -> array_fold_right_from - app_tl_vect -> array_app_tl - cons_vect -> array_cons - map_i_vect -> Array.mapi - map2_vect -> array_map2 - list_of_tl_vect -> array_list_of_tl - - Names - sign_it -> fold_var_context (se fait sur env maintenant) - it_sign -> fold_var_context_reverse (sur env maintenant) - - Generic - noccur_bet -> noccur_between - substn_many -> substnl - - Std - comp -> Util.compose - rev_append -> List.rev_append - - Termenv - mind_specif_of_mind -> Global.lookup_mind_specif - ou Environ.lookup_mind_specif si on a un env sous la main - mis_arity -> instantiate_arity - mis_lc -> instantiate_lc - - Ex-Environ - mind_of_path -> Global.lookup_mind - - Printer - gentermpr -> gen_pr_term - term0 -> prterm_env - pr_sign -> pr_var_context - pr_context_opt -> pr_context_of - pr_ne_env -> pr_ne_context_of - - Typing, Machops - type_of_type -> judge_of_type - fcn_proposition -> judge_of_prop_contents - safe_fmachine -> safe_infer - - Reduction, Clenv - whd_betadeltat -> whd_betaevar - whd_betadeltatiota -> whd_betaiotaevar - find_mrectype -> Inductive.find_mrectype - find_minductype -> Inductive.find_inductive - find_mcoinductype -> Inductive.find_coinductive - - Astterm - constr_of_com_casted -> interp_casted_constr - constr_of_com_sort -> interp_type - constr_of_com -> interp_constr - rawconstr_of_com -> interp_rawconstr - type_of_com -> type_judgement_of_rawconstr - judgement_of_com -> judgement_of_rawconstr - - Termast - bdize -> ast_of_constr - - Tacmach - pf_constr_of_com_sort -> pf_interp_type - pf_constr_of_com -> pf_interp_constr - pf_get_hyp -> pf_get_hyp_typ - pf_hyps, pf_untyped_hyps -> pf_env (tout se fait sur env maintenant) - - Pattern - raw_sopattern_of_compattern -> Astterm.interp_constrpattern - somatch -> is_matching - dest_somatch -> matches - - Tacticals - matches -> gl_is_matching - dest_match -> gl_matches - suff -> utiliser sort_of_goal - lookup_eliminator -> utiliser sort_of_goal pour le dernier arg - - Divers - initial_sign -> var_context - - Sign - ids_of_sign -> ids_of_var_context (or Environ.ids_of_context) - empty_sign -> empty_var_context - - Pfedit - list_proofs -> get_all_proof_names - get_proof -> get_current_proof_name - abort_goal -> abort_proof - abort_goals -> abort_all_proofs - abort_cur_goal -> abort_current_proof - get_evmap_sign -> get_goal_context/get_current_goal_context - unset_undo -> reset_undo - - Proof_trees - mkGOAL -> mk_goal - - Declare - machine_constant -> declare_constant (+ modifs) - - ex-Trad, maintenant Pretyping - inh_cast_rel -> Coercion.inh_conv_coerce_to - inh_conv_coerce_to -> Coercion.inh_conv_coerce_to_fail - ise_resolve1 -> understand, understand_type - ise_resolve -> understand_judgment, understand_type_judgment - - ex-Tradevar, maintenant Evarutil - mt_tycon -> empty_tycon - - Recordops - struc_info -> find_structure - -Changements dans les inductifs ------------------------------- -Nouveaux types "constructor" et "inductive" dans Term -La plupart des fonctions de typage des inductives prennent maintenant -un inductive au lieu d'un oonstr comme argument. Les seules fonctions -à traduire un constr en inductive sont les find_rectype and co. - -Changements dans les grammaires -------------------------------- - - . le lexer (parsing/lexer.mll) est maintenant un lexer ocamllex - - . attention : LIDENT -> IDENT (les identificateurs n'ont pas de - casse particulière dans Coq) - - . Le mot "command" est remplacé par "constr" dans les noms de - fichiers, noms de modules et non-terminaux relatifs au parsing des - termes; aussi les changements suivants "COMMAND"/"CONSTR" dans - g_vernac.ml4, VARG_COMMAND/VARG_CONSTR dans vernac*.ml* - - . Les constructeurs d'arguments de tactiques IDENTIFIER, CONSTR, ...n - passent en minuscule Identifier, Constr, ... - - . Plusieurs parsers ont changé de format (ex: sortarg) - -Changements dans le pretty-printing ------------------------------------ - - . Découplage de la traduction de constr -> rawconstr (dans detyping) - et de rawconstr -> ast (dans termast) - . Déplacement des options d'affichage de printer vers termast - . Déplacement des réaiguillage d'univers du pp de printer vers esyntax - - -Changements divers ------------------- - - . il n'y a plus de script coqtop => coqtop et coqtop.byte sont - directement le résultat du link du code - => debuggage et profiling directs - - . il n'y a plus d'installation locale dans bin/$ARCH - - . #use "include.ml" => #use "include" - go() => loop() - - . il y a "make depend" et "make dependcamlp4" car ce dernier prend beaucoup - de temps diff --git a/dev/doc/cic.dtd b/dev/doc/cic.dtd index f2314e22..cc33efd4 100644 --- a/dev/doc/cic.dtd +++ b/dev/doc/cic.dtd @@ -125,7 +125,7 @@ id ID #REQUIRED sort %sort; #REQUIRED> - + diff --git a/dev/doc/coq-src-description.txt b/dev/doc/coq-src-description.txt index 00e7f5c5..b3d49b7e 100644 --- a/dev/doc/coq-src-description.txt +++ b/dev/doc/coq-src-description.txt @@ -14,11 +14,6 @@ parsing tactics toplevel -highparsing : - - Files in parsing/ that cannot be linked too early. - Contains the grammar rules g_*.ml4 - Special components ------------------ @@ -30,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 new file mode 100644 index 00000000..14a1cc69 --- /dev/null +++ b/dev/doc/debugging.md @@ -0,0 +1,106 @@ +Debugging from Coq toplevel using Caml trace mechanism +====================================================== + + 1. Launch bytecode version of Coq (coqtop.byte) + 2. Access Ocaml toplevel using vernacular command 'Drop.' + 3. Install load paths and pretty printers for terms, idents, ... using + Ocaml command '#use "base_include";;' (use '#use "include";;' for + installing the advanced term pretty printers) + 4. Use #trace to tell which function(s) to trace + 5. Go back to Coq toplevel with 'go();;' + 6. Test your Coq command and observe the result of tracing your functions + 7. Freely switch from Coq to Ocaml toplevels with 'Drop.' and 'go();;' + + You can avoid typing #use "include" (or "base_include") after Drop + by adding the following lines in your $HOME/.ocamlinit : + + if Filename.basename Sys.argv.(0) = "coqtop.byte" + then ignore (Toploop.use_silently Format.std_formatter "include") + + Hints: To remove high-level pretty-printing features (coercions, + notations, ...), use "Set Printing All". It will affect the #trace + printers too. + + +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 + byte-code version of `coqtop` must have been generated with `make byte`. + + 1. M-x camldebug + 2. give the binary name bin/coqtop.byte + 3. give ../dev/ocamldebug-coq + 4. source db (to get pretty-printers) + 5. add breakpoints with C-x C-a C-b from the buffer displaying the ocaml + source + 6. get more help from ocamldebug manual + run + step + back + start + next + last + print x (abbreviated into p x) + ... + 7. some hints: + + - To debug a failure/error/anomaly, add a breakpoint in + `Vernac.interp_vernac` (in `toplevel/vernac.ml`) at the with clause of the "try ... interp com + with ..." block, then go "back" a few steps to find where the + failure/error/anomaly has been raised + - Alternatively, for an error or an anomaly, add breakpoints in the middle + of each of error* functions or anomaly* functions in lib/util.ml + - If "source db" fails, do a "make printers" and try again (it should build + top_printers.cmo and the core cma files). + - If you build Coq with an OCaml version earlier than 4.06, and have the + OCAMLRUNPARAM environment variable set, Coq may hang on startup when run + 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 ` or `p ` 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 +============================ + + Coq must be configured with option -profile + + 1. Run native Coq which must end normally (use Quit or option -batch) + 2. gprof ./coqtop gmon.out + +Per function profiling +====================== + + To profile function foo in file bar.ml, add the following lines, just + after the definition of the function: + + let fookey = CProfile.declare_profile "foo";; + let foo a b c = CProfile.profile3 fookey foo a b c;; + + where foo is assumed to have three arguments (adapt using + Profile.profile1, Profile. profile2, etc). + + This has the effect to cumulate the time passed in foo under a + line of name "foo" which is displayed at the time coqtop exits. diff --git a/dev/doc/debugging.txt b/dev/doc/debugging.txt deleted file mode 100644 index f0df2fc3..00000000 --- a/dev/doc/debugging.txt +++ /dev/null @@ -1,78 +0,0 @@ -Debugging from Coq toplevel using Caml trace mechanism -====================================================== - - 1. Launch bytecode version of Coq (coqtop.byte or coqtop -byte) - 2. Access Ocaml toplevel using vernacular command 'Drop.' - 3. Install load paths and pretty printers for terms, idents, ... using - Ocaml command '#use "base_include";;' (use '#use "include";;' for - installing the advanced term pretty printers) - 4. Use #trace to tell which function(s) to trace - 5. Go back to Coq toplevel with 'go();;' - 6. Test your Coq command and observe the result of tracing your functions - 7. Freely switch from Coq to Ocaml toplevels with 'Drop.' and 'go();;' - - You can avoid typing #use "include" (or "base_include") after Drop - by adding the following lines in your $HOME/.ocamlinit : - - if Filename.basename Sys.argv.(0) = "coqtop.byte" - then ignore (Toploop.use_silently Format.std_formatter "include") - - Hints: To remove high-level pretty-printing features (coercions, - notations, ...), use "Set Printing All". It will affect the #trace - printers too. - - -Debugging from Caml debugger -============================ - - Needs tuareg mode in Emacs - Coq must be configured with -debug and -local (./configure -debug -local) - - 1. M-x camldebug - 2. give the binary name bin/coqtop.byte - 3. give ../dev/ocamldebug-coq - 4. source db (to get pretty-printers) - 5. add breakpoints with C-x C-a C-b from the buffer displaying the ocaml - source - 6. get more help from ocamldebug manual - run - step - back - start - next - last - print x (abbreviated into p x) - ... - 7. some hints: - - - To debug a failure/error/anomaly, add a breakpoint in - Vernac.vernac_com at the with clause of the "try ... interp com - with ..." block, then go "back" a few steps to find where the - failure/error/anomaly has been raised - - Alternatively, for an error or an anomaly, add breakpoints in the middle - of each of error* functions or anomaly* functions in lib/util.ml - - If "source db" fails, recompile printers.cma with - "make dev/printers.cma" and try again - -Global gprof-based profiling -============================ - - Coq must be configured with option -profile - - 1. Run native Coq which must end normally (use Quit or option -batch) - 2. gprof ./coqtop gmon.out - -Per function profiling -====================== - - 1. To profile function foo in file bar.ml, add the following lines, just - after the definition of the function: - - let fookey = Profile.declare_profile "foo";; - let foo a b c = Profile.profile3 fookey foo a b c;; - - where foo is assumed to have three arguments (adapt using - Profile.profile1, Profile. profile2, etc). - - This has the effect to cumulate the time passed in foo under a - line of name "foo" which is displayed at the time coqtop exits. diff --git a/dev/doc/econstr.md b/dev/doc/econstr.md new file mode 100644 index 00000000..bb17e8fb --- /dev/null +++ b/dev/doc/econstr.md @@ -0,0 +1,129 @@ +# Evar-insensitive terms (EConstr) + +Evar-insensitive terms were introduced in 8.7, following +[CEP #10](https://github.com/coq/ceps/blob/master/text/010-econstr.md). We will +not recap the motivations in this document and rather summarize the code changes +to perform. + +## Overview + +The essential datastructures are defined in +[the `EConstr` module](/engine/eConstr.mli) module. It defines +the tactic counterparts of kernel data structures such as terms +(`EConstr.constr`), universes (`EConstr.ESorts.t`) and contexts +(`EConstr.*_context`). + +The main difference with kernel-side types is that observing them requires +an evar-map at hand in order to normalize evars on the fly. The basic primitive +to observe an `EConstr.t` is the following function: +``` +val kind : Evd.evar_map -> t -> (t, t, ESorts.t, EInstance.t) Constr.kind_of_term +(** Same as {!Constr.kind} except that it expands evars and normalizes + universes on the fly. *) +``` + +Essentially, each time it sees an evar which happens to be defined in the +provided evar-map, it replaces it with the corresponding body and carries on. + +Due to universe unification occuring at the tactic level, the same goes for +universe instances and sorts. See the `ESort` and `EInstance` modules in +`EConstr`. + +This normalization is critical for the soundness of tactics. Before EConstr, a +lot of bugs were lurking in the code base, a few still are (most notably in +meta-based unification) and failure to respect the guidelines thereafter may +result in nasal demons. + +## Transition path + +### Types + +As a rule of thumb, all functions living at the tactic level should manipulate +`EConstr.t` instead of `Constr.t`, and similarly for the other data structures. + +To ease the transition, the `EConstr` module defines a handful of aliases to +shadow the type names from the kernel. + +It is recommended to perform the following replacement in headers. +```ocaml +(** Kernel types. You may remove the two following opens if you want. Beware + that [kind_of_term] needs to be in scope if you use [EConstr.kind] so that + you may still need to open one of the two. *) +open Term +open Constr +(** Tactic types. Open this after to shadow kernel types. *) +open EConstr +``` + +Note that the `EConstr` module also redefines a `Vars` submodule. + +### Evar-map-passing + +All functions deconstructing an econstr need to take an evar-map as a parameter. +Therefore, you need to pass one as an argument virtually everywhere. + +In the Coq source code, it is recommended to take the evar-map as a first +argument called `sigma`, except if the function also takes an environment in +which case it is passed second. Namely, the two typical instances are: +```ocaml +let foo sigma c = mycode +val foo : Evd.evar_map -> EConstr.t -> Foo.t + +let bar env sigma c = mycode +val bar : Environ.env -> Evd.evar_map -> EConstr.t -> Bar.t +``` + +The EConstr API makes the code much more sensitive to evar-maps, because a +lot of now useless normalizations were removed. Thus one should be cautious of +**not** dropping the evar-map when it has been updated, and should rather stick +to a strict state-passing discipline. Unsound primitives like +`Typing.unsafe_type_of` are also a known source of problems, so you should +replace them with the corresponding evar-map-returning function and thread it +properly. + +### Functions + +Many functions from `Constr` and `Term` are redefined to work on econstr in +the `EConstr` module, so that it is often enough to perform the `open` as +described above to replace them. Their type may differ though, because they now +need access to an evar-map. A lot of econstr-manipulating functions are also +defined in [`Termops`](/engine/termops.mli). + +Functions manipulating tactic terms and kernel terms share the same name if they +are the equivalent one of the other. Do not hesitate to grep Coq mli files to +find the equivalent of a function you want to port if it is neither in `EConstr` +nor in `Termops` (this should be very rare). + +### Conversion + +Sometimes you do not have any other choice than calling kernel-side functions +on terms, and conversely to turn a kernel term into a tactic term. + +There are two functions to do so. +* `EConstr.of_constr` turns kernel terms into tactic terms. It is currently +the physical identity, and thus O(1), but this may change in the future. +* `EConstr.to_constr` turns tactic terms into kernel terms. It performs a +full-blown normalization of the given term, which is O(n) and potentially +costly. + +For performance reasons, avoiding to jump back and forth between kernel and +tactic terms is recommended. + +There are also a few unsafe conversion functions that take advantage of the +fact that `EConstr.t` is internally the same as `Constr.t`. Namely, +`EConstr.Unsafe.to_constr` is the physical identity. It should **not** be used +in typical code and is instead provided for efficiency **when you know what you +are doing**. Either use it to reimplement low-level functions that happen to +be insensitive externally, or use it to provide backward compatibility with +broken code that relies on evar-sensitivity. **Do not use it because it is +easier than stuffing evar-maps everywhere.** You've been warned. + +## Notes + +The EConstr branch fixed a lot of eisenbugs linked to lack of normalization +everywhere, most notably in unification. It may also have introduced a few, so +if you see a change in behaviour *that looks like a bug*, please report it. +Obviously, unification is not specified, so it's hard to tell apart, but still. + +Efficiency has been affected as well. We now pay an overhead when observing a +term, but at the same time a lot of costly upfront normalizations were removed. diff --git a/dev/doc/naming-conventions.tex b/dev/doc/naming-conventions.tex index 34916494..337b9226 100644 --- a/dev/doc/naming-conventions.tex +++ b/dev/doc/naming-conventions.tex @@ -267,7 +267,7 @@ If the conclusion is in the other way than listed below, add suffix {forall x y:D, op (op' x y) = op' x (op y)} \itemrule{Idempotency of binary operator {\op} on domain {\D}}{Dop\_idempotent} -{forall x:D, op x n = x} +{forall x:D, op x x = x} \itemrule{Idempotency of unary operator {\op} on domain {\D}}{Dop\_idempotent} {forall x:D, op (op x) = op x} diff --git a/dev/doc/notes-on-conversion b/dev/doc/notes-on-conversion deleted file mode 100644 index a81f170c..00000000 --- a/dev/doc/notes-on-conversion +++ /dev/null @@ -1,73 +0,0 @@ -(**********************************************************************) -(* A few examples showing the current limits of the conversion algorithm *) -(**********************************************************************) - -(*** We define (pseudo-)divergence from Ackermann function ***) - -Definition ack (n : nat) := - (fix F (n0 : nat) : nat -> nat := - match n0 with - | O => S - | S n1 => - fun m : nat => - (fix F0 (n2 : nat) : nat := - match n2 with - | O => F n1 1 - | S n3 => F n1 (F0 n3) - end) m - end) n. - -Notation OMEGA := (ack 4 4). - -Definition f (x:nat) := x. - -(* Evaluation in tactics can somehow be controlled *) -Lemma l1 : OMEGA = OMEGA. -reflexivity. (* succeed: identity *) -Qed. (* succeed: identity *) - -Lemma l2 : OMEGA = f OMEGA. -reflexivity. (* fail: conversion wants to convert OMEGA with f OMEGA *) -Abort. (* but it reduces the right side first! *) - -Lemma l3 : f OMEGA = OMEGA. -reflexivity. (* succeed: reduce left side first *) -Qed. (* succeed: expected concl (the one with f) is on the left *) - -Lemma l4 : OMEGA = OMEGA. -assert (f OMEGA = OMEGA) by reflexivity. (* succeed *) -unfold f in H. (* succeed: no type-checking *) -exact H. (* succeed: identity *) -Qed. (* fail: "f" is on the left *) - -(* This example would fail whatever the preferred side is *) -Lemma l5 : OMEGA = f OMEGA. -unfold f. -assert (f OMEGA = OMEGA) by reflexivity. -unfold f in H. -exact H. -Qed. (* needs to convert (f OMEGA = OMEGA) and (OMEGA = f OMEGA) *) - -(**********************************************************************) -(* Analysis of the inefficiency in Nijmegen/LinAlg/LinAlg/subspace_dim.v *) -(* (proof of span_ind_uninject_prop *) - -In the proof, a problem of the form (Equal S t1 t2) -is "simpl"ified, then "red"uced to (Equal S' t1 t1) -where the new t1's are surrounded by invisible coercions. -A reflexivity steps conclude the proof. - -The trick is that Equal projects the equality in the setoid S, and -that (Equal S) itself reduces to some (fun x y => Equal S' (f x) (g y)). - -At the Qed time, the problem to solve is (Equal S t1 t2) = (Equal S' t1 t1) -and the algorithm is to first compare S and S', and t1 and t2. -Unfortunately it does not work, and since t1 and t2 involve concrete -instances of algebraic structures, it takes a lot of time to realize that -it is not convertible. - -The only hope to improve this problem is to observe that S' hides -(behind two indirections) a Setoid constructor. This could be the -argument to solve the problem. - - diff --git a/dev/doc/notes-on-conversion.v b/dev/doc/notes-on-conversion.v new file mode 100644 index 00000000..a81f170c --- /dev/null +++ b/dev/doc/notes-on-conversion.v @@ -0,0 +1,73 @@ +(**********************************************************************) +(* A few examples showing the current limits of the conversion algorithm *) +(**********************************************************************) + +(*** We define (pseudo-)divergence from Ackermann function ***) + +Definition ack (n : nat) := + (fix F (n0 : nat) : nat -> nat := + match n0 with + | O => S + | S n1 => + fun m : nat => + (fix F0 (n2 : nat) : nat := + match n2 with + | O => F n1 1 + | S n3 => F n1 (F0 n3) + end) m + end) n. + +Notation OMEGA := (ack 4 4). + +Definition f (x:nat) := x. + +(* Evaluation in tactics can somehow be controlled *) +Lemma l1 : OMEGA = OMEGA. +reflexivity. (* succeed: identity *) +Qed. (* succeed: identity *) + +Lemma l2 : OMEGA = f OMEGA. +reflexivity. (* fail: conversion wants to convert OMEGA with f OMEGA *) +Abort. (* but it reduces the right side first! *) + +Lemma l3 : f OMEGA = OMEGA. +reflexivity. (* succeed: reduce left side first *) +Qed. (* succeed: expected concl (the one with f) is on the left *) + +Lemma l4 : OMEGA = OMEGA. +assert (f OMEGA = OMEGA) by reflexivity. (* succeed *) +unfold f in H. (* succeed: no type-checking *) +exact H. (* succeed: identity *) +Qed. (* fail: "f" is on the left *) + +(* This example would fail whatever the preferred side is *) +Lemma l5 : OMEGA = f OMEGA. +unfold f. +assert (f OMEGA = OMEGA) by reflexivity. +unfold f in H. +exact H. +Qed. (* needs to convert (f OMEGA = OMEGA) and (OMEGA = f OMEGA) *) + +(**********************************************************************) +(* Analysis of the inefficiency in Nijmegen/LinAlg/LinAlg/subspace_dim.v *) +(* (proof of span_ind_uninject_prop *) + +In the proof, a problem of the form (Equal S t1 t2) +is "simpl"ified, then "red"uced to (Equal S' t1 t1) +where the new t1's are surrounded by invisible coercions. +A reflexivity steps conclude the proof. + +The trick is that Equal projects the equality in the setoid S, and +that (Equal S) itself reduces to some (fun x y => Equal S' (f x) (g y)). + +At the Qed time, the problem to solve is (Equal S t1 t2) = (Equal S' t1 t1) +and the algorithm is to first compare S and S', and t1 and t2. +Unfortunately it does not work, and since t1 and t2 involve concrete +instances of algebraic structures, it takes a lot of time to realize that +it is not convertible. + +The only hope to improve this problem is to observe that S' hides +(behind two indirections) a Setoid constructor. This could be the +argument to solve the problem. + + diff --git a/dev/doc/primproj.md b/dev/doc/primproj.md new file mode 100644 index 00000000..ea76aeea --- /dev/null +++ b/dev/doc/primproj.md @@ -0,0 +1,41 @@ +Primitive Projections +--------------------- + + | Proj of Projection.t * constr + +Projections are always applied to a term, which must be of a record +type (i.e. reducible to an inductive type `I params`). Type-checking, +reduction and conversion are fast (not as fast as they could be yet) +because we don't keep parameters around. As you can see, it's +currently a `constant` that is used here to refer to the projection, +that will change to an abstract `projection` type in the future. +Basically a projection constant records which inductive it is a +projection for, the number of params and the actual position in the +constructor that must be projected. For compatibility reason, we also +define an eta-expanded form (accessible from user syntax `@f`). The +constant_entry of a projection has both informations. Declaring a +record (under `Set Primitive Projections`) will generate such +definitions. The API to declare them is not stable at the moment, but +the inductive type declaration also knows about the projections, i.e. +a record inductive type decl contains an array of terms representing +the projections. This is used to implement eta-conversion for record +types (with at least one field and having all projections definable). +The canonical value being `Build_R (pn x) ... (pn x)`. Unification and +conversion work up to this eta rule. The records can also be universe +polymorphic of course, and we don't need to keep track of the universe +instance for the projections either. Projections are reduced _eagerly_ +everywhere, and introduce a new `Zproj` constructor in the abstract +machines that obeys both the delta (for the constant opacity) and iota +laws (for the actual reduction). Refolding works as well (afaict), but +there is a slight hack there related to universes (not projections). + +For the ML programmer, the biggest change is that pattern-matchings on +kind_of_term require an additional case, that is handled usually +exactly like an `App (Const p) arg`. + +There are slight hacks related to hints is well, to use the primitive +projection form of f when one does `Hint Resolve f`. Usually hint +resolve will typecheck the term, resulting in a partially applied +projection (disallowed), so we allow it to take +`constr_or_global_reference` arguments instead and special-case on +projections. Other tactic extensions might need similar treatment. diff --git a/dev/doc/profiling.txt b/dev/doc/profiling.txt index 9d2ebf0d..b5dd8445 100644 --- a/dev/doc/profiling.txt +++ b/dev/doc/profiling.txt @@ -7,7 +7,7 @@ want to profile time or memory consumption. AFAIK, this only works for Linux. In Coq source folder: -opam switch 4.02.1+fp +opam switch 4.02.3+fp ./configure -local -debug make perf record -g bin/coqtop -compile file.v diff --git a/dev/doc/proof-engine.md b/dev/doc/proof-engine.md new file mode 100644 index 00000000..8f96ac22 --- /dev/null +++ b/dev/doc/proof-engine.md @@ -0,0 +1,133 @@ +Tutorial on the new proof engine for ML tactic writers +====================================================== + +Starting from Coq 8.5, a new proof engine has been introduced, replacing the old +meta-based engine which had a lot of drawbacks, ranging from expressivity to +soundness, the major one being that the type of tactics was transparent. This +was pervasively abused and made virtually impossible to tweak the implementation +of the engine. + +The old engine is deprecated and is slowly getting removed from the source code. + +The new engine relies on a monadic API defined in the `Proofview` module. Helper +functions and higher-level operations are defined in the `Tacmach` and +`Tacticals` modules, and end-user tactics are defined amongst other in the +`Tactics` module. + +At the root of the engine is a representation of proofs as partial terms that +can contain typed holes, called evars, short for *existential variable*. An evar +is essentially defined by its context and return type, that we will write +`?e : [Γ ⊢ _ : A]`. An evar `?e` must be applied to a substitution `σ` of type +`Γ` (i.e. a list of terms) to produce a term of type `A`, which is done by +applying `EConstr.mkEvar`, and which we will write `?e{σ}`. + +The engine monad features a notion of global state called `evar_map`, defined in +the `Evd` module, which is the structure containing the incremental refinement +of evars. `Evd` is a low-level API and its use is discouraged in favour of the +`Evarutil` module which provides more abstract primitives. + +In addition to this state, the monad also features a goal state, that is +an ordered list of current holes to be filled. While these holes are referred +to as goals at a high-enough level, they are actually no more than evars. The +API provided to deal with these holes can be found in the `Proofview.Goal` +module. Tactics are naturally operating on several goals at once, so that it is +usual to use the `Proofview.Goal.enter` function and its variants to dispatch a +tactic to each of the goals under focus. + +Primitive tactics by term refining +------------------------------------- + +A typical low-level tactic will be defined by plugging partial terms in the +goal holes thanks to the `Refine` module, and in particular to the +`Refine.refine` primitive. + +```ocaml +val refine : typecheck:bool -> Constr.t Sigma.run -> unit tactic +(** In [refine typecheck t], [t] is a term with holes under some + [evar_map] context. The term [t] is used as a partial solution + for the current goal (refine is a goal-dependent tactic), the + new holes created by [t] become the new subgoals. Exceptions + raised during the interpretation of [t] are caught and result in + tactic failures. If [typecheck] is [true] [t] is type-checked beforehand. *) +``` + +In a first approximation, we can think of `'a Sigma.run` as +`evar_map -> 'a * evar_map`. What the function does is first evaluate the +`Constr.t Sigma.run` argument in the current proof state, and then use the +resulting term as a filler for the proof under focus. All evars that have been +created by the invocation of this thunk are then turned into new goals added in +the order of their creation. + +To see how we can use it, let us have a look at an idealized example, the `cut` +tactic. Assuming `X` is a type, `cut X` fills the current goal `[Γ ⊢ _ : A]` +with a term `let x : X := ?e2{Γ} in ?e1{Γ} x` where `x` is a fresh variable and +`?e1 : [Γ ⊢ _ : X -> A]` and `?e2 : [Γ ⊢ _ : X]`. The current goal is solved and +two new holes `[e1, e2]` are added to the goal state in this order. + +```ocaml +let cut c = + let open Sigma in + Proofview.Goal.nf_enter { enter = begin fun gl -> + (** In this block, we focus on one goal at a time indicated by gl *) + let env = Proofview.Goal.env gl in + (** Get the context of the goal, essentially [Γ] *) + let concl = Proofview.Goal.concl gl in + (** Get the conclusion [A] of the goal *) + let hyps = Tacmach.New.pf_ids_of_hyps gl in + (** List of hypotheses from the context of the goal *) + let id = Namegen.next_name_away Anonymous hyps in + (** Generate a fresh identifier *) + let t = mkArrow c (Vars.lift 1 concl) in + (** Build [X -> A]. Note the lifting of [A] due to being on the right hand + side of the arrow. *) + Refine.refine { run = begin fun sigma -> + (** All evars generated by this block will be added as goals *) + let Sigma (f, sigma, p) = Evarutil.new_evar env sigma t in + (** Generate ?e1 : [Γ ⊢ _ : X -> A], add it to sigma, and return the + term [f := Γ ⊢ ?e1{Γ} : X -> A] with the updated sigma. The identity + substitution for [Γ] is extracted from the [env] argument, so that + one must be careful to pass the correct context here in order for the + resulting term to be well-typed. The [p] return value is a proof term + used to enforce sigma monotonicity. *) + let Sigma (x, sigma, q) = Evarutil.new_evar env sigma c in + (** Generate ?e2 : [Γ ⊢ _ : X] in sigma and return + [x := Γ ⊢ ?e2{Γ} : X]. *) + let r = mkLetIn (Name id, x, c, mkApp (Vars.lift 1 r, [|mkRel 1|])) in + (** Build [r := Γ ⊢ let id : X := ?e2{Γ} in ?e1{Γ} id : A] *) + Sigma (r, sigma, p +> q) + (** Fills the current hole with [r]. The [p +> q] thingy ensures + monotonicity of sigma. *) + end } + end } +``` + +The `Evarutil.new_evar` function is the preferred way to generate evars in +tactics. It returns a ready-to-use term, so that one does not have to call +the `mkEvar` primitive. There are lower-level variants whose use is dedicated to +special use cases, *e.g.* whenever one wants a non-identity substitution. One +should take care to call it with the proper `env` argument so that the evar +and term it generates make sense in the context they will be plugged in. + +For the sake of completeness, the old engine was relying on the `Tacmach.refine` +function to provide a similar feature. Nonetheless, it was using untyped metas +instead of evars, so that it had to mangle the argument term to actually produce +the term that would be put into the hole. For instance, to work around the +untypedness, some metas had to be coerced with a cast to enforce their type, +otherwise leading to runtime errors. This was working for very simple +instances, but was unreliable for everything else. + +High-level composition of tactics +------------------------------------ + +It is possible to combine low-level refinement tactics to create more powerful +abstractions. While it was the standard way of doing things in the old engine +to overcome its technical limitations (namely that one was forced to go through +a limited set of derivation rules), it is recommended to generate proofs as +much as possible by refining in ML tactics when it is possible and easy enough. +Indeed, this prevents dependence on fragile constructions such as unification. + +Obviously, it does not forbid the use of tacticals to mimick what one would do +in Ltac. Each Ltac primitive has a corresponding ML counterpart with simple +semantics. A list of such tacticals can be found in the `Tacticals` module. Most +of them are a porting of the tacticals from the old engine to the new one, so +that if they share the same name they are expected to have the same semantics. diff --git a/dev/doc/setup.txt b/dev/doc/setup.txt index 1b016a4e..c48c2d5d 100644 --- a/dev/doc/setup.txt +++ b/dev/doc/setup.txt @@ -12,7 +12,7 @@ How to compile Coq Getting build dependencies: - sudo apt-get install make opam git mercurial darcs + sudo apt-get install make opam git opam init --comp 4.02.3 # Then follow the advice displayed at the end as how to update your ~/.bashrc and ~/.ocamlinit files. @@ -41,17 +41,15 @@ Building coqtop: cd ~/git/coq git checkout trunk make distclean - ./configure -annotate -with-doc no -local -debug -usecamlp5 + ./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 - -The "-debug" option is essential if one wants to use ocamldebug with the coqtop binary. - -Then check if +Once the compilation is over check if - bin/coqtop - bin/coqide behave as expected. @@ -60,30 +58,12 @@ behave as expected. A note about rlwrap ------------------- -Running "coqtop" under "rlwrap" is possible, but 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) @@ -281,7 +261,7 @@ You can load them by switching to the window holding the "ocamldebug" shell and Some of the functions were you might want to set a breakpoint and see what happens next --------------------------------------------------------------------------------------- -- Coqtop.start : This function is called by the code produced by "coqmktop". +- Coqtop.start : This function is the main entry point of coqtop. - Coqtop.parse_args : This function is responsible for parsing command-line arguments. - Coqloop.loop : This function implements the read-eval-print loop. - Vernacentries.interp : This function is called to execute the Vernacular command user have typed.\ diff --git a/dev/doc/style.txt b/dev/doc/style.txt index 27695a09..2ee3dadd 100644 --- a/dev/doc/style.txt +++ b/dev/doc/style.txt @@ -1,75 +1,142 @@ - -<< L'uniformité du style est plus importante que le style lui-même. >> -(Kernigan & Pike, The Practice of Programming) - -Mode Emacs -========== - Tuareg, que l'on trouve ici : http://www.prism.uvsq.fr/~acohen/tuareg/ - - avec le réglage suivant : (setq tuareg-in-indent 2) - -Types récursifs et filtrages -============================ - Une barre de séparation y compris sur le premier constructeur - -type t = - | A - | B of machin - -match expr with - | A -> ... - | B x -> ... - -Remarque : à partir de la 8.2 environ, la tendance est à utiliser le -format suivant qui permet de limiter l'escalade d'indentation tout en -produisant un aspect visuel intéressant de bloc : - -type t = -| A -| B of machin - -match expr with -| A -> ... -| B x -> ... - -let f expr = match expr with -| A -> ... -| B x -> ... - -let f expr = function -| A -> ... -| B x -> ... - -Le deuxième cas est obtenu sous tuareg avec les réglages - - (setq tuareg-with-indent 0) - (setq tuareg-function-indent 0) - (setq tuareg-let-always-indent nil) /// notons que cette dernière est bien - /// pour les let mais pas pour les let-in - -Conditionnelles -=============== - if condition then - premier-cas - else - deuxieme-cas - - Si effets de bord dans les branches, utilisez begin ... end et non des - parenthèses i.e. - - if condition then begin - instr1; - instr2 - end else begin - instr3; - instr4 - end - - Si la première branche lève une exception, évitez le else i.e. - - if condition then if condition then error "machin"; - error "machin" -----> suite +<< Style uniformity is more important than style itself >> + (Kernigan & Pike, The Practice of Programming) + +OCaml Style: +- Spacing and indentation + - indent your code (using tuareg default) + - no strong constraints in formatting "let in"; possible styles are: + "let x = ... in" + "let x = + ... in" + "let + x = ... + in" + - but: no extra indentation before a "in" coming on next line, + otherwise, it first shifts further and further on the right, + reducing the amount of space available; second, it is not robust to + insertion of a new "let" + - it is established usage to have space around "|" as in + "match c with + | [] | [a] -> ... + | a::b::l -> ..." + - in a one-line "match", it is preferred to have no "|" in front of + the first case (this saves spaces for the match to hold in the line) + - from about 8.2, the tendency is to use the following format which + limit excessive indentation while providing an interesting "block" aspect + type t = + | A + | B of machin + + let f expr = match expr with + | A -> ... + | B x -> ... + + let f expr = function + | A -> ... + | B x -> ... + - add spaces around = and == (make the code "breaths") + - the common usage is to write "let x,y = ... in ..." rather than + "let (x,y) = ... in ..." + - parenthesizing with either "(" and ")" or with "begin" and "end" is + common practice + - preferred layout for conditionals: + if condition then + premier-cas else - suite - - + deuxieme-cas + - in case of effects in branches, use "begin ... end" rather than + parentheses + if condition then begin + instr1; + instr2 + end else begin + instr3; + instr4 + end + - if the first branch raises an exception, avoid the "else", i.e.: + if condition then if condition then error "foo"; + error "foo" -----> bar + else + bar + - it is the usage not to use ;; to end OCaml sentences (however, + inserting ";;" can be useful for debugging syntax errors crossing + the boundary of functions) + - relevant options in tuareg: + (setq tuareg-in-indent 2) + (setq tuareg-with-indent 0) + (setq tuareg-function-indent 0) + (setq tuareg-let-always-indent nil) + +- Coding methodology + - no "try ... with _ -> ..." which catches even Sys.Break (Ctrl-C), + Out_of_memory, Stack_overflow, etc. + at least, use "try with e when Errors.noncritical e -> ..." + (to be detailed, Pierre L. ?) + - do not abuse of fancy combinators: sometimes what a "let rec" loop + does is more readable and simpler to grasp than what a "fold" does + - do not break abstractions: if an internal property is hidden + behind an interface, do no rely on it in code which uses this + interface (e.g. do not use List.map thinking it is left-to-right, + use map_left) + - in particular, do not use "=" on abstract types: there is no + reason a priori that it is the intended equality on this type; use the + "equal" function normally provided with the abstract type + - avoid polymorphically typed "=" whose implementation is not + optimized in OCaml and which has moreover no reason to be the + intended implementation of the equality when it comes to be + instantiated on a particular type (e.g. use List.mem_f, + List.assoc_f, rather than List.mem, List.assoc, etc, unless it is + absolutely clear that "=" will implement the intended equality, and + with the right complexity) + - any new general-purpose enough combinator on list should be put in + cList.ml, on type option in cOpt.ml, etc. + - unless of a good reason not to so, follow the style of the + surrounding code in the same file as much as possible, + the general guidelines are otherwise "let spacing breaths" (we + have large screen nowadays), "make your code easy to read and + to understand" + - document what is tricky, but do not overdocument, sometimes the + choice of names and the structuration of the code is a better + documentation than a long discourse; use of unicode in comments is + welcome if it can make comments more readable (then + "toggle-enable-multibyte-characters" can help when using the + debugger in emacs) + - all of initial "open File", or of small-scope File.(...), or + per-ident File.foo are common practices + +- Choice of variable names + - be consistent when naming from one function to another + - be consistent with the naming adopted in the functions from the + same file, or with the naming used elsewhere by similar functions + - use variable names which express meaning + - keep "cst" for constants and avoid it for constructors which is + otherwise a source of confusion + - for constructors, use "cstr" in type constructor (resp. "cstru" in + constructor puniverse); avoid "constr" for "constructor" which + could be think as the name of an arbitrary Constr.t + - for inductive types, use "ind" in the type inductive (resp "indu" + in inductive puniverse) + - for env, use "env" + - for evar_map, use "sigma", with tolerance into "evm" and "evd" + - for named_context or rel_context, use "ctxt" or "ctx" (or "sign") + - for formal/actual indices of inductive types: "realdecls", "realargs" + - for formal/actual parameters of inductive types: "paramdecls", "paramargs" + - for terms, use e.g. c, b, a, ... + - if a term is known to be a function: f, ... + - if a term is known to be a type: t, u, typ, ... + - for a declaration, use d or "decl" + - for errors, exceptions, use e + +- Common OCaml pitfalls + - in "match ... with Case1 -> try ... with ... -> ... | Case2 -> ...", or in + "match ... with Case1 -> match ... with SubCase -> ... | Case2 -> ...", or in + parentheses are needed around the "try" and the inner "match" + - even if stream are lazy, the Pp.(++) combinator is strict and + forces the evaluation of its arguments (use a "lazy" or a "fun () ->") + to make it lazy explicitly + - in "if ... then ... else ... ++ ...", the default parenthesizing + is somehow counter-intuitive; use "(if ... then ... else ...) ++ ..." + - in "let myspecialfun = mygenericfun args", be sure that it does no + do side-effect; prefer otherwise "let mygenericfun arg = + mygenericfun args arg" to ensure that the function is evaluated at + runtime diff --git a/dev/doc/universes.md b/dev/doc/universes.md new file mode 100644 index 00000000..c276603e --- /dev/null +++ b/dev/doc/universes.md @@ -0,0 +1,226 @@ +Notes on universe polymorphism +------------------------------ + +The implementation of universe polymorphism introduces a few changes +to the API of Coq. First and foremost, the term language changes, as +global references now carry a universe level substitution: + +~~~ocaml +type 'a puniverses = 'a * Univ.Instance.t +type pconstant = constant puniverses +type pinductive = inductive puniverses +type pconstructor = constructor puniverses + +type constr = ... + | Const of puniverses + | Ind of pinductive + | Constr of pconstructor +~~~ + +Universes +--------- + +Universe instances (an array of levels) gets substituted when +unfolding definitions, are used to typecheck and are unified according +to the rules in the ITP'14 paper on universe polymorphism in Coq. + +~~~ocaml +type Level.t = Set | Prop | Level of int * dirpath (* hashconsed *) +type Instance.t = Level.t array +type Universe.t = Level.t list (* hashconsed *) +~~~ + +The universe module defines modules and abstract types for levels, +universes etc.. Structures are hashconsed (with a hack to take care +of the fact that deserialization breaks sharing). + + Definitions (constants, inductives) now carry around not only +constraints but also the universes they introduced (a Univ.UContext.t). +There is another kind of contexts `Univ.ContextSet.t`, the latter has +a set of universes, while the former has serialized the levels in an +array, and is used for polymorphic objects. Both have "reified" +constraints depending on global and local universes. + + A polymorphic definition is abstract w.r.t. the variables in this +context, while a monomorphic one (or template polymorphic) just adds the +universes and constraints to the global universe context when it is put +in the environment. No other universes than the global ones and the +declared local ones are needed to check a declaration, hence the kernel +does not produce any constraints anymore, apart from module +subtyping.... There are hence two conversion functions now: `check_conv` +and `infer_conv`: the former just checks the definition in the current env +(in which we usually push_universe_context of the associated context), +and `infer_conv` which produces constraints that were not implied by the +ambient constraints. Ideally, that one could be put out of the kernel, +but currently module subtyping needs it. + + Inference of universes is now done during refinement, and the evar_map +carries the incrementally built universe context, starting from the +global universe constraints (see `Evd.from_env`). `Evd.conversion` is a +wrapper around `infer_conv` that will do the bookkeeping for you, it +uses `evar_conv_x`. There is a universe substitution being built +incrementally according to the constraints, so one should normalize at +the end of a proof (or during a proof) with that substitution just like +we normalize evars. There are some nf_* functions in +library/universes.ml to do that. Additionally, there is a minimization +algorithm in there that can be applied at the end of a proof to simplify +the universe constraints used in the term. It is heuristic but +validity-preserving. No user-introduced universe (i.e. coming from a +user-written anonymous Type) gets touched by this, only the fresh +universes generated for each global application. Using +~~~ocaml +val pf_constr_of_global : Globnames.global_reference -> (constr -> tactic) -> tactic +~~~ +Is the way to make a constr out of a global reference in the new API. +If they constr is polymorphic, it will add the necessary constraints to +the evar_map. Even if a constr is not polymorphic, we have to take care +of keeping track of its universes. Typically, using: +~~~ocaml + mkApp (coq_id_function, [| A; a |]) +~~~ +and putting it in a proof term is not enough now. One has to somehow +show that A's type is in cumululativity relation with id's type +argument, incurring a universe constraint. To do this, one can simply +call Typing.resolve_evars env evdref c which will do some infer_conv to +produce the right constraints and put them in the evar_map. Of course in +some cases you might know from an invariant that no new constraint would +be produced and get rid of it. Anyway the kernel will tell you if you +forgot some. As a temporary way out, `Universes.constr_of_global` allows +you to make a constr from any non-polymorphic constant, but it will fail +on polymorphic ones. + +Other than that, unification (w_unify and evarconv) now take account of universes and +produce only well-typed evar_maps. + +Some syntactic comparisons like the one used in `change` have to be +adapted to allow identification up-to-universes (when dealing with +polymorphic references), `make_eq_univs_test` is there to help. +In constr, there are actually many new comparison functions to deal with +that: +~~~ocaml +(** [equal a b] is true if [a] equals [b] modulo alpha, casts, + and application grouping *) +val equal : constr -> constr -> bool + +(** [eq_constr_univs u a b] is [true] if [a] equals [b] modulo alpha, casts, + application grouping and the universe equalities in [u]. *) +val eq_constr_univs : constr Univ.check_function + +(** [leq_constr_univs u a b] is [true] if [a] is convertible to [b] modulo + alpha, casts, application grouping and the universe inequalities in [u]. *) +val leq_constr_univs : constr Univ.check_function + +(** [eq_constr_universes a b] [true, c] if [a] equals [b] modulo alpha, casts, + application grouping and the universe equalities in [c]. *) +val eq_constr_universes : constr -> constr -> bool Univ.universe_constrained + +(** [leq_constr_universes a b] [true, c] if [a] is convertible to [b] modulo + alpha, casts, application grouping and the universe inequalities in [c]. *) +val leq_constr_universes : constr -> constr -> bool Univ.universe_constrained + +(** [eq_constr_univs a b] [true, c] if [a] equals [b] modulo alpha, casts, + application grouping and ignoring universe instances. *) +val eq_constr_nounivs : constr -> constr -> bool +~~~ +The `_univs` versions are doing checking of universe constraints +according to a graph, while the `_universes` are producing (non-atomic) +universe constraints. The non-atomic universe constraints include the +`ULub` constructor: when comparing `f (* u1 u2 *) c` and `f (* u1' u2' +*) c` we add ULub constraints on `u1, u1'` and `u2, u2'`. These are +treated specially: as unfolding `f` might not result in these +unifications, we need to keep track of the fact that failure to satisfy +them does not mean that the term are actually equal. This is used in +unification but probably not necessary to the average programmer. + +Another issue for ML programmers is that tables of constrs now usually +need to take a `constr Univ.in_universe_context_set` instead, and +properly refresh the universes context when using the constr, e.g. using +Clenv.refresh_undefined_univs clenv or: +~~~ocaml +(** Get fresh variables for the universe context. + Useful to make tactics that manipulate constrs in universe contexts polymorphic. *) +val fresh_universe_context_set_instance : universe_context_set -> + universe_level_subst * universe_context_set +~~~ +The substitution should be applied to the constr(s) under consideration, +and the context_set merged with the current evar_map with: +~~~ocaml +val merge_context_set : rigid -> evar_map -> Univ.universe_context_set -> evar_map +~~~ +The `rigid` flag here should be `Evd.univ_flexible` most of the +time. This means the universe levels of polymorphic objects in the +constr might get instantiated instead of generating equality constraints +(Evd.univ_rigid does that). + +On this issue, I recommend forcing commands to take `global_reference`s +only, the user can declare his specialized terms used as hints as +constants and this is cleaner. Alas, backward-compatibility-wise, +this is the only solution I found. In the case of global_references +only, it's just a matter of using `Evd.fresh_global` / +`pf_constr_of_global` to let the system take care of universes. + + +The universe graph +------------------ + +To accomodate universe polymorphic definitions, the graph structure in +kernel/univ.ml was modified. The new API forces every universe to be +declared before it is mentionned in any constraint. This forces to +declare every universe to be >= Set or > Set. Every universe variable +introduced during elaboration is >= Set. Every _global_ universe is now +declared explicitly > Set, _after_ typechecking the definition. In +polymorphic definitions Type@{i} ranges over Set and any other universe +j. However, at instantiation time for polymorphic references, one can +try to instantiate a universe parameter with Prop as well, if the +instantiated constraints allow it. The graph invariants ensure that +no universe i can be set lower than Set, so the chain of universes +always bottoms down at Prop < Set. + +Modules +------- + +One has to think of universes in modules as being globally declared, so +when including a module (type) which declares a type i (e.g. through a +parameter), we get back a copy of i and not some fresh universe. + +Incompatibilities +----------------- + +Old-style universe polymorphic definitions were implemented by taking +advantage of the fact that elaboration (i.e., pretyping and unification) +were _not_ universe aware, so some of the constraints generated during +pretypechecking would be forgotten. In the current setting, this is not +possible, as unification ensures that the substitution is built is +entirely well-typed, even w.r.t universes. This means that some terms +that type-checked before no longer do, especially projections of the +pair: +~~~coq +@fst ?x ?y : prod ?x ?y : Type (max(Datatypes.i, Datatypes.j)). +~~~ +The "template universe polymorphic" variables i and j appear during +typing without being refreshed, meaning that they can be lowered (have +upper constraints) with user-introduced universes. In most cases this +won't work, so ?x and ?y have to be instantiated earlier, either from +the type of the actual projected pair term (some t : prod A B) or the +typing constraint. Adding the correct type annotations will always fix +this. + + +Unification semantics +--------------------- + +In Ltac, matching with: + +- a universe polymorphic constant `c` matches any instance of the + constant. +- a variable ?x already bound to a term `t` (non-linear pattern) uses + strict equality of universes (e.g., Type@{i} and Type@{j} are not + equal). + +In tactics: + +- `change foo with bar`, `pattern foo` will unify all instances of `foo` + (and convert them with `bar`). This might incur unifications of + universes. `change` uses conversion while `pattern` only does + syntactic matching up-to unification of universes. +- `apply`, `refine` use unification up to universes. diff --git a/dev/doc/universes.txt b/dev/doc/universes.txt deleted file mode 100644 index a40706e9..00000000 --- a/dev/doc/universes.txt +++ /dev/null @@ -1,26 +0,0 @@ -How to debug universes? - -1. There is a command Print Universes in Coq toplevel - - Print Universes. - prints the graph of universes in the form of constraints - - Print Universes "file". - produces the "file" containing universe constraints in the form - univ1 # univ2 ; - where # can be either > >= or = - - If "file" ends with .gv or .dot, the resulting file will be in - dot format. - - - *) for dot see http://www.research.att.com/sw/tools/graphviz/ - - -2. There is a printing option - - {Set,Unset} Printing Universes. - - which, when set, makes all pretty-printed Type's annotated with the - name of the universe. - diff --git a/dev/doc/univpoly.txt b/dev/doc/univpoly.txt deleted file mode 100644 index 6a69c579..00000000 --- a/dev/doc/univpoly.txt +++ /dev/null @@ -1,279 +0,0 @@ -Notes on universe polymorphism and primitive projections, M. Sozeau -=================================================================== - -The new implementation of universe polymorphism and primitive -projections introduces a few changes to the API of Coq. First and -foremost, the term language changes, as global references now carry a -universe level substitution: - -type 'a puniverses = 'a * Univ.Instance.t -type pconstant = constant puniverses -type pinductive = inductive puniverses -type pconstructor = constructor puniverses - -type constr = ... - | Const of puniversess - | Ind of pinductive - | Constr of pconstructor - | Proj of constant * constr - - -Universes -========= - - Universe instances (an array of levels) gets substituted when -unfolding definitions, are used to typecheck and are unified according -to the rules in the ITP'14 paper on universe polymorphism in Coq. - -type Level.t = Set | Prop | Level of int * dirpath (* hashconsed *) -type Instance.t = Level.t array -type Universe.t = Level.t list (* hashconsed *) - -The universe module defines modules and abstract types for levels, -universes etc.. Structures are hashconsed (with a hack to take care -of the fact that deserialization breaks sharing). - - Definitions (constants, inductives) now carry around not only -constraints but also the universes they introduced (a Univ.UContext.t). -There is another kind of contexts [Univ.ContextSet.t], the latter has -a set of universes, while the former has serialized the levels in an -array, and is used for polymorphic objects. Both have "reified" -constraints depending on global and local universes. - - A polymorphic definition is abstract w.r.t. the variables in this -context, while a monomorphic one (or template polymorphic) just adds the -universes and constraints to the global universe context when it is put -in the environment. No other universes than the global ones and the -declared local ones are needed to check a declaration, hence the kernel -does not produce any constraints anymore, apart from module -subtyping.... There are hence two conversion functions now: [check_conv] -and [infer_conv]: the former just checks the definition in the current env -(in which we usually push_universe_context of the associated context), -and [infer_conv] which produces constraints that were not implied by the -ambient constraints. Ideally, that one could be put out of the kernel, -but currently module subtyping needs it. - - Inference of universes is now done during refinement, and the evar_map -carries the incrementally built universe context, starting from the -global universe constraints (see [Evd.from_env]). [Evd.conversion] is a -wrapper around [infer_conv] that will do the bookkeeping for you, it -uses [evar_conv_x]. There is a universe substitution being built -incrementally according to the constraints, so one should normalize at -the end of a proof (or during a proof) with that substitution just like -we normalize evars. There are some nf_* functions in -library/universes.ml to do that. Additionally, there is a minimization -algorithm in there that can be applied at the end of a proof to simplify -the universe constraints used in the term. It is heuristic but -validity-preserving. No user-introduced universe (i.e. coming from a -user-written anonymous Type) gets touched by this, only the fresh -universes generated for each global application. Using - -val pf_constr_of_global : Globnames.global_reference -> (constr -> tactic) -> tactic - -Is the way to make a constr out of a global reference in the new API. -If they constr is polymorphic, it will add the necessary constraints to -the evar_map. Even if a constr is not polymorphic, we have to take care -of keeping track of its universes. Typically, using: - - mkApp (coq_id_function, [| A; a |]) - -and putting it in a proof term is not enough now. One has to somehow -show that A's type is in cumululativity relation with id's type -argument, incurring a universe constraint. To do this, one can simply -call Typing.resolve_evars env evdref c which will do some infer_conv to -produce the right constraints and put them in the evar_map. Of course in -some cases you might know from an invariant that no new constraint would -be produced and get rid of it. Anyway the kernel will tell you if you -forgot some. As a temporary way out, [Universes.constr_of_global] allows -you to make a constr from any non-polymorphic constant, but it will fail -on polymorphic ones. - -Other than that, unification (w_unify and evarconv) now take account of universes and -produce only well-typed evar_maps. - -Some syntactic comparisons like the one used in [change] have to be -adapted to allow identification up-to-universes (when dealing with -polymorphic references), [make_eq_univs_test] is there to help. -In constr, there are actually many new comparison functions to deal with -that: - -(** [equal a b] is true if [a] equals [b] modulo alpha, casts, - and application grouping *) -val equal : constr -> constr -> bool - -(** [eq_constr_univs u a b] is [true] if [a] equals [b] modulo alpha, casts, - application grouping and the universe equalities in [u]. *) -val eq_constr_univs : constr Univ.check_function - -(** [leq_constr_univs u a b] is [true] if [a] is convertible to [b] modulo - alpha, casts, application grouping and the universe inequalities in [u]. *) -val leq_constr_univs : constr Univ.check_function - -(** [eq_constr_universes a b] [true, c] if [a] equals [b] modulo alpha, casts, - application grouping and the universe equalities in [c]. *) -val eq_constr_universes : constr -> constr -> bool Univ.universe_constrained - -(** [leq_constr_universes a b] [true, c] if [a] is convertible to [b] modulo - alpha, casts, application grouping and the universe inequalities in [c]. *) -val leq_constr_universes : constr -> constr -> bool Univ.universe_constrained - -(** [eq_constr_univs a b] [true, c] if [a] equals [b] modulo alpha, casts, - application grouping and ignoring universe instances. *) -val eq_constr_nounivs : constr -> constr -> bool - -The [_univs] versions are doing checking of universe constraints -according to a graph, while the [_universes] are producing (non-atomic) -universe constraints. The non-atomic universe constraints include the -[ULub] constructor: when comparing [f (* u1 u2 *) c] and [f (* u1' u2' -*) c] we add ULub constraints on [u1, u1'] and [u2, u2']. These are -treated specially: as unfolding [f] might not result in these -unifications, we need to keep track of the fact that failure to satisfy -them does not mean that the term are actually equal. This is used in -unification but probably not necessary to the average programmer. - -Another issue for ML programmers is that tables of constrs now usually -need to take a [constr Univ.in_universe_context_set] instead, and -properly refresh the universes context when using the constr, e.g. using -Clenv.refresh_undefined_univs clenv or: - -(** Get fresh variables for the universe context. - Useful to make tactics that manipulate constrs in universe contexts polymorphic. *) -val fresh_universe_context_set_instance : universe_context_set -> - universe_level_subst * universe_context_set - -The substitution should be applied to the constr(s) under consideration, -and the context_set merged with the current evar_map with: - -val merge_context_set : rigid -> evar_map -> Univ.universe_context_set -> evar_map - -The [rigid] flag here should be [Evd.univ_flexible] most of the -time. This means the universe levels of polymorphic objects in the -constr might get instantiated instead of generating equality constraints -(Evd.univ_rigid does that). - -On this issue, I recommend forcing commands to take [global_reference]s -only, the user can declare his specialized terms used as hints as -constants and this is cleaner. Alas, backward-compatibility-wise, -this is the only solution I found. In the case of global_references -only, it's just a matter of using [Evd.fresh_global] / -[pf_constr_of_global] to let the system take care of universes. - - -The universe graph -================== - -To accomodate universe polymorphic definitions, the graph structure in -kernel/univ.ml was modified. The new API forces every universe to be -declared before it is mentionned in any constraint. This forces to -declare every universe to be >= Set or > Set. Every universe variable -introduced during elaboration is >= Set. Every _global_ universe is now -declared explicitly > Set, _after_ typechecking the definition. In -polymorphic definitions Type@{i} ranges over Set and any other universe -j. However, at instantiation time for polymorphic references, one can -try to instantiate a universe parameter with Prop as well, if the -instantiated constraints allow it. The graph invariants ensure that -no universe i can be set lower than Set, so the chain of universes -always bottoms down at Prop < Set. - -Modules -======= - -One has to think of universes in modules as being globally declared, so -when including a module (type) which declares a type i (e.g. through a -parameter), we get back a copy of i and not some fresh universe. - -Projections -=========== - - | Proj of constant * constr - -Projections are always applied to a term, which must be of a record type -(i.e. reducible to an inductive type [I params]). Type-checking, -reduction and conversion are fast (not as fast as they could be yet) -because we don't keep parameters around. As you can see, it's currently -a [constant] that is used here to refer to the projection, that will -change to an abstract [projection] type in the future. Basically a -projection constant records which inductive it is a projection for, the -number of params and the actual position in the constructor that must be -projected. For compatibility reason, we also define an eta-expanded form -(accessible from user syntax @f). The constant_entry of a projection has -both informations. Declaring a record (under [Set Primitive -Projections]) will generate such definitions. The API to declare them is -not stable at the moment, but the inductive type declaration also knows -about the projections, i.e. a record inductive type decl contains an -array of terms representing the projections. This is used to implement -eta-conversion for record types (with at least one field and having all -projections definable). The canonical value being [Build_R (pn x) -... (pn x)]. Unification and conversion work up to this eta rule. The -records can also be universe polymorphic of course, and we don't need to -keep track of the universe instance for the projections either. -Projections are reduced _eagerly_ everywhere, and introduce a new Zproj -constructor in the abstract machines that obeys both the delta (for the -constant opacity) and iota laws (for the actual reduction). Refolding -works as well (afaict), but there is a slight hack there related to -universes (not projections). - -For the ML programmer, the biggest change is that pattern-matchings on -kind_of_term require an additional case, that is handled usually exactly -like an [App (Const p) arg]. - -There are slight hacks related to hints is well, to use the primitive -projection form of f when one does [Hint Resolve f]. Usually hint -resolve will typecheck the term, resulting in a partially applied -projection (disallowed), so we allow it to take -[constr_or_global_reference] arguments instead and special-case on -projections. Other tactic extensions might need similar treatment. - -WIP -=== - -- [vm_compute] does not deal with universes and projections correctly, -except when it goes to a normal form with no projections or polymorphic -constants left (the most common case). E.g. Ring with Set Universe -Polymorphism and Set Primitive Projections work (at least it did at some -point, I didn't recheck yet). - -- [native_compute] works with universes and projections. - - -Incompatibilities -================= - -Old-style universe polymorphic definitions were implemented by taking -advantage of the fact that elaboration (i.e., pretyping and unification) -were _not_ universe aware, so some of the constraints generated during -pretypechecking would be forgotten. In the current setting, this is not -possible, as unification ensures that the substitution is built is -entirely well-typed, even w.r.t universes. This means that some terms -that type-checked before no longer do, especially projections of the -pair: - -@fst ?x ?y : prod ?x ?y : Type (max(Datatypes.i, Datatypes.j)). - -The "template universe polymorphic" variables i and j appear during -typing without being refreshed, meaning that they can be lowered (have -upper constraints) with user-introduced universes. In most cases this -won't work, so ?x and ?y have to be instantiated earlier, either from -the type of the actual projected pair term (some t : prod A B) or the -typing constraint. Adding the correct type annotations will always fix -this. - - -Unification semantics -===================== - -In Ltac, matching with: - -- a universe polymorphic constant [c] matches any instance of the - constant. -- a variable ?x already bound to a term [t] (non-linear pattern) uses - strict equality of universes (e.g., Type@{i} and Type@{j} are not - equal). - -In tactics: - -- [change foo with bar], [pattern foo] will unify all instances of [foo] - (and convert them with [bar]). This might incur unifications of - universes. [change] uses conversion while [pattern] only does - syntactic matching up-to unification of universes. -- [apply], [refine] use unification up to universes. diff --git a/dev/doc/versions-history.tex b/dev/doc/versions-history.tex index 492e75a7..3867d4af 100644 --- a/dev/doc/versions-history.tex +++ b/dev/doc/versions-history.tex @@ -376,9 +376,27 @@ Coq V8.5 beta1 & released 21 January 2015 & \feature{computation via compilation && \feature{new proof engine deployed} [2-11-2013]\\ && \feature{universe polymorphism} [6-5-2014]\\ && \feature{primitive projections} [6-5-2014]\\ +&& \feature{miscellaneous optimizations}\\ Coq V8.5 beta2 & released 22 April 2015 & \feature{MMaps library} [4-3-2015]\\ +Coq V8.5 & released 22 January 2016 & \\ + +Coq V8.6 beta 1 & released 19 November 2016 & \feature{irrefutable patterns} [15-2-2016]\\ +&& \feature{Ltac profiling} [14-6-2016]\\ +&& \feature{warning system} [29-6-2016]\\ +&& \feature{miscellaneous optimizations}\\ + +Coq V8.6 & released 14 December 2016 & \\ + +Coq V8.7 beta 1 & released 6 September 2017 & \feature{bundled with Ssreflect plugin} [6-6-2017]\\ +&& \feature{cumulative polymorphic inductive types} [19-6-2017]\\ +&& \feature{further optimizations}\\ + +Coq V8.7 beta 2 & released 6 October 2017 & \\ + +Coq V8.7 & released 18 October 2016 & \\ + \end{tabular} \medskip diff --git a/dev/doc/xml-protocol.md b/dev/doc/xml-protocol.md new file mode 100644 index 00000000..b35571e9 --- /dev/null +++ b/dev/doc/xml-protocol.md @@ -0,0 +1,755 @@ +# Coq XML Protocol + +This document is based on documentation originally written by CJ Bell +for his [vscoq](https://github.com/siegebell/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. + +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). +OCaml types for the protocol can be found in the [`ide/interface.mli` file](/ide/interface.mli). + +Changes to the XML protocol are documented as part of [`dev/doc/changes.txt`](/dev/doc/changes.txt). + +* [Commands](#commands) + - [About](#command-about) + - [Add](#command-add) + - [EditAt](#command-editAt) + - [Init](#command-init) + - [Goal](#command-goal) + - [Status](#command-status) + - [Query](#command-query) + - [Evars](#command-evars) + - [Hints](#command-hints) + - [Search](#command-search) + - [GetOptions](#command-getoptions) + - [SetOptions](#command-setoptions) + - [MkCases](#command-mkcases) + - [StopWorker](#command-stopworker) + - [PrintAst](#command-printast) + - [Annotate](#command-annotate) +* [Feedback messages](#feedback) + - [Added Axiom](#feedback-addedaxiom) + - [Processing](#feedback-processing) + - [Processed](#feedback-processed) + - [Incomplete](#feedback-incomplete) + - [Complete](#feedback-complete) + - [GlobRef](#feedback-globref) + - [Error](#feedback-error) + - [InProgress](#feedback-inprogress) + - [WorkerStatus](#feedback-workerstatus) + - [File Dependencies](#feedback-filedependencies) + - [File Loaded](#feedback-fileloaded) + - [Message](#feedback-message) + - [Custom](#feedback-custom) + +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." +In practice, the command sentences sent to Coqtop are terminated at the "." and start with any previous whitespace. +Each sentence is assigned a unique stateId after being sent to Coq (via Add). +States: + * Processing: has been received by Coq and has no obvious syntax error (that would prevent future parsing) + * Processed: + * InProgress: + * Incomplete: the validity of the sentence cannot be checked due to a prior error + * Complete: + * Error: the sentence has an error + +State ID 0 is reserved as a 'dummy' state. + +-------------------------- + +## Commands + +### **About(unit)** +Returns information about the protocol and build dates for Coqtop. +``` + + + +``` +#### *Returns* +```html + + 8.6 + 20150913 + December 2016 + Dec 23 2016 16:16:30 + + +``` +The string fields are the Coq version, the protocol version, the release date, and the compile time of Coqtop. +The protocol version is a date in YYYYMMDD format, where "20150913" corresponds to Coq 8.6. An IDE that wishes +to support multiple Coq versions can use the protocol version information to know how to handle output from Coqtop. + +### **Add(stateId: integer, command: string, verbose: boolean)** +Adds a toplevel command (e.g. vernacular, definition, tactic) to the given state. +`verbose` controls whether out-of-band messages will be generated for the added command (e.g. "foo is assumed" in response to adding "Axiom foo: nat."). +```html + + + + ${command} + ${editId} + + + + + + + +``` + +#### *Returns* +* The added command is given a fresh `stateId` and becomes the next "tip". +```html + + + + + + ${message} + + + +``` +* When closing a focused proof (in the middle of a bunch of interpreted commands), +the `Qed` will be assigned a prior `stateId` and `nextStateId` will be the id of an already-interpreted +state that should become the next tip. +```html + + + + + + ${message} + + + +``` +* Failure: + - Syntax error. Error offsets are byte offsets (not character offsets) with respect to the start of the sentence, starting at 0. + ```html + + + ${errorMessage} + + ``` + - Another kind of error, for example, Qed with a pending goal. + ```html + ${errorMessage} + ``` + +------------------------------- + +### **EditAt(stateId: integer)** +Moves current tip to `${stateId}`, such that commands may be added to the new state ID. +```html + +``` +#### *Returns* +* Simple backtrack; focused stateId becomes the parent state +```html + + + +``` + +* New focus; focusedQedStateId is the closing Qed of the new focus; senteneces between the two should be cleared +```html + + + + + + + + + + + +``` +* Failure: If `stateId` is in an error-state and cannot be jumped to, `errorFreeStateId` is the parent state of ``stateId` that shopuld be edited instead. +```html + + + ${errorMessage} + +``` + +------------------------------- + +### **Init()** +* No options. +```html + +``` +* With options. Looking at + [ide_slave.ml](https://github.com/coq/coq/blob/c5d0aa889fa80404f6c291000938e443d6200e5b/ide/ide_slave.ml#L355), + it seems that `options` is just the name of a script file, whose path + is added via `Add LoadPath` to the initial state. +```html + + + +``` +Providing the script file enables Coq to use .aux files created during +compilation. Those file contain timing information that allow Coq to +choose smartly between asynchronous and synchronous processing of +proofs. + +#### *Returns* +* The initial stateId (not associated with a sentence) +```html + + + +``` + +------------------------------- + + +### **Goal()** +```html + +``` +#### *Returns* +* If there is a goal. `shelvedGoals` and `abandonedGoals` have the same structure as the first set of (current/foreground) goals. `backgroundGoals` contains a list of pairs of lists of goals (list ((list Goal)*(list Goal))); it represents a "focus stack" ([see code for reference](https://github.com/coq/coq/blob/trunk/engine/proofview.ml#L113)). Each time a proof is focused, it will add a new pair of lists-of-goals. The first pair is the most nested set of background goals, the last pair is the top level set of background goals. The first list in the pair is in reverse order. Each time you focus the goal (e.g. using `Focus` or a bullet), a new pair will be prefixed to the list. +```html + + + +``` + +For example, this script: +```coq +Goal P -> (1=1/\2=2) /\ (3=3 /\ (4=4 /\ 5=5) /\ 6=6) /\ 7=7. +intros. +split; split. (* current visible goals are [1=1, 2=2, 3=3/\(4=4/\5=5)/\6=6, 7=7] *) +Focus 3. (* focus on 3=3/\(4=4/\5=5)/\6=6; bg-before: [1=1, 2=2], bg-after: [7=7] *) +split; [ | split ]. (* current visible goals are [3=3, 4=4/\5=5, 6=6] *) +Focus 2. (* focus on 4=4/\5=5; bg-before: [3=3], bg-after: [6=6] *) +* (* focus again on 4=4/\5=5; bg-before: [], bg-after: [] *) +split. (* current visible goals are [4=4,5=5] *) +``` +should generate the following goals structure: +``` +goals: [ P|-4=4, P|-5=5 ] +background: +[ + ( [], [] ), (* bullet with one goal has no before or after background goals *) + ( [ P|-3=3 ], [ P|-6=6 ] ), (* Focus 2 *) + ( [ P|-2=2, P|-1=1 ], [ P|-7=7 ] ) (* Focus 3; notice that 1=1 and 2=2 are reversed *) +] +``` +Pseudocode for listing all of the goals in order: `rev (flat_map fst background) ++ goals ++ flat_map snd background`. + +* No goal: +```html + +``` + +------------------------------- + + +### **Status(force: bool)** +Returns information about the current proofs. CoqIDE typically sends this +message with `force = false` after each sentence, and with `force = true` if +the user wants to force the checking of all proofs (wheels button). In terms of +the STM API, `force` triggers a `Join`. +```html + +``` +#### *Returns* +* +```html + + ${path} + ${proofName} + ${allProofs} + ${proofNumber} + +``` + +------------------------------- + +### **Query(route_id: integer, query: string, stateId: integer)** + +`routeId` can be used to distinguish the result of a particular query, +`stateId` should be set to the state the query should be run. + +```html + + + + + ${query} + + + + +``` +#### *Returns* +* +```html + + ${message} + +``` + +Before 8.8, `Query` only executed the first command present in the +`query` string; starting with 8.8, the caller may include several +statements. This is useful for instance for temporarily setting an +option and then executing a command. + +------------------------------- + + + +### **Evars()** +```html + +``` +#### *Returns* +* +```html + + + +``` + +------------------------------- + + +### **Hints()** +```html + +``` +#### *Returns* +* +```html + + + +``` + +------------------------------- + + +### **Search([(constraintTypeN: string, constraintValueN: string, positiveConstraintN: boolean)])** +Searches for objects that satisfy a list of constraints. If `${positiveConstraint}` is `false`, then the constraint is inverted. +```html + + + + + ${constraintValue1} + + + + ... + + + + bool_rect + + + + + +``` +#### *Returns* +* +```html + + + + + ${metaInfo} + ... + + + ${name} + + ${definition} + + ... + + +``` +##### Types of constraints: +* Name pattern: `${constraintType} = "name_pattern"`; `${constraintValue}` is a regular expression string. +* Type pattern: `${constraintType} = "type_pattern"`; `${constraintValue}` is a pattern (???: an open gallina term) string. +* SubType pattern: `${constraintType} = "subtype_pattern"`; `${constraintValue}` is a pattern (???: an open gallina term) string. +* In module: `${constraintType} = "in_module"`; `${constraintValue}` is a list of strings specifying the module/directory structure. +* Include blacklist: `${constraintType} = "include_blacklist"`; `${constraintValue}` *is ommitted*. + +------------------------------- + + +### **GetOptions()** +```html + +``` +#### *Returns* +* +```html + + + + ${string1}... + + ${sync} + ${deprecated} + ${name} + ${option_value} + + + ... + + +``` + +------------------------------- + + +### **SetOptions(options)** +Sends a list of option settings, where each setting roughly looks like: +`([optionNamePart1, ..., optionNamePartN], value)`. +```html + + + + + optionNamePart1 + ... + optionNamePartN + + + + + + ... + + + + Printing + Width + + + + + + + +``` +CoqIDE sends the following settings (defaults in parentheses): +``` +Printing Width : (60), +Printing Coercions : (), +Printing Matching : (...true...) +Printing Notations : (...true...) +Printing Existential Instances : (...false...) +Printing Implicit : (...false...) +Printing All : (...false...) +Printing Universes : (...false...) +``` +#### *Returns* +* +```html + +``` + +------------------------------- + + +### **MkCases(...)** +```html +... +``` +#### *Returns* +* +```html + + + ${string1}... + ... + + +``` + +------------------------------- + + +### **StopWorker(worker: string)** +```html +${worker} +``` +#### *Returns* +* +```html + +``` + +------------------------------- + + +### **PrintAst(stateId: integer)** +```html + +``` +#### *Returns* +* +```html + + + + + + + + ... + ${token} + ... + + ... + + + ... + + +``` + +------------------------------- + + + +### **Annotate(annotation: string)** +```html +${annotation} +``` +#### *Returns* +* + +take `Theorem plus_0_r : forall n : nat, n + 0 = n.` as an example. + +```html + + + + Theorem +  plus_0_r :  + + forall +  n :  + nat + ,  + + + + + n + +  + +   + + 0 + + + +  = +   + + n + + + + + . + + +``` + +------------------------------- + +## Feedback messages + +Feedback messages are issued out-of-band, + giving updates on the current state of sentences/stateIds, + worker-thread status, etc. + +In the descriptions of feedback syntax below, wherever a `state_id` +tag may occur, there may instead be an `edit_id` tag. + +* Added Axiom: in response to `Axiom`, `admit`, `Admitted`, etc. +```html + + + + +``` +* Processing +```html + + + + ${workerName} + + +``` +* Processed +```html + + + + + +``` +* Incomplete +```html + + + + +``` +* Complete +* GlobRef +* Error. Issued, for example, when a processed tactic has failed or is unknown. +The error offsets may both be 0 if there is no particular syntax involved. +* InProgress +```html + + + + 1 + + +``` +* WorkerStatus +Ex: `workername = "proofworker:0"` +Ex: `status = "Idle"` or `status = "proof: myLemmaName"` or `status = "Dead"` +```html + + + + + ${workerName} + ${status} + + + +``` +* File Dependencies. Typically in response to a `Require`. Dependencies are *.vo files. + - State `stateId` directly depends on `dependency`: + ```html + + + + + + ``` + - State `stateId` depends on `dependency` via dependency `sourceDependency` + ```xml + + + + + ${dependency} + + + ``` +* File Loaded. For state `stateId`, module `module` is being loaded from `voFileName` +```xml + + + + ${module} + ${voFileName`} + + +``` + +* Message. `level` is one of `{info,warning,notice,error,debug}`. For example, in response to an add `"Axiom foo: nat."` with `verbose=true`, message `foo is assumed` will be emitted in response. +```xml + + + + + + ${message} + + + +``` + +* Custom. A feedback message that Coq plugins can use to return structured results, including results from Ltac profiling. Optionally, `startPos` and `stopPos` define a range of offsets in the document that the message refers to; otherwise, they will be 0. `customTag` is intended as a unique string that identifies what kind of payload is contained in `customXML`. +```xml + + + + + ${customTag} + ${customXML} + + +``` + -- cgit v1.2.3