fix: do not modify infotrees in withSetOptionIn

[thorimur]

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.

We give an optional flag (addInfo := true) to Elab.elabSetOption which controls whether info is added to the infotrees.

This was brought up on Zulip here, and discussed briefly in office hours.

[thorimur]

changelog-language

[thorimur]

awaiting-review

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-11-21 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-11-21 23:05:12)

[leanprover-community-bot]

Mathlib CI status (docs):

• 🟡 Mathlib branch lean-pr-testing-11313 build against this PR was cancelled. (2025-11-21 23:52:24) View Log
• ✅ Mathlib branch lean-pr-testing-11313 has successfully built against this PR. (2025-11-22 00:52:33) View Log
• ✅ Mathlib branch lean-pr-testing-11313 has successfully built against this PR. (2025-11-25 19:19:52) View Log

[Kha]

I think we also noticed that existing core linters worked around this, could you adjust them as well (and check that their behavior is covered by a test)?

[Kha]

Can we move it to Linter.Basic then?

[thorimur]

Hmm, I'm having difficulty doing so without introducing a build cycle.

withSetOptionIn uses definitions in Lean.Elab.Command, but Lean.Elab.Command depends on Lean.Elab.Binders, which depends on Lean.Linter.Basic (only) in order to log a deprecation for let_fun in elabLetFunDecl. (Haven't checked if that's the only dependency Lean.Linter.Basic → Lean.Elab.Command.)

Should we leave withSetOptionIn in Lean.Elab.Command for now, or can we shuffle things around somehow?

(I've reverted my failing attempts to move it for now.)

[Kha]

Hmm, Linter.Util then?

[thorimur]

Thought about this a bit:

1. I feel that ideally Lean.Linter.Basic should give you everything you need to define a typical linter. withSetOptionIn ought to be part of that, as it's only an unusual linter which avoids it.
2. Moreover, Lean.Elab.Command should also be part of that, as it has addLinter, which you will always want. So it would be nice if Lean.Linter.Basic could actually publicly import Lean.Elab.Command.

Assuming let_fun is the only issue (I'm testing this at #11497), what do you say to either (a) removing let_fun (seems it was deprecated 5 months ago, June 29; not sure if that's long enough) or (b) moving it somewhere else? (The option logic for logLintIf seems inextricable from Linter.Basic, so inlining that code isn't easy. We could of course issue a "worse" deprecation warning that just checks the option directly; I'm not sure if anyone is likely to be relying on linter sets/linter.all to turn off that warning...)

It might make sense to do this in another couple of PRs, of course. :)

EDIT: It seems more things prior to Lean.Elab.Command log deprecation warnings than let_fun. :( It would be nice to have one module that people import to write a linter, though...Lean.Linter seems to also include actual linters, and I imagine would therefore not be most people's first choice; Util connotes optional utilities, not the basic infrastructure. Either way it does seem that the contents of Lean.Linter.Basic have to precede Lean.Elab.Command, though.

[thorimur]

What do you think about:

• moving the contents of Lean.Linter.Basic to a new file, e.g. Lean.Linter.Log (or Lean.Linter.Option, Lean.Linter.Init, or something else)
• putting withSetOptionIn in the now-empty Lean.Linter.Basic, and publicly importing Lean.Elab.Command there.

Or, of course, we can just make Lean.Linter.Util the file to import when writing linters. I'm willing to make either of these changes, ultimately; I just have a preference for providing all the basic linter necessities in Lean.Linter.Basic (which includes Lean.Elab.Command and addLinter) if possible instead. :)