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.
86 lines
2.1 KiB
Text
86 lines
2.1 KiB
Text
import DeprecatedOption.Def
|
|
|
|
-- Cross-file: deprecated option without custom text
|
|
/--
|
|
warning: `test.deprecated.plain` has been deprecated
|
|
-/
|
|
#guard_msgs in
|
|
set_option test.deprecated.plain true
|
|
|
|
-- Cross-file: deprecated option with custom text
|
|
/--
|
|
warning: `test.deprecated.withText` has been deprecated: use `test.newOption` instead
|
|
-/
|
|
#guard_msgs in
|
|
set_option test.deprecated.withText 7
|
|
|
|
-- Cross-file: non-deprecated option produces no warning
|
|
#guard_msgs in
|
|
set_option test.notDeprecated false
|
|
|
|
-- set_option ... in block
|
|
/--
|
|
warning: `test.deprecated.plain` has been deprecated
|
|
-/
|
|
#guard_msgs in
|
|
set_option test.deprecated.plain true in
|
|
example := 0
|
|
|
|
-- Custom text in set_option ... in block
|
|
/--
|
|
warning: `test.deprecated.withText` has been deprecated: use `test.newOption` instead
|
|
-/
|
|
#guard_msgs in
|
|
set_option test.deprecated.withText 100 in
|
|
example := 0
|
|
|
|
-- Nested deprecated options in set_option ... in blocks
|
|
/--
|
|
warning: `test.deprecated.plain` has been deprecated
|
|
---
|
|
warning: `test.deprecated.withText` has been deprecated: use `test.newOption` instead
|
|
-/
|
|
#guard_msgs in
|
|
set_option test.deprecated.plain true in
|
|
set_option test.deprecated.withText 0 in
|
|
example := 0
|
|
|
|
-- Tactic context
|
|
/--
|
|
warning: `test.deprecated.plain` has been deprecated
|
|
-/
|
|
#guard_msgs in
|
|
example : True := by
|
|
set_option test.deprecated.plain true in
|
|
trivial
|
|
|
|
-- Tactic context with custom text
|
|
/--
|
|
warning: `test.deprecated.withText` has been deprecated: use `test.newOption` instead
|
|
-/
|
|
#guard_msgs in
|
|
example : True := by
|
|
set_option test.deprecated.withText 0 in
|
|
trivial
|
|
|
|
-- Suppressing warnings via linter.deprecated.options
|
|
#guard_msgs in
|
|
set_option linter.deprecated.options false in
|
|
set_option test.deprecated.plain true
|
|
|
|
#guard_msgs in
|
|
set_option linter.deprecated.options false in
|
|
set_option test.deprecated.withText 7
|
|
|
|
-- Suppressing in set_option ... in blocks
|
|
#guard_msgs in
|
|
set_option linter.deprecated.options false in
|
|
set_option test.deprecated.plain true in
|
|
example := 0
|
|
|
|
-- Suppressing in tactic context
|
|
#guard_msgs in
|
|
set_option linter.deprecated.options false in
|
|
example : True := by
|
|
set_option test.deprecated.plain true in
|
|
trivial
|