The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 20/05/2014 22:13, AUGER Cédric wrote:
> I wanted to know if a date is planned for Coq 8.5.

The current realistic estimation would be « when it's done ». At first
we thought we were to branch in February, so...

> And last, on the proof market, there seem to be an axiom free proof
> of False, I do not know how it works, but I am wondering if this is
> an exploit of the system or a true inconsistency, and if so, if the
> coq dev team is working on it.

Recently, a relatively important number of inconsistencies in Coq have
been discovered, mainly thanks to Maxime Dénès. The one on proof market
was a DeBruijn overflow in the kernel, dating back to the beginning of
ages, if I remember well. (But it was rather difficult to exploit, though.)

Yet, after the merge of the polyproj branch, the trunk needs quite a bit
of polishing. It is known to be inconsistent for stupid reasons, but
hopefully that should be solved soon.

PMP

Attachment: signature.asc
Description: OpenPGP digital signature