keep going

Stream: general

[Floris van Doorn]

Back in ye olden days of Lean 2, there was an option to build Lean with the option -k N or --keep-going N. This would build Lean, and if there were N different files that raised at least one error, then the build would stop.

I think a feature like this would be really useful for the Github Actions. Currently my workflow is

• Push a probably-broken commit to mathlib
• Wait for Github actions to raise an error
• Run leanproject get-cache and fix all errors in the file where the error was raised.
• Go to step 1.

This workflow would speed-up quite a bit if Github actions showed the next 5-10 files with at least one error. The compilation after errors often still runs fine: usually it's a broken proof, and that raises 0 future errors (it might raise warnings of the form imported a file containing 'sorry'). If a definition/instance breaks, there will probably be many unrelated errors.

Would it be possible / desirable to do this?

[Reid Barton]

Maybe a more targeted version of this would be to only stop the build on an error in the main task?

[Floris van Doorn]

Here is a commit that mentions the original --keep-going: https://github.com/leanprover-community/lean/commit/cfa9cd116cdb02668135fbb890e9d8d1ad962137

[Floris van Doorn]

What do you mean by the main task?

[Reid Barton]

The one that processes definitions, statements (but not proofs) of lemmas, other user commands

[Reid Barton]

Another idea would be to try to not build a module that imports another module that had an error outside a proof

[Reid Barton]

but continue to build the other parts of the import graph

[Reid Barton]

linja!

[Floris van Doorn]

Oh yeah, something like that would be nice too

[Reid Barton]

here's make's --keep-going flag:

       -k, --keep-going
            Continue as much as possible after an error.  While the target that failed, and those that depend on it, cannot  be  re‐
            made, the other dependencies of these targets can be processed all the same.