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
1.9 KiB
Text
70 lines
1.9 KiB
Text
set_option linter.listVariables true
|
|
|
|
#guard_msgs in
|
|
example (l : List Nat) : l = l := rfl
|
|
|
|
#guard_msgs in
|
|
example (l' : List Nat) : l' = l' := rfl
|
|
|
|
#guard_msgs in
|
|
example (l₁ : List Nat) : l₁ = l₁ := rfl
|
|
|
|
#guard_msgs in
|
|
example (l₂ : List Nat) : l₂ = l₂ := rfl
|
|
|
|
/--
|
|
warning: Forbidden variable appearing as a `List` name: l₅
|
|
|
|
Note: This linter can be disabled with `set_option linter.listVariables false`
|
|
---
|
|
warning: Forbidden variable appearing as a `List` name: l₅
|
|
|
|
Note: This linter can be disabled with `set_option linter.listVariables false`
|
|
-/
|
|
#guard_msgs in
|
|
example (l₅ : List Nat) : l₅ = l₅ := rfl
|
|
|
|
#guard_msgs in
|
|
example (xs : List Nat) : xs = xs := rfl
|
|
|
|
/--
|
|
warning: Forbidden variable appearing as a `List` name: ps
|
|
|
|
Note: This linter can be disabled with `set_option linter.listVariables false`
|
|
---
|
|
warning: Forbidden variable appearing as a `List` name: ps
|
|
|
|
Note: This linter can be disabled with `set_option linter.listVariables false`
|
|
-/
|
|
#guard_msgs in
|
|
example (ps : List Nat) : ps = ps := rfl
|
|
|
|
/--
|
|
warning: Forbidden variable appearing as a `Array` name: l
|
|
|
|
Note: This linter can be disabled with `set_option linter.listVariables false`
|
|
---
|
|
warning: Forbidden variable appearing as a `Array` name: l
|
|
|
|
Note: This linter can be disabled with `set_option linter.listVariables false`
|
|
-/
|
|
#guard_msgs in
|
|
example (l : Array Nat) : l = l := rfl
|
|
|
|
/- Test that `set_option ... in` works; ensures that `withSetOptionIn` no longer leaves
|
|
context-free info nodes (#11313) -/
|
|
|
|
set_option linter.listVariables false
|
|
|
|
/--
|
|
warning: Forbidden variable appearing as a `Array` name: l
|
|
|
|
Note: This linter can be disabled with `set_option linter.listVariables false`
|
|
---
|
|
warning: Forbidden variable appearing as a `Array` name: l
|
|
|
|
Note: This linter can be disabled with `set_option linter.listVariables false`
|
|
-/
|
|
#guard_msgs in
|
|
set_option linter.listVariables true in
|
|
example (l : Array Nat) : l = l := rfl
|