diff options
Diffstat (limited to 'dev/doc')
| -rw-r--r-- | dev/doc/api.txt | 10 | ||||
| -rw-r--r-- | dev/doc/changes.txt | 178 | ||||
| -rw-r--r-- | dev/doc/debugging.txt | 4 | ||||
| -rw-r--r-- | dev/doc/proof-engine.md | 134 | ||||
| -rw-r--r-- | dev/doc/style.txt | 215 |
5 files changed, 465 insertions, 76 deletions
diff --git a/dev/doc/api.txt b/dev/doc/api.txt new file mode 100644 index 0000000000..5827257b53 --- /dev/null +++ b/dev/doc/api.txt @@ -0,0 +1,10 @@ +Recommendations in using the API: + +The type of terms: constr (see kernel/constr.ml and kernel/term.ml) + +- On type constr, the canonical equality on CIC (up to + alpha-conversion and cast removal) is Constr.equal +- The type constr is abstract, use mkRel, mkSort, etc. to build + elements in constr; use "kind_of_term" to analyze the head of a + constr; use destRel, destSort, etc. when the head constructor is + known diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 3de938d774..7f915b7819 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -1,4 +1,182 @@ ========================================= += CHANGES BETWEEN COQ V8.6 AND COQ V8.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` + +* ML API * + +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. + +** 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. + +** 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` 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`: + + 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. + +========================================= = CHANGES BETWEEN COQ V8.5 AND COQ V8.6 = ========================================= diff --git a/dev/doc/debugging.txt b/dev/doc/debugging.txt index f0df2fc371..79cde48849 100644 --- a/dev/doc/debugging.txt +++ b/dev/doc/debugging.txt @@ -51,8 +51,8 @@ Debugging from Caml debugger 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 + - If "source db" fails, do a "make printers" and try again (it should build + top_printers.cmo and the core cma files). Global gprof-based profiling ============================ diff --git a/dev/doc/proof-engine.md b/dev/doc/proof-engine.md new file mode 100644 index 0000000000..db69b08a20 --- /dev/null +++ b/dev/doc/proof-engine.md @@ -0,0 +1,134 @@ +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 : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic +(** In [refine ?unsafe 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 [unsafe] is [false] (default 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/style.txt b/dev/doc/style.txt index 27695a09b1..2ee3dadd77 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 |