format Syntax into compilable code

Stream: general

[Pavel Klimov]

I've tried PrettyPrinter.formatTactic, but sometimes it produce code which require manual edit to make it compilable. I'm unsure perhaps it's just a bug and I should report issue. So, the case is something like

  have h (p : Prop) : p → p := by {intro p'
    exact p'
  }

it's not exactly my case, but the issue is when I make syntax tree with curly braces and sequence of tactics within. It generates Format with group behavior fill. Which, by default wants to fill the line, but for some reason, it doesn't add new line if position is already outside correct indentation. It doesn't add .align true node in the format. Maybe my syntax tree is bad, maybe it's bug in the formatter. What should I do? I want to avoid manually fix spacing myself.

[Pavel Klimov]

Here is the sample where you may see the issue yourself

import Lean.Elab

elab "custom_tactic" : tactic =>
  Lean.Elab.Tactic.withMainContext do
    let env ← Lean.MonadEnv.getEnv
    let p := Lean.Parser.Tactic.tacticSeq.fn
    let input := "have h (p : Prop) : p → p := by {sorry}\napply h"
    let ictx := Lean.Parser.mkInputContext input "<anonymous>"
    let s := p.run ictx { env, options := {} }
      (Lean.Parser.getTokenTable env)
      (Lean.Parser.mkParserState input)
    let stx := s.stxStack.back
    let input1 := "intro p'\nexact p'\n"
    let ictx1 := Lean.Parser.mkInputContext input1 "<anonymous>"
    let s1 := p.run ictx1 { env, options := {} }
      (Lean.Parser.getTokenTable env)
      (Lean.Parser.mkParserState input1)
    let stx1 := s1.stxStack.back
    let replace1 : Lean.Syntax → StateM String.Pos (Option Lean.Syntax)
      | .node _ ``Lean.Parser.Tactic.tacticSorry _ => pure stx1
      | _ => pure none
    let stx2 := ((Lean.Syntax.replaceM replace1 stx).run' 0).run
    dbg_trace repr ((stx2.prettyPrint).pretty 0)
    Lean.Elab.Tactic.evalTactic stx2

theorem q2 (p : Prop) : p → p := by
  have h (p : Prop) : p → p := by {
    intro p'
    exact p'
  }
  apply h

theorem q3 (p : Prop) : p → p := by
  custom_tactic

If you remove dbg_trace, you'll see that there is no errors, so goal is proved. But, if you copy-paste resulting formated text of proof, you'll have to fix whitespaces manually.

[Ayhon]

You may want to look at how they do it in Aesop
https://github.com/leanprover-community/aesop/blob/323e9f0b9bd41161ba116fe3bff86fc464d454f2/Aesop/Util/Basic.lean#L433-L457

Nevermind, it seems like I missunderstood the question. No idea

[Pavel Klimov]

Strange, but it adds space. I have no idea where it comes from

    Aesop.addTryThisTacticSeqSuggestion stx2 { raw := stx2 : Lean.TSyntax ``Lean.Parser.Tactic.tacticSeq }

Just add it into my previous code.

[Pavel Klimov]

After noticing that for some reason Aesop format this code fine, I have noticed that while making counterexample, I have used .prettyPrint which suddenly doesn't use PrettyPrinter, so the code above is not counterexample. Here is proper one. Had to add skip to make it wrap to the next line. In my actual case line was long because statement of have itself was long.

import Aesop
import Lean.Elab

elab "custom_tactic" : tactic =>
  Lean.Elab.Tactic.withMainContext do
    let env ← Lean.MonadEnv.getEnv
    let p := Lean.Parser.Tactic.tacticSeq.fn
    let input := "have h (p : Prop) : p → p := by { intro p'; skip; skip; skip; skip; skip; skip; skip; skip; skip; skip; skip; skip; exact p' }\napply h"
    let ictx := Lean.Parser.mkInputContext input "<anonymous>"
    let s := p.run ictx { env, options := {} }
      (Lean.Parser.getTokenTable env)
      (Lean.Parser.mkParserState input)
    let stx := s.stxStack.back
    let fmt ← Lean.PrettyPrinter.formatTactic stx
    dbg_trace repr (toString fmt)
    dbg_trace fmt
    Aesop.addTryThisTacticSeqSuggestion stx { raw := stx : Lean.TSyntax ``Lean.Parser.Tactic.tacticSeq }
    Lean.Elab.Tactic.evalTactic stx

theorem q2 (p : Prop) : p → p := by
  have h (p : Prop) : p → p := by {
    intro p'
    exact p'
  }
  apply h

theorem q3 (p : Prop) : p → p := by
  custom_tactic

it produce

  have h (p : Prop) : p → p := by {intro p'; skip; skip; skip; skip; skip; skip; skip; skip; skip; skip; skip; skip;
    exact p'
  }
  apply h

which is incorrect, because intro p' should be aligned.