search

leanprover / lean4

Lean 4 programming language and theorem prover
https://lean-lang.org
Apache License 2.0
4.66k stars 418 forks source link

Add a way to stop `lake build` on first failure #2763

Open Julian opened 2 years ago

Julian commented 2 years ago

Perhaps related to leanprover/lean4#2764, it also might be helpful if there was a -x / --fail-fast option for lake build which stopped immediately on the first error (or first file with error).

tydeu commented 2 years ago

Unfortunately, due to currently heavily parallel nature of Lake builds, this is not very feasible at the moment. There is currently no way, within Lake itself, to know what the failure is "first". And even if that was discoverable, there is also no way to cancel the other running build tasks in order to quit early. However, I will keep this feature request in mind should future refactors make this possible.

Julian commented 2 years ago

Thanks for considering it! For context, I'd see value personally even if this was strictly something that controls output, even if it didn't cancel builds at all (at least initially) -- when doing some refactor I can't cope with lots of output, I want to see just one thing to fix, and have it be quick to see, and then repeat that process as fast as possible. But yeah thanks for considering it regardless!

Kha commented 2 years ago

In parallel build systems, there are various degrees to which this problem is solved - Nix outright kills running tasks if one fails by default, while Make at least does not start any new tasks (perhaps because, unlike Nix, it has to worry about inconsistent build directory state resulting from the abort). If I'm not mistaken, the latter at least should be implementable simply with a global IO.Ref Bool that is checked whenever a build Task is run.If that's not already the case?

tydeu commented 2 years ago

A wrinkle in @Kha's solution is that Lake starts all tasks immediately linking them together (via Task.bind) based on dependencies. So there are no tasks are spawned regardless after the build has started. Conceivably, the task could check some global state after waiting for dependencies and before the start of the next build. However, since tasks are arbitrary functions, this would have to be a manual check within each written task.

Kha commented 2 years ago

Yes, that's what I meant by "whenever a build Task is run" (not "queued"). There could be a wrapper around the Task functions that automatically checks and propagates a CancelToken. Perhaps that should even be integrated into Task itself.