coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: James R Wilcox <jrw12 AT cs.washington.edu>
To: Gabriel Scherer <gabriel.scherer AT gmail.com>, Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Pretty conversion of Coq to HTML?
Date: Wed, 16 Aug 2017 18:14:19 +0000
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jrw12 AT cs.washington.edu; spf=None smtp.mailfrom=jrw12 AT cs.washington.edu; spf=None smtp.helo=postmaster AT mail-pg0-f50.google.com
Ironport-phdr: 9a23:qeZgLhNaLXGJ9z1kVhUl6mtUPXoX/o7sNwtQ0KIMzox0KP/yrarrMEGX3/hxlliBBdydsK0UzbeO+4nbGkU+or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6aijSI4DUTAhTyMxZubqSwQ9aKzpf/6+fn1JTZeQRFgHKGarN/Nhis5VHev8MMgIZmbL06yhbTr2FgdOFfxGcuLlWWyVK0zcCptLVn7i4Y7/km7otLVbjwV6U+V71RSjo8ZTMb/sru4DvKSAaUrkFUbWQSmR1YS1zH9g6jBL/6qW3lv/F92S+VIcrwC704RGLxvO9QVBb0hXJfZHYC+2bNh5k11foDrQ==

James, what tool did you use for you indeed awesome dep-destruct
webpage? The fact that the same goals-on-hover rendering does not
exist for your other posts (
https://homes.cs.washington.edu/~jrw12/SharedMem.html for example )
unfortunately suggests that there may be a fair amount of manual
effort involved.

There is indeed quite a bit of manual effort involved. I use this python script to process a coq file with special commands in comments. To get hover over, contexts must be manually inserted into commands in the coq file. I sometimes use an emacs macro to semi-automate this process, but it still requires keystrokes linear in the number of proof steps.

I wish such trickery were not required, and would be happy to hear of better approaches.

James

Re: [Coq-Club] Pretty conversion of Coq to HTML?, James R Wilcox, 08/16/2017
- Re: [Coq-Club] Pretty conversion of Coq to HTML?, Paul A. Steckler, 08/21/2017