coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: e AT x80.org (Emilio Jesús Gallego Arias)
To: Gabriel Scherer <gabriel.scherer AT gmail.com>
Cc: Coq Club <coq-club AT inria.fr>, jrw12 AT cs.washington.edu
Subject: Re: [Coq-Club] Pretty conversion of Coq to HTML?
Date: Sat, 15 Jul 2017 01:23:25 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=e AT x80.org; spf=Pass smtp.mailfrom=e AT x80.org; spf=Pass smtp.helo=postmaster AT x80.org
Ironport-phdr: 9a23:ERRMQh/FpsPAwP9uRHKM819IXTAuvvDOBiVQ1KB41+McTK2v8tzYMVDF4r011RmSDNqds6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2e2//5/ebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMNboRr4oRzut86ZrSAfpiCgZMT457HrXgdF0gK5CvR6tuwBzz4vSbYqINvRxY7ndcMsaS2RfQ8hRUCJBDI2+YIUMAeUOMvpXopLhp1cStxayGRWgCfntxzJOm3T43bc60+MkEQzewgMtBN0PvXfIoNnvM6cSS++1x7TMwTvMavNW2DP96InPchs8pf+DQ6lwadDKyUIyFg3KlFGQqYj7MDOa0eQGrnSW7/BhVe21kG4rrgd8qSWsyMc0koTFm4EYx1Pe+Sln3oo4JMe0RFN5bNK5Cpdcqi+XO5VuTs4hQmxkoic3x78ctZO/ZiQHy5oqyhjCYPKdaYeI+AjsVOOJLDd4mn1lfLW/ig698EWj1uHwTM600ExFriZdk9nMsG4C1wDL58SaSfZw/V2t1SiR2w3S8O1IPEI5mbfBJ5I8zLM8iIIfsUHZES/3nEX2grWWdkIh+uWw9evqebrnq5yAO4NujQH+KKsultSlAeskKggOQ3Sb+eOk2bL/+k35WaxGgeEykqnEq5/XPt8bp668Aw9NyIkv8Re/DzG80NQZh3YLNlxFeAjUx7Tubn7HKur5APP3uF+snS1m3biSMbTrGJTAKj7Ym7fsZ7tnw0FZwQs3i9tY4sQHJKsGJaf+cl+h7JrfFBBxcyGxwuLmD51f25iMQiqgC6udPazV+XaS5+s0YrrfLLQJsSrwfqB2r8XlimU0zBpEJfGk
Organization: X80 Heavy Industries

Gabriel Scherer
<gabriel.scherer AT gmail.com>
writes:

> 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).

I have mentioned this in the past, but actually doing a proviola-like
tool is fairly easy with the current Coq protocol; for example jsCoq
splits a document in spans and stores all the goals in an array, which
can be inserted again.

At some time we had a hack to allow the user to hover on a particular
sentence and see the goal without the need of running Coq; maybe we
should revive it.

E.

[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