This PR extends `lake lint --builtin-lint` to also support text linters
(i.e. those using `logLint`/`logLintIf`), in addition to the environment
linters added in #13431. Text-linter warnings emitted during the build
are persisted into each module's `.olean` via a new
`Lean.Linter.lintLogExt` environment extension; `lake lint` re-runs the
build for the target modules and reads the entries back, reporting them
alongside the environment linter output.
---------
Co-authored-by: Mac Malone <tydeu@hatpress.net>
Co-authored-by: Thomas R. Murrills <68410468+thorimur@users.noreply.github.com>
