search

leanprover-community / aesop

White-box automation for Lean 4
Apache License 2.0
155 stars 25 forks source link

chore: port latest fixes from nightly-testing #97

Closed semorrison closed 5 months ago

semorrison commented 5 months ago

These are fixes on the nightly-testing branch, mostly due to @JLimperg. This PR is merging them into the bump/v4.6.0 release ready for the end of the month.

(@JLimperg, even though these are your changes, can I leave this PR to you to sanity check and merge?)

JLimperg commented 5 months ago

Can I instead rebase nightly-testing and bump/v4.6.0 onto master? Or will that mess up your setup?

semorrison commented 5 months ago

That should be fine. The only important invariant is that bump/v4.6.0 always works, and all content on it has been reviewed.

(In particular, no bots interact with aesop at all. If Mathlib's bump/v4.6.0 or nightly-testing branch need lake update aesop, that happens manually.)

JLimperg commented 5 months ago

As discussed on Zulip, I rebased and force-pushed bump/v4.6.0 so that it contains essentially the contents of this PR. The only non-cosmetic remaining difference is that bump/v4.6.0 depends on std@bump/v4.6.0 at a later commit than this PR.