aesop panic

Stream: general

[Kevin Buzzard]

Using mathlib master,

import Mathlib.Data.Set.Basic

example {I : Type} [LinearOrder I] (J K : I → Prop) [(i : I) → Decidable (J i)]
    [(i : I) → Decidable (K i)] (h : ∀ (i : I), J i → K i) (x : I → Bool) (i : I) :
  (if J i then if K i then x i else false else false) = if J i then x i else false := by aesop?

aesop works, but aesop? causes a panic on my machine, and an error in a very large font!

Screenshot-from-2023-10-28-12-35-13.png

Should this message be in #std4 ? Is this an issue with TryThis?

[Alex J. Best]

I think that Aesop needs to be updated after https://github.com/leanprover/std4/pull/215, the widget changed so at the very least Aesop needs to add some extra json to call it properly

[Alex J. Best]

maybe docs#Aesop.addTryThisTacticSeqSuggestion can be removed completely now in facvour of docs#Std.Tactic.TryThis.addSuggestion @Thomas Murrills what do you think?

[Thomas Murrills]

Hmm, the docstring says that it’s specifically to handle some bad formatting—I’ve only taken a cursory glance so I’m not sure if it’s the same bad formatting as mentioned here.

std4#215 didn’t address this issue per se, but I think it at least means code no longer needs to be copy-pasted the way it currently is in that definition, since Suggestions (the structure fed into addSuggestion(s)) can also be just raw strings now! So maybe addTacticSeqSuggestion could become more or less return addSuggestion { suggestion := (<- someSpecificPrettyPrinting stx) } until the actual underlying pretty-printing issue is fixed. But again I haven’t looked closely at the code, so I’m not sure if there are any other changes it makes.

[Jannis Limperg]

I can't repro this right now because my VSCode is borked, but as soon as it's unborked I'll fix it. Thanks for the debugging work!

[Jannis Limperg]

This is now fixed on Aesop master, but the mathlib bump is currently blocked by work on continuity (see #mathlib4 > Regression in continuity ).