diff options
| author |  Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
|---|---|---|
| committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
| commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
| tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /doc | |
| parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) | |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/LICENSE | 6 | ||||
| -rw-r--r-- | doc/common/styles/html/coqremote/footer.html | 6 | ||||
| -rw-r--r-- | doc/common/styles/html/coqremote/header.html | 34 | ||||
| -rw-r--r-- | doc/common/styles/html/simple/header.html | 6 | ||||
| -rwxr-xr-x | doc/stdlib/Library.tex | 2 | ||||
| -rw-r--r-- | doc/stdlib/hidden-files | 1 | ||||
| -rw-r--r-- | doc/stdlib/index-list.html.template | 95 | ||||
| -rwxr-xr-x | doc/stdlib/make-library-files | 36 | ||||
| -rwxr-xr-x | doc/stdlib/make-library-index | 8 | ||||
| -rw-r--r-- | doc/whodidwhat/whodidwhat-8.2update.tex | 303 | ||||
| -rw-r--r-- | doc/whodidwhat/whodidwhat-8.3update.tex | 312 | ||||
| -rw-r--r-- | doc/whodidwhat/whodidwhat-8.4update.tex | 334 | ||||
| -rw-r--r-- | doc/whodidwhat/whodidwhat-8.5update.tex | 346 |
13 files changed, 1379 insertions, 110 deletions
diff --git a/doc/LICENSE b/doc/LICENSE index 99087480..ada22e66 100644 --- a/doc/LICENSE +++ b/doc/LICENSE @@ -8,7 +8,7 @@ forth in the Open Publication License, v1.0 or later (the latest version is presently available at http://www.opencontent.org/openpub/). Options A and B are *not* elected. -The Coq Tutorial is a work by Gérard Huet, Gilles Kahn and Christine +The Coq Tutorial is a work by Gérard Huet, Gilles Kahn and Christine Paulin-Mohring. All documents (the LaTeX source and the PostScript, PDF and html outputs) are copyright (c) INRIA 1999-2006. The material connected to the Coq Tutorial may be distributed only subject to the @@ -25,7 +25,7 @@ the PostScript, PDF and html outputs) are copyright (c) INRIA distributed under the terms of the Lesser General Public License version 2.1 or later. -The FAQ (Coq for the Clueless) is a work by Pierre Castéran, Hugo +The FAQ (Coq for the Clueless) is a work by Pierre Castéran, Hugo Herbelin, Florent Kirchner, Benjamin Monate, and Julien Narboux. All documents (the LaTeX source and the PostScript, PDF and html outputs) are copyright (c) INRIA 2004-2006. The material connected to the FAQ @@ -36,7 +36,7 @@ http://www.opencontent.org/openpub/). Options A and B are *not* elected. The Tutorial on [Co-]Inductive Types in Coq is a work by Pierre -Castéran and Eduardo Gimenez. All related documents (the LaTeX and +Castéran and Eduardo Gimenez. All related documents (the LaTeX and BibTeX sources and the PostScript, PDF and html outputs) are copyright (c) INRIA 1997-2006. The material connected to the Tutorial on [Co-]Inductive Types in Coq may be distributed only subject to the diff --git a/doc/common/styles/html/coqremote/footer.html b/doc/common/styles/html/coqremote/footer.html index ff38ba8a..23dfccb6 100644 --- a/doc/common/styles/html/coqremote/footer.html +++ b/doc/common/styles/html/coqremote/footer.html @@ -21,9 +21,9 @@ <div id="footer"> <div id="nav-footer"> <ul class="links-menu-footer"> - <li><a href="mailto:www-coq_@_lix.polytechnique.fr">webmaster</a></li> - <li><a href="http://validator.w3.org/check?uri=referer">xhtml valid</a></li> - <li><a href="http://jigsaw.w3.org/css-validator/check/referer">CSS valid</a></li> + <li><a href="mailto:coq-www_@_inria.fr">webmaster</a></li> + <li><a href="http://validator.w3.org/">xhtml valid</a></li> + <li><a href="http://jigsaw.w3.org/css-validator/">CSS valid</a></li> </ul> </div> </div> diff --git a/doc/common/styles/html/coqremote/header.html b/doc/common/styles/html/coqremote/header.html index 891fb328..c6c45091 100644 --- a/doc/common/styles/html/coqremote/header.html +++ b/doc/common/styles/html/coqremote/header.html @@ -2,18 +2,16 @@ <html xmlns="http://www.w3.org/1999/xhtml" lang="en" xml:lang="en"> <head> -<meta http-equiv="Content-Type" content="text/html; charset=ISO-8859-1"> -<title>Standard Library | The Coq Proof Assistant</title> - -<link rel="shortcut icon" href="favicon.ico" type="image/x-icon" /> -<style type="text/css" media="all">@import "http://coq.inria.fr/modules/node/node.css";</style> +<meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> +<link rel="shortcut icon" href="/favicon.ico" type="image/x-icon" /> +<link type="text/css" rel="stylesheet" media="all" href="/modules/node/node.css" /> +<link type="text/css" rel="stylesheet" media="all" href="/modules/system/defaults.css" /> +<link type="text/css" rel="stylesheet" media="all" href="/modules/system/system.css" /> +<link type="text/css" rel="stylesheet" media="all" href="/modules/user/user.css" /> +<link type="text/css" rel="stylesheet" media="all" href="/sites/all/themes/coq/style.css" /> +<link type="text/css" rel="stylesheet" media="all" href="/sites/all/themes/coq/coqdoc.css" /> -<style type="text/css" media="all">@import "http://coq.inria.fr/modules/system/defaults.css";</style> -<style type="text/css" media="all">@import "http://coq.inria.fr/modules/system/system.css";</style> -<style type="text/css" media="all">@import "http://coq.inria.fr/modules/user/user.css";</style> - -<style type="text/css" media="all">@import "http://coq.inria.fr/sites/all/themes/coq/style.css";</style> -<style type="text/css" media="all">@import "http://coq.inria.fr/sites/all/themes/coq/coqdoc.css";</style> +<title>Standard Library | The Coq Proof Assistant</title> </head> @@ -23,20 +21,20 @@ <div id="headertop"> <div id="nav"> <ul class="links-menu"> - <li><a href="http://coq.inria.fr/" class="active">Home</a></li> - <li><a href="http://coq.inria.fr/about-coq" title="More about coq">About Coq</a></li> - <li><a href="http://coq.inria.fr/download">Get Coq</a></li> - <li><a href="http://coq.inria.fr/documentation">Documentation</a></li> - <li><a href="http://coq.inria.fr/community">Community</a></li> + <li><a href="/" class="active">Home</a></li> + <li><a href="/about-coq" title="More about coq">About Coq</a></li> + <li><a href="/download">Get Coq</a></li> + <li><a href="/documentation">Documentation</a></li> + <li><a href="/community">Community</a></li> </ul> </div> </div> <div id="header"> <div id="logoWrapper"> - <div id="logo"><a href="http://coq.inria.fr/" title="Home"><img src="http://coq.inria.fr/files/barron_logo.png" alt="Home" /></a> + <div id="logo"><a href="/" title="Home"><img src="/files/barron_logo.png" alt="Home" /></a> </div> - <div id="siteName"><a href="http://coq.inria.fr/" title="Home">The Coq Proof Assistant</a> + <div id="siteName"><a href="/" title="Home">The Coq Proof Assistant</a> </div> </div> </div> diff --git a/doc/common/styles/html/simple/header.html b/doc/common/styles/html/simple/header.html index 14d2f988..c350a8b9 100644 --- a/doc/common/styles/html/simple/header.html +++ b/doc/common/styles/html/simple/header.html @@ -1,11 +1,11 @@ -<!DOCTYPE html +<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> <html xmlns="http://www.w3.org/1999/xhtml" xml:lang="en" lang="en"> <head> -<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-15"/> -<link rel="stylesheet" href="coqdoc.css" type="text/css"/> +<meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> +<link rel="stylesheet" href="coqdoc.css" type="text/css" /> <title>The Coq Standard Library</title> </head> diff --git a/doc/stdlib/Library.tex b/doc/stdlib/Library.tex index cb32adfc..44a0b1d3 100755 --- a/doc/stdlib/Library.tex +++ b/doc/stdlib/Library.tex @@ -1,9 +1,11 @@ \documentclass[11pt]{report} +\usepackage[mathletters]{ucs} \usepackage[utf8x]{inputenc} \usepackage[T1]{fontenc} \usepackage{fullpage} \usepackage{amsfonts} +\usepackage{url} \usepackage[color]{../../coqdoc} \input{../common/version} diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files index e69de29b..8b137891 100644 --- a/doc/stdlib/hidden-files +++ b/doc/stdlib/hidden-files @@ -0,0 +1 @@ + diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 833b5c4c..854c786c 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -3,7 +3,7 @@ <p>Here is a short description of the Coq standard library, which is distributed with the system. -It provides a set of modules directly available +It provides a set of modules directly available through the <tt>Require Import</tt> command.</p> <p>The standard library is composed of the following subdirectories:</p> @@ -12,27 +12,26 @@ through the <tt>Require Import</tt> command.</p> <dt> <b>Init</b>: The core library (automatically loaded when starting Coq) </dt> - <dd> + <dd> theories/Init/Notations.v theories/Init/Datatypes.v theories/Init/Logic.v theories/Init/Logic_Type.v + theories/Init/Nat.v theories/Init/Peano.v theories/Init/Specif.v theories/Init/Tactics.v theories/Init/Wf.v (theories/Init/Prelude.v) </dd> - + <dt> <b>Logic</b>: - Classical logic and dependent equality + Classical logic, dependent equality, extensionality, choice axioms </dt> <dd> theories/Logic/SetIsType.v - theories/Logic/Classical_Pred_Set.v theories/Logic/Classical_Pred_Type.v theories/Logic/Classical_Prop.v - theories/Logic/Classical_Type.v (theories/Logic/Classical.v) theories/Logic/ClassicalFacts.v theories/Logic/Decidable.v @@ -57,8 +56,11 @@ through the <tt>Require Import</tt> command.</p> theories/Logic/IndefiniteDescription.v theories/Logic/FunctionalExtensionality.v theories/Logic/ExtensionalityFacts.v + theories/Logic/WeakFan.v + theories/Logic/WKL.v + theories/Logic/FinFun.v </dd> - + <dt> <b>Structures</b>: Algebraic structures (types with equality, with order, ...). DecidableType* and OrderedType* are there only for compatibility. @@ -83,7 +85,7 @@ through the <tt>Require Import</tt> command.</p> <dt> <b>Bool</b>: Booleans (basic functions and results) </dt> - <dd> + <dd> theories/Bool/Bool.v theories/Bool/BoolEq.v theories/Bool/DecBool.v @@ -92,12 +94,12 @@ through the <tt>Require Import</tt> command.</p> theories/Bool/Zerob.v theories/Bool/Bvector.v </dd> - + <dt> <b>Arith</b>: Basic Peano arithmetic </dt> - <dd> - theories/Arith/Arith_base.v + <dd> + theories/Arith/PeanoNat.v theories/Arith/Le.v theories/Arith/Lt.v theories/Arith/Plus.v @@ -107,6 +109,7 @@ through the <tt>Require Import</tt> command.</p> theories/Arith/Between.v theories/Arith/Peano_dec.v theories/Arith/Compare_dec.v + (theories/Arith/Arith_base.v) (theories/Arith/Arith.v) theories/Arith/Min.v theories/Arith/Max.v @@ -173,8 +176,6 @@ through the <tt>Require Import</tt> command.</p> theories/ZArith/Zpow_def.v theories/ZArith/Zpow_alt.v theories/ZArith/Zpower.v - theories/ZArith/ZOdiv_def.v - theories/ZArith/ZOdiv.v theories/ZArith/Zdiv.v theories/ZArith/Zquot.v theories/ZArith/Zeuclid.v @@ -206,10 +207,13 @@ through the <tt>Require Import</tt> command.</p> theories/QArith/Qminmax.v </dd> - <dt> <b>Numbers</b>: + <dt> <b>Numbers</b>: An experimental modular architecture for arithmetic </dt> - <dt> <b> Prelude</b>: + <dd> + <dl> + <dt> <b> Prelude</b>: + </dt> <dd> theories/Numbers/BinNums.v theories/Numbers/NumPrelude.v @@ -219,6 +223,7 @@ through the <tt>Require Import</tt> command.</p> <dt> <b> NatInt</b>: Abstract mixed natural/integer/cyclic arithmetic + </dt> <dd> theories/Numbers/NatInt/NZAdd.v theories/Numbers/NatInt/NZAddOrder.v @@ -237,10 +242,10 @@ through the <tt>Require Import</tt> command.</p> theories/Numbers/NatInt/NZGcd.v theories/Numbers/NatInt/NZBits.v </dd> - </dt> - <dt> <b> Cyclic</b>: + <dt> <b> Cyclic</b>: Abstract and 31-bits-based cyclic arithmetic + </dt> <dd> theories/Numbers/Cyclic/Abstract/CyclicAxioms.v theories/Numbers/Cyclic/Abstract/NZCyclic.v @@ -259,10 +264,10 @@ through the <tt>Require Import</tt> command.</p> theories/Numbers/Cyclic/Int31/Int31.v theories/Numbers/Cyclic/ZModulo/ZModulo.v </dd> - </dt> - <dt> <b> Natural</b>: + <dt> <b> Natural</b>: Abstract and 31-bits-words-based natural arithmetic + </dt> <dd> theories/Numbers/Natural/Abstract/NAdd.v theories/Numbers/Natural/Abstract/NAddOrder.v @@ -293,10 +298,11 @@ through the <tt>Require Import</tt> command.</p> theories/Numbers/Natural/BigN/NMake.v theories/Numbers/Natural/BigN/NMake_gen.v </dd> - </dt> - <dt> <b> Integer</b>: - Abstract and concrete (especially 31-bits-words-based) integer arithmetic + <dt> <b> Integer</b>: + Abstract and concrete (especially 31-bits-words-based) integer + arithmetic + </dt> <dd> theories/Numbers/Integer/Abstract/ZAdd.v theories/Numbers/Integer/Abstract/ZAddOrder.v @@ -323,32 +329,32 @@ through the <tt>Require Import</tt> command.</p> theories/Numbers/Integer/BigZ/BigZ.v theories/Numbers/Integer/BigZ/ZMake.v </dd> - </dt> <dt><b> Rational</b>: Abstract and 31-bits-words-based rational arithmetic + </dt> <dd> theories/Numbers/Rational/SpecViaQ/QSig.v theories/Numbers/Rational/BigQ/BigQ.v theories/Numbers/Rational/BigQ/QMake.v </dd> - </dt> - </dt> - + </dl> + </dd> + <dt> <b>Relations</b>: Relations (definitions and basic results) </dt> - <dd> + <dd> theories/Relations/Relation_Definitions.v theories/Relations/Relation_Operators.v theories/Relations/Relations.v theories/Relations/Operators_Properties.v </dd> - + <dt> <b>Sets</b>: Sets (classical, constructive, finite, infinite, powerset, etc.) </dt> - <dd> + <dd> theories/Sets/Classical_sets.v theories/Sets/Constructive_sets.v theories/Sets/Cpo.v @@ -372,32 +378,39 @@ through the <tt>Require Import</tt> command.</p> theories/Sets/Relations_3.v theories/Sets/Uniset.v </dd> - + <dt> <b>Classes</b>: - <dd> + </dt> + <dd> theories/Classes/Init.v theories/Classes/RelationClasses.v theories/Classes/Morphisms.v theories/Classes/Morphisms_Prop.v theories/Classes/Morphisms_Relations.v theories/Classes/Equivalence.v + theories/Classes/CRelationClasses.v + theories/Classes/CMorphisms.v + theories/Classes/CEquivalence.v theories/Classes/EquivDec.v theories/Classes/SetoidTactics.v theories/Classes/SetoidClass.v theories/Classes/SetoidDec.v theories/Classes/RelationPairs.v + theories/Classes/DecidableClass.v </dd> <dt> <b>Setoids</b>: - <dd> + </dt> + <dd> theories/Setoids/Setoid.v </dd> - + <dt> <b>Lists</b>: Polymorphic lists, Streams (infinite sequences) </dt> - <dd> + <dd> theories/Lists/List.v + theories/Lists/ListDec.v theories/Lists/ListSet.v theories/Lists/SetoidList.v theories/Lists/SetoidPermutation.v @@ -413,13 +426,14 @@ through the <tt>Require Import</tt> command.</p> theories/Vectors/Fin.v theories/Vectors/VectorDef.v theories/Vectors/VectorSpec.v + theories/Vectors/VectorEq.v (theories/Vectors/Vector.v) </dd> <dt> <b>Sorting</b>: Axiomatizations of sorts </dt> - <dd> + <dd> theories/Sorting/Heap.v theories/Sorting/Permutation.v theories/Sorting/Sorting.v @@ -432,7 +446,7 @@ through the <tt>Require Import</tt> command.</p> <dt> <b>Wellfounded</b>: Well-founded Relations </dt> - <dd> + <dd> theories/Wellfounded/Disjoint_Union.v theories/Wellfounded/Inclusion.v theories/Wellfounded/Inverse_Image.v @@ -500,11 +514,11 @@ through the <tt>Require Import</tt> command.</p> theories/Strings/Ascii.v theories/Strings/String.v </dd> - + <dt> <b>Reals</b>: Formalization of real numbers </dt> - <dd> + <dd> theories/Reals/Rdefinitions.v theories/Reals/Raxioms.v theories/Reals/RIneq.v @@ -566,14 +580,13 @@ through the <tt>Require Import</tt> command.</p> theories/Reals/SeqSeries.v theories/Reals/Sqrt_reg.v theories/Reals/Rlogic.v - theories/Reals/LegacyRfield.v (theories/Reals/Reals.v) </dd> - + <dt> <b>Program</b>: Support for dependently-typed programming. </dt> - <dd> + <dd> theories/Program/Basics.v theories/Program/Wf.v theories/Program/Subset.v diff --git a/doc/stdlib/make-library-files b/doc/stdlib/make-library-files deleted file mode 100755 index c071c4a2..00000000 --- a/doc/stdlib/make-library-files +++ /dev/null @@ -1,36 +0,0 @@ -#!/bin/sh - -# Needs COQSRC and GALLINA set - -# On garde la liste de tous les *.v avec dates dans library.files.ls -# Si elle a change depuis la derniere fois ou library.files n'existe pas -# on fabrique des .g (si besoin) et la liste library.files dans -# l'ordre de ls -tr des *.vo -# Ce dernier trie les fichiers dans l'ordre inverse de leur date de création -# En supposant que make fait son boulot, ca fait un tri topologique du -# graphe des dépendances - -LIBDIRS="Arith PArith NArith ZArith Reals Logic Bool Lists Relations Sets Sorting Wellfounded Setoids Program Classes Numbers" - -rm -f library.files.ls.tmp -(cd $COQSRC/theories; find $LIBDIR -name "*.v" -ls) > library.files.ls.tmp -if ! test -e library.files || ! cmp library.files.ls library.files.ls.tmp; then - mv -f library.files.ls.tmp library.files.ls - rm -f library.files; touch library.files - ABSOLUTE=`pwd`/library.files - cd $COQSRC/theories - echo $LIBDIRS - for rep in $LIBDIRS ; do - (cd $rep - echo $rep/intro.tex >> $ABSOLUTE - VOFILES=`ls -tr *.vo` - for file in $VOFILES ; do - VF=`basename $file \.vo` - if [ \( ! -e $VF.g \) -o \( $VF.v -nt $VF.g \) ] ; then - $GALLINA $VF.v - fi - echo $rep/$VF.g >> $ABSOLUTE - done - ) - done -fi diff --git a/doc/stdlib/make-library-index b/doc/stdlib/make-library-index index 1a70567f..43802efa 100755 --- a/doc/stdlib/make-library-index +++ b/doc/stdlib/make-library-index @@ -6,17 +6,14 @@ FILE=$1 HIDDEN=$2 cp -f $FILE.template tmp -echo -n Building file index-list.prehtml ... +echo -n "Building file index-list.prehtml... " #LIBDIRS="Init Logic Structures Bool Arith PArith NArith ZArith QArith Relations Sets Classes Setoids Lists Vectors Sorting Wellfounded MSets FSets Reals Program Numbers Numbers/Natural/Abstract Numbers/Natural/Peano Numbers/Natural/Binary Numbers/Natural/BigN Numbers/Natural/SpecViaZ Numbers/Integer/Abstract Numbers/Integer/NatPairs Numbers/Integer/Binary Numbers/Integer/SpecViaZ Numbers/Integer/BigZ Numbers/NatInt Numbers/Cyclic/Abstract Numbers/Cyclic/Int31 Numbers/Cyclic/ZModulo Numbers/Cyclic/DoubleCyclic Numbers/Rational/BigQ Numbers/Rational/SpecViaQ Strings" -LIBDIRS=`find theories/* -type d | sed -e "s:^theories/::"` +LIBDIRS=`find theories/* -type d ! -name .coq-native | sed -e "s:^theories/::"` for k in $LIBDIRS; do i=theories/$k - echo $i - d=`basename $i` - if [ "$d" != "CVS" ]; then ls $i | grep -q \.v'$' if [ $? = 0 ]; then for j in $i/*.v; do @@ -46,7 +43,6 @@ for k in $LIBDIRS; do fi done fi - fi rm -f tmp2 sed -e "s/#$d#//" tmp > tmp2 mv -f tmp2 tmp diff --git a/doc/whodidwhat/whodidwhat-8.2update.tex b/doc/whodidwhat/whodidwhat-8.2update.tex new file mode 100644 index 00000000..4f4f0e95 --- /dev/null +++ b/doc/whodidwhat/whodidwhat-8.2update.tex @@ -0,0 +1,303 @@ +\documentclass{article} + +\usepackage{fullpage} +\usepackage[utf8]{inputenc} +\usepackage{t1enc} + +\begin{document} + +\title{Who did what in the Coq archive?} + +\author{The Coq development team} + +\maketitle + +\centerline{(updated for Coq 8.2)} + +\section{The Calculus of Inductive Constructions} + +\begin{itemize} +\item The Calculus of Constructions + \begin{itemize} + \item Core type-checker: Gérard Huet and Thierry Coquand with + optimizations by Chet Murthy, Bruno Barras + \item Head reduction functions: Gérard Huet, Christine Paulin, Bruno Barras + \end{itemize} +\item Conversion and reduction + \begin{itemize} + \item Lazy conversion machine: Bruno Barras + \item Transparency/opacity: Bruno Barras + \item Bytecode-based conversion: Benjamin Grégoire + \item Binary-words retroknowledge: Arnaud Spiwack + \end{itemize} +\item The universe hierarchy + \begin{itemize} + \item Floating universes: Gérard Huet, with contributions from Bruno Barras + \item Algebraic universes: Hugo Herbelin + \end{itemize} +\item Mutual inductive types and recursive definitions + \begin{itemize} + \item Type-checking: Christine Paulin + \item Positivity condition: Christine Paulin + \item Guardness condition for fixpoints: Christine Paulin; + extensions by Eduardo Gimenez and Bruno Barras + \item Recursively non-uniform parameters: Christine Paulin + \item Sort-polymorphism of inductive types: Hugo Herbelin + \end{itemize} +\item Local definitions: Hugo Herbelin +\item Mutual coinductive types and corecursive definitions: Eduardo Gimenez +\item Module system + \begin{itemize} + \item Core system: Jacek Chrz\k{a}szcz + \item Inlining: Claudio Sacerdoti Coen and Élie Soubiran + \item Module inclusion: Élie Soubiran + \item Functorial signature application: Élie Soubiran + \item Transparent name space: Élie Soubiran + \item Resolution of qualified names: Hugo Herbelin + \end{itemize} +\item Minimalist stand-alone type-checker (\texttt{coqchk}): Bruno Barras +\end{itemize} + +\section{Specification language} + +\begin{itemize} +\item Sections: Gilles Dowek with extra contributions by Gérard + Huet, Chet Murthy, Hugo Herbelin +\item The \texttt{Russell} specifications language, proof obligations (\texttt{Program}): Matthieu Sozeau +\item Type inference: Chet Murthy, with extra contributions by Bruno + Barras, Hugo Herbelin and Matthieu Sozeau +\item Pattern-matching: Hugo Herbelin on top of a first version by + Cristina Cornes +\item Implicit arguments: Amokrane Saïbi, with extensions by Hugo + Herbelin and Matthieu Sozeau +\item Coercions: Amokrane Saïbi +\item Records: Amokrane Saïbi with extensions by Arnaud Spiwack and + Matthieu Sozeau +\item Canonical structures: Amokrane Saïbi +\item Type classes: Matthieu Sozeau +\item Functional schemes (\texttt{Function}, \texttt{Functional Scheme}, ...): Julien Forest and Pierre Courtieu (preliminary version by Yves Bertot) +\item Generation of induction schemes: Christine Paulin, Vincent + Siles, Matthieu Sozeau + \end{itemize} + +\section{Tactics} + +\subsection{General tactic support} + +\begin{itemize} +\item Proof engine: Chet Murthy (first version by Thierry Coquand) +\item Ltac: David Delahaye, with extensions by Hugo Herbelin, Bruno Barras, ... +\item Tactic notations: Hugo Herbelin (first version by Chet Murthy) +\item Main tactic unification procedure: Chet Murthy with + contributions from Hugo Herbelin and Matthieu Sozeau +\item Mathematical-style language (C-Zar): Pierre Corbineau +\item Communication with external tools (\texttt{external}): Hugo Herbelin + +\end{itemize} + +\subsection{Predefined tactics} + +\begin{itemize} +\item Basic tactics (\texttt{intro}, \texttt{apply}, + \texttt{assumption}, \texttt{exact}): Thierry Coquand, with further + collective extensions +\item Reduction tactics: Christine Paulin (\texttt{simpl}), Bruno + Barras (\texttt{cbv}, \texttt{lazy}), ... +\item Tacticals: Thierry Coquand, Chet Murthy, Eduardo Gimenez, ... +\item Induction: Christine Paulin (\texttt{elim}, \texttt{case}), Hugo Herbelin (\texttt{induction}, \texttt{destruct} +\item Refinement (\texttt{refine}): Jean-Christophe Filliâtre +\item Introduction patterns: Eduardo Gimenez with collective extensions +\item Forward reasoning: Hugo Herbelin (\texttt{assert}, \texttt{apply in}), Pierre Letouzey (\texttt{specialize}, initial version by Amy Felty) +\item Rewriting tactics (\texttt{rewrite}): basic version by Christine Paulin, + extensions by Jean-Christophe Filliâtre and Pierre Letouzey +\item Tactics about equivalence properties (\texttt{reflexivity}, + \texttt{symmetry}, \texttt{transitivity}): Christine Paulin (?), +\item Equality tactics (\texttt{injection}/\texttt{discriminate}): + Cristina Cornes +\item Inversion tactics (\texttt{inversion}): Cristina Cornes, Chet Murthy +\item Setoid rewriting: Matthieu Sozeau (first version by Clément + Renard, second version by Claudio Sacerdoti Coen), contributions + from Nicolas Tabareau +\item Decision of equality: Eduardo Gimenez +\item Basic Ltac-level tactics: Pierre Letouzey, Matthieu Sozeau, + Evgeny Makarov +\end{itemize} + +\subsection{General automation tactics} + +\begin{itemize} +\item Resolution (\texttt{auto}, \texttt{trivial}): Christine Paulin + with extensions from Chet Murthy, Eduardo Gimenez, Patrick + Loiseleur (hint bases), Matthieu Sozeau +\item Resolution with existential variables (\texttt{eauto}): Chet Murthy, Jean-Christophe Filliâtre, with extensions from Matthieu Sozeau +\item Automatic rewriting (\texttt{autorewrite}): David Delahaye +\end{itemize} + +\subsection{Domain-specific decision tactics} + +\begin{itemize} +\item Congruence closure (\texttt{cc}): Pierre Corbineau +\item Decision of first-order logic (\texttt{firstorder}): Pierre Corbineau +\item Simplification of polynomial fractions (\texttt{field}): Laurent + Théry and Benjamin Grégoire (first version by David Delahaye and + Micaela Mayero) +\item Simplification of polynomial expressions (\texttt{ring}): Assia + Mahboubi, Bruno Barras and Benjamin Grégoire (first version by + Samuel Boutin, second version by Patrick Loiseleur) +\item Decision of systems of linear inequations: Frédéric Besson + (\texttt{psatzl}); Loïc Pottier (\texttt{fourier}) +\item Decision of systems of linear inequations over integers: + Frédéric Besson (\texttt{lia}); Pierre Crégut (\texttt{omega} and + \texttt{romega}) +\item (Partial) decision of systems of polynomical inequations + (\texttt{sos}, \texttt{psatz}): Frédéric Besson, with generalization + over arbitrary rings by Evgeny Makarov; uses HOL-Light interface to + \texttt{csdp} by John Harrisson +\item Decision/simplification of intuitionistic propositional logic: + David Delahaye (\texttt{tauto}, \texttt{intuition}, first version by + Cesar Mu\~noz, second version by Chet Murthy), with contributions + from Judicaël Courant; Pierre Corbineau (\texttt{rtauto}) +\item Decision/simplification of intuition first-order logic: Pierre + Corbineau (\texttt{firstorder}) +\end{itemize} + +\section{Extra tools} + +\begin{itemize} +\item Program extraction: Pierre Letouzey (first implementation by + Benjamin Werner, second by Jean-Christophe Filliâtre) +\item Export of context to external communication tools (\texttt{dp}): + Nicolas Ayache and Jean-Christophe Filliâtre, with contributions by + Claude Marché +\item Export of terms and environments to XML format: Claudio + Sacerdoti Coen, with extensions from Cezary Kaliszyk +\end{itemize} + +\section{Environment management} + +\begin{itemize} +\item Separate compilation: initiated by Chet Murthy +\item Import/Export: initiated by Chet Murthy +\item Options management: Hugo Herbelin with contributions by Arnaud Spiwack +\item Resetting and backtracking: Chet Murthy with contributions from Pierre Courtieu +\item Searching: Hugo Herbelin, Yves Bertot +\item Whelp suppport: Hugo Herbelin +\end{itemize} + +\section{Parsing and printing} + +\begin{itemize} +\item General parsing support: Chet Murthy, Bruno Barras, Daniel de Rauglaudre +\item General printing support: Chet Murthy, Jean-Christophe Filliâtre +\item Lexing: Daniel de Rauglaudre +\item Support for UTF-8: Hugo Herbelin, with contributions from Alexandre Miquel +\item Numerical notations: Hugo Herbelin, Patrick Loiseleur, Micaela Mayero +\item String notations: Hugo Herbelin +\item New ``V8'' syntax: Bruno Barras, Hugo Herbelin with contributions by Olivier Desmettre +\item Abbreviations: Chet Murthy +\item Notations: Chet Murthy, Hugo Herbelin +\end{itemize} + +\section{Libraries} + +\begin{itemize} +\item Init: collective (initiated by Christine Paulin and Gérard Huet) +\item Arith: collective (initiated by Christine Paulin) +\item ZArith: collective (initiated by Pierre Crégut) +\item Bool: collective (initiated by Christine Paulin) +\item NArith: Hugo Herbelin, Pierre Letouzey, Evgeny Makarov (out of + initial contibution by Pierre Crégut) +\item Lists: Pierre Letouzey, Jean-Marc Notin (initiated by Christine Paulin) +\item Reals: Micaela Mayero (axiomatization and main properties), Olivier Desmettre (convergence, derivability, integrals, trigonometric functions), contributions from Russell O'Connor and Cezary Kaliszyk +\item Relations: Bruno Barras, Cristina Cornes with contributions from + Pierre Castéran +\item Wellfounded: Bruno Barras, Cristina Cornes +\item FSets: Pierre Letouzey, from initial work with Jean-Christophe Filliâtre, decision tactic for FSets by Aaron Bohannon +\item Logic: Christine Paulin, Hugo Herbelin, Bruno Barras +\item Numbers: Evgeny Makarov (abstractions), Laurent Théry and Benjamin Grégoire (big numbers), Arnaud Spiwack and Pierre Letouzey (word-based arithmetic) +\item Classes: Matthieu Sozeau +\item QArith: Pierre Letouzey, with contributions from Russell O'Connor +\item Setoid: Matthieu Sozeau (first version by Clément Renard, second version by Claudio Sacerdoti Coen) +\item Sets: Gilles Kahn and Gérard Huet +\item Sorting: Gérard Huet +\item Strings: Laurent Théry +\item Program: Matthieu Sozeau +\item Unicode: Claude Marché +\end{itemize} + +\section{Commands} + +\begin{itemize} +\item Batch compiler (\texttt{coqc}): Chet Murthy (?) +\item Compilation dependency calculator (\texttt{coqdep}): + Jean-Christophe Filliâtre +\item Statistic tool (\texttt{coqwc}): Jean-Christophe Filliâtre +\item Simple html presentation tool (\texttt{gallina}) (deprecated): Jean-Christophe Filliâtre +\item Auto-maker (\texttt{coq\_makefile}): Jean-Christophe Filliâtre, + with contributions from Judicaël Courant +\item LaTeX presentation tool (\texttt{coq-tex}): Jean-Christophe Filliâtre +\item Multi-purpose presentation tool (\texttt{coqdoc}): Jean-Christophe Filliâtre with extensions from + Matthieu Sozeau, Jean-Marc Notin, Hugo Herbelin +\item Interactive toplevel (\texttt{coqtop}): Jean-Christophe Filliâtre (?) +\item Custom toplevel builder (\texttt{coqmktop}): Jean-Christophe Filliâtre (?) +\end{itemize} + +\section{Graphical interfaces} + +\begin{itemize} +\item Support for {\em PCoq}: Yves Bertot with contributions by + Laurence Rideau and Loïc Pottier; additional support for {\em TmEgg} + by Lionel Mamane +\item Support for {\em Proof General}: Pierre Courtieu +\item {\em CoqIDE}: Benjamin Monate with contributions from + Jean-Christophe Filliâtre, Claude Marché, Pierre Letouzey, Julien + Narboux, Hugo Herbelin, Pierre Corbineau; uses the Cameleon library + by Maxence Guesdon +\end{itemize} + +\section{Architecture} + +\begin{itemize} +\item Functional-kernel-based architecture: Jean-Christophe Filliâtre +\item Extensible objects and summaries: Chet Murthy +\item Hash-consing: Bruno Barras +\item Error locations: Jean-Christophe Filliâtre, Bruno Barras, Hugo Herbelin +\item Existential variables engine: Chet Murthy with a revision by + Bruno Barras and extensions by Clément Renard and Hugo Herbelin +\end{itemize} + +\section{Development tools} + +\begin{itemize} +\item Makefile's: Chet Murthy, Jean-Christophe Filliâtre, Judicaël + Courant, Lionel Mamane, Pierre Corbineau, Pierre Letouzey +\item Debugging: Jean-Christophe Filliâtre with contributions from Jacek Chrz\k{a}szcz, Hugo Herbelin, Bruno Barras, ... +\item ML quotations: David Delahaye and Daniel de Rauglaudre +\item ML tactic and vernacular extensions: Hugo Herbelin (first version by Chet Murthy) +\item Test suite: collective content, initiated by Jean-Christophe Filliâtre with further extensions by Hugo Herbelin, Jean-Marc Notin +\end{itemize} + +\section{Documentation} + +\begin{itemize} + +\item Reference Manual: collective, layout by Patrick Loiseleur, + Claude Marché (former User's Guide in 1991 by Gilles Dowek, Amy + Felty, Hugo Herbelin, Gérard Huet, Christine Paulin, Benjamin + Werner; initial documentation in 1989 by Thierry Coquand, Gilles + Dowek, Gérard Huet, Christine Paulin), +\item Basic tutorial: Gérard Huet, Gilles Kahn, Christine Paulin +\item Tutorial on recursive types: Eduardo Gimenez with updates by Pierre Castéran +\item FAQ: Hugo Herbelin, Julien Narboux, Florent Kirchner +\end{itemize} + +\section{Features discontinued by lack of support} + +\begin{itemize} +\item Searching modulo isomorphism: David Delahaye +\item Explanation of proofs in pseudo-natural language: Yann Coscoy +\end{itemize} + +Errors may have been inopportunely introduced, please report them to Hugo~\verb=.=~Herbelin~\verb=@=~inria~\verb=.=~fr + +\end{document} diff --git a/doc/whodidwhat/whodidwhat-8.3update.tex b/doc/whodidwhat/whodidwhat-8.3update.tex new file mode 100644 index 00000000..0a073781 --- /dev/null +++ b/doc/whodidwhat/whodidwhat-8.3update.tex @@ -0,0 +1,312 @@ +\documentclass{article} + +\usepackage{fullpage} +\usepackage[utf8]{inputenc} +\usepackage{t1enc} + +\begin{document} + +\title{Who did what in the Coq archive?} + +\author{The Coq development team} + +\maketitle + +\centerline{(updated for Coq 8.3)} + +\section{The Calculus of Inductive Constructions} + +\begin{itemize} +\item The Calculus of Constructions + \begin{itemize} + \item Core type-checker: Gérard Huet and Thierry Coquand with + optimizations by Chet Murthy, Bruno Barras + \item Head reduction functions: Gérard Huet, Christine Paulin, Bruno Barras + \end{itemize} +\item Conversion and reduction + \begin{itemize} + \item Lazy conversion machine: Bruno Barras + \item Transparency/opacity: Bruno Barras + \item Bytecode-based conversion: Benjamin Grégoire + \item Binary-words retroknowledge: Arnaud Spiwack + \end{itemize} +\item The universe hierarchy + \begin{itemize} + \item Floating universes: Gérard Huet, with contributions from Bruno Barras + \item Algebraic universes: Hugo Herbelin + \end{itemize} +\item Mutual inductive types and recursive definitions + \begin{itemize} + \item Type-checking: Christine Paulin + \item Positivity condition: Christine Paulin + \item Guardness condition for fixpoints: Christine Paulin; + extensions by Eduardo Gimenez and Bruno Barras + \item Recursively non-uniform parameters: Christine Paulin + \item Sort-polymorphism of inductive types: Hugo Herbelin + \end{itemize} +\item Local definitions: Hugo Herbelin +\item Mutual coinductive types and corecursive definitions: Eduardo Gimenez +\item Module system + \begin{itemize} + \item Core system: Jacek Chrz\k{a}szcz + \item Inlining: Claudio Sacerdoti Coen and Élie Soubiran + \item Module inclusion: Élie Soubiran + \item Functorial signature application: Élie Soubiran + \item Transparent name space: Élie Soubiran + \item Resolution of qualified names: Hugo Herbelin + \item Operator for nested functor application: Élie Soubiran and + Pierre Letouzey + \end{itemize} +\item Minimalist stand-alone type-checker (\texttt{coqchk}): Bruno Barras, with extra support for modules by Élie Soubiran +\end{itemize} + +\section{Specification language} + +\begin{itemize} +\item Sections: Gilles Dowek with extra contributions by Gérard + Huet, Chet Murthy, Hugo Herbelin +\item The \texttt{Russell} specifications language, proof obligations (\texttt{Program}): Matthieu Sozeau +\item Type inference: Chet Murthy, with extra contributions by Bruno + Barras, Hugo Herbelin and Matthieu Sozeau +\item Pattern-matching: Hugo Herbelin on top of a first version by + Cristina Cornes +\item Implicit arguments: Amokrane Saïbi, with extensions by Hugo + Herbelin and Matthieu Sozeau +\item Coercions: Amokrane Saïbi +\item Records: Amokrane Saïbi with extensions by Arnaud Spiwack and + Matthieu Sozeau +\item Canonical structures: Amokrane Saïbi +\item Type classes: Matthieu Sozeau +\item Functional schemes (\texttt{Function}, \texttt{Functional Scheme}, ...): Julien Forest and Pierre Courtieu (preliminary version by Yves Bertot) +\item Generation of induction schemes: Christine Paulin, Vincent + Siles, Matthieu Sozeau + \end{itemize} + +\section{Tactics} + +\subsection{General tactic support} + +\begin{itemize} +\item Proof engine: Chet Murthy (first version by Thierry Coquand) +\item Ltac: David Delahaye, with extensions by Hugo Herbelin, Bruno Barras, ... +\item Tactic notations: Hugo Herbelin (first version by Chet Murthy) +\item Main tactic unification procedure: Chet Murthy with + contributions from Hugo Herbelin and Matthieu Sozeau +\item Mathematical-style language (C-Zar): Pierre Corbineau +\item Communication with external tools (\texttt{external}): Hugo Herbelin + +\end{itemize} + +\subsection{Predefined tactics} + +\begin{itemize} +\item Basic tactics (\texttt{intro}, \texttt{apply}, + \texttt{assumption}, \texttt{exact}): Thierry Coquand, with further + collective extensions +\item Reduction tactics: Christine Paulin (\texttt{simpl}), Bruno + Barras (\texttt{cbv}, \texttt{lazy}), ... +\item Tacticals: Thierry Coquand, Chet Murthy, Eduardo Gimenez, ... +\item Induction: Christine Paulin (\texttt{elim}, \texttt{case}), Hugo Herbelin (\texttt{induction}, \texttt{destruct}, {\tt e}-variants of them), Matthieu Sozeau ({\tt dependent destruction}, {\tt dependent induction}) +\item Refinement (\texttt{refine}): Jean-Christophe Filliâtre +\item Introduction patterns: Eduardo Gimenez with collective extensions +\item Forward reasoning: Hugo Herbelin (\texttt{assert}, \texttt{apply in}), Pierre Letouzey (\texttt{specialize}, initial version by Amy Felty) +\item Rewriting tactics (\texttt{rewrite}): basic version by Christine Paulin, + extensions by Jean-Christophe Filliâtre ({\tt subst}), Pierre Letouzey (\verb=!=, \verb=?= modifiers) and Matthieu Sozeau (\verb=*=) +\item Tactics about equivalence properties (\texttt{reflexivity}, + \texttt{symmetry}, \texttt{transitivity}): Christine Paulin (?), + {\tt e}-variants by Hugo Herbelin, type-classes-based generalization to + arbitrary appropriate relations by Matthieu Sozeau +\item Equality tactics (\texttt{injection}/\texttt{discriminate}): + Cristina Cornes +\item Inversion tactics (\texttt{inversion}): Cristina Cornes, Chet Murthy +\item Setoid rewriting: Matthieu Sozeau (first version by Clément + Renard, second version by Claudio Sacerdoti Coen), contributions + from Nicolas Tabareau +\item Decision of equality: Eduardo Gimenez +\item Basic Ltac-level tactics: Pierre Letouzey, Matthieu Sozeau, + Evgeny Makarov, Hugo Herbelin +\end{itemize} + +\subsection{General automation tactics} + +\begin{itemize} +\item Resolution (\texttt{auto}, \texttt{trivial}): Christine Paulin + with extensions from Chet Murthy, Eduardo Gimenez, Patrick + Loiseleur (hint bases), Matthieu Sozeau +\item Resolution with existential variables (\texttt{eauto}): Chet Murthy, Jean-Christophe Filliâtre, with extensions from Matthieu Sozeau +\item Automatic rewriting (\texttt{autorewrite}): David Delahaye +\end{itemize} + +\subsection{Domain-specific decision tactics} + +\begin{itemize} +\item Congruence closure (\texttt{cc}): Pierre Corbineau +\item Decision of first-order logic (\texttt{firstorder}): Pierre Corbineau +\item Simplification of polynomial fractions (\texttt{field}): Laurent + Théry and Benjamin Grégoire (first version by David Delahaye and + Micaela Mayero) +\item Simplification of polynomial expressions (\texttt{ring}): Assia + Mahboubi, Bruno Barras and Benjamin Grégoire (first version by + Samuel Boutin, second version by Patrick Loiseleur) +\item Decision of systems of polynomial equations: Loïc Pottier (\texttt{nsatz}) +\item Decision of systems of linear inequations: Frédéric Besson + (\texttt{psatzl}); Loïc Pottier (\texttt{fourier}) +\item Decision of systems of linear inequations over integers: + Frédéric Besson (\texttt{lia}); Pierre Crégut (\texttt{omega} and + \texttt{romega}) +\item (Partial) decision of systems of polynomical inequations + (\texttt{sos}, \texttt{psatz}): Frédéric Besson, with generalization + over arbitrary rings by Evgeny Makarov; uses HOL-Light interface to + \texttt{csdp} by John Harrisson +\item Decision/simplification of intuitionistic propositional logic: + David Delahaye (\texttt{tauto}, \texttt{intuition}, first version by + Cesar Mu\~noz, second version by Chet Murthy), with contributions + from Judicaël Courant; Pierre Corbineau (\texttt{rtauto}) +\item Decision/simplification of intuition first-order logic: Pierre + Corbineau (\texttt{firstorder}) +\item Reification ({\tt quote}): Patrick Loiseleur, with + generalization by Stéphane Glondu +\end{itemize} + +\section{Extra tools} + +\begin{itemize} +\item Program extraction: Pierre Letouzey (first implementation by + Benjamin Werner, second by Jean-Christophe Filliâtre) +\item Export of context to external communication tools (\texttt{dp}): + Nicolas Ayache and Jean-Christophe Filliâtre, with contributions by + Claude Marché +\item Export of terms and environments to XML format: Claudio + Sacerdoti Coen, with extensions from Cezary Kaliszyk +\end{itemize} + +\section{Environment management} + +\begin{itemize} +\item Separate compilation: initiated by Chet Murthy +\item Import/Export: initiated by Chet Murthy +\item Options management: Hugo Herbelin with contributions by Arnaud Spiwack +\item Resetting and backtracking: Chet Murthy with contributions from Pierre Courtieu +\item Searching: Hugo Herbelin and Yves Bertot with extensions by Matthias Puech +\item Whelp suppport: Hugo Herbelin +\end{itemize} + +\section{Parsing and printing} + +\begin{itemize} +\item General parsing support: Chet Murthy, Bruno Barras, Daniel de Rauglaudre +\item General printing support: Chet Murthy, Jean-Christophe Filliâtre +\item Lexing: Daniel de Rauglaudre +\item Support for UTF-8: Hugo Herbelin, with contributions from Alexandre Miquel and Yann Régis-Gianas +\item Numerical notations: Hugo Herbelin, Patrick Loiseleur, Micaela Mayero +\item String notations: Hugo Herbelin +\item New ``V8'' syntax: Bruno Barras, Hugo Herbelin with contributions by Olivier Desmettre +\item Abbreviations: Chet Murthy +\item Notations: Chet Murthy, Hugo Herbelin +\end{itemize} + +\section{Libraries} + +\begin{itemize} +\item Init: collective (initiated by Christine Paulin and Gérard Huet) +\item Arith: collective (initiated by Christine Paulin) +\item ZArith: collective (initiated by Pierre Crégut) +\item Bool: collective (initiated by Christine Paulin) +\item NArith: Hugo Herbelin, Pierre Letouzey, Evgeny Makarov (out of + initial contibution by Pierre Crégut) +\item Lists: Pierre Letouzey, Jean-Marc Notin (initiated by Christine Paulin) +\item Reals: Micaela Mayero (axiomatization and main properties), Olivier Desmettre (convergence, derivability, integrals, trigonometric functions), contributions from Russell O'Connor, Cezary Kaliszyk, Guillaume Melquiond +\item Relations: Bruno Barras, Cristina Cornes with contributions from + Pierre Castéran +\item Wellfounded: Bruno Barras, Cristina Cornes +\item FSets: Pierre Letouzey, from initial work with Jean-Christophe Filliâtre, decision tactic for FSets by Aaron Bohannon +\item MSets: Pierre Letouzey +\item Logic: Christine Paulin, Hugo Herbelin, Bruno Barras +\item Numbers: Evgeny Makarov (abstractions), Laurent Théry and Benjamin Grégoire (big numbers), Arnaud Spiwack and Pierre Letouzey (word-based arithmetic), further extensions by Pierre Letouzey +\item Classes: Matthieu Sozeau +\item QArith: Pierre Letouzey, with contributions from Russell O'Connor +\item Setoid: Matthieu Sozeau (first version by Clément Renard, second version by Claudio Sacerdoti Coen) +\item Sets: Gilles Kahn and Gérard Huet +\item Sorting: Gérard Huet with revisions by Hugo Herbelin +\item Strings: Laurent Théry +\item Program: Matthieu Sozeau +\item Unicode: Claude Marché +\end{itemize} + +\section{Commands} + +\begin{itemize} +\item Batch compiler (\texttt{coqc}): Chet Murthy (?) +\item Compilation dependency calculator (\texttt{coqdep}): + Jean-Christophe Filliâtre +\item Statistic tool (\texttt{coqwc}): Jean-Christophe Filliâtre +\item Simple html presentation tool (\texttt{gallina}) (deprecated): Jean-Christophe Filliâtre +\item Auto-maker (\texttt{coq\_makefile}): Jean-Christophe Filliâtre, + with contributions from Judicaël Courant +\item LaTeX presentation tool (\texttt{coq-tex}): Jean-Christophe Filliâtre +\item Multi-purpose presentation tool (\texttt{coqdoc}): Jean-Christophe Filliâtre with extensions from + Matthieu Sozeau, Jean-Marc Notin, Hugo Herbelin +\item Interactive toplevel (\texttt{coqtop}): Jean-Christophe Filliâtre (?) +\item Custom toplevel builder (\texttt{coqmktop}): Jean-Christophe Filliâtre (?) +\end{itemize} + +\section{Graphical interfaces} + +\begin{itemize} +\item Support for {\em PCoq}: Yves Bertot with contributions by + Laurence Rideau and Loïc Pottier; additional support for {\em TmEgg} + by Lionel Mamane +\item Support for {\em Proof General}: Pierre Courtieu +\item {\em CoqIDE}: Benjamin Monate with contributions from + Jean-Christophe Filliâtre, Claude Marché, Pierre Letouzey, Julien + Narboux, Hugo Herbelin, Pierre Corbineau, Vincent Gross; uses the Cameleon library + by Maxence Guesdon +\end{itemize} + +\section{Architecture} + +\begin{itemize} +\item Functional-kernel-based architecture: Jean-Christophe Filliâtre +\item Extensible objects and summaries: Chet Murthy +\item Hash-consing: Bruno Barras +\item Error locations: Jean-Christophe Filliâtre, Bruno Barras, Hugo Herbelin +\item Existential variables engine: Chet Murthy with revisions by + Bruno Barras and Arnaud Spiwack and extensions by Clément Renard and + Hugo Herbelin +\end{itemize} + +\section{Development tools} + +\begin{itemize} +\item Makefile's: Chet Murthy, Jean-Christophe Filliâtre, Judicaël + Courant, Lionel Mamane, Pierre Corbineau, Pierre Letouzey +\item Debugging: Jean-Christophe Filliâtre with contributions from Jacek Chrz\k{a}szcz, Hugo Herbelin, Bruno Barras, ... +\item ML quotations: David Delahaye and Daniel de Rauglaudre +\item ML tactic and vernacular extensions: Hugo Herbelin (first version by Chet Murthy) +\item Test suite: collective content, initiated by Jean-Christophe Filliâtre with further extensions by Hugo Herbelin, Jean-Marc Notin +\end{itemize} + +\section{Documentation} + +\begin{itemize} + +\item Reference Manual: collective, layout by Patrick Loiseleur, + Claude Marché (former User's Guide in 1991 by Gilles Dowek, Amy + Felty, Hugo Herbelin, Gérard Huet, Christine Paulin, Benjamin + Werner; initial documentation in 1989 by Thierry Coquand, Gilles + Dowek, Gérard Huet, Christine Paulin), +\item Basic tutorial: Gérard Huet, Gilles Kahn, Christine Paulin +\item Tutorial on recursive types: Eduardo Gimenez with updates by Pierre Castéran +\item FAQ: Hugo Herbelin, Julien Narboux, Florent Kirchner +\end{itemize} + +\section{Features discontinued by lack of support} + +\begin{itemize} +\item Searching modulo isomorphism: David Delahaye +\item Explanation of proofs in pseudo-natural language: Yann Coscoy +\end{itemize} + +Errors may have been inopportunely introduced, please report them to Hugo~\verb=.=~Herbelin~\verb=@=~inria~\verb=.=~fr + +\end{document} diff --git a/doc/whodidwhat/whodidwhat-8.4update.tex b/doc/whodidwhat/whodidwhat-8.4update.tex new file mode 100644 index 00000000..696fff4f --- /dev/null +++ b/doc/whodidwhat/whodidwhat-8.4update.tex @@ -0,0 +1,334 @@ +\documentclass{article} + +\usepackage{fullpage} +\usepackage[utf8]{inputenc} +\usepackage{t1enc} + +\begin{document} + +\title{Who did what in the Coq archive?} + +\author{The Coq development team} + +\maketitle + +\centerline{(updated for Coq 8.4)} + +\section{The Calculus of Inductive Constructions} + +\begin{itemize} +\item The Calculus of Constructions + \begin{itemize} + \item Core type-checker: Gérard Huet and Thierry Coquand with + optimizations by Chet Murthy, Bruno Barras + \item Head reduction functions: Gérard Huet, Christine Paulin, Bruno Barras + \end{itemize} +\item Conversion and reduction + \begin{itemize} + \item Lazy conversion machine: Bruno Barras + \item Transparency/opacity: Bruno Barras + \item Bytecode-based conversion: Benjamin Grégoire + \item Binary-words retroknowledge: Arnaud Spiwack + \end{itemize} +\item The universe hierarchy + \begin{itemize} + \item Floating universes: Gérard Huet, with contributions from Bruno Barras + \item Algebraic universes: Hugo Herbelin + \end{itemize} +\item Mutual inductive types and recursive definitions + \begin{itemize} + \item Type-checking: Christine Paulin + \item Positivity condition: Christine Paulin + \item Guardness condition for fixpoints: Christine Paulin; + extensions by Eduardo Gimenez, Bruno Barras, Pierre Boutillier + \item Recursively non-uniform parameters: Christine Paulin + \item Sort-polymorphism of inductive types: Hugo Herbelin + \end{itemize} +\item Local definitions: Hugo Herbelin +\item Mutual coinductive types and corecursive definitions: Eduardo Gimenez +\item Module system + \begin{itemize} + \item Core system: Jacek Chrz\k{a}szcz + \item Inlining: Claudio Sacerdoti Coen and Élie Soubiran + \item Module inclusion: Élie Soubiran + \item Functorial signature application: Élie Soubiran + \item Transparent name space: Élie Soubiran + \item Resolution of qualified names: Hugo Herbelin + \item Operator for nested functor application: Élie Soubiran and + Pierre Letouzey + \end{itemize} +\item Minimalist stand-alone type-checker (\texttt{coqchk}): Bruno Barras, with extra support for modules by Élie Soubiran and Pierre Letouzey +\item Eta-conversion: Hugo Herbelin, with contributions from Stéphane + Glondu, Benjamin Grégoire +\end{itemize} + +\section{Specification language} + +\begin{itemize} +\item Sections: Gilles Dowek with extra contributions by Gérard + Huet, Chet Murthy, Hugo Herbelin +\item The \texttt{Russell} specifications language, proof obligations (\texttt{Program}): Matthieu Sozeau +\item Type inference: Chet Murthy, with extra contributions by Bruno + Barras, Hugo Herbelin, Matthieu Sozeau, Enrico Tassi +\item Pattern-matching: Hugo Herbelin on top of a first version by + Cristina Cornes +\item Implicit arguments: Amokrane Saïbi, with extensions by Hugo + Herbelin, Matthieu Sozeau, Pierre Boutillier +\item Synthetic {\tt Arguments} command: Enrico Tassi +\item Coercions: Amokrane Saïbi +\item Records: Amokrane Saïbi with extensions by Arnaud Spiwack and + Matthieu Sozeau +\item Canonical structures: Amokrane Saïbi +\item Type classes: Matthieu Sozeau +\item Functional schemes (\texttt{Function}, \texttt{Functional Scheme}, ...): Julien Forest and Pierre Courtieu (preliminary version by Yves Bertot) +\item Generation of induction schemes: Christine Paulin, Vincent + Siles, Matthieu Sozeau + \end{itemize} + +\section{Tactics} + +\subsection{General tactic support} + +\begin{itemize} +\item Proof engine: Arnaud Spiwack (first version by Thierry Coquand, second version by Chet Murthy) +\item Ltac: David Delahaye, with extensions by Hugo Herbelin, Bruno Barras, ... +\item Tactic notations: Hugo Herbelin (first version by Chet Murthy) +\item Main tactic unification procedure: Chet Murthy with + contributions from Hugo Herbelin and Matthieu Sozeau +\item Mathematical-style language (C-Zar): Pierre Corbineau +\item Communication with external tools (\texttt{external}): Hugo Herbelin +\item Proof structuring (bullets and brackets): Arnaud Spiwack +\end{itemize} + +\subsection{Predefined tactics} + +\begin{itemize} +\item Basic tactics (\texttt{intro}, \texttt{apply}, + \texttt{assumption}, \texttt{exact}): Thierry Coquand, with further + collective extensions +\item Reduction tactics: Christine Paulin (\texttt{simpl}), Bruno + Barras (\texttt{cbv}, \texttt{lazy}), with contributions from Hugo Herbelin, Enrico Tassi, ... +\item Tacticals: Thierry Coquand, Chet Murthy, Eduardo Gimenez, ...; + new versions of {\tt info} and {\tt Show Script} by Pierre Letouzey; + {\tt timeout} by Pierre Letouzey +\item Induction: Christine Paulin (\texttt{elim}, \texttt{case}), Hugo Herbelin (\texttt{induction}, \texttt{destruct} +\item Refinement (\texttt{refine}): Jean-Christophe Filliâtre +\item Introduction patterns: Eduardo Gimenez with collective extensions +\item Forward reasoning: Hugo Herbelin (\texttt{assert}, \texttt{apply in}), Pierre Letouzey (\texttt{specialize}, initial version by Amy Felty) +\item Rewriting tactics (\texttt{rewrite}): basic version by Christine Paulin, + extensions by Jean-Christophe Filliâtre and Pierre Letouzey +\item Tactics about equivalence properties (\texttt{reflexivity}, + \texttt{symmetry}, \texttt{transitivity}): Christine Paulin (?), +\item Equality tactics (\texttt{injection}/\texttt{discriminate}): + Cristina Cornes +\item Inversion tactics (\texttt{inversion}): Cristina Cornes, Chet Murthy +\item Setoid rewriting: Matthieu Sozeau (first version by Clément + Renard, second version by Claudio Sacerdoti Coen), contributions + from Nicolas Tabareau +\item Decision of equality: Eduardo Gimenez +\item Basic Ltac-level tactics: Pierre Letouzey, Matthieu Sozeau, + Evgeny Makarov +\item Tactics about existential variables: Clément Renard, Pierre Corbineau, Stéphane Glondu, Arnaud Spiwack, ... +\end{itemize} + +\subsection{General automation tactics} + +\begin{itemize} +\item Resolution (\texttt{auto}, \texttt{trivial}): Christine Paulin + with extensions from Chet Murthy, Eduardo Gimenez, Patrick + Loiseleur (hint bases), Matthieu Sozeau +\item Resolution with existential variables (\texttt{eauto}): Chet Murthy, Jean-Christophe Filliâtre, with extensions from Matthieu Sozeau +\item Automatic rewriting (\texttt{autorewrite}): David Delahaye +\end{itemize} + +\subsection{Domain-specific decision tactics} + +\begin{itemize} +\item Congruence closure (\texttt{cc}): Pierre Corbineau +\item Decision of first-order logic (\texttt{firstorder}): Pierre Corbineau +\item Simplification of polynomial fractions (\texttt{field}): Laurent + Théry and Benjamin Grégoire (first version by David Delahaye and + Micaela Mayero) +\item Simplification of polynomial expressions (\texttt{ring}): Assia + Mahboubi, Bruno Barras and Benjamin Grégoire (first version by + Samuel Boutin, second version by Patrick Loiseleur) +\item Decision of systems of polynomial equations: Loïc Pottier (\texttt{nsatz}) +\item Decision of systems of linear inequations: Frédéric Besson + (\texttt{psatzl}); Loïc Pottier (\texttt{fourier}) +\item Decision of systems of linear inequations over integers: + Frédéric Besson (\texttt{lia}); Pierre Crégut (\texttt{omega} and + \texttt{romega}) +\item (Partial) decision of systems of polynomical inequations + (\texttt{sos}, \texttt{psatz}): Frédéric Besson, with generalization + over arbitrary rings by Evgeny Makarov; uses HOL-Light interface to + \texttt{csdp} by John Harrisson +\item Decision/simplification of intuitionistic propositional logic: + David Delahaye (\texttt{tauto}, \texttt{intuition}, first version by + Cesar Mu\~noz, second version by Chet Murthy), with contributions + from Judicaël Courant; Pierre Corbineau (\texttt{rtauto}) +\item Decision/simplification of intuition first-order logic: Pierre + Corbineau (\texttt{firstorder}) +\end{itemize} + +\section{Extra tools} + +\begin{itemize} +\item Program extraction: Pierre Letouzey (first implementation by + Benjamin Werner, second by Jean-Christophe Filliâtre) +\item Export of context to external communication tools (\texttt{dp}): + Nicolas Ayache and Jean-Christophe Filliâtre, with contributions by + Claude Marché +\item Export of terms and environments to XML format: Claudio + Sacerdoti Coen, with extensions from Cezary Kaliszyk +\end{itemize} + +\section{Environment management} + +\begin{itemize} +\item Separate compilation: initiated by Chet Murthy +\item Import/Export: initiated by Chet Murthy +\item Options management: Hugo Herbelin with contributions by Arnaud Spiwack +\item Resetting and backtracking: Chet Murthy with contributions from Pierre Courtieu +\item Searching: Hugo Herbelin and Yves Bertot with extensions by Matthias Puech +\item Whelp suppport: Hugo Herbelin +\end{itemize} + +\section{Parsing and printing} + +\begin{itemize} +\item General parsing support: Chet Murthy, Bruno Barras, Daniel de Rauglaudre +\item General printing support: Chet Murthy, Jean-Christophe Filliâtre +\item Lexing: Daniel de Rauglaudre +\item Support for UTF-8: Hugo Herbelin, with contributions from Alexandre Miquel and Yann Régis-Gianas +\item Numerical notations: Hugo Herbelin, Patrick Loiseleur, Micaela Mayero +\item String notations: Hugo Herbelin +\item New ``V8'' syntax: Bruno Barras, Hugo Herbelin with contributions by Olivier Desmettre +\item Abbreviations: Chet Murthy +\item Notations: Chet Murthy, Hugo Herbelin +\end{itemize} + +\section{Libraries} + +\begin{itemize} +\item Init: collective (initiated by Christine Paulin and Gérard Huet) +\item Arith: collective (initiated by Christine Paulin) +\item ZArith: collective (initiated by Pierre Crégut) +\item Bool: collective (initiated by Christine Paulin) +\item NArith: Hugo Herbelin, Pierre Letouzey, Evgeny Makarov (out of + initial contibution by Pierre Crégut) +\item Lists: Pierre Letouzey, Jean-Marc Notin (initiated by Christine Paulin) +\item Vectors: Pierre Boutillier +\item Reals: Micaela Mayero (axiomatization and main properties), Olivier Desmettre (convergence, derivability, integrals, trigonometric functions), contributions from Russell O'Connor, Cezary Kaliszyk, Guillaume Melquiond, Yves Bertot, Guillaume Allais +\item Relations: Bruno Barras, Cristina Cornes with contributions from + Pierre Castéran +\item Wellfounded: Bruno Barras, Cristina Cornes +\item FSets: Pierre Letouzey, from initial work with Jean-Christophe Filliâtre, decision tactic for FSets by Aaron Bohannon, red-black trees by Andrew Appel and Pierre Letouzey +\item MSets: Pierre Letouzey +\item Logic: Christine Paulin, Hugo Herbelin, Bruno Barras +\item Numbers: Evgeny Makarov (abstractions), Laurent Théry and Benjamin Grégoire (big numbers), Arnaud Spiwack and Pierre Letouzey (word-based arithmetic), further extensions by Pierre Letouzey; integration of Arith and ZArith to Numbers by Pierre Letouzey +\item Classes: Matthieu Sozeau +\item QArith: Pierre Letouzey, with contributions from Russell O'Connor +\item Setoid: Matthieu Sozeau (first version by Clément Renard, second version by Claudio Sacerdoti Coen) +\item Sets: Gilles Kahn and Gérard Huet +\item Sorting: Gérard Huet with revisions by Hugo Herbelin +\item Strings: Laurent Théry +\item Program: Matthieu Sozeau +\item Unicode: Claude Marché +\end{itemize} + +\section{Commands} + +\begin{itemize} +\item Batch compiler (\texttt{coqc}): Chet Murthy (?) +\item Compilation dependency calculator (\texttt{coqdep}): + Jean-Christophe Filliâtre +\item Statistic tool (\texttt{coqwc}): Jean-Christophe Filliâtre +\item Simple html presentation tool (\texttt{gallina}) (deprecated): Jean-Christophe Filliâtre +\item Auto-maker (\texttt{coq\_makefile}): Jean-Christophe Filliâtre, + with contributions from Judicaël Courant, updated by Pierre Boutillier +\item LaTeX presentation tool (\texttt{coq-tex}): Jean-Christophe Filliâtre +\item Multi-purpose presentation tool (\texttt{coqdoc}): Jean-Christophe Filliâtre with extensions from + Matthieu Sozeau, Jean-Marc Notin, Hugo Herbelin and contributions from Adam Chlipala +\item Interactive toplevel (\texttt{coqtop}): Jean-Christophe Filliâtre (?) +\item Custom toplevel builder (\texttt{coqmktop}): Jean-Christophe Filliâtre (?) +\end{itemize} + +\section{Graphical interfaces} + +\begin{itemize} +\item Support for {\em PCoq}: Yves Bertot with contributions by + Laurence Rideau and Loïc Pottier; additional support for {\em TmEgg} + by Lionel Mamane +\item Support for {\em Proof General}: Pierre Courtieu with contributions from Arnaud Spiwack +\item {\em CoqIDE}: Benjamin Monate with contributions from + Jean-Christophe Filliâtre, Claude Marché, Pierre Letouzey, Julien + Narboux, Hugo Herbelin, Pierre Corbineau, Pierre Boutillier, + Pierre-Marie Pédrot; processus-based communication protocol by + Vincent Gross with contributions from Pierre Letouzey, Pierre + Boutillier, Pierre-Marie Pédrot; backtracking revised by Pierre + Letouzey; uses the Cameleon library by Maxence Guesdon; +\end{itemize} + +\section{Architecture} + +\begin{itemize} +\item Functional-kernel-based architecture: Jean-Christophe Filliâtre +\item Extensible objects and summaries: Chet Murthy +\item Hash-consing: Bruno Barras +\item Error locations: Jean-Christophe Filliâtre, Bruno Barras, Hugo Herbelin, with contributions from Arnaud Spiwack +\item Existential variables engine: Chet Murthy with revisions by + Bruno Barras and Arnaud Spiwack and extensions by Clément Renard and + Hugo Herbelin +\end{itemize} + +\section{Development tools} + +\begin{itemize} +\item Makefile's: Chet Murthy, Jean-Christophe Filliâtre, Judicaël + Courant, Lionel Mamane, Pierre Corbineau, Pierre Letouzey with + contributions from Stéphane Glondu, Hugo Herbelin, ... +\item Debugging: Jean-Christophe Filliâtre with contributions from Jacek Chrz\k{a}szcz, Hugo Herbelin, Bruno Barras, ... +\item ML quotations: David Delahaye and Daniel de Rauglaudre +\item ML tactic and vernacular extensions: Hugo Herbelin (first version by Chet Murthy) +\item Test suite: collective content, initiated by Jean-Christophe Filliâtre with further extensions by Hugo Herbelin, Jean-Marc Notin +\end{itemize} + +\section{Maintenance and system engineering} + +\begin{itemize} +\item General bug support: Gérard Huet, Christine Paulin, Chet Murthy, + Jean-Christophe Filliâtre, Hugo Herbelin, Bruno Barras, Pierre + Letouzey with contributions at some time from Benjamin Werner, + Jean-Marc Notin, Pierre Boutillier, ... +\item Team coordination: Gérard Huet, Christine Paulin, Hugo Herbelin, + with various other contributions +\item Packaging tools: Henri Laulhere, David Delahaye, Julien Narboux, + Pierre Letouzey, Enrico Tassi (Windows); Damien Doligez, Hugo + Herbelin, Pierre Boutillier (MacOS); Jean-Christophe Filliâtre, + Judicaël Courant, Hugo Herbelin, Stéphane Glondu (Linux) +\end{itemize} + +\section{Documentation} + +\begin{itemize} + +\item Reference Manual: collective, layout by Patrick Loiseleur, + Claude Marché (former User's Guide in 1991 by Gilles Dowek, Amy + Felty, Hugo Herbelin, Gérard Huet, Christine Paulin, Benjamin + Werner; initial documentation in 1989 by Thierry Coquand, Gilles + Dowek, Gérard Huet, Christine Paulin), +\item Basic tutorial: Gérard Huet, Gilles Kahn, Christine Paulin +\item Tutorial on recursive types: Eduardo Gimenez with updates by Pierre Castéran +\item FAQ: Hugo Herbelin, Julien Narboux, Florent Kirchner +\end{itemize} + +\section{Features discontinued by lack of support} + +\begin{itemize} +\item Searching modulo isomorphism: David Delahaye +\item Explanation of proofs in pseudo-natural language: Yann Coscoy +\end{itemize} + +For probable oversights or accidental errors, please report to Hugo~\verb=.=~Herbelin~\verb=@=~inria~\verb=.=~fr + +\end{document} diff --git a/doc/whodidwhat/whodidwhat-8.5update.tex b/doc/whodidwhat/whodidwhat-8.5update.tex new file mode 100644 index 00000000..ce099dc3 --- /dev/null +++ b/doc/whodidwhat/whodidwhat-8.5update.tex @@ -0,0 +1,346 @@ +\documentclass{article} + +\usepackage{fullpage} +\usepackage[utf8]{inputenc} +\usepackage{t1enc} + +\begin{document} + +\title{Who did what in the Coq archive?} + +\author{The Coq development team} + +\maketitle + +\centerline{(updated for Coq 8.5)} + +\section{The Calculus of Inductive Constructions} + +\begin{itemize} +\item The Calculus of Constructions + \begin{itemize} + \item Core type-checker: Gérard Huet and Thierry Coquand with + optimizations by Chet Murthy, Bruno Barras + \item Head reduction functions: Gérard Huet, Christine Paulin, Bruno Barras + \end{itemize} +\item Conversion and reduction + \begin{itemize} + \item Lazy conversion machine: Bruno Barras + \item Transparency/opacity: Bruno Barras + \item Bytecode-based conversion: Benjamin Grégoire + \item Binary-words retroknowledge: Arnaud Spiwack + \item Native code based conversion: Maxime Dénès, Benjamin Grégoire + \end{itemize} +\item The universe hierarchy + \begin{itemize} + \item Floating universes: Gérard Huet, with contributions from Bruno Barras + \item Algebraic universes: Hugo Herbelin + \end{itemize} +\item Mutual inductive types and recursive definitions + \begin{itemize} + \item Type-checking: Christine Paulin + \item Positivity condition: Christine Paulin + \item Guardness condition for fixpoints: Christine Paulin; + extensions by Eduardo Gimenez, Bruno Barras, Pierre Boutillier; fixes by + Bruno Barras, Maxime Dénès + \item Recursively non-uniform parameters: Christine Paulin + \item Sort-polymorphism of inductive types: Hugo Herbelin + \end{itemize} +\item Local definitions: Hugo Herbelin +\item Mutual coinductive types and corecursive definitions: Eduardo Gimenez +\item Module system + \begin{itemize} + \item Core system: Jacek Chrz\k{a}szcz + \item Inlining: Claudio Sacerdoti Coen and Élie Soubiran + \item Module inclusion: Élie Soubiran + \item Functorial signature application: Élie Soubiran + \item Transparent name space: Élie Soubiran + \item Resolution of qualified names: Hugo Herbelin + \item Operator for nested functor application: Élie Soubiran and + Pierre Letouzey + \end{itemize} +\item Minimalist stand-alone type-checker (\texttt{coqchk}): Bruno Barras, with extra support for modules by Élie Soubiran and Pierre Letouzey +\item Eta-conversion: Hugo Herbelin, with contributions from Stéphane + Glondu, Benjamin Grégoire +\end{itemize} + +\section{Specification language} + +\begin{itemize} +\item Sections: Gilles Dowek with extra contributions by Gérard + Huet, Chet Murthy, Hugo Herbelin +\item The \texttt{Russell} specifications language, proof obligations (\texttt{Program}): Matthieu Sozeau +\item Type inference: Chet Murthy, with extra contributions by Bruno + Barras, Hugo Herbelin, Matthieu Sozeau, Enrico Tassi +\item Pattern-matching: Hugo Herbelin on top of a first version by + Cristina Cornes, contributions by Arnaud Spiwack +\item Implicit arguments: Amokrane Saïbi, with extensions by Hugo + Herbelin, Matthieu Sozeau, Pierre Boutillier +\item Synthetic {\tt Arguments} command: Enrico Tassi +\item Coercions: Amokrane Saïbi +\item Records + \begin{itemize} + \item Core implementation: Amokrane Saïbi with extensions by Matthieu Sozeau + \item Extension to inductive and co-inductive records: Arnaud Spiwack + \item Non-recursive variants: Arnaud Spiwack + \end{itemize} +\item Canonical structures: Amokrane Saïbi +\item Type classes: Matthieu Sozeau +\item Function (\texttt{Function}, \texttt{functional induction}...): + Julien Forest (preliminary versions by Pierre Courtieu + (\texttt{Functional Schemes}) and Yves Bertot (\texttt{Recursive + Definition})) +\item Generation of induction schemes: Christine Paulin, Vincent + Siles, Matthieu Sozeau + \end{itemize} + +\section{Tactics} + +\subsection{General tactic support} + +\begin{itemize} +\item Proof engine: Arnaud Spiwack (first version by Thierry Coquand, second version by Chet Murthy) +\item Ltac: David Delahaye, with extensions by Hugo Herbelin, Bruno Barras, ... + Evolution to the new proof engine Arnaud Spiwack, Pierre-Marie P\'edrot +\item Tactic notations: Hugo Herbelin (first version by Chet Murthy) +\item Main tactic unification procedure: Chet Murthy with + contributions from Hugo Herbelin and Matthieu Sozeau +\item Mathematical-style language (C-Zar): Pierre Corbineau +\item Communication with external tools (\texttt{external}): Hugo Herbelin +\item Proof structuring (bullets and brackets): Arnaud Spiwack +\end{itemize} + +\subsection{Predefined tactics} + +\begin{itemize} +\item Basic refinement tactic (\texttt{refine}): Arnaud Spiwack (previous non-basic version by Jean-Christophe Filliâtre) +\item Core tactics (\texttt{intro}, \texttt{apply}, + \texttt{assumption}, \texttt{exact}): Thierry Coquand, with further + collective extensions +\item Reduction tactics: Christine Paulin (\texttt{simpl}), Bruno + Barras (\texttt{cbv}, \texttt{lazy}), Pierre Boutillier (\texttt{cbn}) + with contributions from Hugo Herbelin, Enrico Tassi, ... +\item Tacticals: Thierry Coquand, Chet Murthy, Eduardo Gimenez, ...; + new versions of {\tt info} and {\tt Show Script} by Pierre Letouzey; + {\tt timeout} by Pierre Letouzey; backtracking-related tacticals by Arnaud Spiwack +\item Generic tactic traces ({\tt Info}) by Arnaud Spiwack (based on the former {\tt info} tactical) +\item Induction: Christine Paulin (\texttt{elim}, \texttt{case}), Hugo Herbelin (\texttt{induction}, \texttt{destruct} +\item Introduction patterns: Eduardo Gimenez with collective extensions +\item Forward reasoning: Hugo Herbelin (\texttt{assert}, \texttt{enough}, \texttt{apply in}), + Pierre Letouzey (\texttt{specialize}, initial version by Amy Felty) +\item Rewriting tactics (\texttt{rewrite}): basic version by Christine Paulin, + extensions by Jean-Christophe Filliâtre and Pierre Letouzey +\item Setoid rewriting: Matthieu Sozeau (first version by Clément + Renard, second version by Claudio Sacerdoti Coen), contributions + from Nicolas Tabareau +\item Tactics about equivalence properties (\texttt{reflexivity}, + \texttt{symmetry}, \texttt{transitivity}): Christine Paulin (?), +\item Equality tactics (\texttt{injection}/\texttt{discriminate}): Cristina Cornes, extensions by Hugo Herbelin +\item Inversion tactics (\texttt{inversion}): Cristina Cornes, Chet Murthy +\item Decision of equality: Eduardo Gimenez +\item Basic Ltac-level tactics: Pierre Letouzey, Matthieu Sozeau, + Evgeny Makarov +\item Tactics about existential variables: Clément Renard, Pierre Corbineau, Stéphane Glondu, Arnaud Spiwack, ... +\end{itemize} + +\subsection{General automation tactics} + +\begin{itemize} +\item Resolution (\texttt{auto}, \texttt{trivial}): Christine Paulin + with extensions from Chet Murthy, Eduardo Gimenez, Patrick + Loiseleur (hint bases), Matthieu Sozeau +\item Resolution with existential variables (\texttt{eauto}): Chet Murthy, Jean-Christophe Filliâtre, with extensions from Matthieu Sozeau +\item Automatic rewriting (\texttt{autorewrite}): David Delahaye +\end{itemize} + +\subsection{Domain-specific decision tactics} + +\begin{itemize} +\item Congruence closure (\texttt{cc}): Pierre Corbineau +\item Decision of first-order logic (\texttt{firstorder}): Pierre Corbineau +\item Simplification of polynomial fractions (\texttt{field}): Laurent + Théry and Benjamin Grégoire (first version by David Delahaye and + Micaela Mayero) +\item Simplification of polynomial expressions (\texttt{ring}): Assia + Mahboubi, Bruno Barras and Benjamin Grégoire (first version by + Samuel Boutin, second version by Patrick Loiseleur) +\item Decision of systems of polynomial equations: Loïc Pottier (\texttt{nsatz}) +\item Decision of systems of linear inequations: Frédéric Besson + (\texttt{psatzl}); Loïc Pottier (\texttt{fourier}) +\item Decision of systems of linear inequations over integers: + Frédéric Besson (\texttt{lia}); Pierre Crégut (\texttt{omega} and + \texttt{romega}) +\item (Partial) decision of systems of polynomical inequations + (\texttt{sos}, \texttt{psatz}): Frédéric Besson, with generalization + over arbitrary rings by Evgeny Makarov; uses HOL-Light interface to + \texttt{csdp} by John Harrisson +\item Decision/simplification of intuitionistic propositional logic: + David Delahaye (\texttt{tauto}, \texttt{intuition}, first version by + Cesar Mu\~noz, second version by Chet Murthy), with contributions + from Judicaël Courant; Pierre Corbineau (\texttt{rtauto}) +\item Decision/simplification of intuition first-order logic: Pierre + Corbineau (\texttt{firstorder}) +\end{itemize} + +\section{Extra tools} + +\begin{itemize} +\item Program extraction: Pierre Letouzey (first implementation by + Benjamin Werner, second by Jean-Christophe Filliâtre) +\end{itemize} + +\section{Environment management} + +\begin{itemize} +\item Separate compilation: initiated by Chet Murthy +\item Import/Export: initiated by Chet Murthy +\item Options management: Hugo Herbelin with contributions by Arnaud Spiwack +\item Resetting and backtracking: Chet Murthy with contributions from Pierre Courtieu +\item Searching: Hugo Herbelin and Yves Bertot with extensions by Matthias Puech +\item Whelp suppport: Hugo Herbelin +\end{itemize} + +\section{Parsing and printing} + +\begin{itemize} +\item General parsing support: Chet Murthy, Bruno Barras, Daniel de Rauglaudre +\item General printing support: Chet Murthy, Jean-Christophe Filliâtre +\item Lexing: Daniel de Rauglaudre +\item Support for UTF-8: Hugo Herbelin, with contributions from Alexandre Miquel and Yann Régis-Gianas +\item Numerical notations: Hugo Herbelin, Patrick Loiseleur, Micaela Mayero +\item String notations: Hugo Herbelin +\item New ``V8'' syntax: Bruno Barras, Hugo Herbelin with contributions by Olivier Desmettre +\item Abbreviations: Chet Murthy +\item Notations: Chet Murthy, Hugo Herbelin +\end{itemize} + +\section{Libraries} + +\begin{itemize} +\item Init: collective (initiated by Christine Paulin and Gérard Huet) +\item Arith: collective (initiated by Christine Paulin) +\item ZArith: collective (initiated by Pierre Crégut) +\item Bool: collective (initiated by Christine Paulin) +\item NArith: Hugo Herbelin, Pierre Letouzey, Evgeny Makarov (out of + initial contibution by Pierre Crégut) +\item Lists: Pierre Letouzey, Jean-Marc Notin (initiated by Christine Paulin) +\item Vectors: Pierre Boutillier +\item Reals: Micaela Mayero (axiomatization and main properties), Olivier Desmettre (convergence, derivability, integrals, trigonometric functions), contributions from Russell O'Connor, Cezary Kaliszyk, Guillaume Melquiond, Yves Bertot, Guillaume Allais +\item Relations: Bruno Barras, Cristina Cornes with contributions from + Pierre Castéran +\item Wellfounded: Bruno Barras, Cristina Cornes +\item FSets: Pierre Letouzey, from initial work with Jean-Christophe Filliâtre, decision tactic for FSets by Aaron Bohannon, red-black trees by Andrew Appel and Pierre Letouzey +\item MSets: Pierre Letouzey +\item Logic: Christine Paulin, Hugo Herbelin, Bruno Barras, contributions by Arnaud Spiwack +\item Numbers: Evgeny Makarov (abstractions), Laurent Théry and Benjamin Grégoire (big numbers), Arnaud Spiwack and Pierre Letouzey (word-based arithmetic), further extensions by Pierre Letouzey; integration of Arith and ZArith to Numbers by Pierre Letouzey +\item Classes: Matthieu Sozeau +\item QArith: Pierre Letouzey, with contributions from Russell O'Connor +\item Setoid: Matthieu Sozeau (first version by Clément Renard, second version by Claudio Sacerdoti Coen) +\item Sets: Gilles Kahn and Gérard Huet +\item Sorting: Gérard Huet with revisions by Hugo Herbelin +\item Strings: Laurent Théry +\item Program: Matthieu Sozeau +\item Unicode: Claude Marché +\end{itemize} + +\section{Commands} + +\begin{itemize} +\item Batch compiler (\texttt{coqc}): Chet Murthy (?) +\item Compilation dependency calculator (\texttt{coqdep}): + Jean-Christophe Filliâtre +\item Statistic tool (\texttt{coqwc}): Jean-Christophe Filliâtre +\item Simple html presentation tool (\texttt{gallina}) (deprecated): Jean-Christophe Filliâtre +\item Auto-maker (\texttt{coq\_makefile}): Jean-Christophe Filliâtre, + with contributions from Judicaël Courant, updated by Pierre Boutillier +\item LaTeX presentation tool (\texttt{coq-tex}): Jean-Christophe Filliâtre +\item Multi-purpose presentation tool (\texttt{coqdoc}): Jean-Christophe Filliâtre with extensions from + Matthieu Sozeau, Jean-Marc Notin, Hugo Herbelin and contributions from Adam Chlipala +\item Interactive toplevel (\texttt{coqtop}): Jean-Christophe Filliâtre (?) +\item Custom toplevel builder (\texttt{coqmktop}): Jean-Christophe Filliâtre (?) +\end{itemize} + +\section{Graphical interfaces} + +\begin{itemize} +\item Support for {\em Proof General}: Pierre Courtieu with contributions from Arnaud Spiwack +\item {\em CoqIDE}: Benjamin Monate with contributions from + Jean-Christophe Filliâtre, Claude Marché, Pierre Letouzey, Julien + Narboux, Hugo Herbelin, Pierre Corbineau, Pierre Boutillier, + Pierre-Marie Pédrot; processus-based communication protocol by + Vincent Gross with contributions from Pierre Letouzey, Pierre + Boutillier, Pierre-Marie Pédrot; backtracking revised by Pierre + Letouzey; uses the Cameleon library by Maxence Guesdon; +\end{itemize} + +\section{Architecture} + +\begin{itemize} +\item Functional-kernel-based architecture: Jean-Christophe Filliâtre +\item Extensible objects and summaries: Chet Murthy +\item Hash-consing: Bruno Barras +\item Error locations: Jean-Christophe Filliâtre, Bruno Barras, Hugo Herbelin, with contributions from Arnaud Spiwack +\item Existential variables engine: Chet Murthy with revisions by + Bruno Barras and Arnaud Spiwack and extensions by Clément Renard and + Hugo Herbelin +\end{itemize} + +\section{Development tools} + +\begin{itemize} +\item Makefile's: Chet Murthy, Jean-Christophe Filliâtre, Judicaël + Courant, Lionel Mamane, Pierre Corbineau, Pierre Letouzey with + contributions from Stéphane Glondu, Hugo Herbelin, ... +\item Debugging: Jean-Christophe Filliâtre with contributions from Jacek Chrz\k{a}szcz, Hugo Herbelin, Bruno Barras, ... +\item ML quotations: David Delahaye and Daniel de Rauglaudre +\item ML tactic and vernacular extensions: Hugo Herbelin (first version by Chet Murthy) +\item Test suite: collective content, initiated by Jean-Christophe Filliâtre with further extensions by Hugo Herbelin, Jean-Marc Notin +\end{itemize} + +\section{Maintenance and system engineering} + +\begin{itemize} +\item General bug support: Gérard Huet, Christine Paulin, Chet Murthy, + Jean-Christophe Filliâtre, Hugo Herbelin, Bruno Barras, Pierre + Letouzey with contributions at some time from Benjamin Werner, + Jean-Marc Notin, Pierre Boutillier, ... +\item Team coordination: Gérard Huet, Christine Paulin, Hugo Herbelin, + with various other contributions +\item Packaging tools: Henri Laulhere, David Delahaye, Julien Narboux, + Pierre Letouzey, Enrico Tassi (Windows); Damien Doligez, Hugo + Herbelin, Pierre Boutillier (MacOS); Jean-Christophe Filliâtre, + Judicaël Courant, Hugo Herbelin, Stéphane Glondu (Linux) +\end{itemize} + +\section{Documentation} + +\begin{itemize} + +\item Reference Manual: collective, layout by Patrick Loiseleur, + Claude Marché (former User's Guide in 1991 by Gilles Dowek, Amy + Felty, Hugo Herbelin, Gérard Huet, Christine Paulin, Benjamin + Werner; initial documentation in 1989 by Thierry Coquand, Gilles + Dowek, Gérard Huet, Christine Paulin), +\item Basic tutorial: Gérard Huet, Gilles Kahn, Christine Paulin +\item Tutorial on recursive types: Eduardo Gimenez with updates by Pierre Castéran +\item FAQ: Hugo Herbelin, Julien Narboux, Florent Kirchner +\end{itemize} + +\section{Features discontinued by lack of support} + +\begin{itemize} +\item Searching modulo isomorphism: David Delahaye +\item Explanation of proofs in pseudo-natural language: Yann Coscoy +\item Export of context to external communication tools (\texttt{dp}): + Nicolas Ayache and Jean-Christophe Filliâtre, with contributions by + Claude Marché +\item Support for {\em PCoq}: Yves Bertot with contributions by + Laurence Rideau and Loïc Pottier; additional support for {\em TmEgg} + by Lionel Mamane +\item Export of terms and environments to XML format: Claudio + Sacerdoti Coen, with extensions from Cezary Kaliszyk +\end{itemize} + +For probable oversights or accidental errors, please report to Hugo~\verb=.=~Herbelin~\verb=@=~inria~\verb=.=~fr + +\end{document} |