These are pre-emptive fixes for nightly-2024-05-01 (which doesn't exist yet) prepared using a local toolchain.
Unfortunately there are still two failing tests that I don't understand yet, in AesopTest/List.lean and AesopTest/DocLists.lean.
@JLimperg, will you be able to look at these soon? Right now it's hard to do, but in about +5 hours from now the toolchain will actually exist. :-) I'm hoping this nightly will become v4.8.0-rc1, so there is some time pressure to get this sorted. If you're busy I can take a further look, or possibly even temporarily disable the tests if they become the release blocker.
These are pre-emptive fixes for nightly-2024-05-01 (which doesn't exist yet) prepared using a local toolchain.
Unfortunately there are still two failing tests that I don't understand yet, in AesopTest/List.lean and AesopTest/DocLists.lean.
@JLimperg, will you be able to look at these soon? Right now it's hard to do, but in about +5 hours from now the toolchain will actually exist. :-) I'm hoping this nightly will become v4.8.0-rc1, so there is some time pressure to get this sorted. If you're busy I can take a further look, or possibly even temporarily disable the tests if they become the release blocker.