CI status

Stream: condensed mathematics

[Ben Toner]

With the bump merged, here's a summary of where things are at with the CI:

• All build failures were due to the github machines running out of memory. Now that the CI is using the Hoskinson runners (thank you, Johan and Scott!), there shouldn't be any more problems.
• Caches of oleans will now be stored for non-master branches... and the clean-up script is now updated so they won't then get deleted (thanks @Rob Lewis!)
• The recent builds on master don't seem to be finding the right olean caches -- I'll look at this sometime if it persists.
• It would probably make sense to build in CI with a -TXXXXXX flag like mathlib does, even if XXXXXX is something high like 400000. Currently we don't specify any -TXXXXXX flag.
• Likewise, when building locally, it might be a good idea to fix slow proofs. You can detect them by building, e.g., like this:

leanpkg configure
leanproject get-mathlib-cache
leanproject clean
lean -T150000 --make src

I won't have much time in the next couple of weeks but everything should be working anyway.

[Johan Commelin]

Thanks for this report! I agree the speeding up slow proofs is a good thing to prioritize, because it will pay off with every future compile.

[Ben Toner]

With the new approval workflow on master, the "update nolints" and "bump mathlib" actions have broken. Assuming you still want these, I can change them so that they do pull requests rather than committing directly to master.

In mathlib, the way the "update nolints" action works is that leanprover-community-bot makes a pull request, which it then tell bors to merge. Do you want something similar where leanprover-community-bot approves its own pull requests? If the latter, can you please add lean-community-bot to the set of people who can approve pull requests?

[Johan Commelin]

Yup, I'll add the bot (assuming I can figure out how)

[Johan Commelin]

I managed this:
image.png
Is that good enough?

[Ben Toner]

That looks like a much better option - should mean I don't have to change anything. Testing now...

[Ben Toner]

It seems like this setting should be good enough but it doesn't work. I'll have to come back to this another day.