leanprover-contrib

Stream: general

[Yaël Dillies]

https://github.com/leanprover-contrib/leanprover-contrib does not compile. Hence con-nf, that we just added to the list of projects, does not show up. Anybody knows what's up?

[Eric Wieser]

This was broken by a lean release occurring with no associated mathlib release (which was my fault for causing a bad lean release)

[Yaël Dillies]

Ah so this is getting fixed soon given that 3.46 is out?

[Eric Wieser]

I'll have a go at fixing it

[Eric Wieser]

Also, @Violeta Hernández has broken it by creating a branch called branch#lean-3.46

[Eric Wieser]

I think the first breakage was because I created the branch called branch#lean-3.44.0-upgrade

[Eric Wieser]

@Violeta Hernández, I've deleted your branch, and pushed its contents to branch#vihdzp/lean-3.46

[Eric Wieser]

branch#upgrade-to-lean-3.44.0 also breaks it

[Yaël Dillies]

What's the rule?

[Eric Wieser]

"Don't use .split() to parse strings unless you intend to check all the pieces"

[Yaël Dillies]

Ah so those break because there's lean-version separated form the rest by hyphens?

[Eric Wieser]

Anything of the form *-lean-(3(\.\d+)*) was treated as a version number, which then blew up due to being rountripped to a branch name lean-{0}.{1}.{2}. Fixed in https://github.com/leanprover-contrib/leanprover-contrib/pull/16

[Eric Wieser]

This should now be fixed.

[Eric Wieser]

Yaël Dillies said:

Hence con-nf, that we just added to the list of projects, does not show up. Anybody knows what's up?

Note that inclusion into the body text is on a different cron job to inclusion into the table; so you might need to wait a day for the former, and a couple hours for the lean 3.45.0 column for the latter.

[Yaël Dillies]

Ahah, you just sniped my question

[Eric Wieser]

(the 3.45 column is missing because I screwed up and made the table blank, so figured I'd manually upload a partial table that at least includes the old results.)

[Eric Wieser]

Unfortunately CI currently over-powers the regular GitHub actions runners. Perhaps the Cron job will eventually get lucky.