vprover/vampire

don't synchronise proofs if we don't print them

MichaelRawson opened this issue · 1 comments

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.

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.