The Coq mailing list

[Gabriel Scherer <gabriel.scherer AT gmail.com>]

It is a shame that proviola is unmaintained, because I think such a
tool remains very useful for the Coq community. (It serves a different
purpose than jsCoq that is more interactive but heavier on the user).

James, what tool did you use for you indeed awesome dep-destruct
webpage? The fact that the same goals-on-hover rendering does not
exist for your other posts (
https://homes.cs.washington.edu/~jrw12/SharedMem.html for example )
unfortunately suggests that there may be a fair amount of manual
effort involved.

Should proviola be revived? Can implementing some features Coq-side
(having a tracing mode that would dump the location-indexed goal
information?) to make such tools more robust and easier to maintain?

On Fri, Jul 14, 2017 at 6:28 AM, Lélio Brun 
<lelio.brun AT inria.fr>
 wrote:
> Hello,
>
> the nicest pretty-printing I've seen so far was here: 
> https://homes.cs.washington.edu/~jrw12/dep-destruct.html
> I don't think it uses proviola, which indeed seems to be unmaintained.
> Maybe you could ask directly the author of the post: 
> jrw12 AT cs.washington.edu
>
> Lélio Brun
>
> ----- Mail original -----
>> De: "Gaetan Gilbert" 
>> <gaetan.gilbert AT ens-lyon.fr>
>> À: 
>> coq-club AT inria.fr
>> Envoyé: Mercredi 12 Juillet 2017 15:07:07
>> Objet: Re: [Coq-Club] Pretty conversion of Coq to HTML?
>>
>> If you mean this
>> http://hott.github.io/HoTT/proviola-html/HoTT.Spaces.Nat.html it's
>> proviola https://arxiv.org/abs/1005.2672
>>
>> I think its site is dead though.
>>
>> Gaëtan Gilbert
>>
>> On 12/07/2017 15:02, François Pottier wrote:
>> >
>> > Hello,
>> >
>> > I believe I have seen somewhere (during an academic presentation,
>> > probably) a
>> > tool that converts Coq files to HTML files, with the feature that
>> > pointing the
>> > mouse cursor anywhere in the middle of a rendered proof script causes the
>> > current proof state (hypotheses and goal) to be displayed. I can't
>> > remember
>> > how it is called, and I can't find it, though. Any help would be welcome.
>> > Thanks,
>> >
>> > --
>> > François Pottier
>> > francois.pottier AT inria.fr
>> > http://gallium.inria.fr/~fpottier/
>>
>>