don't synchronise proofs if we don't print them
MichaelRawson opened this issue · 1 comments
MichaelRawson commented
Vampire uses some mechanism (currently semaphores, might be files in future - #540) to synchronise proof output. We don't need to bother with -p off
, but we don't special-case this yet.
MichaelRawson commented
Idea: each process writes proofs (if enabled) to its own temporary file. The parent selects an arbitrary process that returned 0 and reads its proof file. This would smooth out a lot of the synchronisation logic in #540.