Weird IO Behavior Introduced in v4.12.0

Stream: lean4

[Kaiyu Yang]

Hi,

LeanDojo has been broken starting from Lean v4.12.0. After some debugging, I reduced the problem to the following minimal working example:

import Lean.Elab.Tactic

elab "echo" : tactic => do
  while true do
    println! "Hello!"
    (← IO.getStdout).flush
    let line := (← (← IO.getStdin).getLine).trim
    println! s!"`{line}`"
    if line == "bye" then
      break

example : 1 = 1 := by
  echo
  sorry

When running it with leanprover/lean4:v4.11.0, I got the expected behavior (screenshot below): It prints Helloand waits for the user input. It echos the user input until the user enters bye.
image.png

However, the program hangs starting from leanprover/lean4:v4.12.0:
image.png

I really appreciate any help! Thanks!

[Henrik Böving]

def main : IO Unit := do
  while true do
    IO.println "Hello!"
    (← IO.getStdout).flush
    let line := (← (← IO.getStdin).getLine).trim
    IO.println s!"`{line}`"
    if line == "bye" then
      break
  return ()

running this one with lean --run works so this is most likely related to the way that stdin and out are setup when you are in an elaboration context. @Sebastian Ullrich should have the details on this in his cache.

[Sebastian Ullrich]

I'm afraid this is not a robust approach, it will only be broken further by elaboration parallelism

[Sebastian Ullrich]

External interaction must drive elaboration like in the repl, not the other way around

[Kaiyu Yang]

@Sebastian Ullrich Thanks! Does that mean I/O in TacticM may lead to undefined behaviors (if so, we probably shouldn't have instances of MonadLift IO TacticM)? In general, I'm wondering why it is not advisable for elaboration to drive external interactions, and how this is impacted by elaboration parallelism.

[Henrik Böving]

No, the key issue here is that you are interacting with stdin, it would e.g. be perfectly fine to read a file that contains a proof generated by an external tool from an elaborator

[Kaiyu Yang]

In this context, how is reading from stdin different from a file?

[Henrik Böving]

Things that run in the elaboration context do not actually get to play with the true process stdin anymore.

[Sebastian Ullrich]

Stdin is shared mutable state while opening a file temporarily for reading is usually a very scoped operation (if you did read from the same file you're writing to in another declaration's elaboration that wouldn't be great either, no)

[Kaiyu Yang]

In my use case, it is guaranteed that only one declaration interacts with stdin during elaboration, so shared mutable state may not be a real problem. Is it possible to guard stdin with something like a mutex?