The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

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.
> >
> >See http://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
> >