How to clear terminal in Lean?

Stream: new members

[Srayan Jana]

Tried this but I dont think it works

partial def gameLoop : IO Unit := do

  -- Placeholder for the main game loop

  -- render game world

  let _ := IO.Process.run { cmd := "clear", args := #[] }

  for _ in [1:10] do

      println! "############################################"

  println! "Enter Input:"

  let stdin ← IO.getStdin

  let input ← stdin.getLine

  let inputString := input.dropRightWhile Char.isWhitespace

  gameLoop```

[Srayan Jana]

Like, i get the loop printing out stuff but it doesn't clear when I press enter. I think its probably calling the command but in another process

[Robin Arnez]

Try print "\x1b[H\x1b[2J\x1b[3J" (see https://en.wikipedia.org/wiki/ANSI_escape_code#Control_Sequence_Introducer_commands). That's what clear does itself.

[Jakub Nowak]

On my system clear prints \x1b[H\x1b[J.

[Robin Arnez]

Hmm I guess there's some variation. Either one should work

[Krishna Padmasola]

@Srayan Jana this worked for me, let me know if it works for you

  let stdout ← IO.getStdout
  stdout.write <| ByteArray.mk #[27, 91, 3, 74, 27, 91, 72, 27, 91, 2, 74 ] --"\033[3J\033[H\033[2J" from https://stackoverflow.com/a/64596601
  stdout.flush

[Srayan Jana]

yeah that seemed to do the trick. Thanks!