Aesop status updates

Stream: nightly-testing

[Kim Morrison]

@Jannis Limperg, there are many failures in lake test on the nightly-testing branch of Aesop. A superficial look suggests they are mostly formatting issues. Would you mind taking a look?

[Jannis Limperg]

Seems to be my old nemesis, tactic sequence formatting in Try This suggestions. This was always broken, but it seems nightly made changes that breaks it in a different way and defeats my previous workaround (lean4#10150). I'd appreciate if someone who's familiar with this code could take a look at the core issue.

[Marc Huisinga]

I've commented on the issue.