path: root/CHANGES

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
  <hyp> with <nom du schéma d'élimination>.

- 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)