diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 18:33:25 +0100 |
commit | 1b92c226e563643da187b8614d5888dc4855eb43 (patch) | |
tree | c4c3d204b36468b58cb71050ba95f06b8dd7bc2e /dev/doc | |
parent | 7c9b0a702976078b813e6493c1284af62a3f093c (diff) |
Imported Upstream version 8.6
Diffstat (limited to 'dev/doc')
-rw-r--r-- | dev/doc/README-V1-V5 | 296 | ||||
-rw-r--r-- | dev/doc/README-V1-V5.asciidoc | 378 | ||||
-rw-r--r-- | dev/doc/build-system.dev.txt | 34 | ||||
-rw-r--r-- | dev/doc/build-system.txt | 15 | ||||
-rw-r--r-- | dev/doc/changes.txt | 278 | ||||
-rw-r--r-- | dev/doc/coq-src-description.txt | 7 | ||||
-rw-r--r-- | dev/doc/drop.txt | 44 | ||||
-rw-r--r-- | dev/doc/notes-on-conversion | 2 | ||||
-rw-r--r-- | dev/doc/ocamlbuild.txt | 30 | ||||
-rw-r--r-- | dev/doc/profiling.txt | 76 | ||||
-rw-r--r-- | dev/doc/setup.txt | 289 |
11 files changed, 1117 insertions, 332 deletions
diff --git a/dev/doc/README-V1-V5 b/dev/doc/README-V1-V5 deleted file mode 100644 index ebbc0577..00000000 --- a/dev/doc/README-V1-V5 +++ /dev/null @@ -1,296 +0,0 @@ - - Notes on the prehistory of Coq - -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) -is a version of ML issued from the Edinburgh LCF system and running on -a LISP backend. The main improvements from the original LCF ML are that ML -is compiled rather than interpreted (Gérard Huet building on the original -translator by Lockwood Morris), and that it is 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 (lambda) -at the level of terms/proofs, in the manner of Automath. Substitution -(lambda 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. Invited paper, EUROCAL85, April 1985, Linz, Austria. Springer Verlag -LNCS 203, pp. 151-184. - -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 -computing 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. -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. - -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. 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. - -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", 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). 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" in -Programming of Future Generation Computers, Ed. K. Fuchi and M. Nivat, -North-Holland, 1988. - -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: -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 Realisations et Synthese". -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 summer 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. 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 of early users who saw -their successful proof search ended with QED, followed by silence, followed by -a failure message of universe inconsistency rejection... - -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 1st order -predicate calculus matching, with important performance gain. - -A new representation of the universe hierarchy is then defined by G. 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 89 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 (INRIA Research Report N°1088, Sept. 1989, published in -Logic and Computer Science, ed. P.G. Odifreddi, Academic Press, 1990) -- Inductive definitions in the Calculus of Constructions, by -Christine Paulin-Mohring, -- Extracting Fomega's programs from proofs in the Calculus of Constructions, by -Christine Paulin-Mohring (published in POPL'89) -- The Constructive Engine, by Gérard Huet -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. 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. -An extension of the calculus with primitive inductive types appeared in: -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. - -This lead 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. 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. - -The last version of CONSTR is Version 4.11, which was last distributed -in Spring 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 Ecole 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. diff --git a/dev/doc/README-V1-V5.asciidoc b/dev/doc/README-V1-V5.asciidoc new file mode 100644 index 00000000..631fb92c --- /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/build-system.dev.txt b/dev/doc/build-system.dev.txt index af1120e9..fefcb093 100644 --- a/dev/doc/build-system.dev.txt +++ b/dev/doc/build-system.dev.txt @@ -30,6 +30,11 @@ HISTORY: restricted set of .ml4 (see variable BUILDGRAMMAR). - then on the true target asked by the user. +* June 2016 (Pierre Letouzey) + The files in grammar/ are now self-contained, we could compile + grammar.cma (and q_constr.cmo) directly, no need for a separate + subcall to make nor awkward include-failed-and-retry. + --------------------------------------------------------------------------- @@ -59,29 +64,14 @@ Cons: Makefiles hierachy ------------------ -Le Makefile a été séparé en plusieurs fichiers : - -- Makefile: coquille vide qui lançant Makefile.build sauf pour - clean et quelques petites choses ne nécessitant par de calculs - de dépendances. -- Makefile.common : définitions des variables (essentiellement des - listes de fichiers) -- Makefile.build : contient les regles de compilation, ainsi que - le "include" des dépendances (restreintes ou non selon la variable - BUILDGRAMMAR). -- Makefile.doc : regles specifiques à la compilation de la documentation. - - -Parallélisation ---------------- +The Makefile is separated in several files : -Il y a actuellement un double appel interne à "make -f Makefile.build", -d'abord pour construire grammar.cma/q_constr.cmo, puis le reste. -Cela signifie que ce makefile est un petit peu moins parallélisable -que strictement possible en théorie: par exemple, certaines choses -faites lors du second make pourraient être faites en parallèle avec -le premier. En pratique, ce premier make va suffisemment vite pour -que cette limitation soit peu gênante. +- Makefile: wrapper that triggers a call to Makefile.build, except for + clean and a few other little things doable without dependency analysis. +- Makefile.common : variable definitions (mostly lists of files or + directories) +- Makefile.build : contains compilation rules, and the "include" of dependencies +- Makefile.doc : specific rules for compiling the documentation. FIND_VCS_CLAUSE diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt index 31d9875a..873adc1b 100644 --- a/dev/doc/build-system.txt +++ b/dev/doc/build-system.txt @@ -113,15 +113,20 @@ Targets for cleaning various parts: - docclean: clean documentation -.ml4 files ----------- +.ml4/.mlp files +--------------- -If a .ml4 file uses a grammar extension from Coq (such as grammar.cma -or q_constr.cmo), it must contain a line like: +There is now two kinds of preprocessed files : + - a .mlp do not need grammar.cma (they are in grammar/) + - a .ml4 is now always preprocessed with grammar.cma (and q_constr.cmo), + except coqide_main.ml4 and its specific rule + +This classification replaces the old mechanism of declaring the use +of a grammar extension via a line of the form: (*i camlp4deps: "grammar.cma q_constr.cmo" i*) The use of (*i camlp4use: ... i*) to mention uses of standard -extension such as IFDEF has been discontinued, the Makefile now +extension such as IFDEF has also been discontinued, the Makefile now always calls camlp4 with pa_macros.cmo and a few others by default. For debugging a Coq grammar extension, it could be interesting diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 2f62be9a..3de938d7 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -1,5 +1,281 @@ ========================================= -= CHANGES BETWEEN COQ V8.4 AND CQQ V8.5 = += 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 ** diff --git a/dev/doc/coq-src-description.txt b/dev/doc/coq-src-description.txt index fe896d31..00e7f5c5 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/drop.txt b/dev/doc/drop.txt new file mode 100644 index 00000000..3a584741 --- /dev/null +++ b/dev/doc/drop.txt @@ -0,0 +1,44 @@ +When you start byte-compiled Coq toplevel: + + rlwrap bin/coqtop.byte + +then if you type: + + Drop. + +you will decend from Coq toplevel down to Ocaml toplevel. +So if you want to learn: +- the current values of some global variables you are interested in +- or see what happens when you invoke certain functions +this is the place where you can do that. + +When you try to print values belonging to abstract data types: + + # let sigma, env = Lemmas.get_current_context ();; + + val sigma : Evd.evar_map = <abstr> + val env : Environ.env = <abstr> + + # Typeops.infer env (snd (Pretyping.understand_tcc env sigma (Constrintern.intern_constr env (Pcoq.parse_string Pcoq.Constr.lconstr "plus"))));; + + - : Environ.unsafe_judgment = {Environ.uj_val = <abstr>; uj_type = <abstr>} + +the printed values are not very helpful. + +One way how to deal with that is to load the corresponding printers: + + # #use "dev/include";; + +Consequently, the result of: + + # Typeops.infer env (snd (Pretyping.understand_tcc env sigma (Constrintern.intern_constr env (Pcoq.parse_string Pcoq.Constr.lconstr "plus"))));; + +will be printed as: + + - : Environ.unsafe_judgment = Nat.add : nat -> nat -> nat + +which makes more sense. + +To be able to understand the meaning of the data types, +sometimes the best option is to turn those data types from abstract to concrete +and look at them without any kind of pretty printing. diff --git a/dev/doc/notes-on-conversion b/dev/doc/notes-on-conversion index 6274275c..a81f170c 100644 --- a/dev/doc/notes-on-conversion +++ b/dev/doc/notes-on-conversion @@ -21,7 +21,7 @@ Notation OMEGA := (ack 4 4). Definition f (x:nat) := x. -(* Evaluation in tactics can somehow be controled *) +(* Evaluation in tactics can somehow be controlled *) Lemma l1 : OMEGA = OMEGA. reflexivity. (* succeed: identity *) Qed. (* succeed: identity *) diff --git a/dev/doc/ocamlbuild.txt b/dev/doc/ocamlbuild.txt new file mode 100644 index 00000000..efedbc50 --- /dev/null +++ b/dev/doc/ocamlbuild.txt @@ -0,0 +1,30 @@ +Ocamlbuild & Coq +---------------- + +A quick note in case someone else gets interested someday in compiling +Coq via ocamlbuild : such an experimental build system has existed +in the past (more or less maintained from 2009 to 2013), in addition +to the official build system via gnu make. But this build via +ocamlbuild has been severly broken since early 2014 (and don't work +in 8.5, for instance). This experiment has attracted very limited +interest from other developers over the years, and has been quite +cumbersome to maintain, so it is now officially discontinued. +If you want to have a look at the files of this build system +(especially myocamlbuild.ml), you can fetch : + - my last effort at repairing this build system (up to coqtop.native) : + https://github.com/letouzey/coq-wip/tree/ocamlbuild-partial-repair + - coq official v8.5 branch (recent but broken) + - coq v8.4 branch(less up-to-date, but works). + +For the record, the three main drawbacks of this experiments were: + - recurrent issues with circularities reported by ocamlbuild + (even though make was happy) during the evolution of Coq sources + - no proper support of parallel build + - quite slow re-traversal of already built things +See the two corresponding bug reports on Mantis, or +https://github.com/ocaml/ocamlbuild/issues/52 + +As an interesting feature, I successfully used this to cross-compile +Coq 8.4 from linux to win32 via mingw. + +Pierre Letouzey, june 2016 diff --git a/dev/doc/profiling.txt b/dev/doc/profiling.txt new file mode 100644 index 00000000..9d2ebf0d --- /dev/null +++ b/dev/doc/profiling.txt @@ -0,0 +1,76 @@ +# How to profile Coq? + +I (Pierre-Marie Pédrot) mainly use two OCaml branches to profile Coq, whether I +want to profile time or memory consumption. AFAIK, this only works for Linux. + +## Time + +In Coq source folder: + +opam switch 4.02.1+fp +./configure -local -debug +make +perf record -g bin/coqtop -compile file.v +perf report -g fractal,callee --no-children + +To profile only part of a file, first load it using + +bin/coqtop -l file.v + +and plug into the process + +perf record -g -p PID + +## Memory + +You first need a few commits atop trunk for this to work. + +git remote add ppedrot https://github.com/ppedrot/coq.git +git fetch ppedrot +git checkout ppedrot/allocation-profiling +git rebase master + +Then: + +opam switch 4.00.1+alloc-profiling +./configure -local -debug +make + +Note that linking the coqtop binary takes quite an amount of time with this +branch, so do not worry too much. There are more recent branches of +alloc-profiling on mshinwell's repo which can be found at: + +https://github.com/mshinwell/opam-repo-dev + +### For memory dump: + +CAMLRUNPARAM=T,mj bin/coqtop -compile file.v + +In another terminal: + +pkill -SIGUSR1 $COQTOPPID +... +pkill -SIGUSR1 $COQTOPPID +dev/decode-major-heap.sh heap.$COQTOPPID.$N bin/coqtop + +where $COQTOPPID is coqtop pid and $N the index of the call to pkill. + +First column is the memory taken by the objects (in words), second one is the +number of objects and third is the place where the objects where allocated. + +### For complete memory graph: + +CAMLRUNPARAM=T,gr bin/coqtop -compile file.v + +In another terminal: + +pkill -SIGUSR1 $COQTOPPID +... +pkill -SIGUSR1 $COQTOPPID +ocaml dev/decodegraph.ml edge.$COQTOPPID.$N bin/coqtop > memory.dot +dot -Tpdf -o memory.pdf memory.dot + +where $COQTOPPID is coqtop pid and $N the index of the call to pkill. + +The pdf produced by the last command gives a compact graphical representation of +the various objects allocated. diff --git a/dev/doc/setup.txt b/dev/doc/setup.txt new file mode 100644 index 00000000..1b016a4e --- /dev/null +++ b/dev/doc/setup.txt @@ -0,0 +1,289 @@ +This document provides detailed guidance on how to: +- compile Coq +- take advantage of Merlin in Emacs +- enable auto-completion for Ocaml source-code +- use ocamldebug in Emacs for debugging coqtop +The instructions were tested with Debian 8.3 (Jessie). + +The procedure is somewhat tedious, but the final results are (still) worth the effort. + +How to compile Coq +------------------ + +Getting build dependencies: + + sudo apt-get install make opam git mercurial darcs + opam init --comp 4.02.3 + # Then follow the advice displayed at the end as how to update your ~/.bashrc and ~/.ocamlinit files. + + source ~/.bashrc + + # needed if you want to build "coqtop" target + opam install camlp5 + + # needed if you want to build "coqide" target + sudo apt-get install liblablgtksourceview2-ocaml-dev libgtk2.0-dev libgtksourceview2.0-dev + opam install lablgtk + + # needed if you want to build "doc" target + sudo apt-get install texlive-latex-recommended texlive-fonts-extra texlive-math-extra \ + hevea texlive-latex-extra latex-xcolor + +Cloning Coq: + + # Go to the directory where you want to clone Coq's source-code. E.g.: + cd ~/git + + git clone https://github.com/coq/coq.git + +Building coqtop: + + cd ~/git/coq + git checkout trunk + make distclean + ./configure -annotate -with-doc no -local -debug -usecamlp5 + make clean + make -j4 coqide printers + +The "-annotate" option is essential when one wants to use Merlin. + +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 +- bin/coqtop +- bin/coqide +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: + + 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". + + +How to install and configure Merlin (for Emacs) +----------------------------------------------- + + sudo apt-get install emacs + + opam install tuareg + # Follow the advice displayed at the end as how to update your ~/.emacs file. + + opam install merlin + # Follow the advice displayed at the end as how to update your ~/.emacs file. + +Then add this: + + (push "~/.opam/4.02.3/share/emacs/site-lisp" load-path) ; directory containing merlin.el + (setq merlin-command "~/.opam/4.02.3/bin/ocamlmerlin") ; needed only if ocamlmerlin not already in your PATH + (autoload 'merlin-mode "merlin" "Merlin mode" t) + (add-hook 'tuareg-mode-hook 'merlin-mode) + (add-hook 'caml-mode-hook 'merlin-mode) + (load "~/.opam/4.02.3/share/emacs/site-lisp/tuareg-site-file") + + ;; Do not use TABs. These confuse Merlin. + (setq-default indent-tabs-mode nil) + +to your ~/.emacs file. + +Further Emacs configuration when we start it for the first time. + +Try to open some *.ml file in Emacs, e.g.: + + cd ~/git/coq + emacs toplevel/coqtop.ml & + +Emacs display the following strange message: + + The local variables list in ~/git/coq + contains values that may be safe (*). + + Do you want to apply it? + +Just press "!", i.e. "apply the local variable list, and permanently mark these values (\*) as safe." + +Emacs then shows two windows: +- one window that shows the contents of the "toplevel/coqtop.ml" file +- and the other window that shows greetings for new Emacs users. + +If you do not want to see the second window next time you start Emacs, just check "Never show it again" and click on "Dismiss this startup screen." + +The default key-bindings are described here: + + https://github.com/the-lambda-church/merlin/wiki/emacs-from-scratch + +If you want, you can customize them by replacing the following lines: + + (define-key merlin-map (kbd "C-c C-x") 'merlin-error-next) + (define-key merlin-map (kbd "C-c C-l") 'merlin-locate) + (define-key merlin-map (kbd "C-c &") 'merlin-pop-stack) + (define-key merlin-map (kbd "C-c C-t") 'merlin-type-enclosing) + +in the file "~/.opam/4.02.3/share/emacs/site-lisp/merlin.el" with what you want. +In the text below we assume that you changed the origin key-bindings in the following way: + + (define-key merlin-map (kbd "C-n") 'merlin-error-next) + (define-key merlin-map (kbd "C-l") 'merlin-locate) + (define-key merlin-map (kbd "C-b") 'merlin-pop-stack) + (define-key merlin-map (kbd "C-t") 'merlin-type-enclosing) + +Now, when you press <Ctrl+L>, Merlin will show the definition of the symbol in a separate window. +If you prefer to jump to the definition within the same window, do this: + + <Alt+X> customize-group <ENTER> merlin <ENTER> + + Merlin Locate In New Window + + Value Menu + + Never Open In New Window + + State + + Set For Future Sessions + +Testing (Merlin): + + cd ~/git/coq + emacs toplevel/coqtop.ml & + +Go to the end of the file where you will see the "start" function. + +Go to a line where "init_toplevel" function is called. + +If you want to jump to the position where that function or datatype under the cursor is defined, press <Ctrl+L>. + +If you want to jump back, type: <Ctrl+B> + +If you want to learn the type of the value at current cursor's position, type: <Ctrl+T> + + +Enabling auto-completion in emacs +--------------------------------- + +In Emacs, type: <Alt+M> list-packages <ENTER> + +In the list that is displayed, click on "company". + +A new window appears where just click on "Install" and then answer "Yes". + +These lines: + + (package-initialize) + (require 'company) + ; Make company aware of merlin + (add-to-list 'company-backends 'merlin-company-backend) + ; Enable company on merlin managed buffers + (add-hook 'merlin-mode-hook 'company-mode) + (global-set-key [C-tab] 'company-complete) + +then need to be added to your "~/.emacs" file. + +Next time when you start emacs and partially type some identifier, +emacs will offer the corresponding completions. +Auto-completion can also be manually invoked by typing <Ctrl+TAB>. +Description of various other shortcuts is here. + + http://company-mode.github.io/ + + +Getting along with ocamldebug +----------------------------- + +The default ocamldebug key-bindings are described here. + + http://caml.inria.fr/pub/docs/manual-ocaml/debugger.html#sec369 + +If you want, you can customize them by putting the following commands: + + (global-set-key (kbd "<f5>") 'ocamldebug-break) + (global-set-key (kbd "<f6>") 'ocamldebug-run) + (global-set-key (kbd "<f7>") 'ocamldebug-next) + (global-set-key (kbd "<f8>") 'ocamldebug-step) + (global-set-key (kbd "<f9>") 'ocamldebug-finish) + (global-set-key (kbd "<f10>") 'ocamldebug-print) + (global-set-key (kbd "<f12>") 'camldebug) + +to your "~/.emacs" file. + +Let us try whether ocamldebug in Emacs works for us. +(If necessary, re-)compile coqtop: + + cd ~/git/coq + make -j4 coqide printers + +open Emacs: + + emacs toplevel/coqtop.ml & + +and type: + + <F12> ../bin/coqtop.byte <ENTER> ../dev/ocamldebug-coq <ENTER> + +As a result, a new window is open at the bottom where you should see: + + (ocd) + +i.e. an ocamldebug shell. + + 1. Switch to the window that contains the "coqtop.ml" file. + 2. Go to the end of the file. + 3. Find the definition of the "start" function. + 4. Go to the "let" keyword that is at the beginning of the first line. + 5. By pressing <F5> you set a breakpoint to the cursor's position. + 6. By pressing <F6> you start the bin/coqtop process. + 7. Then you can: + - step over function calls: <F7> + - step into function calls: <F8> + - or finish execution of the current function until it returns: <F9>. + +Other ocamldebug commands, can be typed to the window that holds the ocamldebug shell. + +The points at which the execution of Ocaml program can stop are defined here: + + http://caml.inria.fr/pub/docs/manual-ocaml/debugger.html#sec350 + + +Installing printers to ocamldebug +--------------------------------- + +There is a pretty comprehensive set of printers defined for many common data types. +You can load them by switching to the window holding the "ocamldebug" shell and typing: + + (ocd) source "../dev/db" + + +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.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.\ + It dispatches the control to specific functions handling different Vernacular command. +- Vernacentries.vernac_check_may_eval : This function handles the "Check ..." command. |