forked from SkySkimmer/rocq
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathversions-history.tex
441 lines (316 loc) · 14.1 KB
/
versions-history.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
\documentclass[a4paper]{book}
\usepackage{fullpage}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{amsfonts}
\newcommand{\feature}[1]{{\em #1}}
\begin{document}
\begin{center}
\begin{huge}
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
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.9& & \feature{cumulative hierarchy of universes}\\
CoC V2.13& dated 25 June 1986 (freeze date)\\
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& dated 1 January 1987 & creation of a directory for examples\\
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 & \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.5 and V4.5.5& dated 15 March 1988 & \feature{program extraction}\\
& demonstrated in June 1988\\
CoC V4.6& dated 1 September 1988 & start of LEGO fork\\
CoC V4.7& started 6 September 1988 \\
CoC V4.8& dated 1 December 1988 (release time) & \feature{floating universes}\\
CoC V4.8.5& dated 1 February 1989 & \\
CoC V4.9& dated 1 March 1989 (release date)\\
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
\centerline{\large 1989-now: The Calculus of Inductive Constructions}
\mbox{}\\
\centerline{I- RCS archives in Caml and Caml-Light}
\mbox{}\\
\mbox{}\\
\begin{tabular}{l|l|l}
version & date & comments \\
\hline
Coq V5.0 & headers dated 1 January 1990 & internal use \\
& & \feature{inductive types with primitive recursor}\\
Coq V5.1 & ended 12 July 1990 & internal use \\
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, new \feature{extraction} (version 1) [3-12-90]\\
Coq V5.5 & started 6 December 1990 & internal use \\
Coq V5.6 beta & 1991 & first announce of the new Coq based on CIC \\
& & (in May at TYPES?)\\
& & \feature{rewrite tactic}\\
& & use of RCS at least from February 1991\\
Coq V5.6& 7 August 1991 & \\
Coq V5.6 patch 1& 13 November 1991 & \\
Coq V5.6 (last) & mention of 27 November 1992\\
Coq V5.7.0& 1992 & translation to Caml-Light \footnotemark\\
Coq V5.8& 12 February 1993 & \feature{Program} (version 1), \feature{simpl}\\
& & has the xcoq graphical interface\\
& & first explicit notion of standard library\\
& & includes a MacOS 7-9 version\\
Coq V5.8.1& released 28 April 1993 & with xcoq graphical interface and MacOS 7-9 support\\
Coq V5.8.2& released 9 July 1993 & with xcoq graphical interface and MacOS 7-9 support\\
Coq V5.8.3& released 6 December 1993 % Announce on coq-club
& with xcoq graphical interface and MacOS 7-9 support\\
& & 3 branches: Lyon (V5.8.x), Ulm (V5.10.x) and Rocq (V5.9)\\
Coq V5.9 alpha& 7 July 1993 &
experimental version based on evars refinement \\
& & (merge from experimental ``V6.0'' and some pre-V5.8.3 \\
& & version), not released\\
& March 1994 & \feature{tauto} tactic in V5.9 branch\\
Coq V5.9 & 27 January 1993 & experimental version based on evars refinement\\
& & not released\\
\end{tabular}
\bigskip
\bigskip
\footnotetext{archive lost?}
\newpage
\centerline{II- Starting with CVS archives in Caml-Light}
\mbox{}\\
\mbox{}\\
\begin{tabular}{l|l|l}
version & date & comments \\
\hline
Coq V5.10 ``Murthy'' & 22 January 1994 &
introduction of the ``DOPN'' structure\\
& & \feature{eapply/prolog} tactics\\
& & private use of cvs on madiran.inria.fr\\
Coq V5.10.1 ``Murthy''& 15 April 1994 \\
Coq V5.10.2 ``Murthy''& 19 April 1994 & \feature{mutual inductive types, fixpoint} (from Lyon's branch)\\
Coq V5.10.3& 28 April 1994 \\
Coq V5.10.5& dated 13 May 1994 & \feature{inversion}, \feature{discriminate}, \feature{injection} \\
& & \feature{type synthesis of hidden arguments}\\
& & \feature{separate compilation}, \feature{reset mechanism} \\
Coq V5.10.6& dated 30 May 1994\\
Coq Lyon's archive & in 1994 & cvs server set up on woodstock.ens-lyon.fr\\
Coq V5.10.9& announced on 17 August 1994 &
% Announced by Catherine Parent on coqdev
% Version avec une copie de THEORIES pour les inductifs mutuels
\\
Coq V5.10.11& announced on 2 February 1995 & \feature{compute}\\
Coq Rocq's archive & on 16 February 1995 & set up of ``V5.10'' cvs archive on pauillac.inria.fr \\
& & with first dispatch of files over src/* directories\\
Coq V5.10.12& dated 30 January 1995 & on Lyon's cvs\\
Coq V5.10.13& dated 9 June 1995 & on Lyon's cvs\\
Coq V5.10.14.OO& dated 30 June 1995 & on Lyon's cvs\\
Coq V5.10.14.a& announced 5 September 1995 & bug-fix release \\ % Announce on coq-club by BW
Coq V5.10.14.b& released 2 October 1995 & bug-fix release\\
& & MS-DOS version released on 30 October 1995\\
% still available at ftp://ftp.ens-lyon.fr/pub/LIP/COQ/V5.10.14.old/ in May 2009
% also known in /net/pauillac/constr archive as ``V5.11 old'' \\
% A copy of Coq V5.10.15 dated 1 January 1996 coming from Lyon's CVS is
% known in /net/pauillac/constr archive as ``V5.11 new old'' \\
Coq V5.10.15 & released 20 February 1996 & \feature{Logic, Sorting, new Sets and Relations libraries} \\
% Announce on coq-club by BW
% dated 15 February 1996 and bound to pauillac's cvs in /net/pauillac/constr archive
& & MacOS 7-9 version released on 1 March 1996 \\ % Announce on coq-club by BW
Coq V5.11 & dated 1 March 1996 & not released, not in pauillac's CVS, \feature{eauto} \\
\end{tabular}
\bigskip
\bigskip
\newpage
\centerline{III- A CVS archive in Caml Special Light}
\mbox{}\\
\mbox{}\\
\begin{tabular}{l|l|l}
version & date & comments \\
\hline
Coq ``V6'' archive & 20 March 1996 & new cvs repository on pauillac.inria.fr with code ported \\
& & to Caml Special Light (to later become Objective Caml)\\
& & has implicit arguments and coercions\\
& & has coinductive types\\
Coq V6.1beta& released 18 November 1996 & \feature{coercions} [23-5-1996], \feature{user-level implicit arguments} [23-5-1996]\\
& & \feature{omega} [10-9-1996] \\
& & \feature{natural language proof printing} (stopped from Coq V7) [6-9-1996]\\
& & \feature{pattern-matching compilation} [7-10-1996]\\
& & \feature{ring} (version 1, ACSimpl) [11-12-1996]\\
Coq V6.1& released December 1996 & \\
Coq V6.2beta& released 30 January 1998 & % Announced on coq-club 2-2-1998 by CP
\feature{SearchIsos} (stopped from Coq V7) [9-11-1997]\\
& & grammar extension mechanism moved to Camlp4 [12-6-1997]\\
& & \feature{refine tactic}\\
& & includes a Windows version\\
Coq V6.2& released 4 May 1998 & % Announced on coq-club 5-5-1998 by CP
\feature{ring} (version 2) [7-4-1998] \\
Coq V6.2.1& released 23 July 1998\\
Coq V6.2.2 beta& released 30 January 1998\\
Coq V6.2.2& released 23 September 1998\\
Coq V6.2.3& released 22 December 1998 & \feature{Real numbers library} [from 13-11-1998] \\
Coq V6.2.4& released 8 February 1999\\
Coq V6.3& released 27 July 1999 & \feature{autorewrite} [25-3-1999]\\
& & \feature{Correctness} (deprecated in V8, led to Why) [28-10-1997]\\
Coq V6.3.1& released 7 December 1999\\
\end{tabular}
\medskip
\bigskip
\newpage
\centerline{IV- New CVS, back to a kernel-centric implementation}
\mbox{}\\
\mbox{}\\
\begin{tabular}{l|l|l}
version & date & comments \\
\hline
Coq ``V7'' archive & August 1999 & new cvs archive based on J.-C. Filliâtre's \\
& & \feature{kernel-centric} architecture \\
& & more care for outside readers\\
& & (indentation, ocaml warning protection)\\
Coq V7.0beta& released 27 December 2000 & \feature{${\cal L}_{\mathit{tac}}$} \\
Coq V7.0beta2& released 2 February 2001\\
Coq V7.0& released 25 April 2001 & \feature{extraction} (version 2) [6-2-2001] \\
& & \feature{field} (version 1) [19-4-2001], \feature{fourier} [20-4-2001] \\
Coq V7.1& released 25 September 2001 & \feature{setoid rewriting} (version 1) [10-7-2001]\\
Coq V7.2& released 10 January 2002\\
Coq V7.3& released 16 May 2002\\
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\\
Coq V8.0pl2& released 22 January 2005\\
Coq V8.0pl3& released 13 January 2006\\
Coq V8.0pl4& released 26 January 2007\\
Coq ``svn'' archive & 6 March 2006 & cvs archive moved to subversion control management\\
Coq V8.1beta& released 12 July 2006 & \feature{bytecode compiler} [20-10-2004] \\
& & \feature{setoid rewriting} (version 2) [3-9-2004]\\
& & \feature{functional induction} [1-2-2006]\\
& & \feature{Strings library} [8-2-2006], \feature{FSets/FMaps library} [15-3-2006] \\
& & \feature{Program} (version 2, Russell) [5-3-2006] \\
& & \feature{declarative language} [20-9-2006]\\
& & \feature{ring} (version 3) [18-11-2005]\\
Coq V8.1gamma& released 7 November 2006 & \feature{field} (version 2) [29-9-2006]\\
Coq V8.1& released 10 February 2007 & \\
Coq V8.1pl1& released 27 July 2007 & \\
Coq V8.1pl2& released 13 October 2007 & \\
Coq V8.1pl3& released 13 December 2007 & \\
Coq V8.1pl4& released 9 October 2008 & \\
Coq V8.2 beta1& released 13 June 2008 & \\
Coq V8.2 beta2& released 19 June 2008 & \\
Coq V8.2 beta3& released 27 June 2008 & \\
Coq V8.2 beta4& released 8 August 2008 & \\
Coq V8.2 & released 17 February 2009 & \feature{type classes} [10-12-2007], \feature{machine words} [11-5-2007]\\
& & \feature{big integers} [11-5-2007], \feature{abstract arithmetics} [9-2007]\\
& & \feature{setoid rewriting} (version 3) [18-12-2007] \\
& & \feature{micromega solving platform} [19-5-2008]\\
& & 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]\\
&& \feature{miscellaneous optimizations}\\
Coq V8.5 beta2 & released 22 April 2015 & \feature{MMaps library} [4-3-2015]\\
Coq V8.5 & released 22 January 2016 & \\
Coq V8.6 beta 1 & released 19 November 2016 & \feature{irrefutable patterns} [15-2-2016]\\
&& \feature{Ltac profiling} [14-6-2016]\\
&& \feature{warning system} [29-6-2016]\\
&& \feature{miscellaneous optimizations}\\
Coq V8.6 & released 14 December 2016 & \\
Coq V8.7 beta 1 & released 6 September 2017 & \feature{bundled with Ssreflect plugin} [6-6-2017]\\
&& \feature{cumulative polymorphic inductive types} [19-6-2017]\\
&& \feature{further optimizations}\\
Coq V8.7 beta 2 & released 6 October 2017 & \\
Coq V8.7 & released 18 October 2016 & \\
\end{tabular}
\medskip
\bigskip
\newpage
\centerline{\large Other important dates}
\mbox{}\\
\mbox{}\\
\begin{tabular}{l|l|l}
version & date & comments \\
\hline
Lechenadec's version in C& mention of \\
& 13 January 1985 on \\
& some vernacular files\\
Set up of the coq-club mailing list & 28 July 1993\\
Coq V6.0 ``evars'' & & experimentation based on evars
refinement started \\
& & in 1991 by Gilles from V5.6 beta,\\
& & with work by Hugo in July 1992\\
Coq V6.0 ``evars'' ``light'' & July 1993 & Hugo's port of the first
evars-based experimentation \\
& & to Coq V5.7, version from October/November
1992\\
CtCoq & released 25 October 1995 & first beta-version \\ % Announce on coq-club by Janet
Proto with explicit substitutions & 1997 &\\
Coq web site & 15 April 1998 & new site designed by David Delahaye \\
Coq web site & January 2004 & web site new style \\
& & designed by Julien Narboux and Florent Kirchner \\
Coq web site & April 2009 & new Drupal-based site \\
& & designed by Jean-Marc Notin and Denis Cousineau \\
\end{tabular}
\end{document}