Pretty printing Syntax fails

Stream: lean4

[Reinier van der Gronden]

I'm writing a tactic that gives suggestions on how to change existing tactics to be more legible. This delaborates the goal and combines this with the executed tactic:

let newGoalStx ← delab (← instantiateMVars newGoalDecl.type)
let newStx ← `(suffices $newGoalStx by $tacticStx)
addTrace `structured m!"{newStx}"

The newStx object itself seems valid, however adding the trace fails with the error message:

[structured] [Error pretty printing syntax: parenthesize: uncaught backtrack exception. Falling back to raw printer.]
(Term.suffices
 "suffices"
 (Term.app `Even [(num "0")])
 []
 (Term.byTactic
  "by"
  (Tactic.tacticSeq
   (Tactic.tacticRepeat_
    "repeat"
    (Tactic.tacticSeq
     (Tactic.tacticSeq1Indented
      [(group (Tactic.apply "apply" (Term.app `Even.add_two [(Term.hole "_") (Term.hole "_")])) [])]))))))

Why does this fail? This Syntax 'raw' printing seems in line with what I expect: suffices Even 0 by repeat apply Even.add_two _ _

[Sebastian Ullrich]

No, that syntax tree is missing the sufficesDecl node. Try $newGoalStx:term.

[Sebastian Ullrich]

Actually do you have an #mwe? This should be a type error in recent versions.

[Reinier van der Gronden]

What do you mean by the sufficesDecl node? I've tried adding :term, but then the $tacticStx complains with expected term.

[Reinier van der Gronden]

I'll try creating a mwe for it, good practice anyways

[Reinier van der Gronden]

Also, I've updated to the latest nightly and the error remains the same. Note that I have set pp.rawOnError, so it could still be a type error I guess? VSCode doesn't complain though

[Reinier van der Gronden]

Okay that took longer than expected, I tried to trim it down a little too much. The smallest example without changing the structure of my tactic is:

import Lean
open Lean Lean.Meta Lean.Elab Lean.Elab.Tactic Lean.PrettyPrinter
set_option pp.rawOnError true

inductive Even : Nat → Prop
| zero : Even Nat.zero
| add_two : ∀ k : Nat, Even k → Even (k+2)

def x (stx : Syntax): TacticM Unit := do
  evalTactic stx
  match ← getUnsolvedGoals with
  | [goal] =>
    let goalStx ← delab (← instantiateMVars (← getMVarDecl goal).type)
    let newStx ← `(suffices $goalStx by $stx)
    addTrace `myTactic m!"This message fails with \n{newStx}"
  | _ => logWarning "MWE"

elab &"myTactic " t:tactic : tactic =>
  x t

example : Even 2 := by
  myTactic apply Even.add_two _ _
  sorry

[Sebastian Ullrich]

That doesn't parse for me on current master. "expected ';' or line break" after $goalStx.

[Reinier van der Gronden]

Ah yes, my toolchain was still overriden with an old nightly :sweat_smile: I get the same error now

[Sebastian Ullrich]

I'm starting to wonder whether we should remove toolchain overrides as a mis-feature from elan

[Reinier van der Gronden]

Well the weird thing to me was that I had removed the lean.toolchain from the working directory, but it was overriden by a parent directory that had it. But that might also just be me mismanaging my folder structure :sweat_smile: I haven't worked with Lean 4 that much yet

[Henrik Böving]

Sebastian Ullrich said:

I'm starting to wonder whether we should remove toolchain overrides as a mis-feature from elan

But it's used in the compiler development process right? At least as documented in the manual.

[Sebastian Ullrich]

Not by me, but you're right, yes :sweat_smile: . A lean-toolchain file with contents a la ../build/release/stage0 would be much more explicit and discoverable though.

[Henrik Böving]

Damn NixOS punks :P

[Marc Huisinga]

Sebastian Ullrich said:

I'm starting to wonder whether we should remove toolchain overrides as a mis-feature from elan

I use it for CI

[Sebastian Ullrich]

You can use lake +leanprover/lean4:nightly build for that

[Sébastien Michelland]

I find switching toolchains in VS Code to be quite intuitive/discoverable. Admittedly, it is confusing when a change to lean-toolchain doesn't propagate because of the override. If you get rid of the override, maybe a similar menu command that would instead modify lean-toolchain then restart the server could be provided?

[Sebastian Ullrich]

AFAIK switching toolchains in VS Code does not actually use elan overrides

[Reinier van der Gronden]

So in my m(notworking)e above, I changed the line

let newStx ← `(suffices $goalStx:term by $stx:tactic; exact this; _)

Where I'm unsure on how to 'finish' the syntax quotation. Looking at the macro definition of suffices, we see the second match case:

  | `(suffices $[$x :]? $type by%$b $tac:tacticSeq; $body) => `(have $[$x]? : $type := $body; by%$b $tac:tacticSeq)

Here I don't know all the notation, but I do see that it expects a sequence of tactics, ending with a body element, that is used as a (I assume) proof term outside of tactic mode. In my case, I do not see why I need such a body term. My case would be pretty simple: suffices Even 0 by repeat apply Even.add_two _ _ only contains the tacticSeq, right?

Could someone elaborate on the purpose of the body term? Is there some way I can consider it 'empty' in my case?

[Reinier van der Gronden]

An actual compilable mwe that does still has the same error message is as follows:

import Lean
open Lean Lean.Meta Lean.Elab Lean.Elab.Tactic Lean.PrettyPrinter

-- TODO: Does not seem to work without
open TSyntax.Compat

set_option pp.rawOnError true

#eval Lean.versionString -- "4.0.0-nightly-2022-07-22"

inductive Even : Nat → Prop
| zero : Even Nat.zero
| add_two : ∀ k : Nat, Even k → Even (k+2)

def x (stx : Syntax): TacticM Unit := do
  evalTactic stx
  match ← getUnsolvedGoals with
  | [goal] =>
    let goalStx ← delab (← instantiateMVars (← getMVarDecl goal).type)
    let myTacticSeq ← `(tactic|$stx; exact this)
    let newStx ← `(suffices $goalStx:term by $myTacticSeq:tacticSeq; ?_)
    addTrace `myTactic m!"This message fails with \n{newStx}"
  | _ => logWarning "MWE"

elab &"myTactic " t:tactic : tactic =>
  x t

example : Even 2 := by
  myTactic apply Even.add_two _ _
  -- suffices Even 0 by
  --   apply Even.add_two _ _
  --   exact this
  sorry

With almost the same error:

[myTactic] This message fails with
[Error pretty printing syntax: parenthesize: uncaught backtrack exception. Falling back to raw printer.]
(Term.suffices
 "suffices"
 (Term.sufficesDecl
  []
  (Term.app `Even [(num "0")])
  (Term.byTactic'
   "by"
   (Tactic.seq1
    [(Tactic.apply "apply" (Term.app `Even.add_two [(Term.hole "_") (Term.hole "_")]))
     ";"
     (Tactic.exact "exact" (Lean.termThis "this"))])))
 ";"
 (Term.syntheticHole "?" (Term.hole "_")))

The difference is that I added the TSyntax.Compat open, otherwise $stx is the wrong type. (And seconds before posting I saw that Sebastian Ulrich said on another post that using TSyntax.Compat is a red flag you're doing something wrong :upside_down: )

Additionally, I added ?_ at the end of the suffices block, because the macro definition expects a $body term, even though in my example that is empty. I expect that it now fails because of this last syntheticHole, but I'm unsure on how to figure this out, since I don't really understand why the $body term is mandatory anyways.

Any pointers where I seem to be going wrong?

[Sebastian Ullrich]

Ah, you're using term suffices, but I assume you want tactic

elab "myTactic " t:tactic : tactic => do
  evalTactic t
  match ← getUnsolvedGoals with
  | [goal] =>
    let goalStx ← delab (← instantiateMVars (← getMVarDecl goal).type)
    let newStx ← `(tactic| suffices $goalStx:term by $t; exact this)
    addTrace `myTactic m!"This message fails with \n{newStx}"
  | _ => logWarning "MWE"

[Reinier van der Gronden]

That certainly makes more sense, however, it still has the error message in your mwe. If you add $t:tactic, it works!

elab "myTactic " t:tactic : tactic => do
  evalTactic t
  match ← getUnsolvedGoals with
  | [goal] =>
    let goalStx ← delab (← instantiateMVars (← getMVarDecl goal).type)
    let newStx ← `(tactic|
      suffices $goalStx:term by
        $t:tactic
        exact this)
    addTrace `myTactic m!"This message succeeds with \n{newStx}"
  | _ => logWarning "MWE"

example : Even 2 := by
  myTactic apply Even.add_two _ _
  sorry

Adds the expected trace:

[myTactic] This message succeeds with
suffices Even 0 by
  apply Even.add_two _ _
  exact this

Thanks for the help, all the different types of terms gets confusing sometimes!

[Sebastian Ullrich]

Ah, you need https://github.com/leanprover/lean4-nightly/releases/tag/nightly-2022-07-24 or later for my version

[Reinier van der Gronden]

Yes, that works as well. Guess I should keep a bit more of an eye on nightly changes :smile: Thanks again!