panic

Stream: general

[Kevin Buzzard]

In VS Code on current mathlib master (so lean4:v4.19.0-rc3) if I click on "cases" on line 17 of the following code(which is a half-written line of code)

import Mathlib

open Cardinal

example : Module.finrank ℤ ℚ = 1 := by
  rw [← Module.rank_eq_one_iff_finrank_eq_one]
  suffices Module.rank ℤ ℚ ≤ 1 ∧ Module.rank ℤ ℚ ≠ 0 by
    obtain ⟨h1, h0⟩ := this
    generalize Module.rank ℤ ℚ = c at *
    sorry -- cardinals
  constructor
  · apply rank_le (R := ℤ) (M := ℚ) (n := 1)
    intro s hs
    by_contra! h
    rw [Finset.one_lt_card] at h
    obtain ⟨a, ha, b, hb, h⟩ := h
    cases
    -- clear denominators
    let D := a.den * b.den
    sorry
  · sorry

then I get a panic:

Lean server printed an error: PANIC at Lean.MetavarContext.getDecl Lean.MetavarContext:430:17: unknown metavariable backtrace:

Here's the full text as a github gist. No idea if this is important, made no attempt to minimise. Can others reproduce? I tried it on https://live.lean-lang.org/ and just got the expected error (basically "cases by itself doesn't make sense")

[Vasilii Nesterov]

I minimized it to

import Mathlib

example : True := by
  cases
  let x := 5
  sorry

The panic occurs when I hover over cases. It doesn't panic without import Mathlib.

[Kevin Buzzard]

Oh thanks! I'll minimise more while I'm waiting for FLT CI

[Kevin Buzzard]

Well mathlib's off the hook:

import Batteries.CodeAction

example : True := by
  cases -- click here for panic
  let x := 5
  sorry

[Kevin Buzzard]

I don't really know my way around batteries so I'll leave it here

[Kevin Buzzard]

(what I mean by that is that something annoying happens at this point: I seem to need both of

import Batteries.CodeAction.Basic
import Batteries.CodeAction.Misc

example : True := by
  cases -- click here for panic
  let x := 5
  sorry

to cause the panic -- deleting either import makes the panic go away, so I don't actually know what to do next)

[Edward van de Meent]

since it might be relevant: what version of the extension are you on?

[Kevin Buzzard]

0.0.204

[Kevin Buzzard]

and VS Code 1.96.0. Can you not reproduce?

[Julian Berman]

I can in VSCode (though oddly it does not reproduce in lean.nvim, so it does have something to do with the interaction between the editors and server and not just the server.)

[Kevin Buzzard]

Here's a bit more minimisation: it's the actual code which is probably causing the panic, i.e. if you delete one of these declarations (the 1st or the 4th) then the panic goes away.

import Lean.Elab.Tactic.Induction
import Batteries.Lean.Position
import Batteries.CodeAction.Attr
import Lean.Server.CodeActions.Provider

namespace Batteries.CodeAction

open Lean Meta Elab Server RequestM CodeAction

/-

## Overview

This file contains four declarations, the first copied from `Batteries.CodeAction.Basic`
and the second, third and fourth copied from `Batteries.CodeAction.Misc`. The second is needed to
compile the third, the third is needed to compile the 4th. The 1st and the 4th together cause
the panic; deleting either of them makes the panic not happen.

-/

-- stuff copied from `Batteries.CodeAction.Basic`

-- declaration 1: delete this and the panic goes away

/-- A code action which calls `@[tactic_code_action]` code actions. -/
@[code_action_provider] def tacticCodeActionProvider : CodeActionProvider := fun params snap => do
  let doc ← readDoc
  let startPos := doc.meta.text.lspPosToUtf8Pos params.range.start
  let endPos := doc.meta.text.lspPosToUtf8Pos params.range.end
  let pointerCol :=
    if params.range.start.line == params.range.end.line then
      max params.range.start.character params.range.end.character
    else 0
  let some result := findTactic?
    (fun pos => (doc.meta.text.utf8PosToLspPos pos).character ≤ pointerCol)
    ⟨startPos, endPos⟩ snap.stx | return #[]
  let tgtTac := match result with
    | .tactic (tac :: _)
    | .tacticSeq _ _ (_ :: tac :: _) => tac.1
    | _ => unreachable!
  let tgtRange := tgtTac.getRange?.get!
  have info := findInfoTree? tgtTac.getKind tgtRange none snap.infoTree (canonicalOnly := true)
    fun _ info => info matches .ofTacticInfo _
  let some (ctx, node@(.node (.ofTacticInfo info) _)) := info | return #[]
  let mut out := #[]
  match result with
  | .tactic stk@((tac, _) :: _) => do
    let ctx := { ctx with mctx := info.mctxBefore }
    let actions := (tacticCodeActionExt.getState snap.env).2
    if let some arr := actions.onTactic.find? tac.getKind then
      for act in arr do
        try out := out ++ (← act params snap ctx stk node) catch _ => pure ()
    for act in actions.onAnyTactic do
      try out := out ++ (← act params snap ctx stk node) catch _ => pure ()
  | .tacticSeq _ i stk@((seq, _) :: _) =>
    let (ctx, goals) ← if 2*i < seq.getNumArgs then
      let stx := seq[2*i]
      let some stxRange := stx.getRange? | return #[]
      let some (ctx, .node (.ofTacticInfo info') _) :=
          findInfoTree? stx.getKind stxRange ctx node fun _ info => (info matches .ofTacticInfo _)
        | return #[]
      pure ({ ctx with mctx := info'.mctxBefore }, info'.goalsBefore)
    else
      pure ({ ctx with mctx := info.mctxAfter }, info.goalsAfter)
    for act in (tacticSeqCodeActionExt.getState snap.env).2 do
      try out := out ++ (← act params snap ctx i stk goals) catch _ => pure ()
  | _ => unreachable!
  pure out

-- end of stuff copied from `Batteries.CodeAction.Basic`

-- copied from `Batteries.CodeAction.Misc`

-- declaration 2: needed for declaration 3

/--
Similar to `getElimExprInfo`, but returns the names of binders instead of just the numbers;
intended for code actions which need to name the binders.
-/
def getElimExprNames (elimType : Expr) : MetaM (Array (Name × Array Name)) := do
  -- let inductVal ← getConstInfoInduct inductName
  -- let decl ← getConstInfo declName
  forallTelescopeReducing elimType fun xs type => do
    let motive  := type.getAppFn
    let targets := type.getAppArgs
    let motiveType ← inferType motive
    let mut altsInfo := #[]
    for _h : i in [:xs.size] do
      let x := xs[i]
      if x != motive && !targets.contains x then
        let xDecl ← x.fvarId!.getDecl
        if xDecl.binderInfo.isExplicit then
          let args ← forallTelescopeReducing xDecl.type fun args _ => do
            let lctx ← getLCtx
            pure <| args.filterMap fun y =>
              let yDecl := (lctx.find? y.fvarId!).get!
              if yDecl.binderInfo.isExplicit then some yDecl.userName else none
          altsInfo := altsInfo.push (xDecl.userName, args)
    pure altsInfo

-- declaration 3: needed for declaration 4

/-- Finds the `TermInfo` for an elaborated term `stx`. -/
def findTermInfo? (node : InfoTree) (stx : Term) : Option TermInfo :=
  match node.findInfo? fun
    | .ofTermInfo i => i.stx.getKind == stx.raw.getKind && i.stx.getRange? == stx.raw.getRange?
    | _ => false
  with
  | some (.ofTermInfo info) => pure info
  | _ => none

-- declaration 4: delete this and the panic goes away

/--
Invoking tactic code action "Generate an explicit pattern match for 'induction'" in the
following:
````lean
example (x : Nat) : x = x := by
  induction x
````
produces:
````lean
example (x : Nat) : x = x := by
  induction x with
  | zero => sorry
  | succ n ih => sorry
````

It also works for `cases`.
-/
@[tactic_code_action Parser.Tactic.cases Parser.Tactic.induction]
def casesExpand : TacticCodeAction := fun _ snap ctx _ node => do
  let .node (.ofTacticInfo info) _ := node | return #[]
  let (targets, induction, using_, alts) ← match info.stx with
    | `(tactic| cases $[$[$_ :]? $targets],* $[using $u]? $(alts)?) =>
      pure (targets, false, u, alts)
    | `(tactic| induction $[$[$_ :]? $targets],* $[using $u]? $[generalizing $_*]? $(alts)?) =>
      pure (targets, true, u, alts)
    | _ => return #[]
  let some discrInfos := targets.mapM (findTermInfo? node) | return #[]
  let some discr₀ := discrInfos[0]? | return #[]
  let mut some ctors ← discr₀.runMetaM ctx do
      let targets := discrInfos.map (·.expr)
      match using_ with
      | none =>
        if Tactic.tactic.customEliminators.get (← getOptions) then
          if let some elimName ← getCustomEliminator? targets induction then
            return some (← getElimExprNames (← getConstInfo elimName).type)
        matchConstInduct (← whnf (← inferType discr₀.expr)).getAppFn
            (fun _ => failure) fun val _ => do
          let elimName := if induction then mkRecName val.name else mkCasesOnName val.name
          return some (← getElimExprNames (← getConstInfo elimName).type)
      | some u =>
        let some info := findTermInfo? node u | return none
        return some (← getElimExprNames (← inferType info.expr))
    | return #[]
  let mut fallback := none
  if let some alts := alts then
    if let `(Parser.Tactic.inductionAlts| with $(_)? $alts*) := alts then
      for alt in alts do
        match alt with
        | `(Parser.Tactic.inductionAlt| | _ $_* => $fb) => fallback := fb.raw.getRange?
        | `(Parser.Tactic.inductionAlt| | $id:ident $_* => $_) =>
          ctors := ctors.filter (fun x => x.1 != id.getId)
        | _ => pure ()
  if ctors.isEmpty then return #[]
  let tacName := info.stx.getKind.updatePrefix .anonymous
  let eager := {
    title := s!"Generate an explicit pattern match for '{tacName}'."
    kind? := "quickfix"
  }
  let doc ← readDoc
  pure #[{
    eager
    lazy? := some do
      let tacPos := info.stx.getPos?.get!
      let endPos := doc.meta.text.utf8PosToLspPos info.stx.getTailPos?.get!
      let indent := "\n".pushn ' ' (findIndentAndIsStart doc.meta.text.source tacPos).1
      let (startPos, str') := if alts.isSome then
        let stx' := if fallback.isSome then
          info.stx.modifyArg (if induction then 4 else 3)
            (·.modifyArg 0 (·.modifyArg 2 (·.modifyArgs (·.filter fun s =>
              !(s matches `(Parser.Tactic.inductionAlt| | _ $_* => $_))))))
        else info.stx
        (doc.meta.text.utf8PosToLspPos stx'.getTailPos?.get!, "")
      else (endPos, " with")
      let fallback := if let some ⟨startPos, endPos⟩ := fallback then
        doc.meta.text.source.extract startPos endPos
      else
        "sorry"
      let newText := Id.run do
        let mut str := str'
        for (name, args) in ctors do
          let mut ctor := toString name
          if let some _ := (Parser.getTokenTable snap.env).find? ctor then
            ctor := s!"{idBeginEscape}{ctor}{idEndEscape}"
          str := str ++ indent ++ s!"| {ctor}"
          -- replace n_ih with just ih if there is only one
          let args := if induction &&
            args.foldl (fun c n =>
              if n.eraseMacroScopes.getString!.endsWith "_ih" then c+1 else c) 0 == 1
          then
            args.map (fun n => if !n.hasMacroScopes && n.getString!.endsWith "_ih" then `ih else n)
          else args
          for arg in args do
            str := str ++ if arg.hasNum || arg.isInternal then " _" else s!" {arg}"
          str := str ++ s!" => " ++ fallback
        str
      pure { eager with
        edit? := some <|.ofTextEdit doc.versionedIdentifier {
          range := ⟨startPos, endPos⟩
          newText
        }
      }
  }]

-- end of stuff copied from `Batteries.CodeAction.Misc`

end Batteries.CodeAction

example : True := by
  cases -- click here for panic
  let x := 5
  sorry

[Marc Huisinga]

The getCustomEliminator? call in the casesExpand code action appears to be causing the panic (and in there, inferType), but I haven't investigated it further than that