TODO: classer les changements intervenus entre la V7.0 beta et la V7.0 ? et ceux intervenus entre la V6.3.1 et la V7.0beta ? Ou laisser des listes séparées ? Changes from V7.0 to V7.1 ------------------------- Notes: - items followed by (*) are sources of incompatibilities - items followed by (+) have been introduced in version 7.0 Language - New construction for local definitions (Let-In) with syntax [x:=u]t (+) - New reduction flags Zeta and Evar in Eval Compute, for inlining of local definitions and instantiation of existential variables - Delta reduction flag does not perform Zeta and Evar reduction any more (*) - new visibility discipline for Remark, Fact and Local: Remark's and Fact's now survive at the end of section, but are only accessible using a qualified names as soon as their strength expires; Local's disappear and are moved into local definitions for each construction persistent at section closing - Local definitions allowed in Record (aka record à la Randy Pollack) - known Coercion bugs fixed - Cases predicate inference bug fixed - known dependent Cases predicate bugs fixed - bug with identifiers ended by a number greater than 2^30 fixed (+) Language : long names - Each construction has a unique absolute names built from a base name, the name of the module in which they are defined (Top if in coqtop), and possibly an arbitrary long sequence of directory (e.g. "Coq.Lists.PolyList.flat_map" where "Coq" means that "flat_map" is part of Coq standard library, "Lists" means it is defined in the Lists library and "PolyList" means it is in the file Polylist) (+) - Constructions can be referred by their base name, or, in case of conflict, by a "qualified" name, where the base name is prefixed by the module name (and possibly by a directory name, and so on). A fully qualified name is an absolute name which always refer to the the construction it denotes (to preserve the visibility of all constructions, no conflict is allowed for an absolute name) (+) - Long names are available for modules with the possibility of using the directory name as a component of the module full name (with option -R to coqtop and coqc, or command Add LoadPath) (+) - Improved conflict resolution strategy (the Unix PATH model), allowing more constructions to be referred just by their base name Tactics - New set of tactics to deal with types equipped with specific equalities (aka Setoïds, e.g. nat equipped with eq_nat) [by C. Renard] - New tactic Assert, similar to Cut but expected to be more user-friendly - New tactic NewDestruct and NewInduction intended to replace Elim and Induction, Case and Destruct in a more user-friendly way (see restrictions in the reference manual) - New tactic ROmega: an experimental alternative (based on reflexion) to Omega [by P. Crégut] - Reduction tactics in local definitions apply only to the body - New syntax of the form "Compute in Type of H." to require a reduction on the types of local definitions - Inversion, Injection, Discriminate, ... apply also on the quantified premises of a goal (using the "Intros until" syntax) - Decompose removes temporary hypotheses (*) - Tauto now manages uniformly hypotheses and conclusions of the form "t=t" which all are considered equivalent to "True". Especially, Tauto now solves goals of the form "H : ~ t = t |- A". Efficiency - Excessive memory uses specific to V7.0 fixed - Excessive size of .vo files fixed Parsing and grammar extension - Only identifiers starting with "_" or a letter, and followed by letters, digits, "_" or "'" are allowed (e.g. "$" and "@" are no longer allowed) - Un lieur multiple comme (a:A)(a,b:(P a))(Q a), n'est plus compris comme (a:A)(a0:(P a))(b:(P a))(Q a0), mais comme (a:A)(a0:(P a))(b:(P a0))(Q a0) (*)(+) - More constraints when writing ast - "{...}" and the macros $LIST, $VAR, etc. now expect a metavariable (an identifier starting with $) (*) - identifiers should starts with a letter or "_" and be followed by letters, digits, "_" or "'" (other caracters are still supported but it is not advised to use them) (*)(+) - Entry "command" in "Grammar" and quotations (<<...>> stuff) is renamed "constr" as in "Syntax" (+) - New syntax "[" sentence_1 ... sentence_n"]." to group sentences (useful for Time and to write grammar rules abbreviating several commands) (+) - The default parser for actions in the grammar rules (and for patterns in the pretty-printing rules) is now the one associated to the grammar (i.e. vernac, tactic or constr); no need then for quotations as in <:vernac:<...>>; to return an "ast", the grammar must be explicity typed with tag ": ast" or ": ast list", or if a syntax rule, by using <<...>> in the patterns (expression inside these angle brackets are parsed as "ast"); for grammars other than vernac, tactic or constr, you may explicitly type the action with tags ": constr", ": tactic", or ":vernac" (+) - Interpretation of names in Grammar rule is now based on long names, which allows to avoid problems (or sometimes tricks) related to overloaded names (+) - A dedicated syntax has been introduced for Reals (e.g ``3+1/x``) (+) Commands - Generalization of the usage of qualified identifiers in tactics and commands about globals, e.g. Decompose, Eval Delta; Hints Unfold, Transparent, Require - Require synchronous with Reset; Require's scope stops at Section ending Extraction - New algorithm for extraction able to deal with "Type" (+) Standard library - New library on maps on integers (IntMap, contributed by Jean Goubault) - New lemmas about integer numbers [ZArith] - New lemmas about [Reals] (+) - Exc/Error/Value renamed into Option/Some/None (*) New user contributions - Constructive complex analysis and the Fundamental Theorem of Algebra [FTA] (Herman Geuvers, Freek Wiedijk, Jan Zwanenburg, Randy Pollack, Henk Barendregt, Nijmegen) - A new axiomatization of ZFC set theory [Functions_in_ZFC] (C. Simpson, Sophia-Antipolis) - Basic notions of graph theory [GRAPHS-BASICS] (Jean Duprat, Lyon) - A library for floating-point numbers [Float] (Laurent Théry, Sylvie Boldo, Sophia-Antipolis) - Formalisation of CTL and TCTL temporal logic [CtlTctl] (Carlos Daniel Luna,Montevideo) - Specification and verification of the Railroad Crossing Problem in CTL and TCTL [RailroadCrossing] (Carlos Daniel Luna,Montevideo) - P-automaton and the ABR algorithm [PAutomata] (Christine Paulin, Emmanuel Freund, Orsay) - Correctness proofs of the following imperative algorithms: Bresenham line drawing algorithm [Bresenham], Marché's minimal edition distance algorithm [Diff] (Jean-Christophe Filliâtre, Orsay) - Correctness proofs of Buchberger's algorithm [Buchberger] and RSA cryptographic algorithm [Rsa] (Laurent Théry, Sophia-Antipolis) - Correctness proof of Stalmarck tautology checker algorithm [Stalmarck] (Laurent Théry, Pierre Letouzey, Sophia-Antipolis) Changes from V6.3.1 to V7.0 --------------------------- To report: Langage - On peut (et il est conseillé) associer à un répertoire physique un nom logique dans la structure des noms de Coq. Les définitions de la bibliothèque standard sont associées au préfixe logique `Coq'. Pour associer un répertoire physique à un nom logique, il faut utiliser l'option -R de coqtop et coqc (cf Outils). Par défaut, le nom logique "Scratch" est utilisé pour toute définition globale non associée à un module non associé à un nom logique. - Le nom long des définitions globales est accessible pour l'utilisateur par la notation pointée (style Coq.Arith.Plus.plus_assoc_l). La syntaxe du "." final change (cf Vernac). Le nommage des définitions globales change (cf Métathéorie). Extensions de syntaxe avec Grammar et Syntax - Le non affichage des Infix est corrigé. Syntaxe des constructions - Cases engendre parfois des noms differents (source théorique d'incompatibilité mais insensible dans la pratique) - Les alias de motifs ayant un type dépendant ne sont pour l'instant pas traités - Davantage d'inférence automatique de "?". - Davantage d'arguments implicites engendrés par le discharge. - Les cas des Cases ne se lisent plus de manière séquentielle, sauf en cas de clauses par défaut redondantes auquel cas la première est prise avec un avertissement. Commandes - Changement de nom de certaines commandes AddPath -> Add LoadPath; Print LoadPath -> Print LoadPath; DelPath -> Remove LoadPath; AddRecPath -> Add Rec LoadPath Print Path -> Print Coercion Paths. Implicit Arguments On -> Set Implicit Arguments Implicit Arguments Off -> Unset Implicit Arguments Nouveau: Test Implicit Arguments - End Silent était interprété comme une fin de section Begin Silent -> Set Silent End Silent -> Unset Silent. - Commandes pour associer des chemins physiques à des chemins logiques Add LoadPath physical_dir as logical_dir Add Rec LoadPath physical_dir as logical_dir - Import module (re-)rend visible toutes les définitions et théorèmes définis dans module. - Déclaration manuelle des implicites avec "Implicits ident." pour activer les arguments implicites pour ident indépendamment de l'état courant du mode implicite. "Implicits ident [ num num ... num ]." pour donner explicitement quels arguments doivent être implicites. - SearchPattern / SearchRewrite (contribution de Yves Bertot); Search peut lui aussi être restreint à une recherche dans ou à l'extérieur de modules. - SearchIsos n'a pas encore été porté. - Le point final des commandes doit être suivi d'un blanc (retour chariot, tabulation ou espace) - Légère restriction de la syntaxe de Cbv Delta : l'option [-myconst] de Cbv doit immédiatement suivre Delta - Nouveau: Debug On/Off positionne/débranche le débogueur de tactiques (encore très expérimental). - Fact se comporte différemment Tactiques - Langage de tactiques Ltac: nouvelle couche de métalangage pour traiter de petites automatisations. C'est essentiellement un petit noyau fonctionnel muni d'opérateurs de filtrage élaborés (sur les termes, les contextes de preuves et réalisant du backtracking). Pour plus détails, consulter le manuel de référence (chapitre 10). - Tactique Let renommé en LetTac et utilise le let-in primitif; Induction renommé en OldInduction et nouveau Induction plus "convivial". - Elim avec un schéma d'élimination différent de celui créé à la définition d'un inductif n'est plus possible. Il faut utiliser Elim with . - Decompose - Numérotation dans l'ordre des hypothèses créées - Correction de bugs (quand le type ne commence pas par un inductif) et refus d'agir sous les ->. - Simpl ne déplie plus les appels récursifs d'un Fix mutuel réduit. Rem: c'est une source d'incompatibilité. - Intro échoue si le nom d'hypothèse existe au lieu de mettre un avertissement - Plus de "Require Prolog" (intégré par défaut) - Unfold échoue si on lui donne en argument une définition non dépliable - Tauto et Intuition ont été intégralement réécrites en utilisant le nouveau langage de tactiques Ltac. Les conséquences sont un gain considérable en compacité et en performances. Tauto est totalement conservatif. Intuition perd légèrement en puissance mais gagne une sémantique plus claire. - AutoRewrite ne s'occupe maintenant que du but principal et c'est les Hint Rewrite qui gèrent les sous-buts générés. - Les instantiations redondantes ou incompatibles de Apply ... with ... sont maintenant correctement traitées. - Nouveau: tactique Field pour décider des égalités sur les corps commutatifs. La tactique a été instantiée pour les nombres réels et peut donc être utilisée pour résoudre des égalités sur les réels. - Nouveau: tactique Fourier qui résoud les inégalités linéaires sur les nombres réels. - Nouveau: diverses tactiques pour les nombres réels: DiscrR, SplitRmult, SplitAbsolu. Outils - Deux binaires maximum : coqtop.byte et coqtop.opt si plateforme native; coqtop est un lien vers le plus efficace possible (coqtop.opt s'il existe, coqtop.byte sinon); -full maintenant obsolete - do_Makefile s'appelle maintenant coq_makefile - Utilisation de l'option -R de coqtop et coqc pour associer un répertoire physique à un répertoire logique (cf Métathéorie) - La plupart des erreurs de typage sont maintenant localisée dans le source (à l'exception des erreurs d'univers et de garde). Développeurs - Beaucoup de modification dans le sens de la simplification et de la documentation (mais cela reste une version de transition) Différences V7.0beta / V7.0 - localisation des erreurs avec Syntactif Definition - clauses par défaut de Cases non lues séquentiellement et détection des cas non utilisés - Ajout d'une option Set/Unset/Test Printing Coercions - Possibilité de déplier des définitions locales à un but - Suppression avertissement si pas de .coqrc - Add ML Path est fait automatiquement par Add LoadPath - Nouveau mécanisme de nommage des schémas d'élimination (incompatibilités...) Différences oubliées dans la V7.0beta : - Les noms de variables des projections de Record sont maintenant basés sur l'initiale de leur type. - Du fait des noms qualifiés, les variables de buts n'évitent plus les globaux de même nom de base - Unfold ne peut s'appliquer qu'à des constantes dépliables (en particulier pas à des Syntactic Definition, ni des types inductifs)