forked from coq/coq
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathCHANGES
3391 lines (2869 loc) · 161 KB
/
CHANGES
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
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
Changes beyond V8.6
===================
Tactics
- New tactic "extensionality in H" which applies (possibly dependent)
functional extensionality in H supposed to be a quantified equality
until giving a bare equality.
- New tactic "inversion_sigma" which turns equalities of dependent
pairs (e.g., "existT P x p = existT P y q", frequently left over by
"inversion" on a dependent type family) into pairs of equalities
(e.g., a hypothesis "H : x = y" and a hypothesis of type "rew H in p
= q"); these hypotheses can subsequently be simplified using
"subst", without ever invoking any kind of axiom asserting
uniqueness of identity proofs. If you want to explicitly specify the
hypothesis to be inverted, or name the generated hypotheses, you can
invoke "induction H as [H1 H2] using eq_sigT_rect". The tactic also
works for "sig", "sigT2", and "sig2", and there are similar
"eq_sig*_rect" induction lemmas.
- Tactic "specialize with ..." now accepts any partial bindings.
Missing bindings are either solved by unification or left quantified
in the hypothesis.
- New representation of terms that statically ensure stability by
evar-expansion. This has several consequences.
* In terms of performance, this adds a cost to every term destructuration,
but at the same time most eager evar normalizations were removed, which
couterbalances this drawback and even sometimes outperforms the old
implementation. For instance, many operations that would require O(n)
normalization of the term are now O(1) in tactics. YMMV.
* This triggers small changes in unification, which was not evar-insensitive.
Most notably, the new implementation recognizes Miller patterns that were
missed before because of a missing normalization step. Hopefully this should
be fairly uncommon.
- Tactic "auto with real" can now discharge comparisons of literals.
- The types of variables in patterns of "match" are now
beta-iota-reduced after type-checking. This has an impact on the
type of the variables that the tactic "refine" introduces in the
context, producing types a priori closer to the expectations.
- In "Tactic Notation" or "TACTIC EXTEND", entry "constr_with_bindings"
now uses type classes and rejects terms with unresolved holes, like
entry "constr" does. To get the former behavior use
"open_constr_with_bindings" (possible source of incompatibility.
- New e-variants eassert, eenough, epose proof, eset, eremember, epose
which behave like the corresponding variants with no "e" but turn
unresolved implicit arguments into existential variables, on the
shelf, rather than failing.
Vernacular Commands
- Goals context can be printed in a more compact way when "Set
Printing Compact Contexts" is activated.
- The deprecated `Save` vernacular and its form `Save Theorem id` to
close proofs have been removed from the syntax. Please use `Qed`.
Standard Library
- New file PropExtensionality.v to explicitly work in the axiomatic
context of propositional extensionality.
- New file SetoidChoice.v axiomatically providing choice over setoids,
and, consequently, choice of representatives in equivalence classes.
Various proof-theoretic characterizations of choice over setoids in
file ChoiceFacts.v.
- The BigN, BigZ, BigZ libraries are not part anymore of Coq standard
library, they are now provided by a separate repository
https://github.com/coq/bignums
The split has been done just after the Int31 library.
- IZR (Reals) has been changed to produce a compact representation of
integers. As a consequence, IZR is no longer convertible to INR and
lemmas such as INR_IZR_INZ should be used instead.
- Real constants are now represented using IZR rather than R0 and R1;
this might cause rewriting rules to fail to apply to constants.
Plugins
- The mathematical proof language (also known as declarative mode) was removed.
Dependencies
- Support for camlp4 has been removed.
Tools
- coq_makefile was completely redesigned to improve its maintainability and
the extensibility of generated Makefiles, and to make _CoqProject files
more palatable to IDEs. Overview:
* _CoqProject files contain only Coq specific data (i.e. the list of
files, -R options, ...)
* coq_makefile translates _CoqProject to Makefile.conf and copies in the
desired location a standard Makefile (that reads Makefile.conf)
* Makefile extensions can be implemented in a Makefile.local file (read
by the main Makefile) by installing a hook in the extension points
provided by the standard Makefile
The current version contains code for retro compatibility that prints
warnings when a deprecated feature is used. Please upgrade your _CoqProject
accordingly.
* Additionally, coq_makefile-made Makefiles now support experimental timing
targets `pretty-timed`, `pretty-timed-before`, `pretty-timed-after`,
`print-pretty-timed-diff`, `print-pretty-single-time-diff`,
`all.timing.diff`, and the variable `TIMING=1` (or `TIMING=before` or
`TIMING=after`); see the documentation for more details.
Build Infrastructure
- Note that 'make world' does not build the bytecode binaries anymore.
For that, you can use 'make byte' (and 'make install-byte' afterwards).
Warning: native and byte compilations should *not* be mixed in the same
instance of 'make -j', otherwise both ocamlc and ocamlopt might race for
access to the same .cmi files. In short, use "make -j && make -j byte"
instead of "make -j world byte".
Universes
- Cumulative inductive types. see prefixes "Cumulative", "NonCumulative"
for inductive definitions and the option "Set Inductive Cumulativity"
in the reference manual.
XML Protocol
- The `query` call has been modified, now it carries a mandatory
"route_id" integer parameter, that associated the result of such
query with its generated feedback.
Changes from V8.6beta1 to V8.6
==============================
Kernel
- Fixed critical bug #5248 in VM long multiplication on 32-bit
architectures. Was there only since 8.6beta1, so no stable release impacted.
Other bug fixes in universes, type class shelving,...
Changes from V8.5 to V8.6beta1
==============================
Kernel
- A new, faster state-of-the-art universe constraint checker.
Specification language
- Giving implicit arguments explicitly to a constant with multiple
choices of implicit arguments does not break any more insertion of
further maximal implicit arguments.
- Ability to put any pattern in binders, prefixed by quote, e.g.
"fun '(a,b) => ...", "λ '(a,(b,c)), ...", "Definition foo '(x,y) := ...".
It expands into a "let 'pattern := ..."
Tactics
- Flag "Bracketing Last Introduction Pattern" is now on by default.
- Flag "Regular Subst Tactic" is now on by default: it respects the
initial order of hypothesis, it contracts cycles, it unfolds no
local definitions (common source of incompatibilities, fixable by
"Unset Regular Subst Tactic").
- New flag "Refolding Reduction", now disabled by default, which turns
on refolding of constants/fixpoints (as in cbn) during the reductions
done during type inference and tactic retyping. Can be extremely
expensive. When set off, this recovers the 8.4 behaviour of unification
and type inference. Potential source of incompatibility with 8.5 developments
(the option is set on in Compat/Coq85.v).
- New flag "Shrink Abstract" that minimalizes proofs generated by the abstract
tactical w.r.t. variables appearing in the body of the proof.
On by default and deprecated. Minor source of incompatibility
for code relying on the precise arguments of abstracted proofs.
- Serious bugs are fixed in tactic "double induction" (source of
incompatibilities as soon as the inductive types have dependencies in
the type of their constructors; "double induction" remains however
deprecated).
- In introduction patterns of the form (pat1,...,patn), n should match
the exact number of hypotheses introduced (except for local definitions
for which pattern can be omitted, as in regular pattern-matching).
- Tactic scopes in Ltac like constr: and ltac: now require parentheses around
their argument.
- Every generic argument type declares a tactic scope of the form "name:(...)"
where name is the name of the argument. This generalizes the constr: and ltac:
instances.
- When in strict mode (i.e. in a Ltac definition), if the "intro" tactic is
given a free identifier, it is not bound in subsequent tactics anymore.
In order to introduce a binding, use e.g. the "fresh" primitive instead
(potential source of incompatibilities).
- New tactics is_ind, is_const, is_proj, is_constructor for use in Ltac.
- New goal selectors. Sets of goals can be selected by listing integers
ranges. Example: "1,4-7,24: tac" focuses "tac" on goals 1,4,5,6,7,24.
- For uniformity with "destruct"/"induction" and for a more natural
behavior, "injection" can now work in place by activating option
"Structural Injection". In this case, hypotheses are also put in the
context in the natural left-to-right order and the hypothesis on
which injection applies is cleared.
- Tactic "contradiction" (hence "easy") now also solve goals with
hypotheses of the form "~True" or "t<>t" (possible source of
incompatibilities because of more successes in automation, but
generally a more intuitive strategy).
- Option "Injection On Proofs" was renamed "Keep Proof Equalities". When
enabled, injection and inversion do not drop equalities between objects
in Prop. Still disabled by default.
- New tactics "notypeclasses refine" and "simple notypeclasses refine" that
disallow typeclass resolution when typechecking their argument, for use
in typeclass hints.
- Integration of LtacProf, a profiler for Ltac.
- Reduction tactics now accept more fine-grained flags: iota is now a shorthand
for the new flags match, fix and cofix.
- The ssreflect subterm selection algorithm is now accessible to tactic writers
through the ssrmatching plugin.
- When used as an argument of an ltac function, "auto" without "with"
nor "using" clause now correctly uses only the core hint database by
default.
Hints
- Revised the syntax of [Hint Cut] to follow standard notation for regexps.
- Hint Mode now accepts "!" which means that the mode matches only if the
argument's head is not an evar (it goes under applications, casts, and
scrutinees of matches and projections).
- Hints can now take an optional user-given pattern, used only by
[typeclasses eauto] with the [Filtered Unification] option on.
Typeclasses
- Many new options and new engine based on the proof monad. The
[typeclasses eauto] tactic is now a multi-goal, multi-success tactic.
See reference manual for more information. It is planned to
replace auto and eauto in the following version. The 8.5 resolution
engine is still available to help solve compatibility issues.
Program
- The "Shrink Obligations" flag now applies to all obligations, not only
those solved by the automatic tactic.
- "Shrink Obligations" is on by default and deprecated. Minor source of
incompatibility for code relying on the precise arguments of
obligations.
Notations
- "Bind Scope" can once again bind "Funclass" and "Sortclass".
General infrastructure
- New configurable warning system which can be controlled with the vernacular
command "Set Warnings", or, under coqc/coqtop, with the flag "-w". In
particular, the default is now that warnings are printed by coqc.
- In asynchronous mode, Coq is now capable of recovering from errors and
continue processing the document.
Tools
- coqc accepts a -o option to specify the output file name
- coqtop accepts --print-version to print Coq and OCaml versions in
easy to parse format
- Setting [Printing Dependent Evars Line] can be unset to disable the
computation associated with printing the "dependent evars: " line in
-emacs mode
- Removed the -verbose-compat-notations flag and the corresponding Set
Verbose Compat vernacular, since these warnings can now be silenced or
turned into errors using "-w".
XML protocol
- message format has changed, see dev/doc/changes.txt for more details.
Many bug fixes, minor changes and documentation improvements are not mentioned
here.
Changes from V8.5pl2 to V8.5pl3
===============================
Critical bugfix
- #4876: Guard checker incompleteness when using primitive projections
Other bugfixes
- #4780: Induction with universe polymorphism on was creating ill-typed terms.
- #4673: regression in setoid_rewrite, unfolding let-ins for type unification.
- #4754: Regression in setoid_rewrite, allow postponed unification problems to remain.
- #4769: Anomaly with universe polymorphic schemes defined inside sections.
- #3886: Program: duplicate obligations of mutual fixpoints.
- #4994: Documentation typo.
- #5008: Use the "md5" command on OpenBSD.
- #5007: Do not assume the "TERM" environment variable is always set.
- #4606: Output a break before a list only if there was an empty line.
- #5001: metas not cleaned properly in clenv_refine_in.
- #2336: incorrect glob data for module symbols (bug #2336).
- #4832: Remove extraneous dot in error message.
- Anomaly in printing a unification error message.
- #4947: Options which take string arguments are not backwards compatible.
- #4156: micromega cache files are now hidden files.
- #4871: interrupting par:abstract kills coqtop.
- #5043: [Admitted] lemmas pick up section variables.
- Fix name of internal refine ("simple refine").
- #5062: probably a typo in Strict Proofs mode.
- #5065: Anomaly: Not a proof by induction.
- Restore native compiler optimizations, they were disabled since 8.5!
- #5077: failure on typing a fixpoint with evars in its type.
- Fix recursive notation bug.
- #5095: non relevant too strict test in let-in abstraction.
- Ensuring that the evar name is preserved by "rename".
- #4887: confusion between using and with in documentation of firstorder.
- Bug in subst with let-ins.
- #4762: eauto weaker than auto.
- Remove if_then_else (was buggy). Use tryif instead.
- #4970: confusion between special "{" and non special "{{" in notations.
- #4529: primitive projections unfolding.
- #4416: Incorrect "Error: Incorrect number of goals".
- #4863: abstract in typeclass hint fails.
- #5123: unshelve can impact typeclass resolution
- Fix a collision about the meta-variable ".." in recursive notations.
- Fix printing of info_auto.
- #3209: Not_found due to an occur-check cycle.
- #5097: status of evars refined by "clear" in ltac: closed wrt evars.
- #5150: Missing dependency of the test-suite subsystems in prerequisite.
- Fix a bug in error printing of unif constraints
- #3941: Do not stop propagation of signals when Coq is busy.
- #4822: Incorrect assertion in cbn.
- #3479 parsing of "{" and "}" when a keyword starts with "{" or "}".
- #5127: Memory corruption with the VM.
- #5102: bullets parsing broken by calls to parse_entry.
Various documentation improvements
Changes from V8.5pl1 to V8.5pl2
===============================
Critical bugfix
- Checksums of .vo files dependencies were not correctly checked.
- Unicode-to-ASCII translation was not injective, leading in a soundness bug in
the native compiler.
Other bugfixes
- #4097: more efficient occur-check in presence of primitive projections
- #4398: type_scope used consistently in "match goal".
- #4450: eauto does not work with polymorphic lemmas
- #4677: fix alpha-conversion in notations needing eta-expansion.
- Fully preserve initial order of hypotheses in "Regular Subst Tactic" mode.
- #4644: a regression in unification.
- #4725: Function (Error: Conversion test raised an anomaly) and Program
(Error: Cannot infer this placeholder of type)
- #4747: Problem building Coq 8.5pl1 with OCaml 4.03.0: Fatal warnings
- #4752: CoqIDE crash on files not ended by ".v".
- #4777: printing inefficiency with implicit arguments
- #4818: "Admitted" fails due to undefined universe anomaly after calling
"destruct"
- #4823: remote counter: avoid thread race on sockets
- #4841: -verbose flag changed semantics in 8.5, is much harder to use
- #4851: [nsatz] cannot handle duplicated hypotheses
- #4858: Anomaly: Uncaught exception Failure("hd"). Please report. in variant
of nsatz
- #4880: [nsatz_compute] generates invalid certificates if given redundant
hypotheses
- #4881: synchronizing "Declare Implicit Tactic" with backtrack.
- #4882: anomaly with Declare Implicit Tactic on hole of type with evars
- Fix use of "Declare Implicit Tactic" in refine.
triggered by CoqIDE
- #4069, #4718: congruence fails when universes are involved.
Universes
- Disallow silently dropping universe instances applied to variables
(forward compatible)
- Allow explicit universe instances on notations, when they can apply
to the head reference of their expansion.
Build infrastructure
- New update on how to find camlp5 binary and library at configure time.
Changes from V8.5 to V8.5pl1
============================
Critical bugfix
- The subterm relation for the guard condition was incorrectly defined on
primitive projections (#4588)
Plugin development tools
- add a .merlin target to the makefile
Various performance improvements (time, space used by .vo files)
Other bugfixes
- Fix order of arguments to Big.compare_case in ExtrOcamlZBigInt.v
- Added compatibility coercions from Specif.v which were present in Coq 8.4.
- Fixing a source of inefficiency and an artificial dependency in the printer in the congruence tactic.
- Allow to unset the refinement mode of Instance in ML
- Fixing an incorrect use of prod_appvect on a term which was not a product in setoid_rewrite.
- Add -compat 8.4 econstructor tactics, and tests
- Add compatibility Nonrecursive Elimination Schemes
- Fixing the "No applicable tactic" non informative error message regression on apply.
- Univs: fix get_current_context (bug #4603, part I)
- Fix a bug in Program coercion code
- Fix handling of arity of definitional classes.
- #4630: Some tactics are 20x slower in 8.5 than 8.4.
- #4627: records with no declared arity can be template polymorphic.
- #4623: set tactic too weak with universes (regression)
- Fix incorrect behavior of CS resolution
- #4591: Uncaught exception in directory browsing.
- CoqIDE is more resilient to initialization errors.
- #4614: "Fully check the document" is uninterruptable.
- Try eta-expansion of records only on non-recursive ones
- Fix bug when a sort is ascribed to a Record
- Primitive projections: protect kernel from erroneous definitions.
- Fixed bug #4533 with previous Keyed Unification commit
- Win: kill unreliable hence do not waitpid after kill -9 (Close #4369)
- Fix strategy of Keyed Unification
- #4608: Anomaly "output_value: abstract value (outside heap)".
- #4607: do not read native code files if native compiler was disabled.
- #4105: poor escaping in the protocol between CoqIDE and coqtop.
- #4596: [rewrite] broke in the past few weeks.
- #4533 (partial): respect declared global transparency of projections in unification.ml
- #4544: Backtrack on using full betaiota reduction during keyed unification.
- #4540: CoqIDE bottom progress bar does not update.
- Fix regression from 8.4 in reflexivity
- #4580: [Set Refine Instance Mode] also used for Program Instance.
- #4582: cannot override notation [ x ]. MAY CREATE INCOMPATIBILITIES, see #4683.
- STM: Print/Extraction have to be skipped if -quick
- #4542: CoqIDE: STOP button also stops workers
- STM: classify some variants of Instance as regular `Fork nodes.
- #4574: Anomaly: Uncaught exception Invalid_argument("splay_arity").
- Do not give a name to anonymous evars anymore. See bug #4547.
- STM: always stock in vio files the first node (state) of a proof
- STM: not delegate proofs that contain Vernac(Module|Require|Import), #4530
- Don't fail fatally if PATH is not set.
- #4537: Coq 8.5 is slower in typeclass resolution.
- #4522: Incorrect "Warning..." on windows.
- #4373: coqdep does not know about .vio files.
- #3826: "Incompatible module types" is uninformative.
- #4495: Failed assertion in metasyntax.ml.
- #4511: evar tactic can create non-typed evars.
- #4503: mixing universe polymorphic and monomorphic variables and definitions in sections is unsupported.
- #4519: oops, global shadowed local universe level bindings.
- #4506: Anomaly: File "pretyping/indrec.ml", line 169, characters 14-20: Assertion failed.
- #4548: Coqide crashes when going back one command
Changes from V8.5beta3 to V8.5
==============================
Tools
- Flag "-compat 8.4" now loads Coq.Compat.Coq84. The standard way of
putting Coq in v8.4 compatibility mode is to pass the command line flag
"-compat 8.4". It can be followed by "-require Coq.Compat.AdmitAxiom"
if the 8.4 behavior of admit is needed, in which case it uses an axiom.
Specification language
- Syntax "$(tactic)$" changed to "ltac:(tactic)".
Tactics
- Syntax "destruct !hyp" changed to "destruct (hyp)", and similarly
for induction (rare source of incompatibilities easily solvable by
removing parentheses around "hyp" when not for the purpose of keeping
the hypothesis).
- Syntax "p/c" for on-the-fly application of a lemma c before
introducing along pattern p changed to p%c1..%cn. The feature and
syntax are in experimental stage.
- "Proof using" does not clear unused section variables.
- Tactic "refine" has been changed back to the 8.4 behavior of shelving subgoals
that occur in other subgoals. The "refine" tactic of 8.5beta3 has been
renamed "simple refine"; it does not shelve any subgoal.
- New tactical "unshelve tac" which grab existential variables put on
the tactic shelve by the execution of "tac".
Changes from V8.5beta2 to V8.5beta3
===================================
Vernacular commands
- New command "Redirect" to redirect the output of a command to a file.
- New command "Undelimit Scope" to remove the delimiter of a scope.
- New option "Strict Universe Declaration", set by default. It enforces the
declaration of all polymorphic universes appearing in a definition when
introducing it.
- New command "Show id" to show goal named id.
- Option "Virtual Machine" removed.
Tactics
- New flag "Regular Subst Tactic" which fixes "subst" in situations where
it failed to substitute all substitutable equations or failed to simplify
cycles, or accidentally unfolded local definitions (flag is off by default).
- New flag "Loose Hint Behavior" to handle hints loaded but not imported in a
special way. It accepts three distinct flags:
* "Lax", which is the default one, sets the old behavior, i.e. a non-imported
hint behaves the same as an imported one.
* "Warn" outputs a warning when a non-imported hint is used. Note that this is
an over-approximation, because a hint may be triggered by an eauto run that
will eventually fail and backtrack.
* "Strict" changes the behavior of an unloaded hint to the one of the fail
tactic, allowing to emulate the hopefully future import-scoped hint mechanism.
- New compatibility flag "Universal Lemma Under Conjunction" which
let tactics working under conjunctions apply sublemmas of the form
"forall A, ... -> A".
- New compatibility flag "Bracketing Last Introduction Pattern" which can be
set so that the last disjunctive-conjunctive introduction pattern given to
"intros" automatically complete the introduction of its subcomponents, as the
the disjunctive-conjunctive introduction patterns in non-terminal position
already do.
- New flag "Shrink Abstract" that minimalizes proofs generated by the abstract
tactical w.r.t. variables appearing in the body of the proof.
Program
- The "Shrink Obligations" flag now applies to all obligations, not only those
solved by the automatic tactic.
- Importing Program no longer overrides the "exists" tactic (potential source
of incompatibilities).
- Hints costs are now correctly taken into account (potential source of
incompatibilities).
- Documented the Hint Cut command that allows control of the
proof-search during typeclass resolution (see reference manual).
API
- Some functions from pretyping/typing.ml and their derivatives were potential
source of evarmap leaks, as they dropped their resulting evarmap. The
situation was clarified by renaming them according to a unsafe_* scheme. Their
sound variant is likewise renamed to their old name. The following renamings
were made.
* Typing.type_of -> unsafe_type_of
* Typing.e_type_of -> type_of
* A new e_type_of function that matches the e_ prefix policy
* Tacmach.pf_type_of -> pf_unsafe_type_of
* A new safe pf_type_of function.
All uses of unsafe_* functions should be eventually eliminated.
Tools
- Added an option -w to control the output of coqtop warnings.
- Configure now takes an optional -native-compiler (yes|no) flag replacing
-no-native-compiler. The new flag is set to no by default under Windows.
- Flag -no-native-compiler was removed and became the default for coqc. If
precompilation of files for native conversion test is desired, use
-native-compiler.
- The -compile command-line option now takes the full path of the considered
file, including the ".v" extension, and outputs a warning if such an extension
is lacking.
- The -require and -load-vernac-object command-line options now take a logical
path of a given library rather than a physical path, thus they behave like
Require [Import] path.
- The -vm command-line option has been removed.
Standard Library
- There is now a Coq.Compat.Coq84 library, which sets the various compatibility
options and does a few redefinitions to make Coq behave more like Coq v8.4.
The standard way of putting Coq in v8.4 compatibility mode is to pass the command
line flags "-require Coq.Compat.Coq84 -compat 8.4".
Changes from V8.5beta1 to V8.5beta2
===================================
Logic
- The VM now supports inductive types with up to 8388851 non-constant
constructors and up to 8388607 constant ones.
Specification language
- Syntax "$(tactic)$" changed to "ltac: tactic".
Tactics
- A script using the admit tactic can no longer be concluded by either
Qed or Defined. In the first case, Admitted can be used instead. In
the second case, a subproof should be used.
- The easy tactic and the now tactical now have a more predictable
behavior, but they might now discharge some previously unsolved goals.
Extraction
- Definitions extracted to Haskell GHC should no longer randomly
segfault when some Coq types cannot be represented by Haskell types.
- Definitions can now be extracted to Json for post-processing.
Tools
- Option -I -as has been removed, and option -R -as has been
deprecated. In both cases, option -R can be used instead.
- coq_makefile now generates double-colon rules for rules such as clean.
API
- The interface of [change] has changed to take a [change_arg], which
can be built from a [constr] using [make_change_arg].
Changes from V8.4 to V8.5beta1
==============================
Logic
- Primitive projections for records allow for a compact representation
of projections, without parameters and avoid the behavior of defined
projections that can unfold to a case expression. To turn the use of
native projections on, use [Set Primitive Projections]. Record,
Class and Structure types defined while this option is set will be
defined with primitive projections instead of the usual encoding as
a case expression. For compatibility, when p is a primitive
projection, @p can be used to refer to the projection with explicit
parameters, i.e. [@p] is definitionally equal to [λ params r. r.(p)].
Records with primitive projections have eta-conversion, the
canonical form being [mkR pars (p1 t) ... (pn t)].
- New universe polymorphism (see reference manual)
- New option -type-in-type to collapse the universe hierarchy (this makes the
logic inconsistent).
- The guard condition for fixpoints is now a bit stricter. Propagation
of subterm value through pattern matching is restricted according to
the return predicate. Restores compatibility of Coq's logic with the
propositional extensionality axiom. May create incompatibilities in
recursive programs heavily using dependent types.
- Trivial inductive types are no longer defined in Type but in Prop, which
leads to a non-dependent induction principle being generated in place of
the dependent one. To recover the old behavior, explicitly define your
inductive types in Set.
Vernacular commands
- A command "Variant" allows to define non-recursive variant types.
- The command "Record foo ..." does not generate induction principles
(foo_rect, foo_rec, foo_ind) anymore by default (feature wish
#2693). The command "Variant foo ..." does not either. A flag
"Set/Unset Nonrecursive Elimination Schemes" allows changing this.
The tactic "induction" on a "Record" or a "Variant" is now actually
doing "destruct".
- The "Open Scope" command can now be given also a delimiter (e.g. Z).
- The "Definition" command now allows the "Local" modifier, allowing
for non-importable definitions. The same goes for "Axiom" and "Parameter".
- Section-specific commands such as "Let" (resp. "Variable", "Hypothesis") used
out of a section now behave like the corresponding "Local" command, i.e.
"Local Definition" (resp. "Local Parameter", "Local Axiom"). (potential source
of rare incompatibilities).
- The "Let" command can now define local (co)fixpoints.
- Command "Search" has been renamed into "SearchHead". The command
name "Search" now behaves like former "SearchAbout". The latter name
is deprecated.
- "Search", "About", "SearchHead", "SearchRewrite" and "SearchPattern"
now search for hypothesis (of the current goal by default) first.
They now also support the goal selector prefix to specify another
goal to search: e.g. "n:Search id". This is also true for
SearchAbout although it is deprecated.
- The coq/user-contrib directory and the XDG directories are no longer
recursively added to the load path, so files from installed libraries
now need to be fully qualified for the "Require" command to find them.
The tools/update-require script can be used to convert a development.
- A new Print Strategies command allows visualizing the opacity status
of the whole engine.
- The "Locate" command now searches through all sorts of qualified namespaces of
Coq: terms, modules, tactics, etc. The old behavior of the command can be
retrieved using the "Locate Term" command.
- New "Derive" command to help writing program by derivation.
- New "Refine Instance Mode" option that allows to deactivate the generation of
obligations in incomplete typeclass instances, raising an error instead.
- "Collection" command to name sets of section hypotheses. Named collections
can be used in the syntax of "Proof using" to assert which section variables
are used in a proof.
- The "Optimize Proof" command can be placed in the middle of a proof to
force the compaction of the data structure used to represent the ongoing
proof (evar map). This may result in a lower memory footprint and speed up
the execution of the following tactics.
- "Optimize Heap" command to tell the OCaml runtime to perform a major
garbage collection step and heap compaction.
- "Instance" no longer treats the {|...|} syntax specially; it handles it
in the same way as other commands, e.g. "Definition". Use the {...}
syntax (no pipe symbols) to recover the old behavior.
Specification Language
- Slight changes in unification error messages.
- Added a syntax $(...)$ that allows putting tactics in terms (may
break user notations using "$(", fixable by inserting a space or
rewriting the notation).
- Constructors in pattern-matching patterns now respect the same rules
regarding implicit arguments as in applicative position. The old
behavior can be recovered by the command "Set Asymmetric
Patterns". As a side effect, notations for constructors explicitly
mentioning non-implicit parameters can now be used in patterns.
Considering that the pattern language is already rich enough, binding
local definitions is however now forbidden in patterns (source of
incompatibilities for local definitions that delta-reduce to a constructor).
- Type inference algorithm now granting opacity of constants. This might also
affect behavior of tactics (source of incompatibilities, solvable by
re-declaring transparent constants which were set opaque).
- Existential variables are now referred to by an identifier and the
relevant part of their instance is displayed by default. They can be
reparsed. The naming policy is yet unstable and subject to changes
in future releases.
Tactics
- New tactic engine allowing dependent subgoals, fully backtracking
(also known as multiple success) tactics, as well as tactics which
can consider multiple goals together. In the new tactic engine,
instantiation information of existential variables is always
propagated to tactics, removing the need to manually use the
"instantiate" tactics to mark propagation points.
* New tactical (a+b) inserts a backtracking point. When (a+b);c fails
during the execution of c, it can backtrack and try b instead of a.
* New tactical (once a) removes all the backtracking points from a
(i.e. it selects the first success of a).
* Tactic "constructor" is now fully backtracking. In case of
incompatibilities (e.g. combinatoric explosion), the former
behavior of "constructor" can be retrieved by using instead
"[> once constructor ..]". Thanks to backtracking, undocumented
"constructor <tac>" syntax is now equivalent to
"[> once (constructor; tac) ..]".
* New "multimatch" variant of "match" tactic which backtracks to
new branches in case of a later failure. The "match" tactic is
equivalent to "once multimatch".
* New selector "all:" such that "all:tac" applies tactic "tac" to
all the focused goals, instead of just the first one as is the
default.
* A corresponding new option Set Default Goal Selector "all" makes
the tactics in scripts be applied to all the focused goal by default
* New selector "par:" such that "par:tac" applies the (terminating)
tactic "tac" to all the focused goal in parallel. The number of worker
can be selected with -async-proofs-tac-j and also limited using the
coqworkmgr utility.
* New tactics "revgoals", "cycle" and "swap" to reorder goals.
* The semantics of recursive tactics (introduced with "Ltac t := ..."
or "let rec t := ... in ...") changed slightly as t is now
applied to every goal, not each goal independently. In particular
it may be applied when no goals are left. This may cause tactics
such as "let rec t := constructor;t" to loop indefinitely. The
simple fix is to rewrite the recursive calls as follows:
"let rec t := constructor;[t..]" which recovers the earlier behavior
(source of rare incompatibilities).
* New tactic language feature "numgoals" to count number of goals. It is
accompanied by a "guard" tactic which fails if a Boolean test over
integers does not pass.
* New tactical "[> ... ]" to apply tactics to individual goals.
* New tactic "gfail" which works like "fail" except it will also
fail if every goal has been solved.
* The refine tactic is changed not to use an ad hoc typing algorithm
to generate subgoals. It also uses the dependent subgoal feature
to generate goals to materialize every existential variable which
is introduced by the refinement (source of incompatibilities).
* A tactic shelve is introduced to manage the subgoals which may be
solved by unification: shelve removes every goal it is applied to
from focus. These goals can later be called back into focus by the
Unshelve command.
* A variant shelve_unifiable only removes those goals which appear
as existential variables in other goals. To emulate the old
refine, use "refine c;shelve_unifiable". This can still cause
incompatibilities in rare occasions.
* New "give_up" tactic to skip over a goal. A proof containing
given up goals cannot be closed with "Qed", but only with "Admitted".
- The implementation of the admit tactic has changed: no axiom is
generated for the admitted sub proof. "admit" is now an alias for
"give_up". Code relying on this specific behavior of "admit"
can be made to work by:
* Adding an "Axiom" for each admitted subproof.
* Adding a single "Axiom proof_admitted : False." and the Ltac definition
"Ltac admit := case proof_admitted.".
- Matching using "lazymatch" was fundamentally modified. It now behaves
like "match" (immediate execution of the matching branch) but without
the backtracking mechanism in case of failure.
- New "tryif t then u else v" tactical which executes "u" in case of success
of "t" and "v" in case of failure.
- New conversion tactic "native_compute": evaluates the goal (or an hypothesis)
with a call-by-value strategy, using the OCaml native compiler. Useful on
very intensive computations.
- New "cbn" tactic, a well-behaved simpl.
- Repeated identical calls to omega should now produce identical proof terms.
- Tactics btauto, a reflexive Boolean tautology solver.
- Tactic "tauto" was exceptionally able to destruct other connectives
than the binary connectives "and", "or", "prod", "sum", "iff". This
non-uniform behavior has been fixed (bug #2680) and tauto is
slightly weaker (possible source of incompatibilities). On the
opposite side, new tactic "dtauto" is able to destruct any
record-like inductive types, superseding the old version of "tauto".
- Similarly, "intuition" has been made more uniform and, where it now
fails, "dintuition" can be used (possible source of incompatibilities).
- New option "Unset Intuition Negation Unfolding" for deactivating automatic
unfolding of "not" in intuition.
- Tactic notations can now be defined locally to a module (use "Local" prefix).
- Tactic "red" now reduces head beta-iota redexes (potential source of
rare incompatibilities).
- Tactic "hnf" now reduces inner beta-iota redexes
(potential source of rare incompatibilities).
- Tactic "intro H" now reduces beta-iota redexes if these hide a product
(potential source of rare incompatibilities).
- In Ltac matching on patterns of the form "_ pat1 ... patn" now
behaves like if matching on "?X pat1 ... patn", i.e. accepting "_"
to be instantiated by an applicative term (experimental at this
stage, potential source of incompatibilities).
- In Ltac matching on goal, types of hypotheses are now interpreted in
the %type scope (possible source of incompatibilities).
- "change ... in ..." and "simpl ... in ..." now properly consider nested
occurrences (possible source of incompatibilities since this alters
the numbering of occurrences), but do not support nested occurrences.
- Tactics simpl, vm_compute and native_compute can be given a notation string
to a constant as argument.
- When given a reference as argument, simpl, vm_compute and
native_compute now strictly interpret it as the head of a pattern
starting with this reference.
- The "change p with c" tactic semantics changed, now type-checking
"c" at each matching occurrence "t" of the pattern "p", and
converting "t" with "c".
- Now "appcontext" and "context" behave the same. The old buggy behavior of
"context" can be retrieved at parse time by setting the
"Tactic Compat Context" flag (possible source of incompatibilities).
- New introduction pattern p/c which applies lemma c on the fly on the
hypothesis under consideration before continuing with introduction pattern p.
- New introduction pattern [= x1 .. xn] applies "injection as [x1 .. xn]"
on the fly if injection is applicable to the hypothesis under consideration
(idea borrowed from Georges Gonthier). Introduction pattern [=] applies
"discriminate" if a discriminable equality.
- New introduction patterns * and ** to respectively introduce all forthcoming
dependent variables and all variables/hypotheses dependent or not.
- Tactic "injection c as ipats" now clears c if c refers to an
hypothesis and moves the resulting equations in the hypotheses
independently of the number of ipats, which has itself to be less
than the number of new hypotheses (possible source of incompatibilities;
former behavior obtainable by "Unset Injection L2R Pattern Order").
- Tactic "injection" now automatically simplifies subgoals
"existT n p = existT n p'" into "p = p'" when "n" is in an inductive type for
which a decidable equality scheme has been generated with "Scheme Equality"
(possible source of incompatibilities).
- New tactic "rewrite_strat" for generalized rewriting with user-defined
strategies, subsuming autorewrite.
- Injection can now also deduce equality of arguments of sort Prop, by using
the option "Set Injection On Proofs" (disabled by default). Also improved the
error messages.
- Tactic "subst id" now supports id occurring in dependent local definitions.
- Bugs fixed about intro-pattern "*" might lead to some rare incompatibilities.
- New tactical "time" to display time spent executing its argument.
- Tactics referring or using a constant dependent in a section variable which
has been cleared or renamed in the current goal context now fail
(possible source of incompatibilities solvable by avoiding clearing
the relevant hypotheses).
- New construct "uconstr:c" and "type_term c" to build untyped terms.
- Binders in terms defined in Ltac (either "constr" or "uconstr") can
now take their names from identifiers defined in Ltac. As a
consequence, a name cannot be used in a binder "constr:(fun x =>
...)" if an Ltac variable of that name already exists and does not
contain an identifier. Source of occasional incompatibilities.
- The "refine" tactic now accepts untyped terms built with "uconstr"
so that terms with holes can be constructed piecewise in Ltac.
- New bullets --, ++, **, ---, +++, ***, ... made available.
- More informative messages when wrong bullet is used.
- Bullet suggestion when a subgoal is solved.
- New tactic "enough", symmetric to "assert", but with subgoals
swapped, as a more friendly replacement of "cut".
- In destruct/induction, experimental modifier "!" prefixing the
hypothesis name to tell not erasing the hypothesis.
- Bug fixes in "inversion as" may occasionally lead to incompatibilities.
- Behavior of introduction patterns -> and <- made more uniform
(hypothesis is cleared, rewrite in hypotheses and conclusion and
erasing the variable when rewriting a variable).
- New experimental option "Set Standard Proposition Elimination Names"
so that case analysis or induction on schemes in Type containing
propositions now produces "H"-based names.
- Tactics from plugins are now active only when the corresponding module
is imported (source of incompatibilities, solvable by adding an "Import";
in the particular case of Omega, use "Require Import OmegaTactic").
- Semantics of destruct/induction has been made more regular in some
edge cases, possibly leading to incompatibilities:
- new goals are now opened when the term does not match a subterm of
the goal and has unresolved holes, while in 8.4 these holes were
turned into existential variables
- when no "at" option is given, the historical semantics which
selects all subterms syntactically identical to the first subterm
matching the given pattern is used
- non-dependent destruct/induction on an hypothesis with premises in
an inductive type with indices is fixed
- residual local definitions are now correctly removed.
- The rename tactic may now replace variables in parallel.
- A new "Info" command replaces the "info" tactical discontinued in
v8.4. It still gives informative results in many cases.
- The "info_auto" tactic is known to be broken and does not print a
trace anymore. Use "Info 1 auto" instead. The same goes for
"info_trivial". On the other hand "info_eauto" still works fine,
while "Info 1 eauto" prints a trivial trace.
- When using a lemma of the prototypical form "forall A, {a:A & P a}",
"apply" and "apply in" do not instantiate anymore "A" with the
current goal and use "a" as the proof, as they were sometimes doing,
now considering that it is a too powerful decision.
Program
- "Solve Obligations using" changed to "Solve Obligations with",
consistent with "Proof with".
- Program Lemma, Definition now respect automatic introduction.
- Program Lemma, Definition, etc.. now interpret "->" like Lemma and
Definition as a non-dependent arrow (potential source of
incompatibility).
- Add/document "Set Hide Obligations" (to hide obligations in the final
term inside an implicit argument) and "Set Shrink Obligations" (to
minimize dependencies of obligations defined by tactics).
Notations
- The syntax "x -> y" is now declared at level 99. In particular, it has
now a lower priority than "<->": "A -> B <-> C" is now "A -> (B <-> C)"
(possible source of incompatibilities)
- Notations accept term-providing tactics using the $(...)$ syntax.
- "Bind Scope" can no longer bind "Funclass" and "Sortclass".
- A notation can be given a (compat "8.x") annotation, making it behave
like a "only parsing" notation, but the annotation may lead to eventually
issue warnings or errors in further versions when this notation is used.
- More systematic insertion of spaces as a default for printing
notations ("format" still available to override the default).
- In notations, a level modifier referring to a non-existent variable is
now considered an error rather than silently ignored.
Tools
- Option -I now only adds directories to the ml path.
- Option -Q behaves as -R, except that the logical path of any loaded file has
to be fully qualified.
- Option -R no longer adds recursively to the ml path; only the root
directory is added. (Behavior with respect to the load path is
unchanged.)
- Option -nois prevents coq/theories and coq/plugins to be recursively
added to the load path. (Same behavior as with coq/user-contrib.)
- coqdep accepts a -dumpgraph option generating a dot file.
- Makefiles generated through coq_makefile have three new targets "quick"
"checkproofs" and "vio2vo", allowing respectively to asynchronously compile
the files without playing the proof scripts, asynchronously checking
that the quickly generated proofs are correct and generating the object
files from the quickly generated proofs.
- The XML plugin was discontinued and removed from the source.
- A new utility called coqworkmgr can be used to limit the number of
concurrent workers started by independent processes, like make and CoqIDE.
This is of interest for users of the par: goal selector.
Interfaces
- CoqIDE supports asynchronous edition of the document, ongoing tasks and
errors are reported in the bottom right window. The number of workers
taking care of processing proofs can be selected with -async-proofs-j.
- CoqIDE highlights in yellow "unsafe" commands such as axiom
declarations, and tactics like "give_up".
- CoqIDE supports Proof General like key bindings;
to activate the PG mode go to Edit -> Preferences -> Editor.
For the documentation see Help -> Help for PG mode.
- CoqIDE automatically retracts the locked area when one edits the
locked text.
- CoqIDE search and replace got regular expressions power. See the
documentation of OCaml's Str module for the supported syntax.
- Many CoqIDE windows, including the query one, are now detachable to
improve usability on multi screen work stations.
- Coqtop/coqc outputs highlighted syntax. Colors can be configured thanks
to the COQ_COLORS environment variable, and their current state can
be displayed with the -list-tags command line option.
- Third party user interfaces can install their main loop in $COQLIB/toploop
and call coqtop with the -toploop flag to select it.
Internal Infrastructure
- Many reorganizations in the ocaml source files. For instance,
many internal a.s.t. of Coq are now placed in mli files in
a new directory intf/, for instance constrexpr.mli or glob_term.mli.
More details in dev/doc/changes.
- The file states/initial.coq does not exist anymore. Instead, coqtop
initially does a "Require" of Prelude.vo (or nothing when given
the options -noinit or -nois).
- The format of vo files has slightly changed: cf final comments in
checker/cic.mli.
- The build system does not produce anymore programs named coqtop.opt
and a symbolic link to coqtop. Instead, coqtop is now directly
an executable compiled with the best OCaml compiler available.
The bytecode program coqtop.byte is still produced. Same for other
utilities.
- Some options of the ./configure script slightly changed:
* The -coqrunbyteflags and its blank-separated argument is replaced
by option -vmbyteflags which expects a comma-separated argument.
* The -coqtoolsbyteflags option is discontinued, see -no-custom instead.
Miscellaneous
- ML plugins now require a "DECLARE PLUGIN \"foo\"" statement. The "foo" name
must be exactly the name of the ML module that will be loaded through a
"Declare ML \"foo\"" command.
Changes from V8.4beta2 to V8.4
==============================
Vernacular commands
- The "Reset" command is now supported again in files given to coqc or Load.
- "Show Script" now indents again the displayed scripts. It can also work
correctly across Load'ed files if the option "Unset Atomic Load" is used.
- "Open Scope" can now be given the delimiter (e.g. Z) instead of the full
scope name (e.g. Z_scope).
Notations
- Most compatibility notations of the standard library are now tagged as
(compat xyz), where xyz is a former Coq version, for instance "8.3".
These notations behave as (only parsing) notations, except that they may
triggers warnings (or errors) when used while Coq is not in a corresponding
-compat mode.
- To activate these compatibility warnings, use "Set Verbose Compat Notations"
or the command-line flag -verbose-compat-notations.
- For a strict mode without these compatibility notations, use
"Unset Compat Notations" or the command-line flag -no-compat-notations.