coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover)

From: Clément Pit--Claudel <clement.pit AT gmail.com>
To: "Lucian M. Patcas" <lucian.patcas AT gmail.com>, coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover)
Date: Sat, 5 Mar 2016 18:26:47 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=clement.pit AT gmail.com; spf=SoftFail smtp.mailfrom=clement.pit AT gmail.com; spf=None smtp.helo=postmaster AT mout.kundenserver.de
Ironport-phdr: 9a23:6nwn4RZKPGaAH40snzKEiF//LSx+4OfEezUN459isYplN5qZpM68bnLW6fgltlLVR4KTs6sC0LqJ9f+wEjVcv96oizMrTt9lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUiv2OQc9HOnpAIma153xjLDtvcKDKFwU2nKUWvBbElaflU3prM4YgI9veO4a6yDihT92QdlQ3n5iPlmJnhzxtY+a9Z9n9DlM6bp6r5YTGY2zRakzTKRZATI6KCh1oZSz7ViQBTeIszE4T24XmxwAJk6N1BjmVZ7q+GOusvd22SCce9X/Ubs9Qhyt6q5qTFnjjyJRc3Yy93iSgchthuoPqxW44hd73oT8YYePNfM4cLmLLv0AQm8UdcLQUiFHHrSEbpdKSsEFNPtUoo2181AKoB6zAxXqHOLz4jBNj37ym6Y91rJyQkn9wAU8EodW4zzvp9LvOfJXCLjtwQ==

On 03/03/2016 11:59 PM, Lucian M. Patcas wrote:
> 3. Is it possible to generate prettified coqdoc documents?

Extending prettifications to the output of coqdoc would be nice. I don't know
much about CoqDoc, but I'd be happy to talk to someone who does. Here's an
example of what exporting a prettified Emacs buffer to Emacs looks like:

http://web.mit.edu/cpitcla/www/html-export/FMapAVL.v.html

One of the tricky aspects is prettifying HTML content without breaking
copy-paste; that is, it should be possible to copy Coq code from a prettified
page. The page above works fine with Firefox and Chrome; I don't know about
Safari and IE.

Clément.

Attachment: signature.asc
Description: OpenPGP digital signature

Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), (continued)