coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Suggestions for Proof General?

From: e+coq-club AT x80.org (Emilio Jesús Gallego Arias)
To: Gabriel Scherer <gabriel.scherer AT gmail.com>
Cc: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Suggestions for Proof General?
Date: Fri, 17 Jun 2016 16:12:29 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=e+coq-club AT x80.org; spf=Neutral smtp.mailfrom=e+coq-club AT x80.org; spf=None smtp.helo=postmaster AT boipeva.ensmp.fr
Ironport-phdr: 9a23:9h2k0xXaKd5mukGzXlu05zgb7e7V8LGtZVwlr6E/grcLSJyIuqrYZh2Bt8tkgFKBZ4jH8fUM07OQ6PCxHz1YqsnZ+Fk5M7VyFDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3CwN5K6zPF5LIiIzvjqbpq8yVMl0D22L1SIgxBSv1hD2ZjtMRj4pmJ/R54TryiVwMRd5rw3h1L0mYhRf265T41pdi9yNNp6BprJYYAu3SNp41Rr1ADTkgL3t9pIiy7UGCHkOz4S4zW28MkxdMSzPO7BzgU4255iTzvPB81S3cJsb2QKo5Qxyt6q5qTFnjjyJRZBAj92SCh497i7seqxa8rTRvk9aSZ5uafLpTe6LZfNRSZ2dazN0ZeCVFBo6zaMMmFesIJqcL/MHGu1ISoE7mVkGXD+T1x2oN3yeu0A==
Organization: X80 Heavy Industries

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

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

Even if still not 100% production ready, I would recommend tyring jscoq
for that use case. A 5 minutes hack:

https://x80.org/rhino-coq/examples/dep_destruct.html

It is pretty easy to setup; however we need nicer css/html.
Also, support for Provila-like features is planned.

E.

Re: [Coq-Club] Suggestions for Proof General?, (continued)