The Coq mailing list

[Bas Spitters <spitters AT cs.ru.nl>]

On Thu, Mar 4, 2010 at 3:22 PM, Mathieu Boespflug 
<mboes AT tweag.net>
 wrote:
> By the end
> of the week we should have a significantly more user-friendly version
> for you to try.

Great!

>> I would be keen to try it on our real number computations:
>> Certified Exact Transcendental Real Number Computation in Coq (Russell 
>> O'Connor)
>> http://arxiv.org/abs/0805.2438
>> A computer verified, monadic, functional implementation of the
>> integral (Russell O'Connor, Bas Spitters)
>> http://arxiv.org/abs/0809.1552
>
> Great! We are always looking for new benchmarks.

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.

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

Best,

Bas