search

vprover / vampire

The Vampire Theorem Prover
https://vprover.github.io/
Other
282 stars 49 forks source link

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

Open MichaelRawson opened 4 months ago

MichaelRawson commented 4 months ago

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 2 months ago

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.