The Coq mailing list

[Clément Pit--Claudel <clement.pit AT gmail.com>]

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

Attachment: signature.asc
Description: OpenPGP digital signature