A decade ago we extracted our implementation of the Riemann integral to haskell and used the par/seq operations in Coq to get an easy 3x speedup on a 4 core machine. http://arxiv.org/abs/0809.1552

I now have a similar use case and would like to run extracted code on a cluster. Any experience with this?

This https://ocamlverse.github.io/content/parallelism.html

suggests targeting either parmap or parallel-for, of course, we could also use par/seq in haskell as before.

I'm just curious whether others have tried this.

Last updated: Feb 01 2023 at 12:30 UTC