Stream: lean4

Topic: parenthesizer backtrack errors?

Daniel Selsam (Apr 14 2021 at 02:22):

I see a bunch of "HACK" warnings in https://github.com/leanprover/lean4/blob/master/src/Lean/PrettyPrinter/Parenthesizer.lean Are errors @ https://github.com/leanprover/lean4/blob/master/src/Lean/PrettyPrinter/Parenthesizer.lean#L539 expected? Here is a short example that triggers it:

import Lean
open Lean Lean.PrettyPrinter.Delaborator

axiom Nat.mul2plus (n : Nat) : 2 * n = n + n

theorem foo (n : Nat) (h : 2 * n = n + n) : n + n = n + n := by
simp only [Nat.mul2plus] at h
exact h

@[delab app.Eq.mp]
def delabSimpHyp : Delab := do
let arg := (← getExpr).appArg!
let h := mkIdent (← Meta.getFVarLocalDecl arg).userName
let lemmas := #[Nat.mul2plus].map mkIdent

@Sebastian Ullrich Thanks, indeed $h:ident fixes it. Any suggestions for how I might have diagnosed/debugged that on my own? Sebastian Ullrich (Apr 14 2021 at 18:11): My line of reasoning basically was "I hope it's not a bug in the parenthesizer... so let's assume the syntax tree is malformed. $lemmas:term looks good, it is actually fed a term. So maybe $h is underspecified? Oh yeah, at also takes other arguments like *, so let's try :ident." Sebastian Ullrich (Apr 14 2021 at 18:14): But using quotations correctly in non-trivial syntax is simply tough right now. Ideally the original code should fail to typecheck because mkIdent should return some TSyntax ident while $h would expect some TSyntax location (or maybe the former even automatically coerces into the latter in the right way), but that would be a pretty fundamental and extensive change.

Last updated: May 07 2021 at 12:15 UTC