Commit 2025-10-13 06:34 91ddcb0f

fix(lint-style): parse linter options and load environment extensions correctly (#29513) Parse options and load linter set extension correctly. This fixes two issues:

• We never called the toOptions function that parses Lakefile options into a Lean.Options structure: the function we use instead is only meant for command-line options and doesn't handle the weak. prefix correctly.
• The way we load linter sets was incorrect: withImportModules stopped updating environment extensions since [lean4#6325](https://github.com/leanprover/lean4/pull/6325), and that is exactly what we use to store linter sets. At the time of writing, importModules might be a suitable replacement (but this is not very safe, and not documented to be stable). Instead, write a small elaborator returning the environment at the point of elaboration, and use that instead.