aesop in Mathlib

Stream: mathlib4

[Newell Jensen]

For contributing code, are there any conventions to follow when using aesop in proofs? The reasonable thing to me would be to use just aesop in the event that aesop?'s output is unwieldy.

[Scott Morrison]

Yes, it is fine to use aesop dirrctly.

[Scott Morrison]

(as long as it is reasonably fast. dont't increase maxheartbeats or anything!)

[Newell Jensen]

Speaking of setting maxHeartbeats, obviously this is in Mathlib in certain areas so I take it that this is only in conjunction with aesop, correct?

[Scott Morrison]

I think all of our maxHeartbeats are leftovers from porting hacks.

[Scott Morrison]

Ideally there will never be genuinely new ones.

[Scott Morrison]

"Ideally" may be doing a lot of work there. :-)

[Junyan Xu]

Some are being added here (a category theory PR).

[Joël Riou]

Junyan Xu said:

Some are being added here (a category theory PR).

I have managed to remove these two set_option maxHeartbeats 400000.