Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Coq 8.4pl1

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Coq 8.4pl1


Chronological Thread 
  • From: Pierre Letouzey <pierre.letouzey AT inria.fr>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: [Coq-Club] Coq 8.4pl1
  • Date: Tue, 25 Dec 2012 17:49:40 +0100 (CET)


Joyeux noel everyone

As some of you may already have noticed, the first bugfix release
of Coq 8.4 is now available in the usual "crémerie". A precompiled
package for Windows is also already there, and the MacOSX package
should follow soon. See below for the list of fixed bugs and
other changes. Of course, the bug tracker is still far from fully
emptied, sorry if you've encountered an issue that remains unsolved,
please stay tuned.

By the way, I'd like to advertise a neat trick proposed by Pierre-Marie
Pédrot: tweaking the OCaml GC parameters might bring interesting
speed-up of Coq, at the cost of higher memory footprint. We're still
investigating the precise effects of these GC parameters, more
experiments are underway, so these tweaks have been considered
too preliminary for inclusion in the official 8.4 branch. Nonetheless,
it's easy to try them if you want, just set a OCAMLRUNPARAM variable
before launching coqtop, for instance:

export OCAMLRUNPARAM='s=32M,o=120'

Happy Coq hacking!
Pierre Letouzey, for the Coq Dev Team


Changes from V8.4 to V8.4pl1
============================

Bug fixes

- Solved bugs :
#2851 #2863 #2865 #2893 #2895 #2892 #2905 #2906 #2907 #2917 #2921
#2930 #2941 #2878
- Partially fixed bug : #2904
- Various fixes concerning coq_makefile

Optimizations

- "Union by rank" optimization for universes contributed by J.H. Jourdan
and G. Sherrer (see union-find-and-coq-universes on gagallium blog).

Libraries

- Internal organisation of some modular libraries have slightly changed
due to bug #2904 (GenericMinMax, OrdersTac)
- No more constant "int" in ZArith/Int.v to avoid name clash with OCaml
(cf bug #2878).

Coqide

- Improved shutdown of coqtop processes spawned by coqide
(in particular added a missing close_on_exec primitive before forking).
- On windows, launching coqide with the -debug option now produces
a log file in the user's temporary directory. The location of this
log file is displayed in the "About" message.


  • [Coq-Club] Coq 8.4pl1, Pierre Letouzey, 12/25/2012

Archive powered by MHonArc 2.6.18.

Top of Page