json output from lake build

Stream: lean4

[Eric Wieser]

In mathlib3 CI, we use lean --make --json so that we can get structured error messages and propagate these to github. How can we achieve the same thing in lean4?

[Sebastian Ullrich]

I guess there is nothing like that in either Lake or Lean itself atm. An "interesting" alternative would be to install a custom linter that does the formatting (duplicating the message), but that would still require post-processing for the noisy files feature.