Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] CoqdocJS: foldable proofs and better Unicode support for Coqdoc

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] CoqdocJS: foldable proofs and better Unicode support for Coqdoc


Chronological Thread 
  • From: Gabriel Scherer <gabriel.scherer AT gmail.com>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] CoqdocJS: foldable proofs and better Unicode support for Coqdoc
  • Date: Sun, 15 May 2016 08:38:48 -0400
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=gabriel.scherer AT gmail.com; spf=Pass smtp.mailfrom=gabriel.scherer AT gmail.com; spf=None smtp.helo=postmaster AT mail-io0-f171.google.com
  • Ironport-phdr: 9a23:GoUZSxH+yfArKmbWfvDCfp1GYnF86YWxBRYc798ds5kLTJ75oMuwAkXT6L1XgUPTWs2DsrQf27uQ6fyrAjJIyK3CmU5BWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYsExnyfTB4Ov7yUtaLyZ/nhqbop9aIPU1hv3mUX/BbFF2OtwLft80b08NJC50a7V/3mEZOYPlc3mhyJFiezF7W78a0+4N/oWwL46pyv+YJa6jxfrw5QLpEF3xmdjltvIy4/SXEGCCI/zM3Vngc2k5DBBGA5xXnVL/wtDH7v6xzwn/JE9fxSOUbUD647qpvACTjiCodOiRxpG7egNZxgaYduxmhqgZy2abbZYiUMLx1eaaLLoBSfnZIQssED38JOYi7dYZaSrNZZes=

This is very nice, thanks!

Do you think that it would eventually make sense to integrate this
into upstream coqdoc?
In my experience, people do not necessarily take the time to inform
themselves about the various coqdoc-improvements option laying around;
they want to get a reasonable HTML rendering real quick, and are
likely to use exactly what is most easy to run from their existing
development -- which is likely to be the coqdoc-related target of
coq_makefile's output. To reach a large number of user, being enable
"by default" is thus fairly important.

On Fri, May 13, 2016 at 3:15 PM, Tobias Tebbi
<ttebbi AT ps.uni-saarland.de>
wrote:
> Hi,
>
> I wrote some Javascript to improve the output of Coqdoc by adding foldable
> proofs and extensible replacement of ASCII with Unicode such that copy-paste
> still produces ASCII.
> You can have a look at the result here:
> https://www.ps.uni-saarland.de/autosubst/doc/Ssr.POPLmark.html
>
> This is really easy to integrate into any Coq development, see here:
> https://www.ps.uni-saarland.de/~ttebbi/coqdocjs/
>
> Best,
> Tobias



Archive powered by MHonArc 2.6.18.

Top of Page