The Coq mailing list

[Frédéric Blanqui <frederic.blanqui AT inria.fr>]

Hello.

Thanks for the Coq developers for having found a way to solve my 
problems quickly.

This new release of Coq is a great job anyway!

I will release a new version of CoLoR for Coq 8.5 very quickly.

However, I would like to mention that the compilation time (not using 
Enrico's new compilation procedure) increased by 33% between Coq 8.4pl6 
and Coq 8.5 when using make -j20!... :-(

make -j20 with Coq 8.4pl6 gives:
real    6m9.043s
user    31m30.582s
sys    1m23.429s

make -j20 with Coq 8.5 gives:
real    8m12.333s
user    32m43.505s
sys    1m43.168s

Best regards,

Frédéric.

Le 22/01/2016 15:37, Maxime Dénès a écrit :
> Hello Frédéric,
>
> Thanks for the feedback!
>
> I'd like to seize the opportunity to recall a few things about the Coq 
> development process:
> - no Coq release is claimed or expected to be bug free
> - bugs reported *early* in the release cycle are *more likely* to be 
> fixed in the next release
> - we follow the bug tracker very closely, so there is in general no 
> need to repeat reports on Coq-club
>
> The beta phase of Coq 8.5 lasted close to a year, with a lot of bugs 
> fixed, so we hope that the final version will provide a good user 
> experience. However, we also hope to see Coq users quickly contribute 
> bug reports on 8.5, so that we can provide, as Hugo said, a patch 
> level release that will make the user experience even better!
>
> Best,
>
> Maxime.
>
>
> On 01/22/16 12:17, Hugo Herbelin wrote:
> > Dear Frédéric,
> >
> > I"m very sorry for this bad experience you encountered. I understand
> > your frustration to see 8.5 released just one day after you submitting
> > two bugs which are blocking for you, but the release process of 8.5
> > final was already started when you submitted your bugs.
> >
> > About your bug #4506, note that it is not specific to 8.5. It is
> > reproducible in former versions, including e.g. 8.5rc1, and even
> > already 8.0. It can be circumvented by using "Unset Elimination
> > Schemes.", but congratulation for having found it.
> >
> > About your bug #4605, it would require more inspection. I'm travelling
> > today while other developers are at POPL and other teaching at a
> > winter school, all having given a lot for this release, but be sure
> > that we will take care of your bug by the next patch level release.
> >
> > Best regards,
> >
> > Hugo
> >
> >
> > On Fri, Jan 22, 2016 at 07:09:47AM +0100, Frédéric Blanqui wrote:
> > > Hello. Unfortunately, with the development version of CoLoR for 8.5
> > > (http://rewriting.gforge.inria.fr/divers/color8.5rc1.tar.gz), I get
> > > two bugs:
> > >
> > > 07:00 ~/src/color-svn-8.5 make -j20 -k
> > > make -r -f Makefile.coq
> > > make[1]: entrant dans le répertoire « 
> > > /local/blanqui/src/color-svn-8.5 »
> > > "coqc"  -q  -R "." CoLoR   Util/FMap/FMapUtil
> > > "coqc"  -q  -R "." CoLoR   Util/Relation/Tarski
> > > File "./Util/Relation/Tarski.v", line 99, characters 4-92:
> > > Anomaly: File "pretyping/indrec.ml", line 169, characters 14-20:
> > > Assertion failed.
> > > Please report.
> > > make[1]: *** [Util/Relation/Tarski.vo] Erreur 129
> > > File "./Util/FMap/FMapUtil.v", line 808, characters 0-9:
> > > Anomaly: Uncaught exception Not_found. Please report.
> > > make[1]: *** [Util/FMap/FMapUtil.vo] Erreur 129
> > > make[1]: La cible « all » n'a pas pu être refabriquée à cause 
> > > d'erreurs.
> > > make[1]: quittant le répertoire « /local/blanqui/src/color-svn-8.5 »
> > > make: *** [default] Erreur 2
> > >
> > > I filled the corresponding bug reports:
> > > https://coq.inria.fr/bugs/show_bug.cgi?id=4506
> > > https://coq.inria.fr/bugs/show_bug.cgi?id=4505
> > >
> > > Le 22/01/2016 01:22, Maxime Dénès a écrit :
> > > > Dear Coq-Clubers,
> > > >
> > > >   The Coq development team is pleased to announce the final release
> > > > of Coq 8.5 available at:
> > > >
> > > >   http://coq.inria.fr/coq-85
> > > >
> > > >   This release includes many bug fixes with respect to the previous
> > > > versions, and a few incompatible changes, see the following file for
> > > > more information:
> > > >
> > > >   https://coq.inria.fr/distrib/V8.5/CHANGES
> > > >
> > > > Source, Windows and OS X packages are available.
> > > >
> > > > We recall the new available features of version 8.5:
> > > >
> > > > - asynchronous edition of documents under CoqIDE to keep working on a
> > > >   proof while Coq checks the other proofs in the background (by Enrico
> > > >   Tassi);
> > > > - universe polymorphism making it possible to reuse the same
> > > >   definitions at various universe levels (by Matthieu Sozeau);
> > > > - primitive projections improving space and time efficiency of
> > > >   records, and adding eta-conversion for records (by Matthieu Sozeau);
> > > > - extensions of the new proof engine featuring dependent subgoals
> > > >   management, fully backtracking tactics, as well as tactics which can
> > > >   consider multiple goals together (by Arnaud Spiwack);
> > > > - a new reduction procedure called native_compute to evaluate terms
> > > >   using the OCaml native compiler, for proofs with large computational
> > > >   steps (by Maxime Dénès).
> > > >
> > > > The main other changes are:
> > > >
> > > > - a new fast compilation chain that skips checking of proofs 
> > > > (producing
> > > >   .vio files);
> > > > - a new construct ltac:(..) to call tactics from term definitions;
> > > > - a more restrictive guard condition to recover compatibility with 
> > > > axioms
> > > >   like propositional extensionality and (some consequences of)
> > > > univalence;
> > > > - a new option -type-in-type to collapse the universe hierarchy (makes
> > > >   the logic inconsistent but useful for exploration);
> > > > - a better-behaved alternative to simpl, called cbn;
> > > > - various improvements to the tactic language, like a new introduction
> > > >   pattern [= x1 ... xn] which applies injection on the fly (inspired
> > > >   by SSReflect); new constructs uconstr:c and type_term c to build
> > > >   untyped terms in Ltac;
> > > > - significant improvements of general efficiency.
> > > >
> > > > Seehttp://coq.inria.fr/  for more details, and the CHANGES file in the
> > > > distribution for a comprehensive list.
> > > >
> > > > The Coq development team wishes to acknowledge the many
> > > > people who made Coq 8.5 possible: Pierre Boutillier,
> > > > Pierre Courtieu, Maxime Dénès, Hugo Herbelin, Pierre Letouzey,
> > > > Pierre-Marie Pédrot, Yann Régis-Gianas, Matthieu Sozeau, Arnaud
> > > > Spiwack, Enrico Tassi with contributions also from Bruno Barras, Yves
> > > > Bertot, Frédéric Besson, Xavier Clerc, Pierre Corbineau,
> > > > Jean-Christophe Filliâtre, Julien Forest, Sébastien Hinderer, Assia
> > > > Mahboubi, Guillaume Melquiond, Jean-Marc Notin, François Ripault,
> > > > Carst Tankink as well as many external contributors.
> > > >
> > > > The Coq Development Team