bug: withSetOptionIn creates context-free info nodes

Stream: lean4

[Thomas Murrills]

It looks like withSetOptionIn alters the info state to create context-free info nodes. This causes panics when using InfoTree.visitM in typical linters.

import Lean

open Lean Elab Command Term InfoTree

partial def showContextFreeNodes : InfoTree → CommandElabM Unit :=
  go none
where go
  | ctx?, context ctx t => go (ctx.mergeIntoOuter? ctx?) t
  | some ctx, node i cs => do
    let _ ← cs.toList.mapM (go <| i.updateContext? ctx)
  | none, node i _ =>
    -- `visitM` panics here; log instead
    logInfo m!"no context: {i.stx}"
  | _, hole .. => pure ()

elab "#show_ctx_free_nodes" ppLine cmd:command : command => do
  elabCommand cmd
  let run :=
    withSetOptionIn -- comment out to see that no info is logged
      fun _ =>
        for t in (← getInfoState).substituteLazy.get.trees do
          showContextFreeNodes t
  run cmd

/- no context for two (maximal) info nodes with syntax:
1. full command
2. `linter.unusedVariables` -/
#show_ctx_free_nodes
set_option linter.unusedVariables false in
theorem x : True := True.intro

[Thomas Murrills]

My thinking is that withSetOptionIn, being used only during linting (when all elaboration is supposed to be finished), should simply not touch the infotrees at all. (Likewise, it probably should not error on invalid option values either, but just silently ignore them).

I can make a PR doing this if that sounds good. :)

[Thomas Murrills]

lean4#11313