unindent tacticSeq

Stream: lean4

[Jon Eugster]

Is there a way to unindent a tactic Sequence? If you look at the following example where I pretty-print a tacticSeq into a string, you see that each line has indentation at the beginning, which I would like to get rid of.

import Lean

open Lean Meta Elab Command

elab "Template" tacs:tacticSeq : tactic => do
  -- Do some modification or something:
  let newTacs : TSyntax `Lean.Parser.Tactic.tacticSeq := tacs

  -- turn tactic sequence into a string:
  let template ← PrettyPrinter.ppCategory `Lean.Parser.Tactic.tacticSeq newTacs
  logInfo s!"Template:\n{template}"

example : 2 = 2 := by
  Template
    simp
    · simp
      rfl
      sorry
      rfl
  rfl

the log-info message looks like

Template:
  simp
  · simp
    rfl
    sorry
    rfl

Can I get rid of that indentation in Lean somehow? Or would I just assume that it is always exactly two spaces and just do that manually by editing the string?

[Jon Eugster]

An even shorter MWE:

import Mathlib

example (A B : Prop) (h : A ∧ B) : B → A ∨ ¬ A := by
  aesop?

Clicking on the "try this" suggestion inserts the following with wrong indentation:

import Mathlib

example (A B : Prop) (h : A ∧ B) : B → A ∨ ¬ A := by
  intro a
    simp_all only [and_true, not_true, or_false] -- error: wrong indentation

[Thomas Murrills]

See also: #std4 > TryThis widget doesn't support multi-line suggestions

[Thomas Murrills]

(Unfortunately that thread contains no solution either, but is discussing the same issue)

[Jon Eugster]

oh thanks I didnt see that before. I guess that means Ill make a javascript hack formatting the string and see if I can get away with that

[Jannis Limperg]

I've now 'fixed' this on Aesop master, in the sense that it'll do the right thing if aesop? is the only tactic on a line. For situations like have : Foo := by aesop?, more work would be needed.

[Jon Eugster]

Let me go and have a look so that I can steel your fix:wink: