Zulip Chat Archive

Stream: mathlib4

Topic: Deprecated lemmas in Mathlib.SetTheory.Ordinal.Arithmetic

Kim Morrison (Mar 02 2025 at 22:38):

There are many things deprecated in file#SetTheory/Ordinal/Arithmetic but that are still being used by undeprecated things. These have now reached the 6 month rolling window for removing deprecations, so I would like to see some progress here in disentangling this file.

@Mario Carneiro, @Floris van Doorn, you are both listed as authors here, any interest in taking a look?

Mario Carneiro (Mar 02 2025 at 22:41):

cc: @Violeta Hernández , who put most of these deprecations in place

Violeta Hernández (Mar 02 2025 at 23:24):

The deprecations in question are all related to docs#Ordinal.sup, right?

Violeta Hernández (Mar 02 2025 at 23:27):

I think the only other non-deprecated things that should be using that definition are docs#Ordinal.bsup, docs#Ordinal.lsub, and docs#Ordinal.blsub, and all of these are also on the deprecation chopping block (see #17033)

Violeta Hernández (Mar 02 2025 at 23:35):

And the only things that use these are

docs#PGame.Birthday uses Ordinal.lsub. Since this definition is now part of the new CGT repo, is it ok to just deprecate / delete the entire file?
~~docs#Ordinal.nadd uses Ordinal.blsub~~ I already fixed this in #19236
A few lemmas in the cofinality file, e.g. docs#Ordinal.cof_eq_inf_lsub. I have a pending refactor #19698 which entirely rewrites this file, and in particular gets rid of these lemmas. That refactor depends on #19723 and #21972, the first of which has been on maintainer-merge for a week.

Kim Morrison (Mar 06 2025 at 05:48):

Where is the new repo? Googling doesn't find it (in fact, it finds my student's report from 2019, starting this whole thing off!)

Does it have proper CI set? Mathlib linters enabled?

Violeta Hernández (Mar 06 2025 at 05:49):

https://github.com/vihdzp/combinatorial-games

Kim Morrison (Mar 06 2025 at 05:49):

Violeta, #19723 has a merge conflict.

Violeta Hernández (Mar 06 2025 at 05:49):

We've been holding off on making an announcement since we're doing some very major refactors, and the code isn't production ready

Kim Morrison (Mar 06 2025 at 05:50):

Violeta Hernández said:

https://github.com/vihdzp/combinatorial-games

This doesn't seem to run any linters?

Violeta Hernández (Mar 06 2025 at 05:51):

I don't really have experience with configuring CI

Kim Morrison (Mar 06 2025 at 05:51):

We really need to write a document standardizing the requirements for "child of Mathlib" repositories.... If you feel like getting a head start on that while you're setting up this repository... ? :-)

Violeta Hernández (Mar 06 2025 at 05:51):

I can send you an invitation to be a maintainer if you'd like to help set that up

Kim Morrison (Mar 06 2025 at 05:51):

Violeta Hernández said:

I don't really have experience with configuring CI

Okay, we'll need to find such people amongst potential maintainers of this repo before we can "launch".

Violeta Hernández (Mar 06 2025 at 06:19):

Kim Morrison said:

We really need to write a document standardizing the requirements for "child of Mathlib" repositories.... If you feel like getting a head start on that while you're setting up this repository... ? :-)

@Yaël Dillies mentioned they wanted to do that a week ago or so