Lurk debugger

[arthurpaulino]

Proposed by @porcuquine on Zulip

We can/should model on Common Lisp, and especially Slime (the emacs mode for interacting with CL). Meanwhile, we can try to approximate SBCL from CLI, in baby steps. I'd encourage you, if you haven't already, to at least get set up to the point that you can run an SBCL REPL to experiment.

Here's what I'm thinking as the MVP:

• When an error is encountered at the REPL, enter a break loop.
• This means that you get a prompt showing you that you are no longer at toplevel.
• You are presented with a menu of options (in SBCL these are numeric), including — minimally: continue and abort.
• Abort returns you to toplevel and is equivalent to what we have now.
• There should be 'other options' (eventually, or initially, discoverable via help when in debugger).
• Minimally, we should be able to see a backtrace (of some kind — needs design, but we have all the frames).
• It would be nice to be able to inspect the frames of the backtrace, including fully or partially expanding continuations.
• It would be nice to be able to step forward and backward through the execution up to the point of failure.
• Related to the above, it would be nice to be able to intentionally enter the debugger for this purpose, without any error.
• As a single 'other option' to begin with, it might be nice to be able to replace whatever value led to the error with one supplied by the user instead. This allows experimentation to fix problems and continue running code that may be broken. That can be useful for actual computation, although in a Lurk context probably won't lead to a proof. It's still useful for debugging in a Lurk context, though.

SBCL debugging example