Zulip Chat Archive

Stream: general

Topic: mathlib broke

Simon Hudon (Feb 27 2018 at 09:53):

I'm trying to build mathlib with the latest lean-nightly and data/set/countable.lean seems to be broken. Did someone else try the latest nightly (in last 9 hours or so)?

Violeta Hernández (Dec 09 2021 at 20:45):

This PR failed at a completely unrelated point, at presheaves. Gives a deterministic timeout. I have no idea why, nor how to fix it.

Andrew Yang (Dec 09 2021 at 20:50):

When merging PRs into master, bors would bundle a bunch of approved PR and try to run CI on it. If it failed it might be someone else's PR that is failing. If you see "Build failed (retrying...):", your PR is probably still in queue and bors will try later with a smaller bunch.

Andrew Yang (Dec 09 2021 at 20:55):

That said, algebraic_geometry/presheafed_space/has_colimits.lean has also been giving me some deterministic timeouts that are unreproducible on my local machine, and I will probably try to make it faster in the near future.

Adam Topaz (Dec 09 2021 at 21:17):

What's the offending proof in that file?

Andrew Yang (Dec 09 2021 at 21:19):

Its docs#algebraic_geometry.PresheafedSpace.colimit_cocone_is_colimit.
Breaking the definition up probably helps.

Adam Topaz (Dec 09 2021 at 21:21):

Yeah, it seems that desc in this def is nested 3 deep

Adam Topaz (Dec 09 2021 at 21:22):

Although the proof of naturality of c is just a term, so I don't know if that's the issue.

Violeta Hernández (Dec 10 2021 at 01:11):

I know pretty much nilch about categories, so I don't think I can help much here

Eric Wieser (Dec 10 2021 at 10:46):

This failure is starting to affect a lot of CI runs

Andrew Yang (Dec 10 2021 at 10:50):

Hopefully #10703 helps?

Violeta Hernández (Dec 10 2021 at 17:08):

Currently restarting my own PR, hopefully that fixes it

Anatole Dedecker (Dec 10 2021 at 17:10):

If not you should try merging master

Notification Bot (Dec 13 2021 at 13:17):

Violeta Hernández has marked this topic as unresolved.

Violeta Hernández (Dec 13 2021 at 13:17):

I think mathlib broke again?

Violeta Hernández (Dec 13 2021 at 13:18):

My PR #10745 failed for something entirely unrelated

Violeta Hernández (Dec 13 2021 at 13:18):

A type mismatch in analysis/convex/strict

Yaël Dillies (Dec 13 2021 at 13:18):

Oh? That's my file.

Yaël Dillies (Dec 13 2021 at 13:19):

Can you link to the logs?

Violeta Hernández (Dec 13 2021 at 13:19):

https://github.com/leanprover-community/mathlib/runs/4506182791?check_suite_focus=true

Violeta Hernández (Dec 13 2021 at 13:20):

Actually, does this mean that mathlib itself does not compile right now?

Violeta Hernández (Dec 13 2021 at 13:20):

Or does it just mean that there's some other broken PRs out there?

Yaël Dillies (Dec 13 2021 at 13:20):

That looks like it's because of #10740, but this one hasn't been merged yet :thinking:

Yaël Dillies (Dec 13 2021 at 13:22):

Oh yeah whoops can someone get #10740 off the queue?

Yaël Dillies (Dec 13 2021 at 13:22):

@maintainers

Yaël Dillies (Dec 13 2021 at 13:23):

I wasn't expecting Johan's tornado of bors merge this morning :sweat_smile:

Yaël Dillies (Dec 13 2021 at 13:24):

Thanks

Johan Commelin (Dec 13 2021 at 13:25):

Whoops, my apologies for borsifying a bad PR.

Yaël Dillies (Dec 13 2021 at 13:26):

You couldn't know #10648 and #10740 were incompatible. That's my bad!

Last updated: Dec 20 2023 at 11:08 UTC