Fork safety

[vadimkantorov]

Is REPL process / lean state - fork-safe?

E.g. is it possible to have a parent REPL process, do all imports there and then just fork this prepared process and then do verification inside the child processes?

Are there any bad global/non-threadlocal state in REPL/Lean?

Thanks!

[habemus-papadum]

Hi -- I agree this would be useful.

One question (probably needs to be asked on Zulip) is what are the threads in LeanRepl?
On startup I see two threads, and then as I issue commands more threads are created -- would be nice to sort out where they are being created.

ultimately, LeanRepl could learn a new command:

• fork input_pipe out_pipe -- forks itself and replaces stdin/stdout with user-provided named pipes.

I will try spelunking into the Lean4 code base to see how threads work in Lean and how they are coming into existance for MetaM tools