Aesop script (`aesop?`) formatting issue

Stream: lean4

[Peiyang Song]

When using aesop? (and when aesop? successfully finds a proof), I observed the proof script in the infoview having a weird format. Specially there are multiple unexpected new lines & indentations (see screenshot below for a minimal example).

aesop_format_issue.png

FYI I tried aesop versions at commits 056ca0fa8f5585539d0b940f532d9750c3a2270f (which supports Lean v4.7.0-rc1) and ca8e6e3244120cd1137705552b72446be3cd0824 (latest commit, which supports Lean v4.7.0-rc2). The above issue appeared on both. I feel this may look like a potential bug? Gently ping @Jannis Limperg who is the author of aesop :)

[Siddhartha Gadgil]

I have found this too. In particular rename_i messes up badly with some arguments on a new line so interpreted as tactic calls (hence errors).

[Mario Carneiro]

Don't put MWEs in screenshots

[Peiyang Song]

Thank you for the tip. Here is a typed MWE.

import Aesop

example (h : PEmpty.{u}) : α := by
  aesop?

[Eric Rodriguez]

I wonder if this is the formatter being optimised for some weird width

[Jannis Limperg]

The mis-indentation of the first tactic in the infoview is a known bug. I tried fairly hard to fix it but didn't manage, so I'm not inclined to put more work into this. Relevant code is here in case someone wants to take a look.

[Jannis Limperg]

The linebreaks look like intended behaviour of the formatter, but they probably hurt more than they help. Maybe I can direct the formatter to use a very large line width to get around this.

[Jannis Limperg]

Siddhartha Gadgil said:

I have found this too. In particular rename_i messes up badly with some arguments on a new line so interpreted as tactic calls (hence errors).

This is very bad since it's not just a cosmetic issue. Could you give me an MWE for this (doesn't need to be super minimal)?

[Jannis Limperg]

(I'm on holiday for a week, so won't be super quick to fix these issues, but they're going on the list.)

[Peiyang Song]

I see! Thank you very much Jannis for the detailed information!

[Kevin Buzzard]

This is very bad since it's not just a cosmetic issue. Could you give me an MWE for this (doesn't need to be super minimal)?

I just tried some random thing and got lucky first time:

import Mathlib.Tactic

theorem foo (A B : Set ℕ) (h : ∀ n, n ∈ A → n + 1 ∈ B) (h2 : ∀ m, m ∈ B → m + 1 ∈ A)
    (h3 : 3 ∈ A) : 7 ∈ A := by
  aesop?
/-
Try this:
    apply
    h2
  apply
    h
  simp_all only
-/

If I click on the blue output in the infoview then it doesn't compile because of the wacky newlines/spacing (the first apply is indented too much). Edit: oh, sorry, is this the "first tactic misaligned" bug, not the more complicated one?

[Josha Dekker]

I recently had a similar problem with formatting (multiple lines, renaming, indentation) where it also suggested some ‘unhygenic’ stuff. Is the desired approach for Mathlib to just write Aesop and forget about it, or to find a way to get rid of the ‘unhygenic’ stuff manually? (I’m assuming we don’t want ‘unhygenic’ in Mathlib?). I’m not near Mathlib now, could try to reproduce this issue tomorrow if wanted.

[Kevin Buzzard]

In the past I've used Aesop when developing, then used Aesop? and then manually tidied up the output when PRing.

[Siddhartha Gadgil]

Jannis Limperg said:

Siddhartha Gadgil said:

I have found this too. In particular rename_i messes up badly with some arguments on a new line so interpreted as tactic calls (hence errors).

This is very bad since it's not just a cosmetic issue. Could you give me an MWE for this (doesn't need to be super minimal)?

There seems to be a short MWE:

variable {α : Type}[LinearOrder α]
example (x a: α )(l₁ l₂ : List α) : x = a ∨ x ∈ l₁ ∨ x ∈ l₂ ↔
  x ∈ l₁ ∨ x = a ∨ x ∈ l₂ := by aesop?

[Siddhartha Gadgil]

@Jannis Limperg In the above the arguments of rename_i overflow the end, go to the next line and give errors.

[Damiano Testa]

Peiyang Song said:

Thank you for the tip. Here is a typed MWE.

import Aesop

example (h : PEmpty.{u}) : α := by
  aesop?

For me, the given example is also a failure.

[Damiano Testa]

This specific case could be resolved simply by "unindenting" the first have.

[Damiano Testa]

That resolves the syntax errors. Even then, "pretty" printing is still far...

[Jannis Limperg]

I finally fixed this, sorry for the delay. aesop? should be usable again once Mathlib updates to the current version. Turns out I was passing the wrong arguments to the pretty-printer, so it was using a very small line width.

[Kim Morrison]

#13303 is the Mathlib bump