Incorrect indents when processing Syntax

Stream: lean4

[Eric Wieser]

What's going on here?

import Lean

open Lean Meta

partial def stripWithReducible {m} [Monad m] [MonadRef m] [MonadQuotation m] (s : Syntax) : m Syntax :=
  s.replaceM fun
    | `(tactic| with_reducible $tacs:tacticSeq) => do
      let tacs := ⟨← stripWithReducible tacs⟩
      return some <| ← `(tactic| $tacs)
    | _ => return none

/--
info: by
    let x✝ := "hello"
    let y✝ := "world"
  let z✝ := "oh no"
  exact "where is my indent"
-/
#guard_msgs in
run_cmd Elab.Command.liftTermElabM do
  let t ← stripWithReducible <| ←`(by
    with_reducible
      let x := "hello"
      let y := "world"
    with_reducible
      let z := "oh no"
    exact "where is my indent")
  Lean.logInfo t

• The resulting syntax has invalid indentation
• The guard_msgss is complaining despite the fact the output is exactly what it claims to expect.

[Damiano Testa]

The Syntax for t contains twice the nodes Lean.Parser.Tactic.tacticSeq Lean.Parser.Tactic.tacticSeq1Indented, since, I think, your match only removed the node corresponding to with_reducible, but not also the formatting.

[Damiano Testa]

This is the syntax tree for t (I hope that this is fairly self-explanatory):

inspect: 'by
    let x✝ := "hello"
    let y✝ := "world"
  let z✝ := "oh no"
  exact "where is my indent"'

node Lean.Parser.Term.byTactic, synthetic: false
|-atom synthetic: false-- 'by'
|-node Lean.Parser.Tactic.tacticSeq, synthetic: false
|   |-node Lean.Parser.Tactic.tacticSeq1Indented, synthetic: false
|   |   |-node null, synthetic: false
|   |   |   |-node Lean.Parser.Tactic.tacticSeq, synthetic: false
|   |   |   |   |-node Lean.Parser.Tactic.tacticSeq1Indented, synthetic: false
|   |   |   |   |   |-node null, synthetic: false
|   |   |   |   |   |   |-node Lean.Parser.Tactic.tacticLet_, synthetic: false
|   |   |   |   |   |   |   |-atom synthetic: false-- 'let'
|   |   |   |   |   |   |   |-node Lean.Parser.Term.letDecl, synthetic: false
|   |   |   |   |   |   |   |   |-node Lean.Parser.Term.letIdDecl, synthetic: false
|   |   |   |   |   |   |   |   |   |-ident synthetic: false-- (x._@.Mathlib.Tactic.mwe_linter._hyg.393,x)
|   |   |   |   |   |   |   |   |   |-node null, synthetic: false
|   |   |   |   |   |   |   |   |   |-node null, synthetic: false
|   |   |   |   |   |   |   |   |   |-atom synthetic: false-- ':='
|   |   |   |   |   |   |   |   |   |-node str, synthetic: false
|   |   |   |   |   |   |   |   |   |   |-atom synthetic: false-- '"hello"'
|   |   |   |   |   |   |-node null, synthetic: false
|   |   |   |   |   |   |-node Lean.Parser.Tactic.tacticLet_, synthetic: false
|   |   |   |   |   |   |   |-atom synthetic: false-- 'let'
|   |   |   |   |   |   |   |-node Lean.Parser.Term.letDecl, synthetic: false
|   |   |   |   |   |   |   |   |-node Lean.Parser.Term.letIdDecl, synthetic: false
|   |   |   |   |   |   |   |   |   |-ident synthetic: false-- (y._@.Mathlib.Tactic.mwe_linter._hyg.393,y)
|   |   |   |   |   |   |   |   |   |-node null, synthetic: false
|   |   |   |   |   |   |   |   |   |-node null, synthetic: false
|   |   |   |   |   |   |   |   |   |-atom synthetic: false-- ':='
|   |   |   |   |   |   |   |   |   |-node str, synthetic: false
|   |   |   |   |   |   |   |   |   |   |-atom synthetic: false-- '"world"'
|   |   |   |-node null, synthetic: false
|   |   |   |-node Lean.Parser.Tactic.tacticSeq, synthetic: false
|   |   |   |   |-node Lean.Parser.Tactic.tacticSeq1Indented, synthetic: false
|   |   |   |   |   |-node null, synthetic: false
|   |   |   |   |   |   |-node Lean.Parser.Tactic.tacticLet_, synthetic: false
|   |   |   |   |   |   |   |-atom synthetic: false-- 'let'
|   |   |   |   |   |   |   |-node Lean.Parser.Term.letDecl, synthetic: false
|   |   |   |   |   |   |   |   |-node Lean.Parser.Term.letIdDecl, synthetic: false
|   |   |   |   |   |   |   |   |   |-ident synthetic: false-- (z._@.Mathlib.Tactic.mwe_linter._hyg.393,z)
|   |   |   |   |   |   |   |   |   |-node null, synthetic: false
|   |   |   |   |   |   |   |   |   |-node null, synthetic: false
|   |   |   |   |   |   |   |   |   |-atom synthetic: false-- ':='
|   |   |   |   |   |   |   |   |   |-node str, synthetic: false
|   |   |   |   |   |   |   |   |   |   |-atom synthetic: false-- '"oh no"'
|   |   |   |-node null, synthetic: false
|   |   |   |-node Lean.Parser.Tactic.exact, synthetic: false
|   |   |   |   |-atom synthetic: false-- 'exact'
|   |   |   |   |-node str, synthetic: false
|   |   |   |   |   |-atom synthetic: false-- '"where is my indent"'

[Eric Wieser]

I figured it might be something like this; so I guess my question is now "are there any helper functions to disassemble this in the right way?"

[Damiano Testa]

Actually, I am investigating where the extra indent is inserted, but it seems that it is not at the return some <| ← `(tactic| $tacs) step, which puzzles me.

[Eric Wieser]

I think the indent might just be a pretty-printer bug; Aesop has a workaround somewhere that refers to indents and tacticSeq

[Eric Wieser]

But perhaps the Syntax I've assembled is illegal so the pretty-printer behavior is not specified.

[Damiano Testa]

Ah, you are saying that it might be last logInfo step that does that?

[Damiano Testa]

Btw, I noticed that most syntax trees are "padded" with null nodes. I wonder if that is what you are missing.

[Damiano Testa]

In case you are curious, this is what the syntax tree for the syntax that you wrote before stripping with reducible:

inspect: 'by
  with_reducible
    let x✝ := "hello"
    let y✝ := "world"
  with_reducible let z✝ := "oh no"
  exact "where is my indent"'

node Lean.Parser.Term.byTactic, synthetic: false
|-atom synthetic: false-- 'by'
|-node Lean.Parser.Tactic.tacticSeq, synthetic: false
|   |-node Lean.Parser.Tactic.tacticSeq1Indented, synthetic: false
|   |   |-node null, synthetic: false
|   |   |   |-node Lean.Parser.Tactic.withReducible, synthetic: false
|   |   |   |   |-atom synthetic: false-- 'with_reducible'
|   |   |   |   |-node Lean.Parser.Tactic.tacticSeq, synthetic: false
|   |   |   |   |   |-node Lean.Parser.Tactic.tacticSeq1Indented, synthetic: false
|   |   |   |   |   |   |-node null, synthetic: false
|   |   |   |   |   |   |   |-node Lean.Parser.Tactic.tacticLet_, synthetic: false
|   |   |   |   |   |   |   |   |-atom synthetic: false-- 'let'
|   |   |   |   |   |   |   |   |-node Lean.Parser.Term.letDecl, synthetic: false
|   |   |   |   |   |   |   |   |   |-node Lean.Parser.Term.letIdDecl, synthetic: false
|   |   |   |   |   |   |   |   |   |   |-ident synthetic: false-- (x._@.Mathlib.Tactic.mwe_linter._hyg.238,x)
|   |   |   |   |   |   |   |   |   |   |-node null, synthetic: false
|   |   |   |   |   |   |   |   |   |   |-node null, synthetic: false
|   |   |   |   |   |   |   |   |   |   |-atom synthetic: false-- ':='
|   |   |   |   |   |   |   |   |   |   |-node str, synthetic: false
|   |   |   |   |   |   |   |   |   |   |   |-atom synthetic: false-- '"hello"'
|   |   |   |   |   |   |   |-node null, synthetic: false
|   |   |   |   |   |   |   |-node Lean.Parser.Tactic.tacticLet_, synthetic: false
|   |   |   |   |   |   |   |   |-atom synthetic: false-- 'let'
|   |   |   |   |   |   |   |   |-node Lean.Parser.Term.letDecl, synthetic: false
|   |   |   |   |   |   |   |   |   |-node Lean.Parser.Term.letIdDecl, synthetic: false
|   |   |   |   |   |   |   |   |   |   |-ident synthetic: false-- (y._@.Mathlib.Tactic.mwe_linter._hyg.238,y)
|   |   |   |   |   |   |   |   |   |   |-node null, synthetic: false
|   |   |   |   |   |   |   |   |   |   |-node null, synthetic: false
|   |   |   |   |   |   |   |   |   |   |-atom synthetic: false-- ':='
|   |   |   |   |   |   |   |   |   |   |-node str, synthetic: false
|   |   |   |   |   |   |   |   |   |   |   |-atom synthetic: false-- '"world"'
|   |   |   |-node null, synthetic: false
|   |   |   |-node Lean.Parser.Tactic.withReducible, synthetic: false
|   |   |   |   |-atom synthetic: false-- 'with_reducible'
|   |   |   |   |-node Lean.Parser.Tactic.tacticSeq, synthetic: false
|   |   |   |   |   |-node Lean.Parser.Tactic.tacticSeq1Indented, synthetic: false
|   |   |   |   |   |   |-node null, synthetic: false
|   |   |   |   |   |   |   |-node Lean.Parser.Tactic.tacticLet_, synthetic: false
|   |   |   |   |   |   |   |   |-atom synthetic: false-- 'let'
|   |   |   |   |   |   |   |   |-node Lean.Parser.Term.letDecl, synthetic: false
|   |   |   |   |   |   |   |   |   |-node Lean.Parser.Term.letIdDecl, synthetic: false
|   |   |   |   |   |   |   |   |   |   |-ident synthetic: false-- (z._@.Mathlib.Tactic.mwe_linter._hyg.238,z)
|   |   |   |   |   |   |   |   |   |   |-node null, synthetic: false
|   |   |   |   |   |   |   |   |   |   |-node null, synthetic: false
|   |   |   |   |   |   |   |   |   |   |-atom synthetic: false-- ':='
|   |   |   |   |   |   |   |   |   |   |-node str, synthetic: false
|   |   |   |   |   |   |   |   |   |   |   |-atom synthetic: false-- '"oh no"'
|   |   |   |-node null, synthetic: false
|   |   |   |-node Lean.Parser.Tactic.exact, synthetic: false
|   |   |   |   |-atom synthetic: false-- 'exact'
|   |   |   |   |-node str, synthetic: false
|   |   |   |   |   |-atom synthetic: false-- '"where is my indent"'

[Mario Carneiro]

@Eric Wieser said:

But perhaps the Syntax I've assembled is illegal so the pretty-printer behavior is not specified.

yes, you constructed invalid syntax here because $tacs is a tacticSeq and you used it as a tactic

[Mario Carneiro]

I think there is a special hack in the `(tactic| ...) syntax quotation to allow this to work even though it is not syntactically correct, because several tactic-taking functions like elabTactic also work on tacticSeq. However this is not one of them - you can't just put multiple tacticSeqs in a single tacticSeq without some kind of grouping like (...)

[Mario Carneiro]

What exactly were you expecting to get?

[Eric Wieser]

Mario Carneiro said:

What exactly were you expecting to get?

Whoops, I should have started with that. I wanted to end up with

by
  let x✝ := "hello"
  let y✝ := "world"
  let z✝ := "oh no"
  exact "where is my indent"

[Eric Wieser]

Mario Carneiro said:

I think there is a special hack in the `(tactic| ...) syntax quotation to allow this to work even though it is not syntactically correct, because several tactic-taking functions like elabTactic also work on tacticSeq. However this is not one of them - you can't just put multiple tacticSeqs in a single tacticSeq without some kind of grouping like (...)

Ouch; I was operating on the assumption that `(tactic| ...) would give an error if I did anything illegal.

[Mario Carneiro]

oh, also you kinda lied to the typechecker with this line

      let tacs := ⟨← stripWithReducible tacs⟩

which is converting a Syntax to TSyntax `tactic even though it's actually a TSyntax `tacticSeq

[Eric Wieser]

Ah, good point

[Mario Carneiro]

I'm not observing your second issue though, #guard_msgs is silent on the original example

[Eric Wieser]

I think this is a caching issue that I seem to keep running into; you can end up with info messages stuck in vscode from a previous compilation

[Kyle Miller]

This isn't relevant to this thread, but, speaking of caching issues, here is a fun syntax highlighting one I had the other day until I restarted Lean:

image.png

[Eric Wieser]

(I ended up just hacking with the raw syntax objects to solve my problem, so I am ok with this thread being derailed)