Tactics outputting to STDOUT

Stream: metaprogramming / tactics

[Shing Tak Lam]

I'm currently writing a Discord Bot for the Xena server, which can run code which the users send it. Right now, I'm trying to get tactics that output things to display their output to the users. By tweaking a few things, I managed to get library_search to output to STDOUT, but I'm getting stuck trying to get squeeze_simp to output to STDOUT. I've replaced all calls to trace with unsafe_perform_io $ io.print but so far when I use lean --make it doesn't output to STDOUT. Is there a better way to get Lean tactics to output to STDOUT?

[Gabriel Ebner]

I'd just use lean 2>&1

[Gabriel Ebner]

You could also check out lean --json if you want to parse the output.

[Shing Tak Lam]

Gabriel Ebner said:

I'd just use lean 2>&1

Thanks! That works for what I need.