lean4
lean4 copied to clipboard
refactor: lake: import errors, job captions, log grouping
This improves job captions, the grouping of logs underneath them, and the handling of import errors. It also adds a number of log-related utilities to help achieve this.
Key Changes:
-
Job captions for facets now include the name of the object (e.g., module, library, facet). A caption has also been added to the top-level build of imports (e.g., for the server and
lake lean
). -
Stray I/O and errors outside the build job in a build function captioned with
withRegisterJob
(e.g., user-defined targets) will now be properly grouped under that caption instead of ending up under "Computing build jobs". Stray I/O will be converted to a single informational log entry. -
Builds no longer fail immediately on erroneous imports. Lake will now attempt to recover as best as possible from any import errors. Information on the import error will appear both in the build of the erroneous import and in the files which transitive import it. For example, uf
Lib.B
imports a missing moduleLib.A
, then the build ofLib.A
will mention that the file does not exist, and the build ofLib.B
will mention the bad import ofLib.A
.
Closes #3351. Closes #3809.