Show tactic state and widget in custom calc

Stream: lean4

[Patrick Massot]

The last thing I want to fix in verbose-lean4 before actually using it for teaching is the infoview during calculations. Verbose Lean has nice calc blocks but they don’t show tactic state when editing proofs of calculation steps and they don’t show Mathlib’s calc widget. I’d be happy to get some help here. I tried something in https://github.com/PatrickMassot/verbose-lean4/blob/master/Verbose/French/Calc.lean with all the %$tk trying to say where to put the widget in https://github.com/PatrickMassot/verbose-lean4/blob/master/Verbose/French/Calc.lean#L88. But I really don’t know how to tell Lean to simply display the goal.

[Patrick Massot]

Hopefully the structure of that file is clear. I have some customized version of calcStep and calcFirstStep and functions to convert from the custom versions to the regular ones.

[Anand Rao Tadipatri]

This is just a guess, but it could be that the syntax tks[i]! is not canonical (as explained in this file in ProofWidgets). If this is indeed the issue, I think using the mkInfoCanonical function defined in that file will fix it.

[Patrick Massot]

@Anand Rao Tadipatri sorry I didn’t see your answer earlier. Thanks a lot for trying to help. Unfortunately this hint doesn’t seem enough to unstuck me. I’ll try to prepare a mwe.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Besides the source info not being canonical, the issue is that the output syntax has no sane positions at all. The goal to display is determined partly based on Syntax positions, so it doesn't show up.

We can see the broken positions by adding

logInfo m!"old syntax: {stx.raw.formatStx (showInfo := true)}"
let calcStx ← `(tactic|calc%$calcstx $steps)
logInfo m!"new syntax: {calcStx.raw.formatStx (showInfo := true)}"

to the elab_rule. Then on the example

example (a b : ℕ) : (a + b)^ 2 = 2*a*b + (a^2 + b^2) := by
  Calc (a+b)^2 = 2*a*b + (a^2 + b^2)   by computation

we see [(group "":4083:"by":4085:" " "":4086:"computation":4097:"\n\n")] in the old syntax, and

(4051:Term.byTactic:4097
     4051:"by":4097
     (4051:Tactic.tacticSeq:4097
      (4051:Tactic.tacticSeq1Indented:4097 [(4051:tacticWeCompute_:4097 4051:"We":4097 4051:"compute":4097 [])])))

in the new syntax. The broken positions 4051-4097 are taken from the ambient ref syntax accessible from MonadRef.

To fix this, let's try copying the by position in convertFirstCalcStep:

| `(CalcFirstStep|$t:term by%$byTk computation) => `(calcFirstStep|$t:term := by%$byTk We compute)

Now the new syntax is

(4063:Term.byTactic:4109
     4095!:"by":4097
     (4063:Tactic.tacticSeq:4109
      (4063:Tactic.tacticSeq1Indented:4109 [(4063:tacticWeCompute_:4109 4063:"We":4109 4063:"compute":4109 [])])))

Here ! indicates that by has canonical source info. Its exact position changed slightly because we made some edits earlier in the file, but we can see the by has correct positions and indeed the goal shows up when the cursor is before b. Unfortunately all the other positions are still nonsense, and the goal doesn't show up before y, for instance.

Quotations pick up positions from the ambient syntax reference. So, let's try setting that when quoting pieces of subsyntax. We end up with this little monstrosity:

  | `(CalcFirstStep|$t:term by%$btk computation%$ctk) =>
    let byCompStx := step.raw[1]
    let tacs ← withRef ctk `(tacticSeq| We compute)
    let pf ← withRef byCompStx `(term| by%$btk $tacs)
    let pf := pf.mkInfoCanonical
    `(calcFirstStep|$t:term := $pf)

In the last step, we recursively make source info canonical using the code below. This is different from the ProofWidgets demo, as there only the top-level info is made canonical. I initially expected this not to be necessary, but it seems to be.

def Lean.SourceInfo.mkCanonical : SourceInfo → SourceInfo
  | .synthetic s e _ => .synthetic s e true
  | si => si

partial def Lean.Syntax.mkInfoCanonical : Syntax → Syntax
  | .missing => .missing
  | .node i k a => .node i.mkCanonical k (a.map mkInfoCanonical)
  | .atom i v => .atom i.mkCanonical v
  | .ident i r v p => .ident i.mkCanonical r v p

def Lean.TSyntax.mkInfoCanonical {k} : TSyntax k → TSyntax k :=
  (⟨·.raw.mkInfoCanonical⟩)

With these changes, the goal state and the calc widget show up on the custom syntax. Note that the calc widget will not work very well as it produces the default := by syntax which Calc doesn't support. Adjusting other cases of the syntax left as an exercise.

As you can see, it is extremely fiddly. Perhaps parsers running in quotations should pick up better positions automatically (e.g. by determining the leading position of (term| by%$btk ...) from the spliced by%$btk), but it is not an easy fix.

[Patrick Massot]

Thanks you very much @Wojciech Nawrocki, this is an extremely useful answer. I will study it carefully.

[Patrick Massot]

@David Thrane Christiansen I’m sure you’ll find inspiration about things to document here :wink:

[David Thrane Christiansen]

Aboslutely!

[Patrick Massot]

Note that #lean4 > System-wide Lean install is also full of hidden things to document.

[Patrick Massot]

Wojciech Nawrocki said:

Adjusting other cases of the syntax left as an exercise.

I’m making progress on this exercise but I need a bit more help when the syntax ends with repeating stuff. Where should I put the %$ctk in `(CalcFirstStep|$t:term from%$btk $prfs and from*)?

[Patrick Massot]

Actually I take back the first claim. I thought I was making progress but I’m not. I really don’t know how to get a usable ctk when the last piece of syntax is not a simple word.

[Patrick Massot]

@David Thrane Christiansen note that I tried reading https://lean-lang.org/doc/reference/latest/Notations-and-Macros/Macros/#quotation to find how to do that token quotation exercise, but it wasn’t enough for me.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Patrick Massot said:

Actually I take back the first claim. I thought I was making progress but I’m not. I really don’t know how to get a usable ctk when the last piece of syntax is not a simple word.

I think there is no right answer to where you should be getting the positions from: it's up to where you want the goal to show up in your custom syntax. Note that I also ran into the issue of "syntax is not a simple word" in the first case: by computation is technically two tokens (I think). In that case, I used step.raw[1] to get the sub-Syntax with the desired positions. Can you do something similar for from $prfs and from*?

[Patrick Massot]

I think the fundamental issue is I don’t understand the difference between btk and ctk in your example.

[Patrick Massot]

I don’t see any difference if I remove ctk from the pattern matching and replace it with btk where it’s used.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Does it help to look at the following debug info? You will see that different positions are copied if you replace ctk with btk.

  | `(CalcFirstStep|$t:term by%$btk computation%$ctk) =>
    let byCompStx := step.raw[1]
    let tacs ← withRef ctk `(tacticSeq| We compute)
    let pf ← withRef byCompStx `(term| by%$btk $tacs)
    let pf := pf.mkInfoCanonical
    logInfo m!"orig: {byCompStx.formatStx (showInfo := true)}"
    logInfo m!"pf: {pf.raw.formatStx (showInfo := true)}"
    `(calcFirstStep|$t:term := $pf)

[Patrick Massot]

I understand those are different positions of course. What I don’t understand is the impact on the displayed tactic state and displayed widgets.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Bearing in mind I haven't looked at the infotree code recently so this may not be entirely accurate, it's like this:

• The language server decides which goal to display at a position P by searching the infotree for TacticInfo nodes at position P.
• TacticInfo nodes don't store a position but rather a piece of syntax. So what it means for a TacticInfo to be "at P" is roughly that its associated syntax contains P within its span.
• When it's evaluated, a tactic stores a TacticInfo node with the syntax that caused the tactic to run.

So overall, if you produce (the syntax of) a tactic script wherein one tactic has incorrect positions, its pre/post goal state will appear at that incorrect position or not at all.

[Patrick Massot]

I understand the general idea, I was asking specifically how the difference between btk and ctk in this example mattered. But really this isn’t so important. I think I’m really unstuck here. Thank you very much for your help.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

I think if you use btk instead of ctk, the no-goals post-state coming from 'We compute' will appear on the 'by'; or something similarly broken (that's what I observed)