leanprover
fix: do not modify infotrees in `withSetOptionIn`
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.
Reference manual CI status:
- ❗ Reference manual CI can not be attempted yet, as the
nightly-testing-2025-11-21tag does not exist there yet. We will retry when you push more commits. If you rebase your branch ontonightly-with-manual, reference manual CI should run now. You can force reference manual CI using theforce-manual-cilabel. (2025-11-21 23:05:12)
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
