search

LeventErkok / sbv

SMT Based Verification in Haskell. Express properties about Haskell programs and automatically prove them using SMT solvers.
https://github.com/LeventErkok/sbv
Other
239 stars 33 forks source link

ExtractIO #692

Closed LeventErkok closed 3 months ago

LeventErkok commented 3 months ago

Hi,

I ran the test-suite on your pull request. Alas, I got test failures. I traced it down to the change you made to ExtractIO. I had to revert it thusly:

https://github.com/LeventErkok/sbv/commit/3c04d86032556053c749e49d9ccb24df52e2d1ac

I don't exactly recall the details of ExtractIO, in fact it was contributed by someone else (either Joel Burger or Brian Schroeder; neither of which use SBV any longer I think). However, since I'm getting test failures I'm hesitant to incorporate this particular change. (I did merge other parts of your commit.)

You can replicate the failure with:

make test TGT=exceptionRemote1

It appears the change to ExtractIO you made changes the exception-processing order, which isn't terribly surprising but leads to confusing behavior.

I'll leave this here so you can investigate yourself to see perhaps you didn't need this change exactly? Having a clean test-suite is important and when an exception happens it's good to have the report more accurate. (If you run the above test you'll see the change in behavior; new error message is much more cryptic.)

LeventErkok commented 3 months ago

This was premature. Closing.