9aad86a576
This PR adds support for marking options as deprecated. When a deprecated option is used via `set_option`, a warning is emitted (controlled by `linter.deprecated.options`). An `OptionDeprecation` structure with a required `since` field and an optional `text?` field is added to `OptionDecl`. Each `set_option` elaborator (command, term, tactic, grind) calls `checkDeprecatedOption` to emit warnings. The C++ `register_option` is updated to account for the new field. As a first use, `backward.eqns.nonrecursive` and `backward.eqns.deepRecursiveSplit` are marked deprecated. Continues earlier work done in #11096.
21 lines
596 B
Text
21 lines
596 B
Text
import Lean
|
|
|
|
-- Deprecated option without custom text
|
|
register_option test.deprecated.plain : Bool := {
|
|
defValue := false
|
|
descr := "A test option."
|
|
deprecation? := some { since := "2026-04-01" }
|
|
}
|
|
|
|
-- Deprecated option with custom text
|
|
register_option test.deprecated.withText : Nat := {
|
|
defValue := 42
|
|
descr := "Another test option."
|
|
deprecation? := some { since := "2026-04-01", text? := some "use `test.newOption` instead" }
|
|
}
|
|
|
|
-- Non-deprecated option (for comparison)
|
|
register_option test.notDeprecated : Bool := {
|
|
defValue := true
|
|
descr := "A non-deprecated test option."
|
|
}
|