Multi-process compilationLib

[sorear]

PolyML seems to scale poorly beyond about 4 threads; even the currently parallel parts of compilationLib cannot keep the current 8 cores busy, much less higher counts. For large projects that want more parallelism, we would need to farm out work to processes, create additional theories, and load them in the original process when done. Starting new HOL processes and saving and loading theories has significant overhead (possibly less so if the source is turned into a heap), so the single-process threaded compilationLib would have to remain as an option.

[mn200]

Isabelle has much more experience with multi-core Poly/ML. Many of Makarius’ papers are likely relevant. But my recollection is that Isabelle also has trouble keeping things busy past 8 cores. Some of the Isabelle concurrency code is ported/available under HOL's src/portable/poly.