diff options
| author | Alasdair | 2019-01-14 21:06:01 +0000 |
|---|---|---|
| committer | Alasdair | 2019-01-14 21:06:01 +0000 |
| commit | ef61b884cecc2c8ab11d7db1c1c593005be865e6 (patch) | |
| tree | c95eb1d920def478ad406999a581a51e3ad1b627 /doc | |
| parent | 154e822f482c63b067bfe62dbbbffc565c1cc6ba (diff) | |
Add a function to perform re-writes in parallel
rewrite_defs_base_parallel j is the same as rewrite_defs_base
except it performs the re-writes in j parallel processes. Currently
only the trivial_sizeof re-write is parallelised this way with a
default of 4. This works on my machine (TM) but may fail elsewhere.
Because 2019 OCaml concurrency support is lacking, we use Unix.fork
and Marshal.to_channel to send the info from the child processes
performing the re-write back to the parent.
Also fix a missing case in pretty_print_lem
Diffstat (limited to 'doc')
0 files changed, 0 insertions, 0 deletions
