benchpress
benchpress copied to clipboard
handle proof checking
-[x] add (proof_produce " --some --additional --args $proof_file")
to prover stanza
- [x] add
(proof_checker "checker $problem --whatever $proof")
to prover stanza (or maybe a separate stanza with the(proof_checker <name>)
field in prover) - [x] add a way in task/cli to specify that proof production is on for some provers; also need to be able to run the prover with and without proof production
- [x] do the proof checking, with new possible results ("unsat but with bad proof", say)
- [ ] have a way to say "checked n subproofs, skipped m subproofs" (to say we have (n/n+m % steps proved)
- [ ] provide views on checked/unchecked proofs in the UI
This is mostly done, although it'll need a lot of polish.