coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Suggestions for Proof General?

From: e+coq-club AT x80.org (Emilio Jesús Gallego Arias)
To: Clément Pit--Claudel <clement.pit AT gmail.com>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Suggestions for Proof General?
Date: Fri, 17 Jun 2016 18:17:37 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=e+coq-club AT x80.org; spf=Neutral smtp.mailfrom=e+coq-club AT x80.org; spf=None smtp.helo=postmaster AT boipeva.ensmp.fr
Ironport-phdr: 9a23:lX/FnhLuFRcfNfzQYdmcpTZWNBhigK39O0sv0rFitYgUI/vxwZ3uMQTl6Ol3ixeRBMOAu6MC2rKd4vCocFdDyKjCmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TWM5DIfUi/yKRBybrysXNWC3oLmj6vjq9X6WEZhunmUWftKNhK4rAHc5IE9oLBJDeIP8CbPuWZCYO9MxGlldhq5lhf44dqsrtY4q3wD89pozcNLUL37cqIkVvQYSW1+ayFmrPHs4DLHzA6C4GdUamQK119jBwHY4Bz+FsP6tib/u+xhnjGbIeX5SLk1XXKp6KI9GzHyjyJSOn0y93iSgchthopL8ErnoAZwi875ZYCRNf02XK7G78hSamNFWsteUGRoGIK1dMpcXKI6Ie9Eotyl9BM1phykCFzpXbu3xw==
Organization: X80 Heavy Industries

Clément Pit--Claudel
<clement.pit AT gmail.com>
writes:

> On 2016-06-17 11:30, Emilio Jesús Gallego Arias wrote:
>> The only downside that is the whole proof will have to be run, but I'm
>> sure there could be a fast mode.
>
> I don't think that'll be an issue, right? The output can be cached at
> publication time.

Indeed it is easy enough to generate a .json with that info.

E.

Re: [Coq-Club] Suggestions for Proof General?, (continued)