The Coq mailing list

[Mathieu Boespflug <mboes AT tweag.net>]

> We have a list of benchmarks in:
> CoRN/examples
> most of them are just reductions of closed terms, no variables.
> For example:
> (* approximate e^pi - pi.  May take a minute *)
> Time Eval vm_compute in answer 20 (exp (compress CRpi) - CRpi)%CR.

Thanks for the pointer.

> > I'm not sure what kind of parralelism you are seeking. Do you mean
> > checking independent parts of a proof in parralel or would like for an
> > expensive conversion test to be run on multiple cores at once? We have
> > not thought about parralelism yet, but I don't think our approach
> > poses any particular problems in that regard. It's conceivable that
> > specific Coq-level axioms be mapped to OCaml primitives for multicore
> > computation, as is possible during extraction.
> 
> During integration we need to sample a real valued function on many points.
> This can be done in parallel.
> 
> Are you saying that the current Coq-extraction supports multicores by 
> default?

I don't know of any specific support in the extraction mechanism for
parallelism. What I was saying is that using the "Extract Constant"
command, you can associate arbitrary OCaml code to Coq-level
constants. Said feature allows you to introduce parralelism in the
extracted code without hand tweaking, as I understand you have done
for Haskell's par and pseq.

-- Mathieu