Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Open
MichaelRawson opened this issue May 3, 2024 · 1 comment
Open

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

MichaelRawson opened this issue May 3, 2024 · 1 comment
Assignees

Comments

@MichaelRawson
Copy link
Contributor

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
Copy link
Contributor Author

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

1 participant