Do not write json to stdout

[eric-wieser]

Otherwise it can't be used with projects that emit diagnostics

[eric-wieser]

This worked fine in my own repository - any idea why it wouldn't be working fine here?

[gebner]

This worked fine in my own repository - any idea why it wouldn't be working fine here?

Unfortunately, we cannot use this for mathlib since string.to_char_buffer is excruciatingly slow. The easiest fix would be to add an io function to lean that can write a string (instead of a char_buffer).

[eric-wieser]

So writing to stdout using a different mechanism to writing to a file handle? Edit: Ah, I get it now.

[gebner]

Unfortunately, put_str also converts to char_buffer under the hood.

[eric-wieser]

Would chunking the conversion help here?

[eric-wieser]

I worked around this downstream by just calling tail -n 1 export.json, which does the job of separating lean diagnostics from json output. It's ugly, but far easier that digging around in the lean IO internals