The Coq mailing list

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

On 03/11/2013 09:51 PM, Pierre-Marie Pédrot wrote:
> I've quickly hacked a proof of concept using Unix.fork and darkest 
> magic to bypass this type of problem. The tactic sends back the proof 
> term through a pipe using OCaml Marshal module. This is ugly and 
> really unsafe, but this should work.
>
> Currently, the tactic only displays the list of proof-term as a 
> proof-of-concept (no pun intended), so you're still having the problem 
> of solving the goals. Nevertheless one should be able to instantiate a 
> goal with this list, but I still don't know how to instantiate all 
> evars representing a goal at once (any avice, Arnaud?).

Nifty!  I'd love to see an evolution of this so that I can use it my 
scenario.  I imagine it would be worth throttling the rate at which 
processes are forked, based on how many cores are available.