The SAW REPL is not in a useful state after a failure while loading a file

[nano-o]

In the SAW REPL, let's say I run include "mydir/file.saw" and a proof in the middle of file.saw fails. At that point I get back a prompt in the REPL. However, none of the definitions appearing in file.saw before the line that fails seem available. So, to debug file.saw interactively, I have to comment-out all the lines after and including the failing line, restart the REPL, and include the file again. This can take a lot of time. What would be great is if, upon failure, one would be left with a REPL in the state it was just before interpreting the failing line in file.saw.

Another issue is that the current directory of the REPL process is now changed to mydir.

[brianhuffman]

I've noticed this behavior too, where if there's an error in the middle of loading a file using include at the REPL, all the declarations get rolled back. The reason for this behavior is how the TopLevel monad is implemented: It uses StateT wrapped around IO (basically TopLevel a is TopLevelState -> IO (a, TopLevelState)). Exceptions and errors are implemented by throwing exceptions in IO. The problem is that when an error occurs in an inner monad, we never get the updated TopLevelState value, so the state changes are lost.

Would you rather change the default behavior so that any changes to the TopLevel state (including top-level saw-script declarations) are preserved up to the point where an error happens? If so, then we should probably reimplement the TopLevel monad so that we can preserve the state updates when errors occur. Probably the easiest way to do this would be to use something like IORef TopLevelState -> IO a instead of TopLevelState -> IO (a, TopLevelState).

[nano-o]

Would you rather change the default behavior so that any changes to the TopLevel state (including top-level saw-script declarations) are preserved up to the point where an error happens?

Yes, that's what I had in mind.