Re:A deep dive into Multicore OCaml garbage collector
by tom_mellior on Sunday July 16, 2017 @03:09PM
(#14783623)
> things like running Quickcheck and Nitpick in a separate thread
In my experience with Isabelle, these tools provide feedback on the order of seconds (because they do expensive things). Maybe several hundreds of milliseconds, for simple cases. At these scales, it makes no noticeable difference what kind of parallelism solution you use. Spawning separate processes and sending messages would work just as well.
So the reason there is no parallel Quickcheck for Coq is more likely due to the fact that there is no Quickcheck for Coq, period.
In my experience with Isabelle, these tools provide feedback on the order of seconds (because they do expensive things). Maybe several hundreds of milliseconds, for simple cases. At these scales, it makes no noticeable difference what kind of parallelism solution you use. Spawning separate processes and sending messages would work just as well.
So the reason there is no parallel Quickcheck for Coq is more likely due to the fact that there is no Quickcheck for Coq, period.