Explain proof for tests that should fail

[silversquirl]

If I have a test, defined with egg::test_fn!, that should_panic, can I have egg print an explanation if it manages to find a proof?
I thought the egg/test-explanations feature would do this, but it doesn't seem to do anything. What is it for?

[mwillsey]

It does generate and check the proof, it just doesn't print it because some proofs are very large. You can use the @check syntax in test_fn to run some code after the runner is done. An example usage: https://github.com/egraphs-good/egg/blob/main/tests/math.rs#L213-L225

[silversquirl]

Makes sense. How would I access the parsed expressions in order to call explain_equivalence?

[mwillsey]

The input term will be available at runner.egraph.roots[0], but the goal terms are not available from that context. You'll have to just repeat them.

[silversquirl]

runner.egraph.id_to_expr(runner.roots[0]) to get the input term as a RecExpr worked great, thanks for the help!