How to access raw terminal mode in Lean?

Stream: new members

[Srayan Jana]

I was working on an ASCII rogue like, but I got frustrated because I wanted to use raw terminal mode so I could read inputs without waiting for a newline. However, I couldn't figure out how to set it up. Any ideas?

[Srayan Jana]

Example of what I'm talking about (kinda) https://www.erlang.org/doc/apps/stdlib/terminal_interface.html

[Anthony Wang]

This works for me, on Linux:

def main : IO Unit := do
  -- Read input immediately without waiting for newline
  _ ← IO.Process.run {
    cmd := "stty"
    args := #["-F", "/dev/tty", "cbreak", "min", "1"],
  }
  -- Hide user input
  _ ← IO.Process.run {
    cmd := "stty"
    args := #["-F", "/dev/tty", "-echo"],
  }
  let stdin ← IO.getStdin
  while true do
    let a ← stdin.read 1
    match String.fromUTF8? a with
    | some str => IO.println s!"Hello {str}"
    | none => return

[Anthony Wang]

It's also possible to do this using ANSI escape sequences as suggested in #new members > How to clear terminal in Lean? but I think the method above is slightly more readable.

[Srayan Jana]

Would be nice to figure out how to do this on Windows, but this is a good start!

[Anthony Wang]

You could try running it in WSL 2, which should work without any changes to the code above.