diff options
| author | letouzey | 2011-08-18 15:08:00 +0000 |
|---|---|---|
| committer | letouzey | 2011-08-18 15:08:00 +0000 |
| commit | 58452e2b0a9847b6bd89941051dc2a0633679f6e (patch) | |
| tree | 28cf2a27de2a0807d38dab9e17b0f899b9a52a2c | |
| parent | 2370dc99519766874be7176ae6eb546018362b51 (diff) | |
Updates in CHANGES
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14416 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | CHANGES | 92 |
1 files changed, 75 insertions, 17 deletions
@@ -23,7 +23,10 @@ Specification language and notations Tactics -- New proof engine supporting bullets. +- New proof engine. +- Scripts can now be structured thanks to bullets - * + and to subgoal + delimitation via { }. Note : for use with ProofGeneral, a cvs version of + ProofGeneral no older than mid-July 2011 is currently required. DOC TODO. - Support for tactical "info" is suspended. - Support for command "Show Script" is suspended. - New tactics constr_eq, is_evar and has_evar. @@ -44,7 +47,13 @@ Tactics Vernacular commands +- 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_". DOC TODO - 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. @@ -57,6 +66,10 @@ Vernacular commands Module System +- 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 @@ -64,21 +77,51 @@ Module System 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. TODO: DOC! +- 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. Libraries -- Creation of PArith, a subdirectory containing files about the positive type, - such as BinPos or Pnat. - Extension of the abstract part of Numbers, which now provide axiomatizations - and results about many more functions, such as pow, gcd, lcm, sqrt, log2. - Implementations of these functions in nat N BigN Z BigZ. See in particular - Npeano for new functions about nat. -- Important revision of NArith and ZArith. In particular some definitions - or lemmas may have moved. The alternative division (Trunc convention - instead of Floor) is now named Zquot (noted ÷) and Zrem by analogy - with Haskell. In Zeven, the behavior of Zdiv2 on negative numbers has been - changed to be consistent with Zdiv, while the old behavior now corresponds - to function Zquot2. TODO: say more later. + 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 @@ -92,6 +135,7 @@ Libraries - 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) Internal infrastructure @@ -103,27 +147,41 @@ Internal infrastructure - 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 toward Windows, contact P. Letouzey - for more informations. +- 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 with all the stdlib. 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". DOC TODO. +- New option "Set/Unset Extraction KeepSingleton" for preventing the + extraction to optimize singleton container types. DOC TODO +- The extraction now identifies and properly rejects a particular case of + universe polymorphism it cannot handle yet (the pair (I,I) being Prop). -Tools +CoqIDE -- Coq now searches directories specified in COQPATH and user-contribs before - the standard library. - 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 Coqide parsing of sentences has be reworked and now supports + tactic delimitation via { }. +- Coqide now accepts the Abort command (wish #2357). + +Tools + +- Coq now searches directories specified in COQPATH and user-contribs before + the standard library. - coq_makefile major cleanup. * mli taken into account, ml not preproccessed anymore, ml4 work * mlihtml generates doc of mli, install-doc install the html doc in DOCDIR |
