lean4
lean4 copied to clipboard
leanprover
feat: `--continue-on-error` to produce .olean file even if elaboration fails
Implementation of the lean side of #3567. Passing --continue-on-error to lean will cause it to produce an .olean file even if the file had an error, but it will still return error code 1 so lake will still not continue after it.
@tydeu How do you think lake should handle this? The issue is that because lean returns a nonzero error code (and I think it would be misleading for it not to), lake will immediately stop the running thread (compileO calls proc which calls error) and all dependent targets will also fail (IIUC). Should proc take a continueOnError flag?
Mathlib CI status (docs):
- 💥 Mathlib branch lean-pr-testing-3568 build failed against this PR. (2024-03-02 14:51:39) View Log
@digama0
@tydeu How do you think lake should handle this? The issue is that because lean returns a nonzero error code.
One other issue to consider is how partial build should be factor into Lake's traces. That is, module should be rebuilt in the future, so Lake somehow needs to invalidate the trace such it that it will trigger a rebuild. Downstream dependencies also need to be rebuilt. I guess it is reasonable to believe the source file or an upstream dependency is expected to have changed after fixing any errors and that will cause everything to cascade properly? There are potential edge cases with dynamic elaboration that could break this assumption, but I guess it is fine to ignore them?
One other issue to consider is how partial build should be factor into Lake's traces. That is, module should be rebuilt in the future, so Lake somehow needs to invalidate the trace such it that it will trigger a rebuild.
I actually disagree with this to some extent: It should be fine for lake to cache the failure and assume that re-elaborating the file assuming up to date inputs should produce exactly the same failure. The only complication is that lake would need to buffer and replay the output instead of re-running the compiler. (This is also what cargo does when you re-run a failed build without any source changes.) If you don't do this, then the second run will produce no output and appear to succeed (possibly even returning error code success, which could confuse downstream tooling). But I think this is an issue that can be handled separately.
Changes that would make the build succeed should already be handled by the usual invalidation mechanisms - either the file or its dependencies should need to be changed, and then it will be rebuilt as normal.
The only complication is that lake would need to buffer and replay the output instead of re-running the compiler.
To some lesser degree this is already desirable for non-error diagnostics in successful builds
