Do not abort build on warnings

[gebner]

For mathlib, we want the following two things simultaneously:

1. warnings should fail CI, but
2. the build should continue even after a warning.

The only way to make (1) work at the moment is to set warningAsError=true, but that stops the build immediately. This situation is particularly annoying in interactive mode, where you can't work on a file if any of its imports produces a warning. Note that we want the build to continue in CI as well, both to see if there are any actual errors as well as to provide cached oleans.

(In Lean 3, this happened to work nicely because all of the linters were run after the build, in a separate step.)

Several people (including me) would like this feature: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/attr.20.3A.3D.20simp/near/323332282

[gebner]

One proposal: we add a new flag --messages-file=Foo.messages.json. With this flag, Lean outputs all messages into the specified file instead of printing to stderr. Lake can then decide to show the messages, and offer options on whether to abort on warnings or not. Lake could also print the warnings for files that have already been built (like cargo does iirc).

We could then add a separate build step in mathlib that checks if there are any warning messages in the persisted json files.

[Kha]

The general plan sounds good, but why not a basic --json flag? Are you concerned about unstructured output we have to stdout?

[gebner]

Yes, that's my concern. Besides, we need to persist the file anyhow so we might as well do that in Lean.

[tydeu]

@gebner

One proposal: we add a new flag --messages-file=Foo.messages.json. With this flag, Lean outputs all messages into the specified file instead of printing to stderr. Lake can then decide to show the messages, and offer options on whether to abort on warnings or not. Lake could also print the warnings for files that have already been built (like cargo does iirc).

I very much like this idea! 😄 I imagine the implementation would be in two parts: First, add this feature to Lean. Second, once it is released, update Lake to make use of it. Is that right?

[kbuzzard]

A very common experience in a large mathematics project is that the development can be at least partially "top-down". That is, you have a file with the big theorem in, and perhaps even a proof using lemmas imported from other files, but several of the import files will have sorrys in. Right now this workflow does not even seem to be possible in Lean 4; you cannot even work on a file which imports a file with a sorry. Is this issue about this phenomenon? (if not then please let me know and I'll open a new issue).

Using warningAsError=true seems to invalidate the mathlib cache files so this is not an option. Right now the only workaround I know is to use a local my_sorry axiom in every file, which is a bit hacky. In Lean 3 importing files with sorrys worked just fine.