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 `(by simp only [$[$lemmas:term],*] at $h) #print foo -- parenthesizer backtracking exception
Sebastian Ullrich (Apr 14 2021 at 07:23):
Yes, these are expected/unavoidable if the syntax tree is malformed. In this case, it should be
Daniel Selsam (Apr 14 2021 at 13:21):
@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
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