question about aesop behavior

Stream: new members

[Alex Gu]

I was running a proof with lake env lean xxx.lean and hit a warning aesop: maximum number of rule applications (200) reached. So I guess this means that aesop did not find the proof, but my command still didn't throw any errors (only warnings). Is this an intended behavior? Is there a way to count this as an error?

Here is the example I am using (I'm not sure how to convert it to a #mwe without Mathlib): https://pastebin.com/CLpAmdB7

[Alex Gu]

Ah, I think I confused myself. It seems to me that this proof is actually correct, just that "aesop" rewrites some of the hypotheses, and then "omega" closes the goal after that. I had thought "aesop" is a no-op if it fails, but seems I'm mistaken :)