From fb860f9ea8dca5395ca9f2f350a68c1760c84ce4 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Wed, 21 Jan 2015 08:41:38 +0100 Subject: Reference manual: fix typo in doc of [tryif/then/else]. Fixes #3939.--- doc/refman/RefMan-ltac.tex | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'doc') diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index b90e682df1..de8c26943c 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -474,7 +474,7 @@ $v_2$). Branching is left-associative. The tactic \begin{quote} -{\tt if {\tacexpr}$_1$ then {\tacexpr}$_2$ else {\tacexpr}$_3$} +{\tt tryif {\tacexpr}$_1$ then {\tacexpr}$_2$ else {\tacexpr}$_3$} \end{quote} is a generalization of the biased-branching tactics above. The expression {\tacexpr}$_1$ is evaluated to $v_1$, which is then applied @@ -482,7 +482,7 @@ to each subgoal independently. For each goal where $v_1$ succeeds at least once, {tacexpr}$_2$ is evaluated to $v_2$ which is then applied collectively to the generated subgoals. The $v_2$ tactic can trigger backtracking points in $v_1$: where $v_1$ succeeds at least once, {\tt - if {\tacexpr}$_1$ then {\tacexpr}$_2$ else {\tacexpr}$_3$} is + tryif {\tacexpr}$_1$ then {\tacexpr}$_2$ else {\tacexpr}$_3$} is equivalent to $v_1;v_2$. In each of the goals where $v_1$ does not succeed at least once, {\tacexpr}$_3$ is evaluated in $v_3$ which is is then applied to the goal. -- cgit v1.2.3 From 2e1ab34a9feaa3fac6220400acbc7c710b0a0211 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Wed, 21 Jan 2015 09:05:36 +0100 Subject: Reference manual: pass over the credit section for English. --- doc/refman/RefMan-pre.tex | 41 +++++++++++++++++++++-------------------- 1 file changed, 21 insertions(+), 20 deletions(-) (limited to 'doc') diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex index e75ade9419..4af5c8fc65 100644 --- a/doc/refman/RefMan-pre.tex +++ b/doc/refman/RefMan-pre.tex @@ -939,9 +939,9 @@ projects: \begin{itemize} \item A new asynchronous evaluation and compilation mode by Enrico Tassi with help from Bruno Barras and Carst Tankink. -\item The full integration of the new proof engine by Arnaud Spiwack +\item Full integration of the new proof engine by Arnaud Spiwack helped by Pierre-Marie Pédrot, -\item The addition of conversion and reduction based on native compilation +\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. @@ -958,20 +958,21 @@ 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. In interactive use, this improves the -reactiveness of the system, since proofs can be processed in the -background. Similarly the 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, .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 the one of Coq making it no -more a special user interface and allowing its release cycle to be -decoupled with the one of Coq. +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 @@ -982,13 +983,13 @@ 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 change of the kernel architecture to +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 invisible to the user. +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 @@ -999,11 +1000,11 @@ 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 partly while the author was working +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 equality and univalence, thanks to +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 -- cgit v1.2.3 From 9e7e259e9f81eefd505b04e5e17b06136055e1ee Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Wed, 21 Jan 2015 09:07:10 +0100 Subject: Reference Manual/Credits: remove a duplicate. --- doc/refman/RefMan-pre.tex | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) (limited to 'doc') diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex index 4af5c8fc65..cf6dae34c3 100644 --- a/doc/refman/RefMan-pre.tex +++ b/doc/refman/RefMan-pre.tex @@ -1023,9 +1023,7 @@ and improvements regarding the different components of the system. Maxime Dénès and Benjamin Grégoire developed an implementation of the conversion test using the OCaml native compiler. -Bruno Barras and Maxime Dénès fixed a problem in the guard condition -leading to a refutation of standard axioms like propositional -extensionality or univalence. + Maxime Dénès maintained the bytecode-based reduction machine. Pierre Courtieu contributed new features for using {\Coq} through Proof -- cgit v1.2.3 From 5b653d2bb4d9f7b4c6f1faf4b3c17d6400cadf48 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Wed, 21 Jan 2015 09:44:24 +0100 Subject: Reference manual/Credits: populate the "various smaller-scale improvements" part. --- doc/refman/RefMan-pre.tex | 22 +++++++++++++++------- 1 file changed, 15 insertions(+), 7 deletions(-) (limited to 'doc') diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex index cf6dae34c3..e160022279 100644 --- a/doc/refman/RefMan-pre.tex +++ b/doc/refman/RefMan-pre.tex @@ -1014,21 +1014,29 @@ the relations between homotopy theory and type theory. {\Coq} 8.5 also comes with a bunch of many various smaller-scale changes and improvements regarding the different components of the system. -% High-Level Specification Language: -% - tactics in terms -% - Universe inconsistency and unification error messages -% - Named existentials - -% Opam Coq Guillaume Claret and Thomas Braibant - Maxime Dénès and Benjamin Grégoire developed an implementation of the conversion test using the OCaml native compiler. Maxime Dénès maintained the bytecode-based reduction machine. +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. + +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). +A distribution channel for Coq packages using the Opam tool has been +developed by Thomas Braibant and Guillaume Claret. + \begin{flushright} Paris, January 2015\\ Hugo Herbelin \& Matthieu Sozeau\\ -- cgit v1.2.3 From b855224b5ce5deda9853af1bed9b135a7ea9a76b Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Wed, 21 Jan 2015 10:01:49 +0100 Subject: Reference Manual/Credits: native compute is a major contribution. It is, at the very least, listed as such in the overview. So, I moved it to the relevant part and expanded the description with a sentence or two.--- doc/refman/RefMan-pre.tex | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) (limited to 'doc') diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex index e160022279..66f3369e3b 100644 --- a/doc/refman/RefMan-pre.tex +++ b/doc/refman/RefMan-pre.tex @@ -1011,12 +1011,14 @@ 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. -Maxime Dénès and Benjamin Grégoire developed an implementation of the -conversion test using the OCaml native compiler. - Maxime Dénès maintained the bytecode-based reduction machine. Pierre-Marie Pédrot has extended the syntax of terms to, -- cgit v1.2.3 From 3527a32a9c055a1438f0c85b77d3dbd8d38cbd32 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Wed, 21 Jan 2015 10:36:37 +0100 Subject: Reference Manual/Credits: expand the paragraph on the new proof engine to match the overall style. --- doc/refman/RefMan-pre.tex | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) (limited to 'doc') diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex index 66f3369e3b..f45072ca43 100644 --- a/doc/refman/RefMan-pre.tex +++ b/doc/refman/RefMan-pre.tex @@ -950,9 +950,18 @@ projects: Matthieu Sozeau. \end{itemize} -The full integration of the proof engine brings to primitive tactics and -the user level Ltac language deep tactic backtracking and multi-goal -handling. +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 make 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 -- cgit v1.2.3