lean4 icon indicating copy to clipboard operation
lean4 copied to clipboard

refactor: lake: import errors, job captions, log grouping

Open tydeu opened this issue 3 months ago • 1 comments

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 module Lib.A, then the build of Lib.A will mention that the file does not exist, and the build of Lib.B will mention the bad import of Lib.A.

Closes #3351. Closes #3809.

tydeu avatar May 09 '24 02:05 tydeu