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.
73 lines
1.9 KiB
Text
73 lines
1.9 KiB
Text
/-!
|
|
This file tests deprecation warnings on options.
|
|
-/
|
|
|
|
-- Basic deprecation warning on a command-level set_option
|
|
/--
|
|
warning: `backward.eqns.deepRecursiveSplit` has been deprecated
|
|
-/
|
|
#guard_msgs in
|
|
set_option backward.eqns.deepRecursiveSplit true
|
|
|
|
/--
|
|
warning: `backward.eqns.nonrecursive` has been deprecated
|
|
-/
|
|
#guard_msgs in
|
|
set_option backward.eqns.nonrecursive true
|
|
|
|
-- set_option ... in should produce exactly ONE warning (not multiple)
|
|
/--
|
|
warning: `backward.eqns.nonrecursive` has been deprecated
|
|
-/
|
|
#guard_msgs in
|
|
set_option backward.eqns.nonrecursive true in
|
|
example := 0
|
|
|
|
-- Nested set_option ... in ... in should produce exactly one warning per deprecated option
|
|
/--
|
|
warning: `backward.eqns.nonrecursive` has been deprecated
|
|
---
|
|
warning: `backward.eqns.deepRecursiveSplit` has been deprecated
|
|
-/
|
|
#guard_msgs in
|
|
set_option backward.eqns.nonrecursive true in
|
|
set_option backward.eqns.deepRecursiveSplit true in
|
|
example := 0
|
|
|
|
-- Duplicate option in nested in blocks: exactly one warning per occurrence
|
|
/--
|
|
warning: `backward.eqns.nonrecursive` has been deprecated
|
|
---
|
|
warning: `backward.eqns.nonrecursive` has been deprecated
|
|
-/
|
|
#guard_msgs in
|
|
set_option backward.eqns.nonrecursive true in
|
|
set_option backward.eqns.nonrecursive false in
|
|
example := 0
|
|
|
|
-- Disabling linter.deprecated.options suppresses warnings
|
|
#guard_msgs in
|
|
set_option linter.deprecated.options false in
|
|
set_option backward.eqns.nonrecursive true
|
|
|
|
#guard_msgs in
|
|
set_option linter.deprecated.options false in
|
|
set_option backward.eqns.nonrecursive true in
|
|
example := 0
|
|
|
|
-- Disabling suppresses warnings in nested in blocks
|
|
#guard_msgs in
|
|
set_option linter.deprecated.options false in
|
|
set_option backward.eqns.nonrecursive true in
|
|
set_option backward.eqns.deepRecursiveSplit true in
|
|
example := 0
|
|
|
|
-- Disabling at command level also works
|
|
set_option linter.deprecated.options false
|
|
|
|
#guard_msgs in
|
|
set_option backward.eqns.nonrecursive true
|
|
|
|
#guard_msgs in
|
|
set_option backward.eqns.nonrecursive false in
|
|
example := 0
|