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.
38 lines
1.2 KiB
Text
38 lines
1.2 KiB
Text
/-
|
|
Tests for the `deprecated_module` command.
|
|
-/
|
|
|
|
-- Missing since (message is optional)
|
|
/--
|
|
warning: `deprecated_module` should specify the date or library version at which the deprecation was introduced, using `(since := "...")`
|
|
-/
|
|
#guard_msgs in
|
|
deprecated_module
|
|
|
|
-- Missing since with message (also warns about duplicate since module is already marked above)
|
|
/--
|
|
warning: module is already marked as deprecated
|
|
---
|
|
warning: `deprecated_module` should specify the date or library version at which the deprecation was introduced, using `(since := "...")`
|
|
-/
|
|
#guard_msgs in
|
|
deprecated_module "use NewModule instead"
|
|
|
|
-- No message, with since (also warns about duplicate)
|
|
/-- warning: module is already marked as deprecated -/
|
|
#guard_msgs in
|
|
deprecated_module (since := "2026-03-19")
|
|
|
|
-- Both message and since: only duplicate warning
|
|
/--
|
|
warning: module is already marked as deprecated
|
|
-/
|
|
#guard_msgs in
|
|
deprecated_module "use NewModule instead" (since := "2026-03-19")
|
|
|
|
-- Duplicate deprecated_module: warns about already being marked (standalone confirmation)
|
|
/--
|
|
warning: module is already marked as deprecated
|
|
-/
|
|
#guard_msgs in
|
|
deprecated_module "use SomethingElse instead" (since := "2026-03-20")
|