diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/README | 3 | ||||
| -rw-r--r-- | dev/base_include | 2 | ||||
| -rw-r--r-- | dev/db | 3 | ||||
| -rw-r--r-- | dev/db_printers.ml | 2 | ||||
| -rw-r--r-- | dev/doc/README-V1-V5.asciidoc | 378 | ||||
| -rw-r--r-- | dev/doc/changes.txt | 85 | ||||
| -rw-r--r-- | dev/doc/coq-src-description.txt | 7 | ||||
| -rw-r--r-- | dev/doc/univpoly.txt | 50 | ||||
| -rw-r--r-- | dev/doc/versions-history.tex | 110 | ||||
| -rw-r--r-- | dev/header | 2 | ||||
| -rwxr-xr-x | dev/make-installer-win32.sh | 2 | ||||
| -rwxr-xr-x | dev/make-installer-win64.sh | 2 | ||||
| -rwxr-xr-x | dev/make-macos-dmg.sh | 35 | ||||
| -rwxr-xr-x | dev/nsis/coq.nsi | 6 | ||||
| -rw-r--r-- | dev/ocamldebug-coq.run | 2 | ||||
| -rwxr-xr-x | dev/ocamldoc/fix-ocamldoc-utf8 | 6 | ||||
| -rw-r--r-- | dev/ocamldoc/header.tex | 14 | ||||
| -rw-r--r-- | dev/printers.mllib | 36 | ||||
| -rw-r--r-- | dev/tools/Makefile.common | 0 | ||||
| -rw-r--r-- | dev/tools/anomaly-traces-parser.el | 28 | ||||
| -rw-r--r-- | dev/top_printers.ml | 31 | ||||
| -rw-r--r-- | dev/v8-syntax/memo-v8.tex | 2 | ||||
| -rw-r--r-- | dev/v8-syntax/syntax-v8.tex | 2 | ||||
| -rw-r--r-- | dev/vm_printers.ml | 9 |
24 files changed, 729 insertions, 88 deletions
diff --git a/dev/README b/dev/README index 5edf64c8f2..814f609576 100644 --- a/dev/README +++ b/dev/README @@ -45,3 +45,6 @@ Makefile.subdir: makefile dedicated to intensive work in a given subdirectory Makefile.devel: utilities to automatically launch coq in various states Makefile.common: used by other Makefiles objects.el: various development utilities at emacs level +anomaly-traces-parser.el: a .emacs-ready elisp snippet to parse + location of Anomaly backtraces and jump to them conveniently from + the Emacs *compilation* output. diff --git a/dev/base_include b/dev/base_include index 197528acdb..86f34b2ac9 100644 --- a/dev/base_include +++ b/dev/base_include @@ -17,6 +17,7 @@ #directory "grammar";; #directory "intf";; #directory "stm";; +#directory "ltac";; #directory "+camlp4";; (* lazy solution: add both of camlp4/5 so that *) #directory "+camlp5";; (* Gramext is found in top_printers.ml *) @@ -149,6 +150,7 @@ open Tactic_debug open Decl_proof_instr open Decl_mode +open Hints open Auto open Autorewrite open Contradiction @@ -1,5 +1,3 @@ -load_printer "gramlib.cma" -load_printer "str.cma" load_printer "printers.cma" install_printer Top_printers.ppfuture @@ -13,6 +11,7 @@ install_printer Top_printers.ppexistentialset install_printer Top_printers.ppintset install_printer Top_printers.pplab install_printer Top_printers.ppdir +install_printer Top_printers.ppmbid install_printer Top_printers.ppmp install_printer Top_printers.ppkn install_printer Top_printers.ppcon diff --git a/dev/db_printers.ml b/dev/db_printers.ml index e843bbc518..500595085e 100644 --- a/dev/db_printers.ml +++ b/dev/db_printers.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/dev/doc/README-V1-V5.asciidoc b/dev/doc/README-V1-V5.asciidoc new file mode 100644 index 0000000000..631fb92c97 --- /dev/null +++ b/dev/doc/README-V1-V5.asciidoc @@ -0,0 +1,378 @@ +Notes on the prehistory of Coq +============================== +:author: Thierry Coquand, Gérard Huet & Christine Paulin-Mohring +:revdate: September 2015 +:toc: +:toc-placement: preamble +:toclevels: 1 +:showtitle: + + +This document is a copy within the Coq archive of a document written +in September 2015 by Gérard Huet, Thierry Coquand and Christine Paulin +to accompany their public release of the archive of versions 1.10 to 6.2 +of Coq and of its CONSTR ancestor. CONSTR, then Coq, was designed and +implemented in the Formel team, joint between the INRIA Rocquencourt +laboratory and the Ecole Normale Supérieure of Paris, from 1984 +onwards. + +Version 1 +--------- + +This software is a prototype type-checker for a higher-order logical +formalism known as the Theory of Constructions, presented in his PhD +thesis by Thierry Coquand, with influences from Girard's system F and +de Bruijn's Automath. The metamathematical analysis of the system is +the PhD work of Thierry Coquand. The software is mostly the work of +Gérard Huet. Most of the mathematical examples verified with the +software are due to Thierry Coquand. + +The programming language of the CONSTR software (as it was called at +the time) was a version of ML adapted from the Edinburgh LCF system +and running on a LISP backend. The main improvements from the original +LCF ML were that ML was compiled rather than interpreted (Gérard Huet +building on the original translator by Lockwood Morris), and that it +was enriched by recursively defined types (work of Guy +Cousineau). This ancestor of CAML was used and improved by Larry +Paulson for his implementation of Cambridge LCF. + +Software developments of this prototype occurred from late 1983 to +early 1985. + +Version 1.10 was frozen on December 22nd 1984. It is the version used +for the examples in Thierry Coquand's thesis, defended on January 31st +1985. There was a unique binding operator, used both for universal +quantification (dependent product) at the level of types and +functional abstraction (λ) at the level of terms/proofs, in the manner +of Automath. Substitution (λ-reduction) was implemented using de +Bruijn's indexes. + +Version 1.11 was frozen on February 19th, 1985. It is the version used +for the examples in the paper: Th. Coquand, G. Huet. __Constructions: A +Higher Order Proof System for Mechanizing Mathematics__ <<CH85>>. + +Christine Paulin joined the team at this point, for her DEA research +internship. In her DEA memoir (August 1985) she presents developments +for the _lambo_ function – _lambo(f)(n)_ computes the minimal _m_ such +that _f(m)_ is greater than _n_, for _f_ an increasing integer +function, a challenge for constructive mathematics. She also encoded +the majority voting algorithm of Boyer and Moore. + +Version 2 +--------- + +The formal system, now renamed as the _Calculus of Constructions_, was +presented with a proof of consistency and comparisons with proof +systems of Per Martin Löf, Girard, and the Automath family of N. de +Bruijn, in the paper: T. Coquand and G. Huet. __The Calculus of +Constructions__ <<CH88>>. + +An abstraction of the software design, in the form of an abstract +machine for proof checking, and a fuller sequence of mathematical +developments was presented in: Th. Coquand, G. Huet. __Concepts +Mathématiques et Informatiques Formalisés dans le Calcul des +Constructions__<<CH87>>. + +Version 2.8 was frozen on December 16th, 1985, and served for +developing the exemples in the above papers. + +This calculus was then enriched in version 2.9 with a cumulative +hierarchy of universes. Universe levels were initially explicit +natural numbers. Another improvement was the possibility of automatic +synthesis of implicit type arguments, relieving the user of tedious +redundant declarations. + +Christine Paulin wrote an article __Algorithm development in the +Calculus of Constructions__ <<P86>>. Besides _lambo_ and _majority_, +she presents quicksort and a text formatting algorithm. + +Version 2.13 of the Calculus of Constructions with universes was +frozen on June 25th, 1986. + +A synthetic presentation of type theory along constructive lines with +ML algorithms was given by Gérard Huet in his May 1986 CMU course +notes _Formal Structures for Computation and Deduction_. Its chapter +_Induction and Recursion in the Theory of Constructions_ was presented +as an invited paper at the Joint Conference on Theory and Practice of +Software Development TAPSOFT’87 at Pise in March 1987, and published +as __Induction Principles Formalized in the Calculus of +Constructions__ <<H88>>. + +Version 3 +--------- + +This version saw the beginning of proof automation, with a search +algorithm inspired from PROLOG and the applicative logic programming +programs of the course notes _Formal structures for computation and +deduction_. The search algorithm was implemented in ML by Thierry +Coquand. The proof system could thus be used in two modes: proof +verification and proof synthesis, with tactics such as `AUTO`. + +The implementation language was now called CAML, for Categorical +Abstract Machine Language. It used as backend the LLM3 virtual machine +of Le Lisp by Jérôme Chailloux. The main developers of CAML were +Michel Mauny, Ascander Suarez and Pierre Weis. + +V3.1 was started in the summer of 1986, V3.2 was frozen at the end of +November 1986. V3.4 was developed in the first half of 1987. + +Thierry Coquand held a post-doctoral position in Cambrige University +in 1986-87, where he developed a variant implementation in SML, with +which he wrote some developments on fixpoints in Scott's domains. + +Version 4 +--------- + +This version saw the beginning of program extraction from proofs, with +two varieties of the type `Prop` of propositions, indicating +constructive intent. The proof extraction algorithms were implemented +by Christine Paulin-Mohring. + +V4.1 was frozen on July 24th, 1987. It had a first identified library +of mathematical developments (directory exemples), with libraries +Logic (containing impredicative encodings of intuitionistic logic and +algebraic primitives for booleans, natural numbers and list), `Peano` +developing second-order Peano arithmetic, `Arith` defining addition, +multiplication, euclidean division and factorial. Typical developments +were the Knaster-Tarski theorem and Newman's lemma from rewriting +theory. + +V4.2 was a joint development of a team consisting of Thierry Coquand, +Gérard Huet and Christine Paulin-Mohring. A file V4.2.log records the +log of changes. It was frozen on September 1987 as the last version +implemented in CAML 2.3, and V4.3 followed on CAML 2.5, a more stable +development system. + +V4.3 saw the first top-level of the system. Instead of evaluating +explicit quotations, the user could develop his mathematics in a +high-level language called the mathematical vernacular (following +Automath terminology). The user could develop files in the vernacular +notation (with .v extension) which were now separate from the `ml` +sources of the implementation. Gilles Dowek joined the team to +develop the vernacular language as his DEA internship research. + +A notion of sticky constant was introduced, in order to keep names of +lemmas when local hypotheses of proofs were discharged. This gave a +notion of global mathematical environment with local sections. + +Another significant practical change was that the system, originally +developped on the VAX central computer of our lab, was transferred on +SUN personal workstations, allowing a level of distributed +development. The extraction algorithm was modified, with three +annotations `Pos`, `Null` and `Typ` decorating the sorts `Prop` and +`Type`. + +Version 4.3 was frozen at the end of November 1987, and was +distributed to an early community of users (among those were Hugo +Herbelin and Loic Colson). + +V4.4 saw the first version of (encoded) inductive types. Now natural +numbers could be defined as: + +[source, coq] +Inductive NAT : Prop = O : NAT | Succ : NAT->NAT. + +These inductive types were encoded impredicatively in the calculus, +using a subsystem _rec_ due to Christine Paulin. V4.4 was frozen on +March 6th 1988. + +Version 4.5 was the first one to support inductive types and program +extraction. Its banner was _Calcul des Constructions avec +Réalisations et Synthèse_. The vernacular language was enriched to +accommodate extraction commands. + +The verification engine design was presented as: G. Huet. _The +Constructive Engine_. Version 4.5. Invited Conference, 2nd European +Symposium on Programming, Nancy, March 88. The final paper, +describing the V4.9 implementation, appeared in: A perspective in +Theoretical Computer Science, Commemorative Volume in memory of Gift +Siromoney, Ed. R. Narasimhan, World Scientific Publishing, 1989. + +Version 4.5 was demonstrated in June 1988 at the YoP Institute on +Logical Foundations of Functional Programming organized by Gérard Huet +at Austin, Texas. + +Version 4.6 was started during the summer of 1988. Its main +improvement was the complete rehaul of the proof synthesis engine by +Thierry Coquand, with a tree structure of goals. + +Its source code was communicated to Randy Pollack on September 2nd +1988. It evolved progressively into LEGO, proof system for Luo's +formalism of Extended Calculus of Constructions. + +The discharge tactic was modified by Gérard Huet to allow for +inter-dependencies in discharged lemmas. Christine Paulin improved the +inductive definition scheme in order to accommodate predicates of any +arity. + +Version 4.7 was started on September 6th, 1988. + +This version starts exploiting the CAML notion of module in order to +improve the modularity of the implementation. Now the term verifier is +identified as a proper module Machine, which the structure of its +internal data structures being hidden and thus accessible only through +the legitimate operations. This machine (the constructive engine) was +the trusted core of the implementation. The proof synthesis mechanism +was a separate proof term generator. Once a complete proof term was +synthesized with the help of tactics, it was entirely re-checked by +the engine. Thus there was no need to certify the tactics, and the +system took advantage of this fact by having tactics ignore the +universe levels, universe consistency check being relegated to the +final type-checking pass. This induced a certain puzzlement in early +users who saw, after a successful proof search, their `QED` followed +by silence, followed by a failure message due to a universe +inconsistency… + +The set of examples comprise set theory experiments by Hugo Herbelin, +and notably the Schroeder-Bernstein theorem. + +Version 4.8, started on October 8th, 1988, saw a major +re-implementation of the abstract syntax type `constr`, separating +variables of the formalism and metavariables denoting incomplete terms +managed by the search mechanism. A notion of level (with three values +`TYPE`, `OBJECT` and `PROOF`) is made explicit and a type judgement +clarifies the constructions, whose implementation is now fully +explicit. Structural equality is speeded up by using pointer equality, +yielding spectacular improvements. Thierry Coquand adapts the proof +synthesis to the new representation, and simplifies pattern matching +to first-order predicate calculus matching, with important performance +gain. + +A new representation of the universe hierarchy is then defined by +Gérard Huet. Universe levels are now implemented implicitly, through +a hidden graph of abstract levels constrained with an order relation. +Checking acyclicity of the graph insures well-foundedness of the +ordering, and thus consistency. This was documented in a memo _Adding +Type:Type to the Calculus of Constructions_ which was never published. + +The development version is released as a stable 4.8 at the end of +1988. + +Version 4.9 is released on March 1st 1989, with the new ``elastic'' +universe hierarchy. + +The spring of 1989 saw the first attempt at documenting the system +usage, with a number of papers describing the formalism: + +- _Metamathematical Investigations of a Calculus of Constructions_, by + Thierry Coquand <<C90>>, +- _Inductive definitions in the Calculus of Constructions_, by + Christine Paulin-Mohrin, +- _Extracting Fω's programs from proofs in the Calculus of + Constructions_, by Christine Paulin-Mohring <<P89>>, +- _The Constructive Engine_, by Gérard Huet <<H89>>, + +as well as a number of user guides: + +- _A short user's guide for the Constructions_ Version 4.10, by Gérard Huet +- _A Vernacular Syllabus_, by Gilles Dowek. +- _The Tactics Theorem Prover, User's guide_, Version 4.10, by Thierry + Coquand. + +Stable V4.10, released on May 1st, 1989, was then a mature system, +distributed with CAML V2.6. + +In the mean time, Thierry Coquand and Christine Paulin-Mohring had +been investigating how to add native inductive types to the Calculus +of Constructions, in the manner of Per Martin-Löf's Intuitionistic +Type Theory. The impredicative encoding had already been presented in: +F. Pfenning and C. Paulin-Mohring. __Inductively defined types in the +Calculus of Constructions__ <<PP90>>. An extension of the calculus +with primitive inductive types appeared in: Th. Coquand and +C. Paulin-Mohring. __Inductively defined types__ <<CP90>>. + +This led to the Calculus of Inductive Constructions, logical formalism +implemented in Versions 5 upward of the system, and documented in: +C. Paulin-Mohring. __Inductive Definitions in the System Coq - Rules +and Properties__ <<P93>>. + +The last version of CONSTR is Version 4.11, which was last distributed +in the spring of 1990. It was demonstrated at the first workshop of +the European Basic Research Action Logical Frameworks In Sophia +Antipolis in May 1990. + +At the end of 1989, Version 5.1 was started, and renamed as the system +Coq for the Calculus of Inductive Constructions. It was then ported to +the new stand-alone implementation of ML called Caml-light. + +In 1990 many changes occurred. Thierry Coquand left for Chalmers +University in Göteborg. Christine Paulin-Mohring took a CNRS +researcher position at the LIP laboratory of École Normale Supérieure +de Lyon. Project Formel was terminated, and gave rise to two teams: +Cristal at INRIA-Roquencourt, that continued developments in +functional programming with Caml-light then Ocaml, and Coq, continuing +the type theory research, with a joint team headed by Gérard Huet at +INRIA-Rocquencourt and Christine Paulin-Mohring at the LIP laboratory +of CNRS-ENS Lyon. + +Chetan Murthy joined the team in 1991 and became the main software +architect of Version 5. He completely rehauled the implementation for +efficiency. Versions 5.6 and 5.8 were major distributed versions, +with complete documentation and a library of users' developements. The +use of the RCS revision control system, and systematic ChangeLog +files, allow a more precise tracking of the software developments. + +Developments from Version 6 upwards are documented in the credits +section of Coq's Reference Manual. + +==== +September 2015 + +Thierry Coquand, Gérard Huet and Christine Paulin-Mohring. +==== + +[bibliography] +.Bibliographic references + +- [[[CH85]]] Th. Coquand, G. Huet. _Constructions: A Higher Order + Proof System for Mechanizing Mathematics_. Invited paper, EUROCAL85, + April 1985, Linz, Austria. Springer Verlag LNCS 203, pp. 151-184. + +- [[[CH88]]] T. Coquand and G. Huet. _The Calculus of Constructions_. + Submitted on June 30th 1985, accepted on December 5th, 1985, + Information and Computation. Preprint as Rapport de Recherche Inria + n°530, Mai 1986. Final version in Information and Computation + 76,2/3, Feb. 88. + +- [[[CH87]]] Th. Coquand, G. Huet. _Concepts Mathématiques et + Informatiques Formalisés dans le Calcul des Constructions_. Invited + paper, European Logic Colloquium, Orsay, July 1985. Preprint as + Rapport de recherche INRIA n°463, Dec. 85. Published in Logic + Colloquium 1985, North-Holland, 1987. + +- [[[P86]]] C. Paulin. _Algorithm development in the Calculus of + Constructions_, preprint as Rapport de recherche INRIA n°497, + March 86. Final version in Proceedings Symposium on Logic in Computer + Science, Cambridge, MA, 1986 (IEEE Computer Society Press). + +- [[[H88]]] G. Huet. _Induction Principles Formalized in the Calculus + of Constructions_ in Programming of Future Generation Computers, + Ed. K. Fuchi and M. Nivat, North-Holland, 1988. + +- [[[C90]]] Th. Coquand. _Metamathematical Investigations of a + Calculus of Constructions_, by INRIA Research Report N°1088, + Sept. 1989, published in Logic and Computer Science, + ed. P.G. Odifreddi, Academic Press, 1990. + +- [[[P89]]] C. Paulin. _Extracting F ω's programs from proofs in the + calculus of constructions_. 16th Annual ACM Symposium on Principles + of Programming Languages, Austin. 1989. + +- [[[H89]]] G. Huet. _The constructive engine_. A perspective in + Theoretical Computer Science. Commemorative Volume for Gift + Siromoney. World Scientific Publishing (1989). + +- [[[PP90]]] F. Pfenning and C. Paulin-Mohring. _Inductively defined + types in the Calculus of Constructions_. Preprint technical report + CMU-CS-89-209, final version in Proceedings of Mathematical + Foundations of Programming Semantics, volume 442, Lecture Notes in + Computer Science. Springer-Verlag, 1990 + +- [[[CP90]]] Th. Coquand and C. Paulin-Mohring. _Inductively defined + types_. In P. Martin-Löf and G. Mints, editors, Proceedings of + Colog'88, volume 417, Lecture Notes in Computer Science. + Springer-Verlag, 1990. + +- [[[P93]]] C. Paulin-Mohring. _Inductive Definitions in the System + Coq - Rules and Properties_. In M. Bezem and J.-F. Groote, editors, + Proceedings of the conference Typed Lambda Calculi and Applications, + volume 664, Lecture Notes in Computer Science, 1993. diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 2f62be9aff..2f631c6338 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -1,5 +1,88 @@ ========================================= -= CHANGES BETWEEN COQ V8.4 AND CQQ V8.5 = += CHANGES BETWEEN COQ V8.5 AND COQ V8.6 = +========================================= + +- 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.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.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. + +- 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. + +========================================= += CHANGES BETWEEN COQ V8.4 AND COQ V8.5 = ========================================= ** Refactoring : more mli interfaces and simpler grammar.cma ** diff --git a/dev/doc/coq-src-description.txt b/dev/doc/coq-src-description.txt index fe896d3160..00e7f5c53c 100644 --- a/dev/doc/coq-src-description.txt +++ b/dev/doc/coq-src-description.txt @@ -19,13 +19,6 @@ highparsing : Files in parsing/ that cannot be linked too early. Contains the grammar rules g_*.ml4 -hightactics : - - Files in tactics/ that cannot be linked too early. - These are the .ml4 files that uses the EXTEND possibilities - provided by grammar.cma, for instance eauto.ml4. - - Special components ------------------ diff --git a/dev/doc/univpoly.txt b/dev/doc/univpoly.txt index 4c89af01db..6a69c57934 100644 --- a/dev/doc/univpoly.txt +++ b/dev/doc/univpoly.txt @@ -1,5 +1,5 @@ -Notes on universe polymorphism and primitive projections, M. Sozeau - WIP -========================================================================= +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 @@ -46,15 +46,16 @@ 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 hance two conversion functions now: check_conv -and infer_conv: the former just checks the definition in the current env +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 +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 again, module subtyping needs it. +but currently module subtyping needs it. Inference of universes is now done during refinement, and the evar_map -carries the incrementally built universe context. [Evd.conversion] is a +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 @@ -72,7 +73,7 @@ val pf_constr_of_global : Globnames.global_reference -> (constr -> tactic) -> ta 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 it's universes. Typically, using: +of keeping track of its universes. Typically, using: mkApp (coq_id_function, [| A; a |]) @@ -81,11 +82,11 @@ 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 now from an invariant that no new constraint would +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 might -forget constraints. +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. @@ -157,6 +158,30 @@ 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 =========== @@ -208,8 +233,7 @@ 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] is untested: it should deal with primitive -projections right but not universes. +- [native_compute] works with universes and projections. Incompatibilities diff --git a/dev/doc/versions-history.tex b/dev/doc/versions-history.tex index 9892a4419f..492e75a7bb 100644 --- a/dev/doc/versions-history.tex +++ b/dev/doc/versions-history.tex @@ -10,55 +10,76 @@ \begin{center} \begin{huge} -An history of Coq versions +A history of Coq versions \end{huge} \end{center} \bigskip \centerline{\large 1984-1989: The Calculus of Constructions} + +\bigskip +\centerline{\large (see README.V1-V5 for details)} \mbox{}\\ \mbox{}\\ \begin{tabular}{l|l|l} version & date & comments \\ \hline -CoC V1.10& mention of dates from 6 December & implementation language is Caml\\ - & 1984 to 13 February 1985 \\ -CoC V1.11& mention of dates from 6 December\\ - & 1984 to 19 February 1985\\ +CONSTR V1.10& mention of dates from 6 December & \feature{type-checker for Coquand's Calculus }\\ + & 1984 to 13 February 1985 & \feature{of Constructions}, implementation \\ + & frozen 22 December 1984 & language is a predecessor of CAML\\ + +CONSTR V1.11& mention of dates from 6 December\\ + & 1984 to 19 February 1985 (freeze date) &\\ + +CoC V2.8& dated 16 December 1985 (freeze date)\\ -CoC V2.13& dated 16 December 1985\\ +CoC V2.9& & \feature{cumulative hierarchy of universes}\\ -CoC V2.13& dated 25 June 1986\\ +CoC V2.13& dated 25 June 1986 (freeze date)\\ -CoC V3.1& dated 20 November 1986 & \feature{auto}\\ +CoC V3.1& started summer 1986 & \feature{AUTO tactic}\\ + & dated 20 November 1986 & implementation language now named CAML\\ CoC V3.2& dated 27 November 1986\\ -CoC V3.3 and V3.4& dated 1 January 1987 & creation of a directory for examples\\ +CoC V3.3& dated 1 January 1987 & creation of a directory for examples\\ -CoC V4.1& dated 24 July 1987\\ +CoC V3.4& dated 1 January 1987 & \feature{lambda and product distinguished in the syntax}\\ + +CoC V4.1& dated 24 July 1987 (freeze date)\\ CoC V4.2& dated 10 September 1987\\ -CoC V4.3& dated 15 September 1987\\ +CoC V4.3& dated 15 September 1987 & \feature{mathematical vernacular toplevel}\\ + & frozen November 1987 & \feature{section mechanism}\\ + & & \feature{logical vs computational content (sorte Spec)}\\ + & & \feature{LCF engine}\\ + +CoC V4.4& dated 27 January 1988 & \feature{impredicatively encoded inductive types}\\ + & frozen March 1988\\ -CoC V4.4& dated 27 January 1988\\ +CoC V4.5 and V4.5.5& dated 15 March 1988 & \feature{program extraction}\\ + & demonstrated in June 1988\\ -CoC V4.5 and V4.5.5& dated 15 March 1988\\ +CoC V4.6& dated 1 September 1988 & start of LEGO fork\\ -CoC V4.6 and V4.7& dated 1 September 1988\\ +CoC V4.7& started 6 September 1988 \\ -CoC V4.8& dated 1 December 1988\\ +CoC V4.8& dated 1 December 1988 (release time) & \feature{floating universes}\\ -CoC V4.8.5& dated 1 February 1989\\ +CoC V4.8.5& dated 1 February 1989 & \\ -CoC V4.9& dated 1 March 1989\\ +CoC V4.9& dated 1 March 1989 (release date)\\ -CoC V4.10 and 4.10.1& dated 1 May 1989 & first public release - in English\\ +CoC V4.10 and 4.10.1& dated 1 May 1989 & released with documentation in English\\ \end{tabular} \bigskip + +\noindent Note: CoC above stands as an abbreviation for {\em Calculus of + Constructions}, official name of the system. +\bigskip \bigskip \newpage @@ -80,7 +101,7 @@ Coq V5.2 & log dated 4 October 1990 & internal use \\ Coq V5.3 & log dated 12 October 1990 & internal use \\ -Coq V5.4 & headers dated 24 October 1990 & internal use, \feature{extraction} (version 1) [3-12-90]\\ +Coq V5.4 & headers dated 24 October 1990 & internal use, new \feature{extraction} (version 1) [3-12-90]\\ Coq V5.5 & started 6 December 1990 & internal use \\ @@ -202,6 +223,7 @@ version & date & comments \\ Coq ``V6'' archive & 20 March 1996 & new cvs repository on pauillac.inria.fr with code ported \\ & & to Caml Special Light (to later become Objective Caml)\\ & & has implicit arguments and coercions\\ + & & has coinductive types\\ Coq V6.1beta& released 18 November 1996 & \feature{coercions} [23-5-1996], \feature{user-level implicit arguments} [23-5-1996]\\ & & \feature{omega} [10-9-1996] \\ @@ -265,7 +287,17 @@ Coq V7.3.1& released 5 October 2002 & \feature{module system} [2-8-2002]\\ & & \feature{pattern-matching compilation} (version 2) [13-6-2002]\\ Coq V7.4& released 6 February 2003 & \feature{notation}, \feature{scopes} [13-10-2002]\\ +\end{tabular} +\medskip +\bigskip + +\centerline{V- New concrete syntax} +\mbox{}\\ +\mbox{}\\ +\begin{tabular}{l|l|l} +version & date & comments \\ +\hline Coq V8.0& released 21 April 2004 & \feature{new concrete syntax}, \feature{Set predicative}, \feature{CoqIDE} [from 4-2-2003]\\ Coq V8.0pl1& released 18 July 2004\\ @@ -307,6 +339,46 @@ Coq V8.2 & released 17 February 2009 & \feature{type classes} [10-12-2007], \fea & & a first package released on February 11 was incomplete\\ +Coq V8.2pl1& released 4 July 2009 & \\ +Coq V8.2pl2& released 29 June 2010 & \\ +\end{tabular} + +\medskip +\bigskip + +\newpage +\mbox{}\\ +\mbox{}\\ +\begin{tabular}{l|l|l} +Coq V8.3 beta & released 16 February 2010 & \feature{MSets library} [13-10-2009] \\ +Coq V8.3 & released 14 October 2010 & \feature{nsatz} [3-6-2010] \\ +Coq V8.3pl1& released 23 December 2010 & \\ +Coq V8.3pl2& released 19 April 2011 & \\ +Coq V8.3pl3& released 19 December 2011 & \\ +Coq V8.3pl3& released 26 March 2012 & \\ +Coq V8.3pl5& released 28 September 2012 & \\ +Coq V8.4 beta & released 27 December 2011 & \feature{modular arithmetic library} [2010-2012]\\ +&& \feature{vector library} [10-12-2010]\\ +&& \feature{structured scripts} [22-4-2010]\\ +&& \feature{eta-conversion} [20-9-2010]\\ +&& \feature{new proof engine available} [10-12-2010]\\ +Coq V8.4 beta2 & released 21 May 2012 & \\ +Coq V8.4 & released 12 August 2012 &\\ +Coq V8.4pl1& released 22 December 2012 & \\ +Coq V8.4pl2& released 4 April 2013 & \\ +Coq V8.4pl3& released 21 December 2013 & \\ +Coq V8.4pl4& released 24 April 2014 & \\ +Coq V8.4pl5& released 22 October 2014 & \\ +Coq V8.4pl6& released 9 April 2015 & \\ + +Coq V8.5 beta1 & released 21 January 2015 & \feature{computation via compilation to OCaml} [22-1-2013]\\ +&& \feature{asynchonous evaluation} [8-8-2013]\\ +&& \feature{new proof engine deployed} [2-11-2013]\\ +&& \feature{universe polymorphism} [6-5-2014]\\ +&& \feature{primitive projections} [6-5-2014]\\ + +Coq V8.5 beta2 & released 22 April 2015 & \feature{MMaps library} [4-3-2015]\\ + \end{tabular} \medskip diff --git a/dev/header b/dev/header index e5184df31c..4132051791 100644 --- a/dev/header +++ b/dev/header @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/dev/make-installer-win32.sh b/dev/make-installer-win32.sh index d405e66cc0..51d428dd1e 100755 --- a/dev/make-installer-win32.sh +++ b/dev/make-installer-win32.sh @@ -16,7 +16,7 @@ if [ ! -e bin/make.exe ]; then fi VERSION=`grep ^VERSION= config/Makefile | cut -d = -f 2` cd dev/nsis -"$NSIS" -DVERSION=$VERSION -DGTK_RUNTIME="`cygpath -w $BASE`" coq.nsi +"$NSIS" -DVERSION=$VERSION -DGTK_RUNTIME="`cygpath -w $BASE`" -DARCH="win32" coq.nsi echo Installer: ls -h $PWD/*exe cd ../.. diff --git a/dev/make-installer-win64.sh b/dev/make-installer-win64.sh index 2f765c1a10..438f4ae5b7 100755 --- a/dev/make-installer-win64.sh +++ b/dev/make-installer-win64.sh @@ -22,7 +22,7 @@ if [ ! -e bin/make.exe ]; then fi VERSION=`grep ^VERSION= config/Makefile | cut -d = -f 2` cd dev/nsis -"$NSIS" -DVERSION=$VERSION -DGTK_RUNTIME="`cygpath -w $BASE`" coq.nsi +"$NSIS" -DVERSION=$VERSION -DGTK_RUNTIME="`cygpath -w $BASE`" -DARCH="win64" coq.nsi echo Installer: ls -h $PWD/*exe cd ../.. diff --git a/dev/make-macos-dmg.sh b/dev/make-macos-dmg.sh new file mode 100755 index 0000000000..b43ada9076 --- /dev/null +++ b/dev/make-macos-dmg.sh @@ -0,0 +1,35 @@ +#!/bin/bash + +# Fail on first error +set -e + +# Configuration setup +eval `opam config env` +make distclean +OUTDIR=$PWD/_install +DMGDIR=$PWD/_dmg +./configure -debug -prefix $OUTDIR -native-compiler no +VERSION=$(sed -n -e '/^let coq_version/ s/^[^"]*"\([^"]*\)"$/\1/p' configure.ml) +APP=bin/CoqIDE_${VERSION}.app + +# Create a .app file with CoqIDE +~/.local/bin/jhbuild run make -j -l2 $APP + +# Build Coq and run test-suite +make && make check + +# Add Coq to the .app file +make OLDROOT=$OUTDIR COQINSTALLPREFIX=$APP/Contents/Resources/ install-coq install-ide-toploop + +# Sign the .app file +codesign -f -s - $APP + +# Create the dmg bundle +mkdir -p $DMGDIR +ln -sf /Applications $DMGDIR/Applications +cp -r $APP $DMGDIR + +# Temporary countermeasure to hdiutil error 5341 +head -c9703424 /dev/urandom > $DMGDIR/.padding + +hdiutil create -imagekey zlib-level=9 -volname CoqIDE_$VERSION -srcfolder $DMGDIR -ov -format UDZO CoqIDE_$VERSION.dmg diff --git a/dev/nsis/coq.nsi b/dev/nsis/coq.nsi index 5b421e49dd..e1052b1e1b 100755 --- a/dev/nsis/coq.nsi +++ b/dev/nsis/coq.nsi @@ -13,7 +13,7 @@ SetCompressor lzma !define MY_PRODUCT "Coq" ;Define your own software name here !define COQ_SRC_PATH "..\.." -!define OUTFILE "coq-installer-${VERSION}.exe" +!define OUTFILE "coq-installer-${VERSION}-${ARCH}.exe" !include "MUI2.nsh" !include "FileAssociation.nsh" @@ -95,8 +95,8 @@ Section "Coq" Sec1 File /r ${COQ_SRC_PATH}\theories\*.vo File /r ${COQ_SRC_PATH}\theories\*.v File /r ${COQ_SRC_PATH}\theories\*.glob - File /r ${COQ_SRC_PATH}\theories\*.cmi - File /r ${COQ_SRC_PATH}\theories\*.cmxs + ; File /r ${COQ_SRC_PATH}\theories\*.cmi + ; File /r ${COQ_SRC_PATH}\theories\*.cmxs SetOutPath "$INSTDIR\lib\plugins" File /r ${COQ_SRC_PATH}\plugins\*.vo File /r ${COQ_SRC_PATH}\plugins\*.v diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run index b00d084edb..f9310e076a 100644 --- a/dev/ocamldebug-coq.run +++ b/dev/ocamldebug-coq.run @@ -20,7 +20,7 @@ exec $OCAMLDEBUG \ -I $COQTOP/library -I $COQTOP/engine \ -I $COQTOP/pretyping -I $COQTOP/parsing \ -I $COQTOP/interp -I $COQTOP/proofs -I $COQTOP/tactics -I $COQTOP/stm \ - -I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config \ + -I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config -I $COQTOP/ltac \ -I $COQTOP/plugins/cc -I $COQTOP/plugins/dp \ -I $COQTOP/plugins/extraction -I $COQTOP/plugins/field \ -I $COQTOP/plugins/firstorder -I $COQTOP/plugins/fourier \ diff --git a/dev/ocamldoc/fix-ocamldoc-utf8 b/dev/ocamldoc/fix-ocamldoc-utf8 new file mode 100755 index 0000000000..fe2e0c1155 --- /dev/null +++ b/dev/ocamldoc/fix-ocamldoc-utf8 @@ -0,0 +1,6 @@ +#!/bin/sh + +# This reverts automatic translation of latin1 accentuated letters by ocamldoc +# Usage: fix-ocamldoc-utf8 file + +sed -i -e 's/\\`a/\d224/g' -e "s/\\\^a/\d226/g" -e "s/\\\'e/\d233/g" -e 's/\\`e/\d232/g' -e "s/\\\^e/\d234/g" -e 's/\\\"e/\d235/g' -e "s/\\\^o/\d244/g" -e 's/\\\"o/\d246/g' -e "s/\\\^i/\d238/g" -e 's/\\\"i/\d239/g' -e 's/\\`u/\d249/g' -e "s/\\\^u/\d251/g" -e "s/\\\c{c}/\d231/g" $1 diff --git a/dev/ocamldoc/header.tex b/dev/ocamldoc/header.tex new file mode 100644 index 0000000000..4091f8144f --- /dev/null +++ b/dev/ocamldoc/header.tex @@ -0,0 +1,14 @@ +\documentclass[11pt]{article} +\usepackage[utf8x]{inputenc} +\usepackage[T1]{fontenc} +\usepackage{textcomp} +\usepackage{tipa} +\usepackage{textgreek} +\usepackage{fullpage} +\usepackage{url} +\usepackage{ocamldoc} +\title{Coq mlis documentation} +\begin{document} +\maketitle +\tableofcontents +\vspace{0.2cm} diff --git a/dev/printers.mllib b/dev/printers.mllib index 07b48ed573..9f25ba55e7 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -8,6 +8,7 @@ Hashcons CSet CMap Int +Dyn HMap Option Store @@ -16,6 +17,9 @@ Backtrace IStream Pp_control Loc +CList +CString +Tok Compat Flags Control @@ -28,15 +32,12 @@ Segmenttree Unicodetable Unicode CObj -CList -CString CArray CStack Util Ppstyle Errors Bigint -Dyn CUnix System Envars @@ -48,13 +49,14 @@ Rtree Heap Genarg Stateid -Ephemeron +CEphemeron Future RemoteCounter Monad Names Univ +UGraph Esubst Uint31 Sorts @@ -116,17 +118,21 @@ Miscops Universes Termops Namegen +UState Evd +Sigma Glob_ops Redops +Pretype_errors +Evarutil Reductionops Inductiveops Arguments_renaming Nativenorm Retyping Cbv -Pretype_errors -Evarutil + +Evardefine Evarsolve Recordops Evarconv @@ -137,6 +143,9 @@ Find_subterm Tacred Classops Typeclasses_errors +Logic_monad +Proofview_monad +Proofview Typeclasses Detyping Indrec @@ -150,7 +159,6 @@ Library States Genprint -Tok Lexer Ppextend Pputils @@ -160,18 +168,17 @@ Constrarg Constrexpr_ops Genintern Notation_ops -Topconstr Notation Dumpglob +Syntax_def +Smartlocate +Topconstr Reserve Impargs -Syntax_def Implicit_quantifiers -Smartlocate Constrintern Modintern Constrextern -Proof_type Goal Miscprint Logic @@ -179,15 +186,13 @@ Refiner Clenv Evar_refiner Proof_errors -Logic_monad -Proofview_monad -Proofview +Refine Proof Proof_global Pfedit -Tactic_debug Decl_mode Ppconstr +Entry Pcoq Printer Pptactic @@ -195,7 +200,6 @@ Ppdecl_proof Egramml Egramcoq Tacsubst -Tacenv Trie Dn Btermdn diff --git a/dev/tools/Makefile.common b/dev/tools/Makefile.common deleted file mode 100644 index e69de29bb2..0000000000 --- a/dev/tools/Makefile.common +++ /dev/null diff --git a/dev/tools/anomaly-traces-parser.el b/dev/tools/anomaly-traces-parser.el new file mode 100644 index 0000000000..68f54266f9 --- /dev/null +++ b/dev/tools/anomaly-traces-parser.el @@ -0,0 +1,28 @@ +;; This Elisp snippet adds a regexp parser for the format of Anomaly +;; backtraces (coqc -bt ...), to the error parser of the Compilation +;; mode (C-c C-c: "Compile command: ..."). Once the +;; coq-change-error-alist-for-backtraces function has run, file +;; locations in traces are recognized and can be jumped from easily +;; from the *compilation* buffer. + +;; You can just copy everything below to your .emacs and this will be +;; enabled from any compilation command launched from an OCaml file. + +(defun coq-change-error-alist-for-backtraces () + "Hook to change the compilation-error-regexp-alist variable, to + search the coq backtraces for error locations" + (interactive) + (add-to-list + 'compilation-error-regexp-alist-alist + '(coq-backtrace + "^ *\\(?:raise\\|frame\\) @ file \\(\"?\\)\\([^,\" \n\t<>]+\\)\\1,\ + lines? \\([0-9]+\\)-?\\([0-9]+\\)?\\(?:$\\|,\ + \\(?: characters? \\([0-9]+\\)-?\\([0-9]+\\)?:?\\)?\\)" + 2 (3 . 4) (5 . 6))) + (add-to-list 'compilation-error-regexp-alist 'coq-backtrace)) + +;; this Anomaly parser should be available when one is hacking +;; on the *OCaml* code of Coq (adding bugs), so we enable it +;; through the OCaml mode hooks. +(add-hook 'caml-mode-hook 'coq-change-error-alist-for-backtraces) +(add-hook 'tuareg-mode-hook 'coq-change-error-alist-for-backtraces) diff --git a/dev/top_printers.ml b/dev/top_printers.ml index f9f2e1b09e..29ea08e025 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -40,10 +40,10 @@ let ppid id = pp (pr_id id) let pplab l = pp (pr_lab l) let ppmbid mbid = pp (str (MBId.debug_to_string mbid)) let ppdir dir = pp (pr_dirpath dir) -let ppmp mp = pp(str (string_of_mp mp)) +let ppmp mp = pp(str (ModPath.debug_to_string mp)) let ppcon con = pp(debug_pr_con con) let ppproj con = pp(debug_pr_con (Projection.constant con)) -let ppkn kn = pp(pr_kn kn) +let ppkn kn = pp(str (KerName.to_string kn)) let ppmind kn = pp(debug_pr_mind kn) let ppind (kn,i) = pp(debug_pr_mind kn ++ str"," ++int i) let ppsp sp = pp(pr_path sp) @@ -221,7 +221,7 @@ let ppuniverseconstraints c = pp (Universes.Constraints.pr c) let ppuniverse_context_future c = let ctx = Future.force c in ppuniverse_context ctx -let ppuniverses u = pp (Univ.pr_universes Level.pr u) +let ppuniverses u = pp (UGraph.pr_universes Level.pr u) let ppnamedcontextval e = pp (pr_named_context (Global.env ()) Evd.empty (named_context_of_val e)) @@ -467,12 +467,13 @@ let pp_generic_argument arg = pp(str"<genarg:"++pr_argument_type(genarg_tag arg)++str">") let prgenarginfo arg = - let tpe = pr_argument_type (genarg_tag arg) in - let pr_gtac _ x = Pptactic.pr_glob_tactic (Global.env()) x in - try - let data = Pptactic.pr_top_generic pr_constr pr_lconstr pr_gtac pr_constr_pattern arg in - str "<genarg:" ++ tpe ++ str " := [ " ++ data ++ str " ] >" - with _any -> + let Val.Dyn (tag, _) = arg in + let tpe = Val.pr tag in + (** FIXME *) +(* try *) +(* let data = Pptactic.pr_top_generic (Global.env ()) arg in *) +(* str "<genarg:" ++ tpe ++ str " := [ " ++ data ++ str " ] >" *) +(* with _any -> *) str "<genarg:" ++ tpe ++ str ">" let ppgenarginfo arg = pp (prgenarginfo arg) @@ -509,7 +510,7 @@ let _ = try Vernacinterp.vinterp_add false ("PrintConstr", 0) (function - [c] when genarg_tag c = ConstrArgType && true -> + [c] when genarg_tag c = unquote (topwit wit_constr) && true -> let c = out_gen (rawwit wit_constr) c in (fun () -> in_current_context constr_display c) | _ -> failwith "Vernac extension: cannot occur") @@ -519,14 +520,13 @@ let _ = extend_vernac_command_grammar ("PrintConstr", 0) None [GramTerminal "PrintConstr"; GramNonTerminal - (Loc.ghost,ConstrArgType,Aentry ("constr","constr"), - Some (Names.Id.of_string "c"))] + (Loc.ghost,rawwit wit_constr,Extend.Aentry (Pcoq.name_of_entry Pcoq.Constr.constr))] let _ = try Vernacinterp.vinterp_add false ("PrintPureConstr", 0) (function - [c] when genarg_tag c = ConstrArgType && true -> + [c] when genarg_tag c = unquote (topwit wit_constr) && true -> let c = out_gen (rawwit wit_constr) c in (fun () -> in_current_context print_pure_constr c) | _ -> failwith "Vernac extension: cannot occur") @@ -536,8 +536,7 @@ let _ = extend_vernac_command_grammar ("PrintPureConstr", 0) None [GramTerminal "PrintPureConstr"; GramNonTerminal - (Loc.ghost,ConstrArgType,Aentry ("constr","constr"), - Some (Names.Id.of_string "c"))] + (Loc.ghost,rawwit wit_constr,Extend.Aentry (Pcoq.name_of_entry Pcoq.Constr.constr))] (* Setting printer of unbound global reference *) open Names diff --git a/dev/v8-syntax/memo-v8.tex b/dev/v8-syntax/memo-v8.tex index 8d116de26f..ae4b569b36 100644 --- a/dev/v8-syntax/memo-v8.tex +++ b/dev/v8-syntax/memo-v8.tex @@ -253,7 +253,7 @@ became \TERM{context}. Syntax is unified with subterm matching. \subsection{Occurrences} To avoid ambiguity between a numeric literal and the optionnal -occurence numbers of this term, the occurence numbers are put after +occurrence numbers of this term, the occurrence numbers are put after the term itself. This applies to tactic \TERM{pattern} and also \TERM{unfold} \begin{transbox} diff --git a/dev/v8-syntax/syntax-v8.tex b/dev/v8-syntax/syntax-v8.tex index 6630be06ab..64431ea161 100644 --- a/dev/v8-syntax/syntax-v8.tex +++ b/dev/v8-syntax/syntax-v8.tex @@ -81,7 +81,7 @@ Parenthesis are used to group regexps. Beware to distinguish this operator $\GR{~}$ from the terminals $\ETERM{( )}$, and $\mid$ from terminal \TERMbar. -Rules are optionaly annotated in the right margin with: +Rules are optionally annotated in the right margin with: \begin{itemize} \item a precedence and associativity (L for left, R for right and N for no associativity), indicating how to solve conflicts; lower levels are tighter; diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml index 3d688011c2..1c501df808 100644 --- a/dev/vm_printers.ml +++ b/dev/vm_printers.ml @@ -13,7 +13,7 @@ let ppripos (ri,pos) = ("annot : MutInd("^(string_of_mind sp)^","^(string_of_int i)^")\n") | Reloc_const _ -> print_string "structured constant\n" - | Reloc_getglobal (kn,_) -> + | Reloc_getglobal kn -> print_string ("getglob "^(string_of_con kn)^"\n")); print_flush () @@ -30,7 +30,7 @@ let ppsort = function let print_idkey idk = match idk with - | ConstKey (sp,_) -> + | ConstKey sp -> print_string "Cons("; print_string (string_of_con sp); print_string ")" @@ -61,8 +61,8 @@ and ppstack s = and ppatom a = match a with | Aid idk -> print_idkey idk - | Aiddef(idk,_) -> print_string "&";print_idkey idk - | Aind((sp,i),_) -> print_string "Ind("; + | Atype u -> print_string "Type(...)" + | Aind(sp,i) -> print_string "Ind("; print_string (string_of_mind sp); print_string ","; print_int i; print_string ")" @@ -79,6 +79,7 @@ and ppwhd whd = | Vatom_stk(a,s) -> open_hbox();ppatom a;close_box(); print_string"@";ppstack s + | Vuniv_level lvl -> Pp.pp (Univ.Level.pr lvl) and ppvblock b = open_hbox(); |