doc-gen
doc-gen copied to clipboard
Do not write json to stdout
Otherwise it can't be used with projects that emit diagnostics
This worked fine in my own repository - any idea why it wouldn't be working fine here?
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).
So writing to stdout using a different mechanism to writing to a file handle? Edit: Ah, I get it now.
Unfortunately, put_str
also converts to char_buffer
under the hood.
Would chunking the conversion help here?
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