The Coq mailing list

[Gabriel Scherer <gabriel.scherer AT gmail.com>]

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

On Wed, Jun 15, 2016 at 5:26 PM, Clément Pit--Claudel <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
>