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>
