Code action for showing the term of a tactic proof

Stream: lean4

[Anand Rao]

I am trying to write a code action that converts a tactic proof to the corresponding term-mode proof, using the elabByTactic function at the core. Here is an MWE of the code so far:

import Lean

open Lean Meta Elab Parser Tactic Term

open Server Lsp RequestM

@[codeActionProvider]
def showTermCodeAction : CodeActionProvider := fun params _snap => do
  let doc ← readDoc
  let text := doc.meta.text

  let edit : IO TextEdit := do
    -- the current position in the text document
    let pos : String.Pos := text.lspPosToUtf8Pos params.range.end
    -- the node of the infotree containing the current position
    let some info := _snap.infoTree.findInfo? (·.contains pos) | IO.throwServerError "Infotree not found"
    match info.stx with
    -- TODO allow docstrings
    | `(theorem $nm:ident $args* : $typ:term := $tac:byTactic) =>
      let pptrm : TermElabM Syntax := do
        let typ ← instantiateMVars <| ← elabType typ
        synthesizeSyntheticMVarsNoPostponing
        let trm ← instantiateMVars <| ← elabByTactic tac typ
        synthesizeSyntheticMVarsNoPostponing
        let trm ← reduce trm
        synthesizeSyntheticMVarsNoPostponing
        PrettyPrinter.delab trm
      let some ⟨start, stop⟩ := tac.raw.getRange? | IO.throwServerError "Failed to obtain range"
      let output : TSyntax `term := ⟨← EIO.toIO (fun _ => IO.userError "Code action failed") <|
          _snap.runTermElabM doc.meta pptrm⟩
      return {
        range :=
            ⟨text.leanPosToLspPos <| text.toPosition start,
            text.leanPosToLspPos <| text.toPosition stop⟩,
        newText := ← do
          return output.raw.reprint.get!
      }
    | _ => IO.throwServerError "Parsing input failed. Input must be a `theorem` or `def` with a tactic proof."

  let ca : CodeAction := { title := "Show the term corresponding to the tactic proof.", kind? := "quickfix" }
  return #[{
    eager := ca,
    lazy? := some $ return { ca with
      edit? := WorkspaceEdit.ofTextEdit params.textDocument.uri $ ← edit}
    }]

section Test

theorem xyz : 1 = 1 := by exact Eq.refl 1

theorem abc (n : Nat) (m : Nat) : n ≥ 0 ↔ m ≥ 0 := by
  refine' ⟨fun _ => _, fun _ => _⟩ <;>
  apply Nat.zero_le

end Test

While the code action interface works fine, the byTactic portion of the proof is replaced by a meta-variable instead of the expected term. This is despite using instantiateMVars and synthesizeSyntheticMVarsNoPostponing at various places. The error persists even on replacing $tac:byTactic with by $tacs:tacticSeq in the code above.

The error might be because of the elabByTactic (and the associated private function mkTacticMVar), but I have not been able to find any examples of using elabByTactic either in the Lean4 source code or here on Zulip.

Any help in diagnosing this issue will be greatly appreciated.

[Jannis Limperg]

Try evalTactic instead of elabByTactic. You might also need to use something like withoutModifyingState to ensure that your elaboration doesn't leak out.

Then again, does this require elaboration at all? I would have guessed that when the code action is run, the by block has already been elaborated and the term is available. But I don't know the code actions API, so I could be wrong there.

[Anand Rao]

Thanks for the suggestion. I think you're right about the term already being computed. I will dig into Snapshots.Snapshot.tacticCache further, which seems to store this information.

[Sebastian Ullrich]

No, the info tree is the correct source for this

[Anand Rao]

Thanks, I will try exploring or adapting InfoTree.goalsAt?.