Zulip Chat Archive

Stream: general

Topic: keep going


view this post on Zulip Floris van Doorn (Aug 29 2020 at 22:34):

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?

view this post on Zulip Reid Barton (Aug 29 2020 at 22:35):

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

view this post on Zulip Floris van Doorn (Aug 29 2020 at 22:35):

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

view this post on Zulip Floris van Doorn (Aug 29 2020 at 22:36):

What do you mean by the main task?

view this post on Zulip Reid Barton (Aug 29 2020 at 22:37):

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

view this post on Zulip Reid Barton (Aug 29 2020 at 22:37):

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

view this post on Zulip Reid Barton (Aug 29 2020 at 22:37):

but continue to build the other parts of the import graph

view this post on Zulip Reid Barton (Aug 29 2020 at 22:38):

linja!

view this post on Zulip Floris van Doorn (Aug 29 2020 at 22:40):

Oh yeah, something like that would be nice too

view this post on Zulip Reid Barton (Aug 29 2020 at 22:41):

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.

Last updated: May 16 2021 at 05:21 UTC