PSA: using Aesop for auto-params

Stream: mathlib4

[Jannis Limperg]

By default, Aesop can "succeed" without solving the goal. It seems like this leads to nasty universe issues when Aesop is used as an auto-param, as discussed here. So if you use Aesop as an auto-param, please use options := { terminal := true }, which makes Aesop fail if it can't solve the goal. See !4#2527 for an example.

Currently, the error message when Aesop fails with terminal := true is very uninformative, but I'll fix this shortly.

[Floris van Doorn]

I think we should adopt a mathlib4 policy that discourages/disallows usage of aesop nonterminally, for the same reason that we disallow nonterminal simp: it makes proofs fragile. Note that aesop calls simp.

[Jannis Limperg]

Yes, 100%. Nonterminal aesop is even worse than nonterminal simp.