Flushing stdout in elab commands

Stream: lean4

[Anne Baanen]

I'm trying to write an elab command that does some heavy computation (about 20 minutes' worth, currently). Especially for debugging, it would be nice if I could use println! to see intermediate results before the whole computation is finished. But as far as I can tell, all the output is only flushed when the command is done. Minimized example:

import Lean.Elab.Command

open Lean

def flushTest : IO Unit := do
  println! "Unflushed hello!"
  IO.sleep 500
  println! "Flushed hello!"
  (← IO.getStdout).flush
  IO.sleep 500
  println! "Bye!"

elab "#flushTest" : command =>
  Elab.Command.liftCoreM flushTest

#flushTest

def main := flushTest

I would expect that the three println!s would appear with 500 ms delay between each, or at least the "Flushed hello!" would appear before the "Bye!". But both in my editor (nvim) and building on the command line (with lean flushTest.lean) all three lines appear together, after a second of waiting. On the other hand, when I execute the code (using lean --run flushTest.lean) the three lines do appear separately with about 500ms delay between each as I would expect.

Would it be possible to flush stdout in elab commands?

[Damiano Testa]

I think that this came up other times and the answer was that this was not really possible.

I would be very happy to have partial information available, though, so I hope that I am wrong about this!

[Joachim Breitner]

Try passing -D stderrAsMessages=true to lean

[Anne Baanen]

That doesn't seem to change anything :( (Also if I replace (← IO.getStdout).flush with (← IO.getStderr).flush...)

[Daniel Weber]

What if you use IO.eprintln?