The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

I wouldn't expect the situation to improve much with a purely functional 
tactical data structure.  [abstract] already does a good job of 
confining the chunks of work that I want to parallelize.  There is a 
very stylized kind of side effect to [abstract] that should be trivial 
to merge back into the main process.  In fact, the merge would be much 
harder without this side effect.  I want to merge in proof terms 
associated with proved theorems, not intermediate proof search states, 
which could be much harder.

On 03/09/2013 02:42 PM, Pierre-Marie Pédrot wrote:
> 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.