benchpress icon indicating copy to clipboard operation
benchpress copied to clipboard

handle proof checking

Open c-cube opened this issue 2 years ago • 1 comments

-[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

c-cube avatar Nov 27 '21 04:11 c-cube

This is mostly done, although it'll need a lot of polish.

c-cube avatar Jan 05 '22 20:01 c-cube