Incremental printing to infoview

Stream: lean4

[Adam Topaz]

Suppose I have a command of the form

elab "test" : command => do
  IO.println "test1"
  IO.sleep 5000
  IO.println "test2"

Is there some (simple) way to make the println command actually print incrementally to the infoview, so that test1 prints first, and 5 second later, test2 prints?

[Henrik Böving]

have you tried using trace instead?

[Henrik Böving]

although I am not sure that would work either

[Mac Malone]

You could use an asynchronous Task, but, unfortunately due to lean4#738, asynchronous printing is broken.

[Sebastian Ullrich]

Anything in this direction would require quite a bit of restructuring of the language server

[Adam Topaz]

Thanks all. I'll just work harder at making my code faster :)