48ad8401cd
This PR ensures that `withSetOptionIn` does not modify the infotrees or error on malformed option values, and thus avoids panics in linters that traverse the infotrees with `visitM`. `withSetOptionIn` is only intended to be used in linters, and thus should provide the linter action with the infotrees produced during elaboration without modification. However, `withSetOptionIn` had not only been modifying the infotrees by elaborating the option, but had been producing context-free info nodes in doing so. These caused uses of `visitM` and related functions to panic in typical linters. Likewise, `withSetOptionIn` also should not cause the linter to error if somehow it consumes a malformed option value, but instead should fail silently; the error should (only) be logged during the original elaboration. We give an optional flag `(addInfo := true)` to `Elab.elabSetOption` which controls whether info is added to the infotrees. To clarify that `withSetOptionIn` is used only in linters, we move it into `Lean.Linter.Basic`. To avoid import cycles, we move the current contents of `Lean.Linter.Basic` back to `Lean.Linter.Init`. We also publicly import both `Lean.Linter.Init` and `Lean.Elab.Command` into `Lean.Linter.Basic`, meaning that going forward, linter files need only import `Lean.Linter.Basic` to access the standard linter API. This was brought up on Zulip [here](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/bug.3A.20withSetOptionIn.20creates.20context-free.20info.20nodes/with/556905420), and discussed briefly in office hours. --------- Co-authored-by: Wojciech Rozowski <wojciech@lean-fro.org>
70 lines
2.2 KiB
Text
70 lines
2.2 KiB
Text
set_option linter.indexVariables true
|
|
|
|
#guard_msgs in
|
|
example (xs : List Nat) (i : Nat) (h) : xs[i] = xs[i] := rfl
|
|
|
|
/--
|
|
warning: Forbidden variable appearing as an index: use `i`, `j`, or `k`: m
|
|
|
|
Note: This linter can be disabled with `set_option linter.indexVariables false`
|
|
---
|
|
warning: Forbidden variable appearing as an index: use `i`, `j`, or `k`: m
|
|
|
|
Note: This linter can be disabled with `set_option linter.indexVariables false`
|
|
-/
|
|
#guard_msgs in
|
|
example (xs : List Nat) (m : Nat) (h) : xs[m] = xs[m] := rfl
|
|
|
|
#guard_msgs in
|
|
example (xs : List Nat) (i j : Nat) (h) : xs[i + j] = xs[i + j] := rfl
|
|
|
|
#guard_msgs in
|
|
example (xs : List Nat) (m n : Nat) (h) : xs[m + n] = xs[m + n] := rfl
|
|
|
|
#guard_msgs in
|
|
example (xs : List Nat) (i : Nat) : xs[i]? = xs[i]? := rfl
|
|
|
|
/--
|
|
warning: Forbidden variable appearing as an index: use `i`, `j`, or `k`: m
|
|
|
|
Note: This linter can be disabled with `set_option linter.indexVariables false`
|
|
---
|
|
warning: Forbidden variable appearing as an index: use `i`, `j`, or `k`: m
|
|
|
|
Note: This linter can be disabled with `set_option linter.indexVariables false`
|
|
-/
|
|
#guard_msgs in
|
|
example (xs : List Nat) (m : Nat) : xs[m]? = xs[m]? := rfl
|
|
|
|
#guard_msgs in
|
|
example (xs : List Nat) (i : Nat) : xs.take i = xs.take i := rfl
|
|
|
|
/--
|
|
warning: Forbidden variable appearing as an index: use `i`, `j`, or `k`: m
|
|
|
|
Note: This linter can be disabled with `set_option linter.indexVariables false`
|
|
---
|
|
warning: Forbidden variable appearing as an index: use `i`, `j`, or `k`: m
|
|
|
|
Note: This linter can be disabled with `set_option linter.indexVariables false`
|
|
-/
|
|
#guard_msgs in
|
|
example (xs : List Nat) (m : Nat) : xs.drop m = xs.drop m := rfl
|
|
|
|
/- Test that `set_option ... in` works; ensures that `withSetOptionIn` no longer leaves
|
|
context-free info nodes (#11313) -/
|
|
|
|
set_option linter.indexVariables false
|
|
|
|
/--
|
|
warning: Forbidden variable appearing as an index: use `i`, `j`, or `k`: m
|
|
|
|
Note: This linter can be disabled with `set_option linter.indexVariables false`
|
|
---
|
|
warning: Forbidden variable appearing as an index: use `i`, `j`, or `k`: m
|
|
|
|
Note: This linter can be disabled with `set_option linter.indexVariables false`
|
|
-/
|
|
#guard_msgs in
|
|
set_option linter.indexVariables true in
|
|
example (xs : List Nat) (m : Nat) : xs.drop m = xs.drop m := rfl
|