coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Pretty conversion of Coq to HTML?

From: Gaetan Gilbert <gaetan.gilbert AT ens-lyon.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Pretty conversion of Coq to HTML?
Date: Wed, 12 Jul 2017 15:07:07 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=gaetan.gilbert AT ens-lyon.fr; spf=Neutral smtp.mailfrom=gaetan.gilbert AT ens-lyon.fr; spf=None smtp.helo=postmaster AT labbe.ens-lyon.fr
Ironport-phdr: 9a23:du4P2xL+aUCaEah1bNmcpTZWNBhigK39O0sv0rFitYgeKPXxwZ3uMQTl6Ol3ixeRBMOAuq0C07KempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9ZDeZwdFiCChbb9uMR67sRjfus4KjIV4N60/0AHJonxGe+RXwWNnO1eelAvi68mz4ZBu7T1et+ou+MBcX6r6eb84TaFDAzQ9L281/szrugLdQgaJ+3ART38ZkhtMAwjC8RH6QpL8uTb0u+ZhxCWXO9D9QLYpUjqg8qhrUgflhjoZOT438G/ZicJ+g6xUrx2juxNxzJXZYJ2WOfdkYq/RYd0XSGhHU81MVyJBGIS8b44XAuQAJ+lXsZX9qEEIrRCjBAesBefvxSRWiX/swa0xzuMsEQ7c0wM+A9IBqnLUoM/6NKcTVeC617fHzS/fb/5Nxzj97pPIfgklofCMWrJwd9DdyUc1Fw7ciFibtILrPzSQ1usXsmib6fJtWvi1i28oqgFxvCKjxsA2ionGno4Vy1bE9T94wIkvP9G4RlR7bcarEJtRqyGaN5Z2Tdg4T2FpvyY3zKANt52jfCUS1ZgqyALTZ+aFfoWK+B7vSeecLDViiH57Zr6zmQ6+/Em+xuHmS8W4zEhGojBYntTDtX0BzQHf58uJR/Z740yvwyyA1xrJ5eFBOU00lbTUK5omwrMokpocq1/METTol0nskqCWcF4k9vGs6+XnZbXmoIWQN4Fuig3mM6QunNKwAfggPwQTUGWX5f6w2b/h8EHjXblHj/87nrPHvJzEO8gXvqu5DBVU0oYn5Ra/FTCm0NEAkHkINl1KZg6HgJLvO13UL/D4DPO/jE+ynzdx2/DLJaPuApPWLnTalLfgfbF960hGxAo919BT/4hUBa0ZIPLvRk/xs8TVAQM+Mwyt2uroFNF91p4FVm+UGa+YMKbSsUeS6e41IumMYpUVuDfnJPQ/6f7ulyxxpVhIdq6wmJATdXqQH/J8Ikzfb2C/rM0GFDIltwciReqip1yGWzNJez7mUKsx+jg9To2nCY3OXJyFjbqamSOqGZsQaHoQWQPEKmvha4jRA6REUymVOMI0yjE=

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/

[Coq-Club] Pretty conversion of Coq to HTML?, François Pottier, 07/12/2017
- Re: [Coq-Club] Pretty conversion of Coq to HTML?, Abhishek Anand, 07/12/2017
- Re: [Coq-Club] Pretty conversion of Coq to HTML?, Gaetan Gilbert, 07/12/2017
  - Re: [Coq-Club] Pretty conversion of Coq to HTML?, Lélio Brun, 07/14/2017
    - Re: [Coq-Club] Pretty conversion of Coq to HTML?, Gabriel Scherer, 07/14/2017
      - Re: [Coq-Club] Pretty conversion of Coq to HTML?, Emilio Jesús Gallego Arias, 07/15/2017