summaryrefslogtreecommitdiff
path: root/language
diff options
context:
space:
mode:
authorAlasdair2019-01-14 21:06:01 +0000
committerAlasdair2019-01-14 21:06:01 +0000
commitef61b884cecc2c8ab11d7db1c1c593005be865e6 (patch)
treec95eb1d920def478ad406999a581a51e3ad1b627 /language
parent154e822f482c63b067bfe62dbbbffc565c1cc6ba (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 'language')
0 files changed, 0 insertions, 0 deletions