The Coq mailing list

[Nico <nlehmann AT dcc.uchile.cl>]

It would be awesome if you add an option to display an animation with fireworks and music of success every time you finish a proof :-)

On Thu, Jun 16, 2016 at 12:30 PM James Wilcox <wilcoxjay AT gmail.com> wrote:

Hi Gabriel,

I'm glad you think it looks nice. I can assure you the way it's produced is not nice at all :)

You can find the python script on github.

The input format is a Coq file with special comments. Content of the blog itself appears in comments starting with "(**". Coq code that should appear in the blog should be surrounded by "(*begin code*)" ... "(*end code*)". All other code and comments are left out of the blog post. This is enough to render the basic code and prose without the fancy hover over contexts. Note: these special comments must appear at the beginning of a line.

If you want the contexts as well, then you have to do quite a bit of manual work. At each line of proof, you copy-paste Coq's display of the goal into a special "(*context ... *)" comment. I usually do this by setting up an emacs macro to repeatedly step Proof General forward one, change buffer to the goal display, copy the goal, change buffer back to the file, paste the goal, and then step again, etc. I can try to share the macro if you are interested, but it's probably best if you just record it yourself using C-x (

There is a python script that understands all of these special comments and generates a (horribly ugly) markdown file that can be processed by pandoc to generate the final html. It also does very stupid syntax highlighting, using a technique that is somewhat analogous to parsing HTML with regular expressions :)

Here is the Coq file that generates the dep-destruct blog post (also the CSS). 

It's pretty embarrassing to show this dirty hack in public. Surely there is a better way! 

James

On Wed, Jun 15, 2016 at 7:45 PM, Clément Pit--Claudel <clement.pit AT gmail.com> wrote:

On 2016-06-15 21:41, Gabriel Scherer wrote:
> Tramp support is super-useful: one can connect to a beefy server from our laptop (or phone!) and it magically does the right thing.
>
> (Re. PG-movie, proviola, etc.: I would love to use these tools if
> they were easy to use and there was good documentation on how to. If
> anyone knows for example how to get a rendering as nice as
> http://homes.cs.washington.edu/~jrw12/dep-destruct.html for a
> Coq-using blog post, I'm all ears.)

Well, why not ask the author? (cc'ed) :) James is also a company-coq contributor, btw ^^

Clément.

> On Wed, Jun 15, 2016 at 5:26 PM, Clément Pit--Claudel <clement.pit AT gmail.com <mailto:clement.pit AT gmail.com>> wrote:
>
>     I think it would also be useful to know which less-common features of Proof General people use, so we can test them and make sure they work well for the final release (examples include Proof Tree, PG-movie (recording and replaying scripts), PG-PBRPM (proof by rules), ML4PG, Tramp support, PG-unicode-tokens, and possibly others that I forget about).
>
>     Cheers,
>     Clément.
>
>     On 2016-06-15 15:59, Paul A. Steckler wrote:
>     > I'm in the process of reworking Proof General to support async
>     > processing in coqtop.
>     >
>     > As part of that exercise, I'll be doing quite a bit of code
>     > reorganization. In particular, I'll be discarding support for the Coq
>     > REPL (as well as other REPLs). This may be a good time to consider
>     > adding other features, or at least accommodating their future
>     > implementation.
>     >
>     > One such feature might be the ability to run multiple coqtop's.
>     >
>     > Anything else that others can suggest?
>     >
>     > -- Paul
>     >
>
>