Save proofs even when successful #2197
Conversation
ttuegel
force-pushed
the
feature--save-proofs-success
branch
from
15b9cd6 to
249d6b9
Compare
|
This should just about be ready. I only need to add some documentation for types I added. |
ttuegel
force-pushed
the
feature--save-proofs-success
branch
2 times, most recently
from
9eb3fc6 to
1d1e8dd
Compare
ttuegel
force-pushed
the
feature--save-proofs-success
branch
from
1d1e8dd to
bc5b93f
Compare
Return the entire stuck claims, instead of the left-hand sides only.
ttuegel
force-pushed
the
feature--save-proofs-success
branch
from
bc5b93f to
7af018d
Compare
ana-pantilie
left a comment
ana-pantilie
left a comment
There was a problem hiding this comment.
I added some questions.
In addition, I saw that you cleaned up the tests in kore/test/Test/Kore/Reachability/Prove.hs, but some of them kept the previous structure (I added a comment on one instance of this). Is there any reason for this, or could we (the reviewers) try to clean up those tests as well, as part of the reviewer refactoring?
kore/src/Kore/Reachability/Prove.hs
Outdated
| -- | The result of proving some claims. | ||
| data ProveClaimsResult = | ||
| ProveClaimsResult | ||
| { stuckClaim :: !StuckClaims |
There was a problem hiding this comment.
Could we rename this field to something more suggestive? In Main, we check if stuckClaim is \\top and it took me a while to realize what this meant (I had to look at the types in this module). I think stuckClaims would be a little clearer, it at least implies this is a collection. stuckClaimsConjunction is even better I think, because it's clear what \\top means, but it's kind of long. Maybe a middle ground solution would be stuckClaims, with the check in Main (line 703) renamed to noStuckClaims (or something similar) in a where clause.
Another question, in what situation can we have more than one stuck claim? I thought we stop execution when we find the first one.
There was a problem hiding this comment.
Maybe a middle ground solution would be
stuckClaims, with the check in Main (line 703) renamed tonoStuckClaims(or something similar) in a where clause.
That sounds good to me!
Another question, in what situation can we have more than one stuck claim? I thought we stop execution when we find the first one.
When we exceed the breadth limit, we will present all the branches for the user to help with debugging.
| in | ||
| [ mkTest "OnePath" simpleOnePathClaim | ||
| , mkTest "AllPath" simpleAllPathClaim | ||
| ] |
There was a problem hiding this comment.
Any reason why we don't want the mixed cases anymore?
There was a problem hiding this comment.
The only thing that these mixed cases actually tested is that the backend doesn't try to use one-path claims to prove all-path claims, or vice versa. There are already tests specifically for that, and I didn't think it made sense to duplicate that check too many times.
| assertEqual "" | ||
| (Right ()) | ||
| actual | ||
| assertEqual "" MultiAnd.top actual |
There was a problem hiding this comment.
Could these tests be combined like the tests above were?
There was a problem hiding this comment.
Yes, I cleaned up the test suite some more.
3 participants
Fixes #2183
Reviewer checklist
stack test --coveragestack haddock