search

leanprover-community / aesop

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

chore: adaptations for leanprover/lean4#2714 #81

Closed semorrison closed 8 months ago

semorrison commented 8 months ago

This has already been merged in nightly-testing, but I would like an approval in time for the next Lean version release next week if possible.

JLimperg commented 8 months ago

What is this nightly-testing exactly? A staging branch for the next Lean release?

JLimperg commented 8 months ago

The actual change is obviously fine. One test seems to be broken (and std as well), but the breakage seems to be trivial and unrelated to this change.

semorrison commented 8 months ago

What is this nightly-testing exactly? A staging branch for the next Lean release?

Sorry, yes, it's a branch of aesop that Mathlib's nightly-testing can depend on, and includes all patches for Lean PRs that have landed in nightlies but not yet joined a release that aesop will bump to.

semorrison commented 8 months ago

I don't really have a solution at present for working CI for these sort of PRs. :-(

JLimperg commented 8 months ago

Superseded by #83.