minirust icon indicating copy to clipboard operation
minirust copied to clipboard

Re-do the way we handle stderr/stdout

Open RalfJung opened this issue 6 months ago • 0 comments

MiniRust programs need to be able to write to stdout/stderr. However, it is a bit unclear what the interpreter should do when the intrinsic is executed. In Coq, this should likely translate to an itree event representing output. But to run the interpreter for the test suite, the event needs to be handled, e.g. by printing this to a terminal or by capturing the output in a buffer so that it can be compared for test purposes.

Currently, we do the rather hacky thing of storing the handler(s) inside the machine state. That's not right, this shouldn't be machine state, the handler lives outside the machine. So probably we should instead add a specr::event method (or a specr::event module with one method for each event type, to ensure the input and output types match). But what should that method do in Rust? Somehow it needs to know the intended handler for the event. Passing the handler through the interpreter is unwieldy, so the next-best option is to use thread-local state. We already rely on TLS for the GC anyway...

After this change, Machine can also finally be a normal value again, and we can stop using shared references and the "no-obj" hack.

Cc @JojoDeveloping since we just talked about that

RalfJung avatar Aug 21 '24 11:08 RalfJung