The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 09/03/2013 19:34, Adam Chlipala wrote:
> This doesn't sound too hard to implement from a scientific perspective,
> though I'm not sure of the engineering challenges. Is anyone working on
> functionality like this, or does anyone have tips on how it could be
> achieved in today's Coq?

I'm unsure about how this may help, but Arnaud Spiwack's new-tacticals 
branch uses an almost purely functional data-structure (except for the 
lower-level IO primitives, which are currently not really used for proof 
construction) to encode the tactic monad. So you may try to write a 
tactic transformer using Unix.fork and message-passing to recover what 
you're hoping for.

Unluckily, there are two problems:

1. Minor one: the [abstract] combinator does do side-effects, by 
defining lemmas. So you need something more fine-grained.

2. Major one: Ltac sequence operator ";" and goal dispatch is 
essentially state-transforming, so most of the time, this won't work. In 
the [abstract] case it should be fine though, because you have no evars.

PMP