aesop

Stream: nightly-testing

[Kim Morrison]

@Jannis Limperg, I ran into trouble bumping Aesop to v4.11.0-rc1, because of some failing tests. Could you take a look at https://github.com/leanprover-community/aesop/pull/150?

[Kim Morrison]

If I can get the ProofWidgets problem sorted out, I'm probably happy to proceed without these tests and we can sort them out later, but in the meantime I'm stuck on bumping Mathlib so won't immediately merge.

[Jannis Limperg]

Fixed now, thanks for the ping.

[Kim Morrison]

@Jannis Limperg, your changes in https://github.com/leanprover-community/aesop/pull/184 conflict with changes already made in nightly-testing, because of changes to how we pass simp configurations around.

Would you be able to take a look at merging master into nightly-testing? If you won't have a change to look at this in the next few days, let me know and I'll try to find time to investigate.

[Kim Morrison]

@Jannis Limperg, cancel that request, I did it, it wasn't too bad.

[Jannis Limperg]

Thank you so much!