|
richards@cs.princeton.edu). Updated package to use PLIST_VARS and CONF_FILES.
Updated coq to version 8.4. Changes include:
Logic
- Standard eta-conversion now supported (dependent product only).
- Guard condition improvement: subterm property is propagated through beta-redex
blocked by pattern-matching, as in "(match v with C .. => fun x => u end) x";
this allows for instance to use "rewrite ... in ..." without breaking
the guard condition.
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).
- Commands "Back" and "BackTo" are now handling the proof states. They may
perform some extra steps of backtrack to avoid states where the proof
state is unavailable (typically a closed proof).
- The commands "Suspend" and "Resume" have been removed.
- A basic Show Script has been reintroduced (no indentation).
- New command "Set Parsing Explicit" for deactivating parsing (and printing)
of implicit arguments (useful for teaching).
- New command "Grab Existential Variables" to transform the unresolved evars
at the end of a proof into goals.
- It is now mandatory to have a space (or tabulation or newline or end-of-file)
after a "." ending a sentence.
- In SearchAbout, the [ ] delimiters are now optional.
- New command "Add/Remove Search Blacklist <substring> ...":
a Search or SearchAbout or similar query will never mention lemmas
whose qualified names contain any of the declared substrings.
The default blacklisted substrings are "_admitted" "_subproof" "Private_".
- When the output file of "Print Universes" ends in ".dot" or ".gv",
the universe graph is printed in the DOT language, and can be
processed by Graphviz tools.
- New command "Print Sorted Universes".
- The undocumented and obsolete option "Set/Unset Boxed Definitions" has
been removed, as well as syntaxes like "Boxed Fixpoint foo".
- A new option "Set Default Timeout n / Unset Default Timeout".
- Qed now uses information from the reduction tactics used in proof script
to avoid conversion at Qed time to go into a very long computation.
- New command "Show Goal ident" to display the statement of a goal, even
a closed one (available from Proof General).
- Command "Proof" accept a new modifier "using" to force generalization
over a given list of section variables at section ending.
- New command "Arguments" generalizing "Implicit Arguments" and
"Arguments Scope" and that also allows to rename the parameters of a
definition and to tune the behavior of the tactic "simpl".
Specification language and 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.
- Maximal implicit arguments can now be set locally by { }. The registration
traverses fixpoints and lambdas. Because there is conversion in types,
maximal implicit arguments are not taken into account in partial
applications (use eta expanded form with explicit { } instead).
- Added support for recursive notations with binders (allows for instance
to write "exists x y z, P").
- Structure/Record printing can be disable by "Unset Printing Records".
In addition, it can be controlled on type by type basis using
"Add Printing Record" or "Add Printing Constructor".
- Pattern-matching compilation algorithm: in "match x, y with ... end",
possible dependencies of x (or of the indices of its type) in the type
of y are now taken into account.
Tactics
- An annotation "eqn:H" or "eqn:?" can be added to a "destruct"
or "induction" to make it generate equations in the spirit of "case_eq".
The former syntax "_eqn" is discontinued.
- The name of the hypothesis introduced by tactic "remember" can be
set via the new syntax "remember t as x eqn:H" (wish #2489).
- Still no general "info" tactical, but new specific tactics info_auto,
info_eauto, info_trivial which provides information on the proofs found
by auto/eauto/trivial. Display of these details could also be activated by
"Set Info Auto"/"Set Info Eauto"/"Set Info Trivial".
- Details on everything tried by auto/eauto/trivial during a proof search
could be obtained by "debug auto", "debug eauto", "debug trivial" or by a
global "Set Debug Auto"/"Set Debug Eauto"/"Set Debug Trivial".
- New command "r string" in Ltac debugger that interprets "idtac
string" in Ltac code as a breakpoint and jumps to its next use.
- Tactics from the Dp plugin (simplify, ergo, yices, cvc3, z3, cvcl,
harvey, zenon, gwhy) have been removed, since Why2 has not been
maintained for the last few years. The Why3 plugin should be a suitable
replacement in most cases.
- New proof engine.
- Scripts can now be structured thanks to bullets - * + and to subgoal
delimitation via { }. Note: for use with Proof General, a cvs version of
Proof General no older than mid-July 2011 is currently required.
- Support for tactical "info" is suspended.
- Support for command "Show Script" is suspended.
- New tactics constr_eq, is_evar and has_evar for use in Ltac.
- Removed the two-argument variant of "decide equality".
- New experimental tactical "timeout <n> <tac>". Since <n> is a time
in second for the moment, this feature should rather be avoided
in scripts meant to be machine-independent.
- Fix in "destruct": removal of unexpected local definitions in context might
result in some rare incompatibilities (solvable by adapting name hypotheses).
- Introduction pattern "_" made more robust.
- Tactic (and Eval command) vm_compute can now be interrupted via Ctrl-C.
- Unification in "apply" supports unification of patterns of the form
?f x y = g(x,y) (compatibility ensured by using
"Unset Tactic Pattern Unification"). It also supports (full) betaiota.
- Tactic autorewrite does no longer instantiate pre-existing
existential variables (theoretical source of possible incompatibilities).
- Tactic "dependent rewrite" now supports equality in "sig".
- Tactic omega now understands Zpred (wish #1912) and can prove any goal
from a context containing an arithmetical contradiction (wish #2236).
- Using "auto with nocore" disables the use of the "core" database (wish #2188).
This pseudo-database "nocore" can also be used with trivial and eauto.
- Tactics "set", "destruct" and "induction" accepts incomplete terms and
use the goal to complete the pattern assuming it is non ambiguous.
- When used on arguments with a dependent type, tactics such as
"destruct", "induction", "case", "elim", etc. now try to abstract
automatically the dependencies over the arguments of the types
(based on initial ideas from Chung-Kil Hur, extension to nested
dependencies suggested by Dan Grayson)
- Tactic "injection" now failing on an equality showing no constructors while
it was formerly generalizing again the goal over the given equality.
- In Ltac, the "context [...]" syntax has now a variant "appcontext [...]"
allowing to match partial applications in larger applications.
- When applying destruct or inversion on a fixpoint hiding an inductive
type, recursive calls to the fixpoint now remain folded by default (rare
source of incompatibility generally solvable by adding a call to simpl).
- In an ltac pattern containing a "match", a final "| _ => _" branch could be
used now instead of enumerating all remaining constructors. Moreover, the
pattern "match _ with _ => _ end" now allows to match any "match". A "in"
annotation can also be added to restrict to a precise inductive type.
- The behavior of "simpl" can be tuned using the "Arguments" vernacular.
In particular constants can be marked so that they are always/never unfolded
by "simpl", or unfolded only when a set of arguments evaluates to a
constructor. Last one can mark a constant so that it is unfolded only if the
simplified term does not expose a match in head position.
Libraries
- Reals: changed definition of PI, no more axiom about sin(PI/2).
- SetoidPermutation: a notion of permutation for lists modulo a setoid equality.
- BigN: fixed the ocaml code doing the parsing/printing of big numbers.
- MSetRBT: a new implementation of MSets via Red-Black trees (initial
contribution by Andrew Appel).
- MSetAVL: for maximal sharing with the new MSetRBT, the argument order
of Node has changed (this should be transparent to regular MSets users).
- Extension of the abstract part of Numbers, which now provide axiomatizations
and results about many more integer functions, such as pow, gcd, lcm, sqrt,
log2 and bitwise functions. These functions are implemented for nat, N, BigN,
Z, BigZ. See in particular file NPeano for new functions about nat.
- The definition of types positive, N, Z is now in file BinNums.v
- Major reorganization of ZArith. The initial file ZArith/BinInt.v now contains
an internal module Z implementing the Numbers interface for integers.
This module Z regroups:
* all functions over type Z : Z.add, Z.mul, ...
* the minimal proofs of specifications for these functions : Z.add_0_l, ...
* an instantation of all derived properties proved generically in Numbers :
Z.add_comm, Z.add_assoc, ...
A large part of ZArith is now simply compatibility notations, for instance
Zplus_comm is an alias for Z.add_comm. The direct use of module Z is now
recommended instead of relying on these compatibility notations.
- Similar major reorganization of NArith, via a module N in NArith/BinNat.v
- Concerning the positive datatype, BinPos.v is now in a specific directory
PArith, and contains an internal submodule Pos. We regroup there functions
such as Pos.add Pos.mul etc as well as many results about them. These results
are here proved directly (no Number interface for strictly positive numbers).
- Note that in spite of the compatibility layers, all these reorganizations
may induce some marginal incompatibilies in scripts. In particular:
* the "?=" notation for positive now refers to a binary function Pos.compare,
instead of the infamous ternary Pcompare (now Pos.compare_cont).
* some hypothesis names generated by the system may changed (typically for
a "destruct Z_le_gt_dec") since naming is done after the short name of
the head predicate (here now "le" in module Z instead of "Zle", etc).
* the internals of Z.add has changed, now relying of Z.pos_sub.
- Also note these new notations:
* "<?" "<=?" "=?" for boolean tests such as Z.ltb Z.leb Z.eqb.
* "รท" for the alternative integer division Z.quot implementing the Truncate
convention (former ZOdiv), while the notation for the Coq usual division
Z.div implementing the Flooring convention remains "/". Their corresponding
modulo functions are Z.rem (no notations) for Z.quot and Z.modulo (infix
"mod" notation) for Z.div.
- Lemmas about conversions between these datatypes are also organized
in modules, see for instance modules Z2Nat, N2Z, etc.
- When creating BigN, the macro-generated part NMake_gen is much smaller.
The generic part NMake has been reworked and improved. Some changes
may introduce incompatibilities. In particular, the order of the arguments
for BigN.shiftl and BigN.shiftr is now reversed: the number to shift now
comes first. By default, the power function now takes two BigN.
- Creation of Vector, an independent library for lists indexed by their length.
Vectors' names overwrite lists' one so you should not "Import" the library.
All old names changed: function names follow the ocaml ones and, for example,
Vcons becomes Vector.cons. You can get [..;..;..]-style notations by importing
Vector.VectorNotations.
- Removal of TheoryList. Requiring List instead should work most of the time.
- New syntax "rew Heq in H" and "rew <- Heq in H" for eq_rect and
eq_rect_r (available by importing module EqNotations).
- Wf.iter_nat is now Peano.nat_iter (with an implicit type argument).
Module System
- The names of modules (and module types) are now in a fully separated
namespace from ordinary definitions: "Definition E:=0. Module E. End E."
is now accepted.
- During subtyping checks, an opaque constant in a module type could now
be implemented by anything of the right type, even if bodies differ.
Said otherwise, with respect to subtyping, an opaque constant behaves
just as a parameter. Coqchk was already implementing this, but not coqtop.
- The inlining done during application of functors can now be controlled
more precisely, by the annotations (no inline) or (inline at level XX).
With the latter annotation, only functor parameters whose levels
are lower or equal than XX will be inlined.
The level of a parameter can be fixed by "Parameter Inline(30) foo".
When levels aren't given, the default value is 100. One can also use
the flag "Set Inline Level ..." to set a level.
- Print Assumptions should now handle correctly opaque modules (#2168).
- Print Module (Type) now tries to print more details, such as types and
bodies of the module elements. Note that Print Module Type could be
used on a module to display only its interface. The option
"Set Short Module Printing" could be used to switch back to the earlier
behavior were only field names were displayed.
CoqIDE
- Coqide now supports the "Restart" command, and "Undo" (with a warning).
Better support for "Abort".
- Coqide now runs coqtop as separated process, making it more robust:
coqtop subprocess can be interrupted, or even killed and relaunched
(cf button "Restart Coq", ex-"Go to Start"). For allowing such
interrupts, the Windows version of coqide now requires Windows >= XP
SP1.
- The communication between CoqIDE and Coqtop is now done via a dialect of XML.
- The backtrack engine of CoqIDE has been reworked, it now uses the
"Backtrack" command similarly to Proof General.
- The Coqide parsing of sentences has be reworked and now supports
tactic delimitation via { }.
- Coqide now accepts the Abort command (wish #2357).
- Coqide can read coq_makefile files as "project file" and use it to
set automatically options to send to coqtop.
- Preference files have moved to $XDG_CONFIG_HOME/coq and accelerators
are not stored as a list anymore.
Internal infrastructure
- Opaque proofs are now loaded lazily by default. This allows to be almost as
fast as -dont-load-proofs, while being safer (no creation of axioms) and
avoiding feature restrictions (Print and Print Assumptions work ok).
- Revised hash-consing code allowing more sharing of memory
- Experimental support added for camlp4 (the one provided alongside ocaml),
simply pass option -usecamlp4 to ./configure. By default camlp5 is used.
- Revised build system: no more stages in Makefile thanks to some recursive
aspect of recent gnu make, use of vo.itarget files containing .v to compile
for both make and ocamlbuild, etc.
- Support of cross-compilation via mingw from unix toward Windows,
contact P. Letouzey for more informations.
- New Makefile rules mli-doc to make html of mli in dev/doc/html and
full-stdlib to get a (huge) pdf reflecting the whole standard library.
Extraction
- By default, opaque terms are now truly considered opaque by extraction:
instead of accessing their body, they are now considered as axioms.
The previous behaviour can be reactivated via the option
"Set Extraction AccessOpaque".
- The pretty-printer for Haskell now produces layout-independant code
- A new command "Separate Extraction cst1 cst2 ..." that mixes a
minimal extracted environment a la "Recursive Extraction" and the
production of several files (one per coq source) a la "Extraction Library".
- New option "Set/Unset Extraction KeepSingleton" for preventing the
extraction to optimize singleton container types.
- The extraction now identifies and properly rejects a particular case of
universe polymorphism it cannot handle yet (the pair (I,I) being Prop).
- Support of anonymous fields in record (#2555).
Tools
- Coq now searches directories specified in COQPATH, $XDG_DATA_HOME/coq,
$XDG_DATA_DIRS/coq, and user-contribs before the standard library.
- Coq rc file has moved to $XDG_CONFIG_HOME/coq.
- Major changes to coq_makefile:
* mli/mlpack/mllib taken into account, ml not preproccessed anymore, ml4 work;
* mlihtml generates doc of mli, install-doc install the html doc in DOCDIR
with the same policy as vo in COQLIB;
* More variables are given by coqtop -config, others are defined only if the
users doesn't have defined them elsewhere. Consequently, generated makefile
should work directly on any architecture;
* Packagers can take advantage of $(DSTROOT) introduction. Installation can
be made in $XDG_DATA_HOME/coq;
* -arg option allows to send option as argument to coqc.
|
