eac9315962
This PR adds a `deprecated_module` command that marks the current module as deprecated. When another module imports a deprecated module, a warning is emitted during elaboration suggesting replacement imports. Example usage: ```lean deprecated_module "use NewModule instead" (since := "2026-03-30") ``` The warning message is optional but recommended. The `since` parameter is required. Warnings can be disabled, by setting `linter.deprecated.module` option to false in the command line. Because the check happens when importing , using `set_option linter.deprecated.module` in the source file won't affect the warnings. Instead, a whole file can be marked not to display depreciation warnings, by putting a comment `deprecated_module: ignore` next to `module` keyword. Similarly, individual keywords can be silenced. A `#show_deprecated_modules` command is also provided for inspecting which modules in the current environment are deprecated. `linter.deprecated.module` has no effect on this command, and hence one can view deprecated modules, even when having warnings silenced.
20 lines
583 B
TOML
20 lines
583 B
TOML
name = "deprecated_module"
|
|
defaultTargets = ["Main"]
|
|
|
|
[[lean_lib]]
|
|
name = "Main"
|
|
roots = [
|
|
"DeprecatedModule.New",
|
|
"DeprecatedModule.Old",
|
|
"DeprecatedModule.OldNoMessage",
|
|
"DeprecatedModule.OldDouble",
|
|
"DeprecatedModule.Transitive",
|
|
"DeprecatedModule.Consumer",
|
|
"DeprecatedModule.TransitiveConsumer",
|
|
"DeprecatedModule.ConsumerIgnoreAll",
|
|
"DeprecatedModule.ConsumerIgnoreOne",
|
|
"DeprecatedModule.ConsumerIgnoreWhitespace",
|
|
"DeprecatedModule.ConsumerIgnoreOnlyImport",
|
|
"DeprecatedModule.ConsumerIgnoreLastImport",
|
|
"DeprecatedModule.ConsumerShowDeprecated",
|
|
]
|