[feature request] Built-in command timeout support

[vadimkantorov]

Currently solutions like

• https://github.com/project-numina/kimina-lean-server/
• https://github.com/augustepoiroux/LeanInteract

have to kill the REPL processes whenever a verification command times out.

This leads to having to restart the REPL process which means re-importing mathlib (currently leading to ~100K I/O syscalls which can stall the server and can increase because of leanprover/lean4#8092).

Would it be possible to natively add timeout option to the JSON commands? I only found a mention that native set_option timeout is not supported by Lean: https://leanprover-community.github.io/archive/stream/113488-general/topic/deterministic.20timeout.html#244454654

If REPL supports natively timeout control, REPL processes would need to be killed and restarted much fewer times

[vadimkantorov]

Oh wow, there are already two PRs for this feature :)

• Implement soft timeout option #92
• Add batch processing to LeanRepl #93