Error reporting in RTac

[jldodds]

@andrew-appel and I were discussing the possibility of returning errors in RTac because it is important to us that when symbolic execution fails we are able to tell the user why.

A possible solution to this is to parameterize RTac over an error type and include something of that type in the failure. I'm not sure what the best way to propagate this information through tactics is though.

[gmalecha]

Do you just need an error message (add one to Fail) or do you need some sort of logging trace?

[jldodds]

I think just an error message (although it should be able to carry things like entailments/programs) would be good, but it would probably be good to have more discussion before anything gets implemented

[gmalecha]

Adding a value to Fail would be pretty simple (if it is parametric, you could put whatever you want there). I guess technically RTac could be parameterized by an arbitrary monad that has a zero, that would allow for a logging implementation or a non-logging implementation, it would probably be a bit more complicated though.

[jesper-bengtson]

I think that adding an error message to Fail would be the way to go. it should be simple enough to do as it has no semantic meaning and just tags along for the ride.

/Jesper

On 13 Nov 2014, at 11:22, Gregory Malecha <notifications@github.commailto:notifications@github.com> wrote:

Adding a value to Fail would be pretty simple (if it is parametric, you could put whatever you want there). I guess technically RTac could be parameterized by an arbitrary monad that has a zero, that would allow for a logging implementation or a non-logging implementation, it would probably be a bit more complicated though.

—
Reply to this email directly or view it on GitHubhttps://github.com//issues/50#issuecomment-62919571.