diff options
Diffstat (limited to 'dev/doc/versions-history.tex')
-rw-r--r-- | dev/doc/versions-history.tex | 109 |
1 files changed, 90 insertions, 19 deletions
diff --git a/dev/doc/versions-history.tex b/dev/doc/versions-history.tex index 9892a441..1b1d3500 100644 --- a/dev/doc/versions-history.tex +++ b/dev/doc/versions-history.tex @@ -10,55 +10,76 @@ \begin{center} \begin{huge} -An history of Coq versions +A history of Coq versions \end{huge} \end{center} \bigskip \centerline{\large 1984-1989: The Calculus of Constructions} + +\bigskip +\centerline{\large (see README.V1-V5 for details)} \mbox{}\\ \mbox{}\\ \begin{tabular}{l|l|l} version & date & comments \\ \hline -CoC V1.10& mention of dates from 6 December & implementation language is Caml\\ - & 1984 to 13 February 1985 \\ -CoC V1.11& mention of dates from 6 December\\ - & 1984 to 19 February 1985\\ +CONSTR V1.10& mention of dates from 6 December & \feature{type-checker for Coquand's Calculus }\\ + & 1984 to 13 February 1985 & \feature{of Constructions}, implementation \\ + & frozen 22 December 1984 & language is a predecessor of CAML\\ + +CONSTR V1.11& mention of dates from 6 December\\ + & 1984 to 19 February 1985 (freeze date) &\\ + +CoC V2.8& dated 16 December 1985 (freeze date)\\ -CoC V2.13& dated 16 December 1985\\ +CoC V2.9& & \feature{cumulative hierarchy of universes}\\ -CoC V2.13& dated 25 June 1986\\ +CoC V2.13& dated 25 June 1986 (freeze date)\\ -CoC V3.1& dated 20 November 1986 & \feature{auto}\\ +CoC V3.1& started summer 1986 & \feature{AUTO tactic}\\ + & dated 20 November 1986 & implementation language now named CAML\\ CoC V3.2& dated 27 November 1986\\ -CoC V3.3 and V3.4& dated 1 January 1987 & creation of a directory for examples\\ +CoC V3.3& dated 1 January 1987 & creation of a directory for examples\\ -CoC V4.1& dated 24 July 1987\\ +CoC V3.4& dated 1 January 1987 & \feature{lambda and product distinguished in the syntax}\\ + +CoC V4.1& dated 24 July 1987 (freeze date)\\ CoC V4.2& dated 10 September 1987\\ -CoC V4.3& dated 15 September 1987\\ +CoC V4.3& dated 15 September 1987 & \feature{mathematical vernacular toplevel}\\ + & frozen November 1987 & \feature{section mechanism}\\ + & & \feature{logical vs computational content (sorte Spec)}\\ + & & \feature{LCF engine}\\ + +CoC V4.4& dated 27 January 1988 & \feature{impredicatively encoded inductive types}\\ + & frozen March 1988\\ -CoC V4.4& dated 27 January 1988\\ +CoC V4.5 and V4.5.5& dated 15 March 1988 & \feature{program extraction}\\ + & demonstrated in June 1988\\ -CoC V4.5 and V4.5.5& dated 15 March 1988\\ +CoC V4.6& dated 1 September 1988 & start of LEGO fork\\ -CoC V4.6 and V4.7& dated 1 September 1988\\ +CoC V4.7& started 6 September 1988 \\ -CoC V4.8& dated 1 December 1988\\ +CoC V4.8& dated 1 December 1988 (release time) & \feature{floating universes}\\ -CoC V4.8.5& dated 1 February 1989\\ +CoC V4.8.5& dated 1 February 1989 & \\ -CoC V4.9& dated 1 March 1989\\ +CoC V4.9& dated 1 March 1989 (release date)\\ -CoC V4.10 and 4.10.1& dated 1 May 1989 & first public release - in English\\ +CoC V4.10 and 4.10.1& dated 1 May 1989 & released with documentation in English\\ \end{tabular} \bigskip + +\noindent Note: CoC above stands as an abbreviation for {\em Calculus of + Constructions}, official name of the system. +\bigskip \bigskip \newpage @@ -80,7 +101,7 @@ Coq V5.2 & log dated 4 October 1990 & internal use \\ Coq V5.3 & log dated 12 October 1990 & internal use \\ -Coq V5.4 & headers dated 24 October 1990 & internal use, \feature{extraction} (version 1) [3-12-90]\\ +Coq V5.4 & headers dated 24 October 1990 & internal use, new \feature{extraction} (version 1) [3-12-90]\\ Coq V5.5 & started 6 December 1990 & internal use \\ @@ -265,7 +286,17 @@ Coq V7.3.1& released 5 October 2002 & \feature{module system} [2-8-2002]\\ & & \feature{pattern-matching compilation} (version 2) [13-6-2002]\\ Coq V7.4& released 6 February 2003 & \feature{notation}, \feature{scopes} [13-10-2002]\\ +\end{tabular} +\medskip +\bigskip + +\centerline{V- New concrete syntax} +\mbox{}\\ +\mbox{}\\ +\begin{tabular}{l|l|l} +version & date & comments \\ +\hline Coq V8.0& released 21 April 2004 & \feature{new concrete syntax}, \feature{Set predicative}, \feature{CoqIDE} [from 4-2-2003]\\ Coq V8.0pl1& released 18 July 2004\\ @@ -307,6 +338,46 @@ Coq V8.2 & released 17 February 2009 & \feature{type classes} [10-12-2007], \fea & & a first package released on February 11 was incomplete\\ +Coq V8.2pl1& released 4 July 2009 & \\ +Coq V8.2pl2& released 29 June 2010 & \\ +\end{tabular} + +\medskip +\bigskip + +\newpage +\mbox{}\\ +\mbox{}\\ +\begin{tabular}{l|l|l} +Coq V8.3 beta & released 16 February 2010 & \feature{MSets library} [13-10-2009] \\ +Coq V8.3 & released 14 October 2010 & \feature{nsatz} [3-6-2010] \\ +Coq V8.3pl1& released 23 December 2010 & \\ +Coq V8.3pl2& released 19 April 2011 & \\ +Coq V8.3pl3& released 19 December 2011 & \\ +Coq V8.3pl3& released 26 March 2012 & \\ +Coq V8.3pl5& released 28 September 2012 & \\ +Coq V8.4 beta & released 27 December 2011 & \feature{modular arithmetic library} [2010-2012]\\ +&& \feature{vector library} [10-12-2010]\\ +&& \feature{structured scripts} [22-4-2010]\\ +&& \feature{eta-conversion} [20-9-2010]\\ +&& \feature{new proof engine available} [10-12-2010]\\ +Coq V8.4 beta2 & released 21 May 2012 & \\ +Coq V8.4 & released 12 August 2012 &\\ +Coq V8.4pl1& released 22 December 2012 & \\ +Coq V8.4pl2& released 4 April 2013 & \\ +Coq V8.4pl3& released 21 December 2013 & \\ +Coq V8.4pl4& released 24 April 2014 & \\ +Coq V8.4pl5& released 22 October 2014 & \\ +Coq V8.4pl6& released 9 April 2015 & \\ + +Coq V8.5 beta1 & released 21 January 2015 & \feature{computation via compilation to OCaml} [22-1-2013]\\ +&& \feature{asynchonous evaluation} [8-8-2013]\\ +&& \feature{new proof engine deployed} [2-11-2013]\\ +&& \feature{universe polymorphism} [6-5-2014]\\ +&& \feature{primitive projections} [6-5-2014]\\ + +Coq V8.5 beta2 & released 22 April 2015 & \feature{MMaps library} [4-3-2015]\\ + \end{tabular} \medskip |