TryThis.addSuggestion mis-indents tactic sequences

[JLimperg]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• [X] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues
• [X] Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to Mathlib or Batteries.
• [X] Test your test case against the latest nightly release, for example on https://live.lean-lang.org/#project=lean-nightly (You can also use the settings there to switch to “Lean nightly”)

Description

The TryThis suggestions API mis-indents tactic sequences. This means that (a) the info message is formatted incorrectly and (b) when clicking the code action, the tactic sequence is inserted in the wrong place, creating a syntax error. MWE:

import Lean

open Lean Lean.Meta.Tactic

elab "suggest_tac_seq" : tactic => do
  let tacSeq ← `(tacticSeq|
    skip
    skip)
  TryThis.addSuggestion (← getRef) {
    suggestion := .tsyntax tacSeq
  }

example : True := by
  suggest_tac_seq
  trivial

/-
(a) Info message:
Try this:
    skip
      skip

(b) Result of applying the code action:
example : True := by
    skip
    skip
  trivial
-/

There are also more challenging examples, but I wouldn't expect these to be formatted correctly (though this one actually remains syntactically correct).

import Lean

open Lean Lean.Meta.Tactic

elab "suggest_tac_seq" : tactic => do
  let tacSeq ← `(tacticSeq|
    skip
    skip)
  TryThis.addSuggestion (← getRef) {
    suggestion := .tsyntax tacSeq
  }

example : True := by
  first | suggest_tac_seq | fail
  trivial

/-
example : True := by
  first | 
    skip
    skip | fail
  trivial
-/

Context

aesop? uses this functionality pervasively. I previously worked around the indentation issues, but nightly breaks the workaround (Zulip).

Versions

Lean 4.24.0-nightly-2025-08-26
Target: x86_64-unknown-linux-gnu

Impact

Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.

[mhuisi]

I previously worked around the indentation issues, but nightly breaks the workaround (Zulip).

Can you say more about the workaround? When I try your example above on 4.22.0, the message is formatted correctly, but applying the suggestion also leads to a broken tactic script (i.e. the message displays something different from what is actually applied to the document). #9966 should merely ensure that the message matches what is actually inserted, not change anything about what is inserted.

[JLimperg]

The workaround was this function:

def addTryThisTacticSeqSuggestion (ref : Syntax)
    (suggestion : TSyntax ``Lean.Parser.Tactic.tacticSeq)
    (origSpan? : Option Syntax := none) : MetaM Unit := do
  let fmt ← PrettyPrinter.ppCategory ``Lean.Parser.Tactic.tacticSeq suggestion
  let msgText := fmt.pretty (indent := 0) (column := 0)
  if let some range := (origSpan?.getD ref).getRange? then
    let map ← getFileMap
    let (indent, column) := Lean.Meta.Tactic.TryThis.getIndentAndColumn map range
    let text := fmt.pretty (indent := indent) (column := column)
    let suggestion := {
      -- HACK: The `tacticSeq` syntax category is pretty-printed with each line
      -- indented by two spaces (for some reason), so we remove this
      -- indentation.
      suggestion := .string $ dedent text
      toCodeActionTitle? := some λ _ => "Replace aesop with the proof it found"
      messageData? := some msgText
      preInfo? := "  "
    }
    Lean.Meta.Tactic.TryThis.addSuggestion ref suggestion (origSpan? := origSpan?)
      (header := "Try this:\n")
where
  dedent (s : String) : String :=
    s.splitOn "\n"
    |>.map (λ line => line.dropPrefix? "  " |>.map (·.toString) |>.getD line)
    |> String.intercalate "\n"

Basically, manually dedenting the suggestion to work around the pretty-printer adding indentation for tactic seqs.

[mhuisi]

Thanks! I'll look into it.

[mhuisi]

@JLimperg I've looked into the root cause for a bit but didn't find a good solution, unfortunately. #10157 re-adds support for messageData? so that your hack works again and aesop is unblocked:

import Lean

open Lean Lean.Meta.Tactic

def addTryThisTacticSeqSuggestion (ref : Syntax)
    (suggestion : TSyntax ``Lean.Parser.Tactic.tacticSeq)
    (origSpan? : Option Syntax := none) : MetaM Unit := do
  let fmt ← PrettyPrinter.ppCategory ``Lean.Parser.Tactic.tacticSeq suggestion
  let msgText := fmt.pretty (indent := 0) (column := 0)
  if let some range := (origSpan?.getD ref).getRange? then
    let map ← getFileMap
    let (indent, column) := Lean.Meta.Tactic.TryThis.getIndentAndColumn map range
    let text := fmt.pretty (indent := indent) (column := column)
    let suggestion := {
      -- HACK: The `tacticSeq` syntax category is pretty-printed with each line
      -- indented by two spaces (for some reason), so we remove this
      -- indentation.
      suggestion := .string $ dedent text
      toCodeActionTitle? := some λ _ => "Replace aesop with the proof it found"
      messageData? := some $ dedent msgText
    }
    Lean.Meta.Tactic.TryThis.addSuggestion ref suggestion (origSpan? := origSpan?)
      (header := "Try this:")
where
  dedent (s : String) : String :=
    s.splitOn "\n"
    |>.map (λ line => line.dropPrefix? "  " |>.map (·.toString) |>.getD line)
    |> String.intercalate "\n"

elab "suggest_tac_seq" : tactic => do
  let tacSeq ← `(tacticSeq|
    skip
    skip)
  addTryThisTacticSeqSuggestion (← getRef) tacSeq

example : True := by
  suggest_tac_seq
  trivial

I hope that we can clean this up in the future when this issue is fixed, though.

[robsimmons]

I believe this is sufficiently related to not be another issue. Quick fixing the following in VSCode:

theorem simpleEquality : {P Q : Prop} → P = (P ∨ False) := by exact?

gives the following broken code:

theorem simpleEquality : {P Q : Prop} → P = (P ∨ False) := by exact fun {P Q} =>
  Eq.symm (or_false P)

it would work fine if we added parens

theorem simpleEquality : {P Q : Prop} → P = (P ∨ False) := by exact (fun {P Q} =>
  Eq.symm (or_false P))

or avoided the linebreak:

theorem simpleEquality : {P Q : Prop} → P = (P ∨ False) := by exact fun {P Q} => Eq.symm (or_false P)

[eric-wieser]

Here's another example:

import Lean

open Lean Elab Tactic in
elab "try_long_this" : tactic => do
  let g ← getMainGoal
  g.admit
  let id := mkIdent `id
  Meta.Tactic.TryThis.addSuggestion (← getRef) {suggestion := .tsyntax <| ← `(tactic|
      (skip;
        -- Needs to be sufficiently long. This comment doesn't matter.
        exact $id $id $id $id $id $id $id $id $id $id $id $id $id $id $id $id sorry)
  )}

-- ok
example : True := by try_long_this

-- substitution is illegal
example : True := by (skip;
  exact id id id id id id id id id id id id id id id id sorry)

-- should be either
example : True := by (skip;
                        exact id id id id id id id id id id id id id id id id sorry)

-- or
example : True := by
  (skip;
    exact id id id id id id id id id id id id id id id id sorry)