Allowing `lake build` to continue despite errors

Stream: new members

[Louis Cabarion]

When compilation errors occur, what determines when lake build stops? From what I’ve seen, it neither stops at the very first error nor continues compiling for as long as possible.

Is there a way to configure lake build so that it doesn’t stop early: in other words, so that it attempts to compile as many files as possible?

[Yaël Dillies]

Is this not the default behavior?

[Arthur Paulino]

You probably need to specify the toolchain version you're using to receive better help.

[Junyan Xu]

I think after an error is encountered in one file it might be possible to continue to compile files depending on it (after all an error in a file doesn't stop compilation of the rest of the file), but maybe the current restriction is that errored file doesn't generated an olean (not sure), and you very quickly get errors in downstream decls due to defeq issues or argument mismatches (a def with errors might pick up less arguments than intended). But both of these only happen for defs as far as I understand, so it should be okay to continue to compile other decls and files after a proof errors out.

[Yaël Dillies]

Can you clarify whether you want the build of unrelated files to continue despite errors (which it already does), or the build of related files?

[Louis Cabarion]

After some testing, I found that the behavior I asked about is already the default: lake build continues compiling unrelated files even if some fail. I had mistakenly assumed it would stop after a certain number of errors, as some other compilers do. Apologies for the confusion!