The Coq mailing list

["Lucian M. Patcas" <lucian.patcas AT gmail.com>]

Hi all,

Any chance that 8.4pl4 will be available in MacPorts any time soon?

Thanks,
Lucian

On 20 May 2014 15:49, Maxime Dénès <mail AT maximedenes.fr> wrote:

Hi,

Let me just add that all closed proofs of False have been fixed in the recent 8.4pl4 release and the fixes were backported to older branches. So sleep soundly :)

As for the incompatibility with propositional extensionality and univalence, we have a fix that restricts the subterm relation used by the guard condition on pattern matching. It seems safe, but we are still trying to extend safely to allow more complex dependently typed programming idioms that used to be accepted. I plan to write all this down as soon as we sort out these last details, hopefully with at least an informal proof of soundness.

Maxime.

On 05/20/2014 02:11 PM, Pierre-Marie Pédrot wrote:

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