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.
30 lines
492 B
Text
30 lines
492 B
Text
module
|
|
|
|
import Std.Data
|
|
|
|
|
|
deprecated_module (since := "30-03-2026")
|
|
|
|
/--
|
|
info: Deprecated modules
|
|
|
|
'elab.deprecatedModule' deprecates to
|
|
#[Std.Data]
|
|
with no message
|
|
-/
|
|
#guard_msgs in
|
|
#show_deprecated_modules
|
|
|
|
/-- warning: module is already marked as deprecated -/
|
|
#guard_msgs in
|
|
deprecated_module "custom message" (since := "30-03-2026")
|
|
|
|
/--
|
|
info: Deprecated modules
|
|
|
|
'elab.deprecatedModule' deprecates to
|
|
#[Std.Data]
|
|
with message 'custom message'
|
|
-/
|
|
#guard_msgs in
|
|
#show_deprecated_modules
|