Skip to content

Enable test suite to check printed output

Ralf Jung requested to merge ci/reftests into gen_proofmode

Also move test suite out of theories/ so it does not get installed.

I added Show. in a few random place in the test suite just to have some things that we check not to regress. I also added it to the invariant open tests, because these validate that the from_option is gone.

@robbertkrebbers if you still remember some of the issues where proofmode simplified too much or not enough, now we could add proper tests for them. :D

Possible issues with this:

  • I didn't bother to wire up coqdep with these test files, so if anything in Iris changes, all tests are re-run. That takes <15sec, though.
  • tests cannot import other tests any more. However, we didn't make any use of that anyway.

Merge request reports