From 9e2a3531f2e82038f74cd5543eeef7418c494a28 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Mon, 12 Mar 2018 13:06:30 +0100 Subject: [Sphinx] Move credits to new infrastructure --- doc/sphinx/credits.rst | 1351 ++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 1351 insertions(+) create mode 100644 doc/sphinx/credits.rst (limited to 'doc/sphinx') diff --git a/doc/sphinx/credits.rst b/doc/sphinx/credits.rst new file mode 100644 index 000000000..05775bfbe --- /dev/null +++ b/doc/sphinx/credits.rst @@ -0,0 +1,1351 @@ +%BEGIN LATEX +\setheaders{Credits} +%END LATEX +\chapter*{Credits} +%HEVEA\cutname{credits.html} +%\addcontentsline{toc}{section}{Credits} + +\Coq{}~ is a proof assistant for higher-order logic, allowing the +development of computer programs consistent with their formal +specification. It is the result of about ten years of research of the +Coq project. We shall briefly survey here three main aspects: the +\emph{logical language} in which we write our axiomatizations and +specifications, the \emph{proof assistant} which allows the development +of verified mathematical proofs, and the \emph{program extractor} which +synthesizes computer programs obeying their formal specifications, +written as logical assertions in the language. + +The logical language used by {\Coq} is a variety of type theory, +called the \emph{Calculus of Inductive Constructions}. Without going +back to Leibniz and Boole, we can date the creation of what is now +called mathematical logic to the work of Frege and Peano at the turn +of the century. The discovery of antinomies in the free use of +predicates or comprehension principles prompted Russell to restrict +predicate calculus with a stratification of \emph{types}. This effort +culminated with \emph{Principia Mathematica}, the first systematic +attempt at a formal foundation of mathematics. A simplification of +this system along the lines of simply typed $\lambda$-calculus +occurred with Church's \emph{Simple Theory of Types}. The +$\lambda$-calculus notation, originally used for expressing +functionality, could also be used as an encoding of natural deduction +proofs. This Curry-Howard isomorphism was used by N. de Bruijn in the +\emph{Automath} project, the first full-scale attempt to develop and +mechanically verify mathematical proofs. This effort culminated with +Jutting's verification of Landau's \emph{Grundlagen} in the 1970's. +Exploiting this Curry-Howard isomorphism, notable achievements in +proof theory saw the emergence of two type-theoretic frameworks; the +first one, Martin-L\"of's \emph{Intuitionistic Theory of Types}, +attempts a new foundation of mathematics on constructive principles. +The second one, Girard's polymorphic $\lambda$-calculus $F_\omega$, is +a very strong functional system in which we may represent higher-order +logic proof structures. Combining both systems in a higher-order +extension of the Automath languages, T. Coquand presented in 1985 the +first version of the \emph{Calculus of Constructions}, CoC. This strong +logical system allowed powerful axiomatizations, but direct inductive +definitions were not possible, and inductive notions had to be defined +indirectly through functional encodings, which introduced +inefficiencies and awkwardness. The formalism was extended in 1989 by +T. Coquand and C. Paulin with primitive inductive definitions, leading +to the current \emph{Calculus of Inductive Constructions}. This +extended formalism is not rigorously defined here. Rather, numerous +concrete examples are discussed. We refer the interested reader to +relevant research papers for more information about the formalism, its +meta-theoretic properties, and semantics. However, it should not be +necessary to understand this theoretical material in order to write +specifications. It is possible to understand the Calculus of Inductive +Constructions at a higher level, as a mixture of predicate calculus, +inductive predicate definitions presented as typed PROLOG, and +recursive function definitions close to the language ML. + +Automated theorem-proving was pioneered in the 1960's by Davis and +Putnam in propositional calculus. A complete mechanization (in the +sense of a semi-decision procedure) of classical first-order logic was +proposed in 1965 by J.A. Robinson, with a single uniform inference +rule called \emph{resolution}. Resolution relies on solving equations +in free algebras (i.e. term structures), using the \emph{unification + algorithm}. Many refinements of resolution were studied in the +1970's, but few convincing implementations were realized, except of +course that PROLOG is in some sense issued from this effort. A less +ambitious approach to proof development is computer-aided +proof-checking. The most notable proof-checkers developed in the +1970's were LCF, designed by R. Milner and his colleagues at U. +Edinburgh, specialized in proving properties about denotational +semantics recursion equations, and the Boyer and Moore theorem-prover, +an automation of primitive recursion over inductive data types. While +the Boyer-Moore theorem-prover attempted to synthesize proofs by a +combination of automated methods, LCF constructed its proofs through +the programming of \emph{tactics}, written in a high-level functional +meta-language, ML. + +The salient feature which clearly distinguishes our proof assistant +from say LCF or Boyer and Moore's, is its possibility to extract +programs from the constructive contents of proofs. This computational +interpretation of proof objects, in the tradition of Bishop's +constructive mathematics, is based on a realizability interpretation, +in the sense of Kleene, due to C. Paulin. The user must just mark his +intention by separating in the logical statements the assertions +stating the existence of a computational object from the logical +assertions which specify its properties, but which may be considered +as just comments in the corresponding program. Given this information, +the system automatically extracts a functional term from a consistency +proof of its specifications. This functional term may be in turn +compiled into an actual computer program. This methodology of +extracting programs from proofs is a revolutionary paradigm for +software engineering. Program synthesis has long been a theme of +research in artificial intelligence, pioneered by R. Waldinger. The +Tablog system of Z. Manna and R. Waldinger allows the deductive +synthesis of functional programs from proofs in tableau form of their +specifications, written in a variety of first-order logic. Development +of a systematic \emph{programming logic}, based on extensions of +Martin-L\"of's type theory, was undertaken at Cornell U. by the Nuprl +team, headed by R. Constable. The first actual program extractor, PX, +was designed and implemented around 1985 by S. Hayashi from Kyoto +University. It allows the extraction of a LISP program from a proof +in a logical system inspired by the logical formalisms of S. Feferman. +Interest in this methodology is growing in the theoretical computer +science community. We can foresee the day when actual computer systems +used in applications will contain certified modules, automatically +generated from a consistency proof of their formal specifications. We +are however still far from being able to use this methodology in a +smooth interaction with the standard tools from software engineering, +i.e. compilers, linkers, run-time systems taking advantage of special +hardware, debuggers, and the like. We hope that {\Coq} can be of use +to researchers interested in experimenting with this new methodology. + +A first implementation of CoC was started in 1984 by G. Huet and T. +Coquand. Its implementation language was CAML, a functional +programming language from the ML family designed at INRIA in +Rocquencourt. The core of this system was a proof-checker for CoC seen +as a typed $\lambda$-calculus, called the \emph{Constructive Engine}. +This engine was operated through a high-level notation permitting the +declaration of axioms and parameters, the definition of mathematical +types and objects, and the explicit construction of proof objects +encoded as $\lambda$-terms. A section mechanism, designed and +implemented by G. Dowek, allowed hierarchical developments of +mathematical theories. This high-level language was called the +\emph{Mathematical Vernacular}. Furthermore, an interactive +\emph{Theorem Prover} permitted the incremental construction of proof +trees in a top-down manner, subgoaling recursively and backtracking +from dead-alleys. The theorem prover executed tactics written in CAML, +in the LCF fashion. A basic set of tactics was predefined, which the +user could extend by his own specific tactics. This system (Version +4.10) was released in 1989. Then, the system was extended to deal +with the new calculus with inductive types by C. Paulin, with +corresponding new tactics for proofs by induction. A new standard set +of tactics was streamlined, and the vernacular extended for tactics +execution. A package to compile programs extracted from proofs to +actual computer programs in CAML or some other functional language was +designed and implemented by B. Werner. A new user-interface, relying +on a CAML-X interface by D. de Rauglaudre, was designed and +implemented by A. Felty. It allowed operation of the theorem-prover +through the manipulation of windows, menus, mouse-sensitive buttons, +and other widgets. This system (Version 5.6) was released in 1991. + +\Coq{} was ported to the new implementation Caml-light of X. Leroy and +D. Doligez by D. de Rauglaudre (Version 5.7) in 1992. A new version +of \Coq{} was then coordinated by C. Murthy, with new tools designed +by C. Parent to prove properties of ML programs (this methodology is +dual to program extraction) and a new user-interaction loop. This +system (Version 5.8) was released in May 1993. A Centaur interface +\textsc{CTCoq} was then developed by Y. Bertot from the Croap project +from INRIA-Sophia-Antipolis. + +In parallel, G. Dowek and H. Herbelin developed a new proof engine, +allowing the general manipulation of existential variables +consistently with dependent types in an experimental version of \Coq{} +(V5.9). + +The version V5.10 of \Coq{} is based on a generic system for +manipulating terms with binding operators due to Chet Murthy. A new +proof engine allows the parallel development of partial proofs for +independent subgoals. The structure of these proof trees is a mixed +representation of derivation trees for the Calculus of Inductive +Constructions with abstract syntax trees for the tactics scripts, +allowing the navigation in a proof at various levels of details. The +proof engine allows generic environment items managed in an +object-oriented way. This new architecture, due to C. Murthy, +supports several new facilities which make the system easier to extend +and to scale up: + +\begin{itemize} +\item User-programmable tactics are allowed +\item It is possible to separately verify development modules, and to + load their compiled images without verifying them again - a quick + relocation process allows their fast loading +\item A generic parsing scheme allows user-definable notations, with a + symmetric table-driven pretty-printer +\item Syntactic definitions allow convenient abbreviations +\item A limited facility of meta-variables allows the automatic + synthesis of certain type expressions, allowing generic notations + for e.g. equality, pairing, and existential quantification. +\end{itemize} + +In the Fall of 1994, C. Paulin-Mohring replaced the structure of +inductively defined types and families by a new structure, allowing +the mutually recursive definitions. P. Manoury implemented a +translation of recursive definitions into the primitive recursive +style imposed by the internal recursion operators, in the style of the +ProPre system. C. Mu{\~n}oz implemented a decision procedure for +intuitionistic propositional logic, based on results of R. Dyckhoff. +J.C. Filli{\^a}tre implemented a decision procedure for first-order +logic without contraction, based on results of J. Ketonen and R. +Weyhrauch. Finally C. Murthy implemented a library of inversion +tactics, relieving the user from tedious definitions of ``inversion +predicates''. + +\begin{flushright} +Rocquencourt, Feb. 1st 1995\\ +Gérard Huet +\end{flushright} + +\section*{Credits: addendum for version 6.1} +%\addcontentsline{toc}{section}{Credits: addendum for version V6.1} + +The present version 6.1 of \Coq{} is based on the V5.10 architecture. It +was ported to the new language {\ocaml} by Bruno Barras. The +underlying framework has slightly changed and allows more conversions +between sorts. + +The new version provides powerful tools for easier developments. + +Cristina Cornes designed an extension of the \Coq{} syntax to allow +definition of terms using a powerful pattern-matching analysis in the +style of ML programs. + +Amokrane Saïbi wrote a mechanism to simulate +inheritance between types families extending a proposal by Peter +Aczel. He also developed a mechanism to automatically compute which +arguments of a constant may be inferred by the system and consequently +do not need to be explicitly written. + +Yann Coscoy designed a command which explains a proof term using +natural language. Pierre Cr{\'e}gut built a new tactic which solves +problems in quantifier-free Presburger Arithmetic. Both +functionalities have been integrated to the \Coq{} system by Hugo +Herbelin. + +Samuel Boutin designed a tactic for simplification of commutative +rings using a canonical set of rewriting rules and equality modulo +associativity and commutativity. + +Finally the organisation of the \Coq{} distribution has been supervised +by Jean-Christophe Filliâtre with the help of Judicaël Courant +and Bruno Barras. + +\begin{flushright} +Lyon, Nov. 18th 1996\\ +Christine Paulin +\end{flushright} + +\section*{Credits: addendum for version 6.2} +%\addcontentsline{toc}{section}{Credits: addendum for version V6.2} + +In version 6.2 of \Coq{}, the parsing is done using camlp4, a +preprocessor and pretty-printer for CAML designed by Daniel de +Rauglaudre at INRIA. Daniel de Rauglaudre made the first adaptation +of \Coq{} for camlp4, this work was continued by Bruno Barras who also +changed the structure of \Coq{} abstract syntax trees and the primitives +to manipulate them. The result of +these changes is a faster parsing procedure with greatly improved +syntax-error messages. The user-interface to introduce grammar or +pretty-printing rules has also changed. + +Eduardo Giménez redesigned the internal +tactic libraries, giving uniform names +to Caml functions corresponding to \Coq{} tactic names. + +Bruno Barras wrote new more efficient reductions functions. + +Hugo Herbelin introduced more uniform notations in the \Coq{} +specification language: the definitions by fixpoints and +pattern-matching have a more readable syntax. Patrick Loiseleur +introduced user-friendly notations for arithmetic expressions. + +New tactics were introduced: Eduardo Giménez improved a mechanism to +introduce macros for tactics, and designed special tactics for +(co)inductive definitions; Patrick Loiseleur designed a tactic to +simplify polynomial expressions in an arbitrary commutative ring which +generalizes the previous tactic implemented by Samuel Boutin. +Jean-Christophe Filli\^atre introduced a tactic for refining a goal, +using a proof term with holes as a proof scheme. + +David Delahaye designed the \textsf{SearchIsos} tool to search an +object in the library given its type (up to isomorphism). + +Henri Laulhère produced the \Coq{} distribution for the Windows environment. + +Finally, Hugo Herbelin was the main coordinator of the \Coq{} +documentation with principal contributions by Bruno Barras, David Delahaye, +Jean-Christophe Filli\^atre, Eduardo +Giménez, Hugo Herbelin and Patrick Loiseleur. + +\begin{flushright} +Orsay, May 4th 1998\\ +Christine Paulin +\end{flushright} + +\section*{Credits: addendum for version 6.3} +The main changes in version V6.3 was the introduction of a few new tactics +and the extension of the guard condition for fixpoint definitions. + + +B. Barras extended the unification algorithm to complete partial terms +and solved various tricky bugs related to universes.\\ +D. Delahaye developed the \texttt{AutoRewrite} tactic. He also designed the new +behavior of \texttt{Intro} and provided the tacticals \texttt{First} and +\texttt{Solve}.\\ +J.-C. Filli\^atre developed the \texttt{Correctness} tactic.\\ +E. Gim\'enez extended the guard condition in fixpoints.\\ +H. Herbelin designed the new syntax for definitions and extended the +\texttt{Induction} tactic.\\ +P. Loiseleur developed the \texttt{Quote} tactic and +the new design of the \texttt{Auto} +tactic, he also introduced the index of +errors in the documentation.\\ +C. Paulin wrote the \texttt{Focus} command and introduced +the reduction functions in definitions, this last feature +was proposed by J.-F. Monin from CNET Lannion. + +\begin{flushright} +Orsay, Dec. 1999\\ +Christine Paulin +\end{flushright} + +%\newpage + +\section*{Credits: versions 7} + +The version V7 is a new implementation started in September 1999 by +Jean-Christophe Filliâtre. This is a major revision with respect to +the internal architecture of the system. The \Coq{} version 7.0 was +distributed in March 2001, version 7.1 in September 2001, version +7.2 in January 2002, version 7.3 in May 2002 and version 7.4 in +February 2003. + +Jean-Christophe Filliâtre designed the architecture of the new system, he +introduced a new representation for environments and wrote a new kernel +for type-checking terms. His approach was to use functional +data-structures in order to get more sharing, to prepare the addition +of modules and also to get closer to a certified kernel. + +Hugo Herbelin introduced a new structure of terms with local +definitions. He introduced ``qualified'' names, wrote a new +pattern-matching compilation algorithm and designed a more compact +algorithm for checking the logical consistency of universes. He +contributed to the simplification of {\Coq} internal structures and the +optimisation of the system. He added basic tactics for forward +reasoning and coercions in patterns. + +David Delahaye introduced a new language for tactics. General tactics +using pattern-matching on goals and context can directly be written +from the {\Coq} toplevel. He also provided primitives for the design +of user-defined tactics in \textsc{Caml}. + +Micaela Mayero contributed the library on real numbers. +Olivier Desmettre extended this library with axiomatic +trigonometric functions, square, square roots, finite sums, Chasles +property and basic plane geometry. + +Jean-Christophe Filliâtre and Pierre Letouzey redesigned a new +extraction procedure from \Coq{} terms to \textsc{Caml} or +\textsc{Haskell} programs. This new +extraction procedure, unlike the one implemented in previous version +of \Coq{} is able to handle all terms in the Calculus of Inductive +Constructions, even involving universes and strong elimination. P. +Letouzey adapted user contributions to extract ML programs when it was +sensible. +Jean-Christophe Filliâtre wrote \verb=coqdoc=, a documentation +tool for {\Coq} libraries usable from version 7.2. + +Bruno Barras improved the reduction algorithms efficiency and +the confidence level in the correctness of {\Coq} critical type-checking +algorithm. + +Yves Bertot designed the \texttt{SearchPattern} and +\texttt{SearchRewrite} tools and the support for the \textsc{pcoq} interface +(\url{http://www-sop.inria.fr/lemme/pcoq/}). + +Micaela Mayero and David Delahaye introduced {\tt Field}, a decision tactic for commutative fields. + +Christine Paulin changed the elimination rules for empty and singleton +propositional inductive types. + +Loïc Pottier developed {\tt Fourier}, a tactic solving linear inequalities on real numbers. + +Pierre Crégut developed a new version based on reflexion of the {\tt Omega} +decision tactic. + +Claudio Sacerdoti Coen designed an XML output for the {\Coq} +modules to be used in the Hypertextual Electronic Library of +Mathematics (HELM cf \url{http://www.cs.unibo.it/helm}). + +A library for efficient representation of finite maps using binary trees +contributed by Jean Goubault was integrated in the basic theories. + +Pierre Courtieu developed a command and a tactic to reason on the +inductive structure of recursively defined functions. + +Jacek Chrz\k{a}szcz designed and implemented the module system of +{\Coq} whose foundations are in Judicaël Courant's PhD thesis. + +\bigskip + +The development was coordinated by C. Paulin. + +Many discussions within the Démons team and the LogiCal project +influenced significantly the design of {\Coq} especially with +%J. Chrz\k{a}szcz, P. Courtieu, +J. Courant, J. Duprat, J. Goubault, A. Miquel, +C. Marché, B. Monate and B. Werner. + +Intensive users suggested improvements of the system : +Y. Bertot, L. Pottier, L. Théry, P. Zimmerman from INRIA, +C. Alvarado, P. Crégut, J.-F. Monin from France Telecom R \& D. +\begin{flushright} +Orsay, May. 2002\\ +Hugo Herbelin \& Christine Paulin +\end{flushright} + +\section*{Credits: version 8.0} + +{\Coq} version 8 is a major revision of the {\Coq} proof assistant. +First, the underlying logic is slightly different. The so-called {\em +impredicativity} of the sort {\tt Set} has been dropped. The main +reason is that it is inconsistent with the principle of description +which is quite a useful principle for formalizing %classical +mathematics within classical logic. Moreover, even in an constructive +setting, the impredicativity of {\tt Set} does not add so much in +practice and is even subject of criticism from a large part of the +intuitionistic mathematician community. Nevertheless, the +impredicativity of {\tt Set} remains optional for users interested in +investigating mathematical developments which rely on it. + +Secondly, the concrete syntax of terms has been completely +revised. The main motivations were + +\begin{itemize} +\item a more uniform, purified style: all constructions are now lowercase, + with a functional programming perfume (e.g. abstraction is now + written {\tt fun}), and more directly accessible to the novice + (e.g. dependent product is now written {\tt forall} and allows + omission of types). Also, parentheses and are no longer mandatory + for function application. +\item extensibility: some standard notations (e.g. ``<'' and ``>'') were + incompatible with the previous syntax. Now all standard arithmetic + notations (=, +, *, /, <, <=, ... and more) are directly part of the + syntax. +\end{itemize} + +Together with the revision of the concrete syntax, a new mechanism of +{\em interpretation scopes} permits to reuse the same symbols +(typically +, -, *, /, <, <=) in various mathematical theories without +any ambiguities for {\Coq}, leading to a largely improved readability of +{\Coq} scripts. New commands to easily add new symbols are also +provided. + +Coming with the new syntax of terms, a slight reform of the tactic +language and of the language of commands has been carried out. The +purpose here is a better uniformity making the tactics and commands +easier to use and to remember. + +Thirdly, a restructuration and uniformisation of the standard library +of {\Coq} has been performed. There is now just one Leibniz' equality +usable for all the different kinds of {\Coq} objects. Also, the set of +real numbers now lies at the same level as the sets of natural and +integer numbers. Finally, the names of the standard properties of +numbers now follow a standard pattern and the symbolic +notations for the standard definitions as well. + +The fourth point is the release of \CoqIDE{}, a new graphical +gtk2-based interface fully integrated to {\Coq}. Close in style from +the Proof General Emacs interface, it is faster and its integration +with {\Coq} makes interactive developments more friendly. All +mathematical Unicode symbols are usable within \CoqIDE{}. + +Finally, the module system of {\Coq} completes the picture of {\Coq} +version 8.0. Though released with an experimental status in the previous +version 7.4, it should be considered as a salient feature of the new +version. + +Besides, {\Coq} comes with its load of novelties and improvements: new +or improved tactics (including a new tactic for solving first-order +statements), new management commands, extended libraries. + +\bigskip + +Bruno Barras and Hugo Herbelin have been the main contributors of the +reflexion and the implementation of the new syntax. The smart +automatic translator from old to new syntax released with {\Coq} is also +their work with contributions by Olivier Desmettre. + +Hugo Herbelin is the main designer and implementor of the notion of +interpretation scopes and of the commands for easily adding new notations. + +Hugo Herbelin is the main implementor of the restructuration of the +standard library. + +Pierre Corbineau is the main designer and implementor of the new +tactic for solving first-order statements in presence of inductive +types. He is also the maintainer of the non-domain specific automation +tactics. + +Benjamin Monate is the developer of the \CoqIDE{} graphical +interface with contributions by Jean-Christophe Filliâtre, Pierre +Letouzey, Claude Marché and Bruno Barras. + +Claude Marché coordinated the edition of the Reference Manual for + \Coq{} V8.0. + +Pierre Letouzey and Jacek Chrz\k{a}szcz respectively maintained the +extraction tool and module system of {\Coq}. + +Jean-Christophe Filliâtre, Pierre Letouzey, Hugo Herbelin and other +contributors from Sophia-Antipolis and Nijmegen participated to the +extension of the library. + +Julien Narboux built a NSIS-based automatic {\Coq} installation tool for +the Windows platform. + +Hugo Herbelin and Christine Paulin coordinated the development which +was under the responsability of Christine Paulin. + +\begin{flushright} +Palaiseau \& Orsay, Apr. 2004\\ +Hugo Herbelin \& Christine Paulin\\ +(updated Apr. 2006) +\end{flushright} + +\section*{Credits: version 8.1} + +{\Coq} version 8.1 adds various new functionalities. + +Benjamin Grégoire implemented an alternative algorithm to check the +convertibility of terms in the {\Coq} type-checker. This alternative +algorithm works by compilation to an efficient bytecode that is +interpreted in an abstract machine similar to Xavier Leroy's ZINC +machine. Convertibility is performed by comparing the normal +forms. This alternative algorithm is specifically interesting for +proofs by reflection. More generally, it is convenient in case of +intensive computations. + +Christine Paulin implemented an extension of inductive types allowing +recursively non uniform parameters. Hugo Herbelin implemented +sort-polymorphism for inductive types (now called template polymorphism). + +Claudio Sacerdoti Coen improved the tactics for rewriting on arbitrary +compatible equivalence relations. He also generalized rewriting to +arbitrary transition systems. + +Claudio Sacerdoti Coen added new features to the module system. + +Benjamin Grégoire, Assia Mahboubi and Bruno Barras developed a new +more efficient and more general simplification algorithm on rings and +semi-rings. + +Laurent Théry and Bruno Barras developed a new significantly more efficient +simplification algorithm on fields. + +Hugo Herbelin, Pierre Letouzey, Julien Forest, Julien Narboux and +Claudio Sacerdoti Coen added new tactic features. + +Hugo Herbelin implemented matching on disjunctive patterns. + +New mechanisms made easier the communication between {\Coq} and external +provers. Nicolas Ayache and Jean-Christophe Filliâtre implemented +connections with the provers {\sc cvcl}, {\sc Simplify} and {\sc +zenon}. Hugo Herbelin implemented an experimental protocol for calling +external tools from the tactic language. + +Matthieu Sozeau developed \textsc{Russell}, an experimental language +to specify the behavior of programs with subtypes. + +A mechanism to automatically use some specific tactic to solve +unresolved implicit has been implemented by Hugo Herbelin. + +Laurent Théry's contribution on strings and Pierre Letouzey and +Jean-Christophe Filliâtre's contribution on finite maps have been +integrated to the {\Coq} standard library. Pierre Letouzey developed a +library about finite sets ``à la {\ocaml}''. With Jean-Marc +Notin, he extended the library on lists. Pierre Letouzey's +contribution on rational numbers has been integrated and extended.. + +Pierre Corbineau extended his tactic for solving first-order +statements. He wrote a reflection-based intuitionistic tautology +solver. + +Pierre Courtieu, Julien Forest and Yves Bertot added extra support to +reason on the inductive structure of recursively defined functions. + +Jean-Marc Notin significantly contributed to the general maintenance +of the system. He also took care of {\textsf{coqdoc}}. + +Pierre Castéran contributed to the documentation of (co-)inductive +types and suggested improvements to the libraries. + +Pierre Corbineau implemented a declarative mathematical proof +language, usable in combination with the tactic-based style of proof. + +Finally, many users suggested improvements of the system through the +Coq-Club mailing list and bug-tracker systems, especially user groups +from INRIA Rocquencourt, Radboud University, University of +Pennsylvania and Yale University. + +\enlargethispage{\baselineskip} +\begin{flushright} +Palaiseau, July 2006\\ +Hugo Herbelin +\end{flushright} + +\section*{Credits: version 8.2} + +{\Coq} version 8.2 adds new features, new libraries and +improves on many various aspects. + +Regarding the language of Coq, the main novelty is the introduction by +Matthieu Sozeau of a package of commands providing Haskell-style +type classes. Type classes, that come with a few convenient features +such as type-based resolution of implicit arguments, plays a new role +of landmark in the architecture of Coq with respect to automatization. +For instance, thanks to type classes support, Matthieu Sozeau could +implement a new resolution-based version of the tactics dedicated to +rewriting on arbitrary transitive relations. + +Another major improvement of Coq 8.2 is the evolution of the +arithmetic libraries and of the tools associated to them. Benjamin +Grégoire and Laurent Théry contributed a modular library for building +arbitrarily large integers from bounded integers while Evgeny Makarov +contributed a modular library of abstract natural and integer +arithmetics together with a few convenient tactics. On his side, +Pierre Letouzey made numerous extensions to the arithmetic libraries on +$\mathbb{Z}$ and $\mathbb{Q}$, including extra support for +automatization in presence of various number-theory concepts. + +Frédéric Besson contributed a reflexive tactic based on +Krivine-Stengle Positivstellensatz (the easy way) for validating +provability of systems of inequalities. The platform is flexible enough +to support the validation of any algorithm able to produce a +``certificate'' for the Positivstellensatz and this covers the case of +Fourier-Motzkin (for linear systems in $\mathbb{Q}$ and $\mathbb{R}$), +Fourier-Motzkin with cutting planes (for linear systems in +$\mathbb{Z}$) and sum-of-squares (for non-linear systems). Evgeny +Makarov made the platform generic over arbitrary ordered rings. + +Arnaud Spiwack developed a library of 31-bits machine integers and, +relying on Benjamin Grégoire and Laurent Théry's library, delivered a +library of unbounded integers in base $2^{31}$. As importantly, he +developed a notion of ``retro-knowledge'' so as to safely extend the +kernel-located bytecode-based efficient evaluation algorithm of Coq +version 8.1 to use 31-bits machine arithmetics for efficiently +computing with the library of integers he developed. + +Beside the libraries, various improvements contributed to provide a +more comfortable end-user language and more expressive tactic +language. Hugo Herbelin and Matthieu Sozeau improved the +pattern-matching compilation algorithm (detection of impossible +clauses in pattern-matching, automatic inference of the return +type). Hugo Herbelin, Pierre Letouzey and Matthieu Sozeau contributed +various new convenient syntactic constructs and new tactics or tactic +features: more inference of redundant information, better unification, +better support for proof or definition by fixpoint, more expressive +rewriting tactics, better support for meta-variables, more convenient +notations, ... + +Élie Soubiran improved the module system, adding new features (such as +an ``include'' command) and making it more flexible and more +general. He and Pierre Letouzey improved the support for modules in +the extraction mechanism. + +Matthieu Sozeau extended the \textsc{Russell} language, ending in an +convenient way to write programs of given specifications, Pierre +Corbineau extended the Mathematical Proof Language and the +automatization tools that accompany it, Pierre Letouzey supervised and +extended various parts of the standard library, Stéphane Glondu +contributed a few tactics and improvements, Jean-Marc Notin provided +help in debugging, general maintenance and {\tt coqdoc} support, +Vincent Siles contributed extensions of the {\tt Scheme} command and +of {\tt injection}. + +Bruno Barras implemented the {\tt coqchk} tool: this is a stand-alone +type-checker that can be used to certify {\tt .vo} files. Especially, +as this verifier runs in a separate process, it is granted not to be +``hijacked'' by virtually malicious extensions added to {\Coq}. + +Yves Bertot, Jean-Christophe Filliâtre, Pierre Courtieu and +Julien Forest acted as maintainers of features they implemented in +previous versions of Coq. + +Julien Narboux contributed to {\CoqIDE}. +Nicolas Tabareau made the adaptation of the interface of the old +``setoid rewrite'' tactic to the new version. Lionel Mamane worked on +the interaction between Coq and its external interfaces. With Samuel +Mimram, he also helped making Coq compatible with recent software +tools. Russell O'Connor, Cezary Kaliscyk, Milad Niqui contributed to +improve the libraries of integers, rational, and real numbers. We +also thank many users and partners for suggestions and feedback, in +particular Pierre Castéran and Arthur Charguéraud, the INRIA Marelle +team, Georges Gonthier and the INRIA-Microsoft Mathematical Components team, +the Foundations group at Radboud university in Nijmegen, reporters of bugs +and participants to the Coq-Club mailing list. + +\begin{flushright} +Palaiseau, June 2008\\ +Hugo Herbelin\\ +\end{flushright} + +\section*{Credits: version 8.3} + +{\Coq} version 8.3 is before all a transition version with refinements +or extensions of the existing features and libraries and a new tactic +{\tt nsatz} based on Hilbert's Nullstellensatz for deciding systems of +equations over rings. + +With respect to libraries, the main evolutions are due to Pierre +Letouzey with a rewriting of the library of finite sets {\tt FSets} +and a new round of evolutions in the modular development of arithmetic +(library {\tt Numbers}). The reason for making {\tt FSets} evolve is +that the computational and logical contents were quite intertwined in +the original implementation, leading in some cases to longer +computations than expected and this problem is solved in the new {\tt + MSets} implementation. As for the modular arithmetic library, it was +only dealing with the basic arithmetic operators in the former version +and its current extension adds the standard theory of the division, +min and max functions, all made available for free to any +implementation of $\mathbb{N}$, $\mathbb{Z}$ or +$\mathbb{Z}/n\mathbb{Z}$. + +The main other evolutions of the library are due to Hugo Herbelin who +made a revision of the sorting library (including a certified +merge-sort) and to Guillaume Melquiond who slightly revised and +cleaned up the library of reals. + +The module system evolved significantly. Besides the resolution of +some efficiency issues and a more flexible construction of module +types, Élie Soubiran brought a new model of name equivalence, the +$\Delta$-equivalence, which respects as much as possible the names +given by the users. He also designed with Pierre Letouzey a new +convenient operator \verb!<+! for nesting functor application, that +provides a light notation for inheriting the properties of cascading +modules. + +The new tactic {\tt nsatz} is due to Loïc Pottier. It works by +computing Gr\"obner bases. Regarding the existing tactics, various +improvements have been done by Matthieu Sozeau, Hugo Herbelin and +Pierre Letouzey. + +Matthieu Sozeau extended and refined the type classes and {\tt + Program} features (the {\sc Russell} language). Pierre Letouzey +maintained and improved the extraction mechanism. Bruno Barras and +\'Elie Soubiran maintained the Coq checker, Julien Forest maintained +the {\tt Function} mechanism for reasoning over recursively defined +functions. Matthieu Sozeau, Hugo Herbelin and Jean-Marc Notin +maintained {\tt coqdoc}. Frédéric Besson maintained the {\sc + Micromega} plateform for deciding systems of inequalities. Pierre +Courtieu maintained the support for the Proof General Emacs +interface. Claude Marché maintained the plugin for calling external +provers ({\tt dp}). Yves Bertot made some improvements to the +libraries of lists and integers. Matthias Puech improved the search +functions. Guillaume Melquiond usefully contributed here and +there. Yann Régis-Gianas grounded the support for Unicode on a more +standard and more robust basis. + +Though invisible from outside, Arnaud Spiwack improved the general +process of management of existential variables. Pierre Letouzey and +Stéphane Glondu improved the compilation scheme of the Coq archive. +Vincent Gross provided support to {\CoqIDE}. Jean-Marc Notin provided +support for benchmarking and archiving. + +Many users helped by reporting problems, providing patches, suggesting +improvements or making useful comments, either on the bug tracker or +on the Coq-club mailing list. This includes but not exhaustively +Cédric Auger, Arthur Charguéraud, François Garillot, Georges Gonthier, +Robin Green, Stéphane Lescuyer, Eelis van der Weegen,~... + +Though not directly related to the implementation, special thanks are +going to Yves Bertot, Pierre Castéran, Adam Chlipala, and Benjamin +Pierce for the excellent teaching materials they provided. + +\begin{flushright} +Paris, April 2010\\ +Hugo Herbelin\\ +\end{flushright} + +\section*{Credits: version 8.4} + +{\Coq} version 8.4 contains the result of three long-term projects: a +new modular library of arithmetic by Pierre Letouzey, a new proof +engine by Arnaud Spiwack and a new communication protocol for {\CoqIDE} +by Vincent Gross. + +The new modular library of arithmetic extends, generalizes and +unifies the existing libraries on Peano arithmetic (types {\tt nat}, +{\tt N} and {\tt BigN}), positive arithmetic (type {\tt positive}), +integer arithmetic ({\tt Z} and {\tt BigZ}) and machine word +arithmetic (type {\tt Int31}). It provides with unified notations +(e.g. systematic use of {\tt add} and {\tt mul} for denoting the +addition and multiplication operators), systematic and generic +development of operators and properties of these operators for all the +types mentioned above, including gcd, pcm, power, square root, base 2 +logarithm, division, modulo, bitwise operations, logical shifts, +comparisons, iterators, ... + +The most visible feature of the new proof engine is the support for +structured scripts (bullets and proof brackets) but, even if yet not +user-available, the new engine also provides the basis for refining +existential variables using tactics, for applying tactics to several +goals simultaneously, for reordering goals, all features which are +planned for the next release. The new proof engine forced to +reimplement {\tt info} and {\tt Show Script} differently, what was +done by Pierre Letouzey. + +Before version 8.4, {\CoqIDE} was linked to {\Coq} with the graphical +interface living in a separate thread. From version 8.4, {\CoqIDE} is a +separate process communicating with {\Coq} through a textual +channel. This allows for a more robust interfacing, the ability to +interrupt {\Coq} without interrupting the interface, and the ability to +manage several sessions in parallel. Relying on the infrastructure +work made by Vincent Gross, Pierre Letouzey, Pierre Boutillier and +Pierre-Marie P\'edrot contributed many various refinements of {\CoqIDE}. + +{\Coq} 8.4 also comes with a bunch of many various smaller-scale changes +and improvements regarding the different components of the system. + +The underlying logic has been extended with $\eta$-conversion thanks +to Hugo Herbelin, St\'ephane Glondu and Benjamin Gr\'egoire. The +addition of $\eta$-conversion is justified by the confidence that the +formulation of the Calculus of Inductive Constructions based on typed +equality (such as the one considered in Lee and Werner to build a +set-theoretic model of CIC~\cite{LeeWerner11}) is applicable to the +concrete implementation of {\Coq}. + +The underlying logic benefited also from a refinement of the guard +condition for fixpoints by Pierre Boutillier, the point being that it +is safe to propagate the information about structurally smaller +arguments through $\beta$-redexes that are blocked by the +``match'' construction (blocked commutative cuts). + +Relying on the added permissiveness of the guard condition, Hugo +Herbelin could extend the pattern-matching compilation algorithm +so that matching over a sequence of terms involving +dependencies of a term or of the indices of the type of a term in the +type of other terms is systematically supported. + +Regarding the high-level specification language, Pierre Boutillier +introduced the ability to give implicit arguments to anonymous +functions, Hugo Herbelin introduced the ability to define notations +with several binders (e.g. \verb=exists x y z, P=), Matthieu Sozeau +made the type classes inference mechanism more robust and predictable, +Enrico Tassi introduced a command {\tt Arguments} that generalizes +{\tt Implicit Arguments} and {\tt Arguments Scope} for assigning +various properties to arguments of constants. Various improvements in +the type inference algorithm were provided by Matthieu Sozeau and Hugo +Herbelin with contributions from Enrico Tassi. + +Regarding tactics, Hugo Herbelin introduced support for referring to +expressions occurring in the goal by pattern in tactics such as {\tt + set} or {\tt destruct}. Hugo Herbelin also relied on ideas from +Chung-Kil Hur's {\tt Heq} plugin to introduce automatic computation of +occurrences to generalize when using {\tt destruct} and {\tt + induction} on types with indices. St\'ephane Glondu introduced new +tactics {\tt constr\_eq}, {\tt is\_evar} and {\tt has\_evar} to be +used when writing complex tactics. Enrico Tassi added support to +fine-tuning the behavior of {\tt simpl}. Enrico Tassi added the +ability to specify over which variables of a section a lemma has +to be exactly generalized. Pierre Letouzey added a tactic {\tt + timeout} and the interruptibility of {\tt vm\_compute}. Bug fixes +and miscellaneous improvements of the tactic language came from Hugo +Herbelin, Pierre Letouzey and Matthieu Sozeau. + +Regarding decision tactics, Lo\"ic Pottier maintained {\tt Nsatz}, +moving in particular to a type-class based reification of goals while +Fr\'ed\'eric Besson maintained {\tt Micromega}, adding in particular +support for division. + +Regarding vernacular commands, St\'ephane Glondu provided new commands +to analyze the structure of type universes. + +Regarding libraries, a new library about lists of a given length +(called vectors) has been provided by Pierre Boutillier. A new +instance of finite sets based on Red-Black trees and provided by +Andrew Appel has been adapted for the standard library by Pierre +Letouzey. In the library of real analysis, Yves Bertot changed the +definition of $\pi$ and provided a proof of the long-standing fact yet +remaining unproved in this library, namely that $sin \frac{\pi}{2} = +1$. + +Pierre Corbineau maintained the Mathematical Proof Language (C-zar). + +Bruno Barras and Benjamin Gr\'egoire maintained the call-by-value +reduction machines. + +The extraction mechanism benefited from several improvements provided by +Pierre Letouzey. + +Pierre Letouzey maintained the module system, with contributions from +\'Elie Soubiran. + +Julien Forest maintained the {\tt Function} command. + +Matthieu Sozeau maintained the setoid rewriting mechanism. + +{\Coq} related tools have been upgraded too. In particular, {\tt + coq\_makefile} has been largely revised by Pierre Boutillier. Also, +patches from Adam Chlipala for {\tt coqdoc} have been integrated by +Pierre Boutillier. + +Bruno Barras and Pierre Letouzey maintained the {\tt coqchk} checker. + +Pierre Courtieu and Arnaud Spiwack contributed new features for using +{\Coq} through Proof General. + +The {\tt Dp} plugin has been removed. Use the plugin provided with +{\tt Why 3} instead (\url{http://why3.lri.fr}). + +Under the hood, the {\Coq} architecture benefited from improvements in +terms of efficiency and robustness, especially regarding universes +management and existential variables management, thanks to Pierre +Letouzey and Yann R\'egis-Gianas with contributions from St\'ephane +Glondu and Matthias Puech. The build system is maintained by Pierre +Letouzey with contributions from St\'ephane Glondu and Pierre +Boutillier. + +A new backtracking mechanism simplifying the task of external +interfaces has been designed by Pierre Letouzey. + +The general maintenance was done by Pierre Letouzey, Hugo Herbelin, +Pierre Boutillier, Matthieu Sozeau and St\'ephane Glondu with also +specific contributions from Guillaume Melquiond, Julien Narboux and +Pierre-Marie Pédrot. + +Packaging tools were provided by Pierre Letouzey (Windows), Pierre +Boutillier (MacOS), St\'ephane Glondu (Debian). Releasing, testing and +benchmarking support was provided by Jean-Marc Notin. + +Many suggestions for improvements were motivated by feedback from +users, on either the bug tracker or the coq-club mailing list. Special +thanks are going to the users who contributed patches, starting with +Tom Prince. Other patch contributors include C\'edric Auger, David +Baelde, Dan Grayson, Paolo Herms, Robbert Krebbers, Marc Lasson, +Hendrik Tews and Eelis van der Weegen. + +\begin{flushright} +Paris, December 2011\\ +Hugo Herbelin\\ +\end{flushright} + + +\section*{Credits: version 8.5} + +{\Coq} version 8.5 contains the result of five specific long-term +projects: +\begin{itemize} +\item A new asynchronous evaluation and compilation mode by Enrico + Tassi with help from Bruno Barras and Carst Tankink. +\item Full integration of the new proof engine by Arnaud Spiwack + helped by Pierre-Marie Pédrot, +\item Addition of conversion and reduction based on native compilation + by Maxime Dénès and Benjamin Grégoire. +\item Full universe polymorphism for definitions and inductive types by + Matthieu Sozeau. +\item An implementation of primitive projections with $\eta$-conversion + bringing significant performance improvements when using records by + Matthieu Sozeau. +\end{itemize} + +The full integration of the proof engine, by Arnaud Spiwack and +Pierre-Marie Pédrot, brings to primitive tactics and the user level +Ltac language dependent subgoals, deep backtracking and multiple goal +handling, along with miscellaneous features and an improved potential +for future modifications. Dependent subgoals allow statements in a +goal to mention the proof of another. Proofs of unsolved subgoals +appear as existential variables. Primitive backtracking makes it +possible to write a tactic with several possible outcomes which are +tried successively when subsequent tactics fail. Primitives are also +available to control the backtracking behavior of tactics. Multiple +goal handling paves the way for smarter automation tactics. It is +currently used for simple goal manipulation such as goal reordering. + +The way {\Coq} processes a document in batch and interactive mode has +been redesigned by Enrico Tassi with help from Bruno Barras. Opaque +proofs, the text between Proof and Qed, can be processed +asynchronously, decoupling the checking of definitions and statements +from the checking of proofs. It improves the responsiveness of +interactive development, since proofs can be processed in the +background. Similarly, compilation of a file can be split into two +phases: the first one checking only definitions and statements and the +second one checking proofs. A file resulting from the first +phase~--~with the .vio extension~--~can be already Required. All .vio +files can be turned into complete .vo files in parallel. The same +infrastructure also allows terminating tactics to be run in parallel +on a set of goals via the \verb=par:= goal selector. + +{\CoqIDE} was modified to cope with asynchronous checking of the +document. Its source code was also made separate from that of {\Coq}, so +that {\CoqIDE} no longer has a special status among user interfaces, +paving the way for decoupling its release cycle from that of {\Coq} in +the future. + +Carst Tankink developed a {\Coq} back-end for user interfaces built on +Makarius Wenzel's Prover IDE framework (PIDE), like PIDE/jEdit (with +help from Makarius Wenzel) or PIDE/Coqoon (with help from Alexander +Faithfull and Jesper Bengtson). The development of such features was +funded by the Paral-ITP French ANR project. + +The full universe polymorphism extension was designed by Matthieu +Sozeau. It conservatively extends the universes system and core calculus +with definitions and inductive declarations parameterized by universes +and constraints. It is based on a modification of the kernel architecture to +handle constraint checking only, leaving the generation of constraints +to the refinement/type inference engine. Accordingly, tactics are now +fully universe aware, resulting in more localized error messages in case +of inconsistencies and allowing higher-level algorithms like unification +to be entirely type safe. The internal representation of universes has +been modified but this is invisible to the user. + +The underlying logic has been extended with $\eta$-conversion for +records defined with primitive projections by Matthieu Sozeau. This +additional form of $\eta$-conversion is justified using the same +principle than the previously added $\eta$-conversion for function +types, based on formulations of the Calculus of Inductive Constructions +with typed equality. Primitive projections, which do not carry the +parameters of the record and are rigid names (not defined as a +pattern-matching construct), make working with nested records more +manageable in terms of time and space consumption. This extension and +universe polymorphism were carried out partly while Matthieu Sozeau was working +at the IAS in Princeton. + +The guard condition has been made compliant with extensional equality +principles such as propositional extensionality and univalence, thanks to +Maxime Dénès and Bruno Barras. To ensure compatibility with the +univalence axiom, a new flag ``-indices-matter'' has been implemented, +taking into account the universe levels of indices when computing the +levels of inductive types. This supports using {\Coq} as a tool to explore +the relations between homotopy theory and type theory. + +Maxime Dénès and Benjamin Grégoire developed an implementation of +conversion test and normal form computation using the OCaml native +compiler. It complements the virtual machine conversion offering much +faster computation for expensive functions. + +{\Coq} 8.5 also comes with a bunch of many various smaller-scale +changes and improvements regarding the different components of the +system. We shall only list a few of them. + +Pierre Boutillier developed an improved tactic for simplification of +expressions called {\tt cbn}. + +Maxime Dénès maintained the bytecode-based reduction machine. Pierre +Letouzey maintained the extraction mechanism. + +Pierre-Marie Pédrot has extended the syntax of terms to, +experimentally, allow holes in terms to be solved by a locally +specified tactic. + +Existential variables are referred to by identifiers rather than mere +numbers, thanks to Hugo Herbelin who also improved the tactic language +here and there. + +Error messages for universe inconsistencies have been improved by +Matthieu Sozeau. Error messages for unification and type inference +failures have been improved by Hugo Herbelin, Pierre-Marie Pédrot and +Arnaud Spiwack. + +Pierre Courtieu contributed new features for using {\Coq} through Proof +General and for better interactive experience (bullets, Search, etc). + +The efficiency of the whole system has been significantly improved +thanks to contributions from Pierre-Marie Pédrot. + +A distribution channel for {\Coq} packages using the OPAM tool has +been initiated by Thomas Braibant and developed by Guillaume Claret, +with contributions by Enrico Tassi and feedback from Hugo Herbelin. + +Packaging tools were provided by Pierre Letouzey and Enrico Tassi +(Windows), Pierre Boutillier, Matthieu Sozeau and Maxime Dénès (MacOS +X). Maxime Dénès improved significantly the testing and benchmarking +support. + +Many power users helped to improve the design of the new features via +the bug tracker, the coq development mailing list or the coq-club +mailing list. Special thanks are going to the users who contributed +patches and intensive brain-storming, starting with Jason Gross, +Jonathan Leivent, Greg Malecha, Clément Pit-Claudel, Marc Lasson, +Lionel Rieg. It would however be impossible to mention with precision +all names of people who to some extent influenced the development. + +Version 8.5 is one of the most important release of {\Coq}. Its +development spanned over about 3 years and a half with about one year +of beta-testing. General maintenance during part or whole of this +period has been done by Pierre Boutillier, Pierre Courtieu, Maxime +Dénès, Hugo Herbelin, Pierre Letouzey, Guillaume Melquiond, +Pierre-Marie Pédrot, Matthieu Sozeau, Arnaud Spiwack, Enrico Tassi as +well as Bruno Barras, Yves Bertot, Frédéric Besson, Xavier Clerc, +Pierre Corbineau, Jean-Christophe Filliâtre, Julien Forest, Sébastien +Hinderer, Assia Mahboubi, Jean-Marc Notin, Yann Régis-Gianas, François +Ripault, Carst Tankink. Maxime Dénès coordinated the release process. + +\begin{flushright} +Paris, January 2015, revised December 2015,\\ +Hugo Herbelin, Matthieu Sozeau and the {\Coq} development team\\ +\end{flushright} + +\section*{Credits: version 8.6} + +{\Coq} version 8.6 contains the result of refinements, stabilization of +8.5's features and cleanups of the internals of the system. Over the +year of (now time-based) development, about 450 bugs were resolved and +over 100 contributions integrated. The main user visible changes are: +\begin{itemize} +\item A new, faster state-of-the-art universe constraint checker, by + Jacques-Henri Jourdan. +\item In CoqIDE and other asynchronous interfaces, more fine-grained + asynchronous processing and error reporting by Enrico Tassi, making {\Coq} + capable of recovering from errors and continue processing the document. +\item More access to the proof engine features from Ltac: goal + management primitives, range selectors and a {\tt typeclasses + eauto} engine handling multiple goals and multiple successes, by + Cyprien Mangin, Matthieu Sozeau and Arnaud Spiwack. +\item Tactic behavior uniformization and specification, generalization + of intro-patterns by Hugo Herbelin and others. +\item A brand new warning system allowing to control warnings, turn them + into errors or ignore them selectively by Maxime Dénès, Guillaume + Melquiond, Pierre-Marie Pédrot and others. +\item Irrefutable patterns in abstractions, by Daniel de Rauglaudre. +\item The {\tt ssreflect} subterm selection algorithm by Georges Gonthier and + Enrico Tassi is now accessible to tactic writers through the {\tt ssrmatching} + plugin. +\item Integration of {\tt LtacProf}, a profiler for {\tt Ltac} by Jason + Gross, Paul Steckler, Enrico Tassi and Tobias Tebbi. +\end{itemize} + +{\Coq} 8.6 also comes with a bunch of smaller-scale changes and +improvements regarding the different components of the system. We shall +only list a few of them. + +The {\tt iota} reduction flag is now a shorthand for {\tt match}, {\tt + fix} and {\tt cofix} flags controlling the corresponding reduction +rules (by Hugo Herbelin and Maxime Dénès). + +Maxime Dénès maintained the native compilation machinery. + +Pierre-Marie Pédrot separated the Ltac code from general purpose +tactics, and generalized and rationalized the handling of generic +arguments, allowing to create new versions of Ltac more easily in the +future. + +In patterns and terms, {\tt @}, abbreviations and notations are now +interpreted the same way, by Hugo Herbelin. + +Name handling for universes has been improved by Pierre-Marie Pédrot and +Matthieu Sozeau. The minimization algorithm has been improved by +Matthieu Sozeau. + +The unifier has been improved by Hugo Herbelin and Matthieu Sozeau, +fixing some incompatibilities introduced in Coq 8.5. Unification +constraints can now be left floating around and be seen by the user +thanks to a new option. The {\tt Keyed Unification} mode has been +improved by Matthieu Sozeau. + +The typeclass resolution engine and associated proof-search tactic have +been reimplemented on top of the proof-engine monad, providing better +integration in tactics, and new options have been introduced to control +it, by Matthieu Sozeau with help from Théo Zimmermann. + +The efficiency of the whole system has been significantly improved +thanks to contributions from Pierre-Marie Pédrot, Maxime Dénès and +Matthieu Sozeau and performance issue tracking by Jason Gross and Paul +Steckler. + +Standard library improvements by Jason Gross, Sébastien Hinderer, Pierre +Letouzey and others. + +Emilio Jesús Gallego Arias contributed many cleanups and refactorings of +the pretty-printing and user interface communication components. + +Frédéric Besson maintained the micromega tactic. + +The OPAM repository for {\Coq} packages has been maintained by Guillaume +Claret, Guillaume Melquiond, Matthieu Sozeau, Enrico Tassi and others. A +list of packages is now available at \url{https://coq.inria.fr/opam/www/}. + +Packaging tools and software development kits were prepared by Michael +Soegtrop with the help of Maxime Dénès and Enrico Tassi for Windows, and +Maxime Dénès and Matthieu Sozeau for MacOS X. Packages are now regularly +built on the continuous integration server. {\Coq} now comes with a {\tt + META} file usable with {\tt ocamlfind}, contributed by Emilio Jesús +Gallego Arias, Gregory Malecha, and Matthieu Sozeau. + +Matej Košík maintained and greatly improved the continuous integration +setup and the testing of {\Coq} contributions. He also contributed many +API improvement and code cleanups throughout the system. + +The contributors for this version are Bruno Barras, C.J. Bell, Yves +Bertot, Frédéric Besson, Pierre Boutillier, Tej Chajed, Guillaume +Claret, Xavier Clerc, Pierre Corbineau, Pierre Courtieu, Maxime Dénès, +Ricky Elrod, Emilio Jesús Gallego Arias, Jason Gross, Hugo Herbelin, +Sébastien Hinderer, Jacques-Henri Jourdan, Matej Kosik, Xavier Leroy, +Pierre Letouzey, Gregory Malecha, Cyprien Mangin, Erik Martin-Dorel, +Guillaume Melquiond, Clément Pit--Claudel, Pierre-Marie Pédrot, Daniel +de Rauglaudre, Lionel Rieg, Gabriel Scherer, Thomas Sibut-Pinote, +Matthieu Sozeau, Arnaud Spiwack, Paul Steckler, Enrico Tassi, Laurent +Théry, Nickolai Zeldovich and Théo Zimmermann. The development process +was coordinated by Hugo Herbelin and Matthieu Sozeau with the help of +Maxime Dénès, who was also in charge of the release process. + +Many power users helped to improve the design of the new features via +the bug tracker, the pull request system, the {\Coq} development mailing +list or the coq-club mailing list. Special thanks to the users who +contributed patches and intensive brain-storming and code reviews, +starting with Cyril Cohen, Jason Gross, Robbert Krebbers, Jonathan +Leivent, Xavier Leroy, Gregory Malecha, Clément Pit--Claudel, Gabriel +Scherer and Beta Ziliani. It would however be impossible to mention +exhaustively the names of everybody who to some extent influenced the +development. + +Version 8.6 is the first release of {\Coq} developed on a time-based +development cycle. Its development spanned 10 months from the release of +{\Coq} 8.5 and was based on a public roadmap. To date, it contains more +external contributions than any previous {\Coq} system. Code reviews +were systematically done before integration of new features, with an +important focus given to compatibility and performance issues, resulting +in a hopefully more robust release than {\Coq} 8.5. + +Coq Enhancement Proposals (CEPs for short) were introduced by Enrico +Tassi to provide more visibility and a discussion period on new +features, they are publicly available \url{https://github.com/coq/ceps}. + +Started during this period, an effort is led by Yves Bertot and Maxime +Dénès to put together a {\Coq} consortium. + +\begin{flushright} +Paris, November 2016,\\ +Matthieu Sozeau and the {\Coq} development team\\ +\end{flushright} + +\section*{Credits: version 8.7} + +{\Coq} version 8.7 contains the result of refinements, stabilization of +features and cleanups of the internals of the system along with a few +new features. The main user visible changes are: +\begin{itemize} +\item New tactics: variants of tactics supporting existential variables + \texttt{eassert}, \texttt{eenough}, etc... by Hugo Herbelin. Tactics + \texttt{extensionality in H} and \texttt{inversion\_sigma} by Jason + Gross, \texttt{specialize with ...} accepting partial bindings by + Pierre Courtieu. +\item Cumulative Polymorphic Inductive Types, allowing cumulativity of + universes to go through applied inductive types, by Amin Timany and + Matthieu Sozeau. +\item Integration of the \texttt{SSReflect} plugin and its documentation in the + reference manual, by Enrico Tassi, Assia Mahboubi and Maxime Dénès. +\item The \texttt{coq\_makefile} tool was completely redesigned to improve its + maintainability and the extensibility of generated Makefiles, and to + make \texttt{\_CoqProject} files more palatable to IDEs by Enrico Tassi. +\end{itemize} + +{\Coq} 8.7 involved a large amount of work on cleaning and speeding up +the code base, notably the work of Pierre-Marie Pédrot on making the +tactic-level system insensitive to existential variable expansion, +providing a safer API to plugin writers and making the code more +robust. The \texttt{dev/doc/changes.txt} file documents the numerous +changes to the implementation and improvements of interfaces. An effort +to provide an official, streamlined API to plugin writers is in +progress, thanks to the work of Matej Košík. + +Version 8.7 also comes with a bunch of smaller-scale changes and improvements +regarding the different components of the system. We shall only list a +few of them. + +The efficiency of the whole system has been significantly improved +thanks to contributions from Pierre-Marie Pédrot, Maxime Dénès and +Matthieu Sozeau and performance issue tracking by Jason Gross and Paul +Steckler. + +Thomas Sibut-Pinote and Hugo Herbelin added support for side effects +hooks in \texttt{cbv}, \texttt{cbn} and \texttt{simpl}. The side +effects are provided via a plugin available at +\url{https://github.com/herbelin/reduction-effects/}. + +The \texttt{BigN}, \texttt{BigZ}, \texttt{BigQ} libraries are no longer +part of the {\Coq} standard library, they are now provided by a separate +repository \url{https://github.com/coq/bignums}, maintained by Pierre +Letouzey. + +In the \texttt{Reals} library, \texttt{IZR} has been changed to produce +a compact representation of integers and real constants are now +represented using \texttt{IZR} (work by Guillaume Melquiond). + +Standard library additions and improvements by Jason Gross, Pierre +Letouzey and others, documented in the CHANGES file. + +The mathematical proof language/declarative mode plugin was removed from +the archive. + +The OPAM repository for {\Coq} packages has been maintained by Guillaume +Melquiond, Matthieu Sozeau, Enrico Tassi with contributions from many +users. A list of packages is available at +\url{https://coq.inria.fr/opam/www/}. + +Packaging tools and software development kits were prepared by Michael +Soegtrop with the help of Maxime Dénès and Enrico Tassi for Windows, and +Maxime Dénès for MacOS X. Packages are regularly built on the +Travis continuous integration server. + +The contributors for this version are Abhishek Anand, C.J. Bell, Yves +Bertot, Frédéric Besson, Tej Chajed, Pierre Courtieu, Maxime Dénès, +Julien Forest, Gaëtan Gilbert, Jason Gross, Hugo Herbelin, Emilio Jesús +Gallego Arias, Ralf Jung, Matej Košík, Xavier Leroy, Pierre Letouzey, +Assia Mahboubi, Cyprien Mangin, Erik Martin-Dorel, Olivier Marty, +Guillaume Melquiond, Sam Pablo Kuper, Benjamin Pierce, Pierre-Marie +Pédrot, Lars Rasmusson, Lionel Rieg, Valentin Robert, Yann Régis-Gianas, +Thomas Sibut-Pinote, Michael Soegtrop, Matthieu Sozeau, Arnaud Spiwack, +Paul Steckler, George Stelle, Pierre-Yves Strub, Enrico Tassi, Hendrik +Tews, Amin Timany, Laurent Théry, Vadim Zaliva and Théo Zimmermann. + +The development process was coordinated by Matthieu Sozeau with the help +of Maxime Dénès, who was also in charge of the release process. Théo +Zimmermann is the maintainer of this release. + +Many power users helped to improve the design of the new features via +the bug tracker, the pull request system, the {\Coq} development mailing +list or the coq-club mailing list. Special thanks to the users who +contributed patches and intensive brain-storming and code reviews, +starting with Jason Gross, Ralf Jung, Robbert Krebbers, Xavier Leroy, +Clément Pit--Claudel and Gabriel Scherer. It would however be impossible +to mention exhaustively the names of everybody who to some extent +influenced the development. + +Version 8.7 is the second release of {\Coq} developed on a time-based +development cycle. Its development spanned 9 months from the release of +{\Coq} 8.6 and was based on a public road-map. It attracted many external +contributions. Code reviews and continuous integration testing were +systematically used before integration of new features, with an +important focus given to compatibility and performance issues, resulting +in a hopefully more robust release than {\Coq} 8.6 while maintaining +compatibility. + +Coq Enhancement Proposals (CEPs for short) and open pull-requests +discussions were used to discuss publicly the new features. + +The {\Coq} consortium, an organization directed towards users and +supporters of the system, is now upcoming and will rely on Inria's +newly created Foundation. + +\begin{flushright} +Paris, August 2017,\\ +Matthieu Sozeau and the {\Coq} development team\\ +\end{flushright} + + +%new Makefile + +%\newpage + +% Integration of ZArith lemmas from Sophia and Nijmegen. + + +% $Id$ + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "Reference-Manual" +%%% End: -- cgit v1.2.3