Repository for combinatorial games

Stream: mathlib4

[Violeta Hernández]

Kim Morrison said:

As an example, I think all concrete "named" combinatorial games (domineering, hackenbush, etc) should be developed outside of Mathlib.

I agree, actually. Those things do meet my two criteria. They're overly specific and don't really lead to much interesting mathematics (besides potentially some connections to other games).

[Violeta Hernández]

I would make an exception for nim, since it's required for Sprague-Grundy (and it motivates my ongoing work with nimbers). But other than that, all other concrete combinatorial games can be their own self-contained projects within a larger repository.

[Violeta Hernández]

Just one thing. We already have some basic work on Domineering on Mathlib (written by Kim themselves!). Would we keep it in Mathlib out of backwards compatibility, or should it eventually be moved to this new repository?

[Violeta Hernández]

Also @Tristan Figueroa-Reid

[Tristan Figueroa-Reid]

Hackenbush is interesting for combinatorial games because it represents the class of cold partisan games. However, no results in CGT depend on Domineering as far as I'm aware.

[Tristan Figueroa-Reid]

I think if there is going to be a separate repository for combinatorial games, though, it absolutely should take all named games with it.

[Kim Morrison]

Yes, domineering should move out.

[Violeta Hernández]

I can host that if you don't mind :smile:

[Kim Morrison]

How about this repository exists at leanprover-community/mathlib-combinatorial-games or leanprover-community/combinatorial-games? We can have a quick process to pick some maintainers. I'd propose that implicit in it being part of leanprover-community is that:

• at the end of the day, the Mathlib admin committee has final say if there a political decisions to be made
• the maintainers commit to maintaining "mathlib like standards" for the library
• and I'd propose per Joseph's post that said maintainers set up CI to regularly and automatically bump the Mathlib dependency

[Ruben Van de Velde]

Not sure if this is implicit in your comment, but:

• (at least) all mathlib maintainers are able to merge PRs to the new repository - if only for refactoring and other changes that are relatively theory-free

[Violeta Hernández]

Having this as an official leanprover repository would be great!

[Joseph Myers]

Something like this could certainly be used for incremental development of / experimentation with the infrastructure for multi-repository mathlib (that is, you wouldn't need to have all the infrastructure I described present when you first add such a repository, though it might be a good idea to have it done before we move from two repositories to three).

[Joseph Myers]

It's possible multi-repository mathlib might end up having per-repository maintainers/reviewers, but it seems reasonable that the core mathlib maintainers/reviewers should also have those abilities in other mathlib repositories and any per-repository maintainers/reviewers would be additional to that.

[Joseph Myers]

One thing that would be useful for more than just multi-repository mathlib is a simple configuration hook (lakefile.toml / lakefile.lean) for "apply mathlib conventions in all linters". All mathlib repositories should have the linters enabled that are disabled by default outside mathlib - but the same also applies for external repositories where people are developing code that they intend to contribute to mathlib once ready.

[Violeta Hernández]

I'd be glad to be a maintainer of this future repo, if you'll let me :smile:

[Yaël Dillies]

The community (aka @Bhavik Mehta, @Gareth Ma and myself) now has produced quite a few "end results" in additive combinatorics. Should we have leanprover-community/mathlib-additive-combinatorics as well to host those results?

[Joseph Myers]

I strongly suggest getting all the infrastructure for two-repository mathlib working (CI, docs, linting, etc.) before moving to three-repository mathlib. Three-repository mathlib is strictly more complicated: it's no longer enough for all the mathlib repositories other than core mathlib to have their mathlib dependency updated frequently, they all need to be updated in sync to the same version of core mathlib so there is always a collection of recent versions of all the mathlib repositories that can be used together.

[Tristan Figueroa-Reid]

Most developer tooling is usually made for monorepo setups, and it might just be a better idea to have these separate libraries inside the mathlib4 repository instead of trying to do a polyrepo setup in the first place.

[Tristan Figueroa-Reid]

Especially GitHub CI/CD: most actions are not designed for polyrepos, and syncing across polyrepos is much messier than just tagging PRs/issues with whichever project they belong in.

[Patrick Massot]

We’ve read so many times that Mathlib is crazy because it’s a monorepo… It seems whatever we do is always bad software engineering.

[Tristan Figueroa-Reid]

Patrick Massot said:

We’ve read so many times that Mathlib is crazy because it’s a monorepo… It seems whatever we do is always bad software engineering.

Haha, yeah, I guess it really is a differing opinion for many people. I personally have slowly gone to favor monorepos after realizing the weaknesses of polyrepos in terms of developer tooling. My early concern with monorepos would have been the huge intake of differing issues and pull requests (i.e. swc deals with this a lot), but it seems easier to deal with them in one place.

[Tristan Figueroa-Reid]

Though, it seems best to pick whatever would be suited for lean4 itself, but I don't think lean4 has great tooling for neither monorepos nor polyrepos.

[Tristan Figueroa-Reid]

Patrick Massot said:

We’ve read so many times that Mathlib is crazy because it’s a monorepo… It seems whatever we do is always bad software engineering.

Was the discussion against mathlib4 being a monorepo, or against it being a single library?

[Patrick Massot]

Oh we had lots of people arguing that everything is bad. So the answer is: both.

[Violeta Hernández]

I actually think Mathlib being a monorepo is one of its biggest strengths. I've been pleasantly surprised more that once in learning that some piece of "ordinal arithmetic" is actually some more general order notion that's broadly useful to others.

[Violeta Hernández]

It's just that for niche topics like combinatorial games, the cost ends up outweighing the benefits.

[Tristan Figueroa-Reid]

Violeta Hernández said:

I actually think Mathlib being a monorepo is one of its biggest strengths. I've been pleasantly surprised more that once in learning that some piece of "ordinal arithmetic" is actually some more general order notion that's broadly useful to others.

I absolutely agree. I'm still a fan of monorepos, but it fits particurally well with the way mathlib4 is designed.

[Tristan Figueroa-Reid]

Violeta Hernández said:

It's just that for niche topics like combinatorial games, the cost ends up outweighing the benefits.

Actually, was there any argument for keeping combinatorial games themselves outside of Archive? Or was it because there might be theory developed on top of specific combinatorial games?

[Violeta Hernández]

The basics of combinatorial games themselves should absolutely be a part of Mathlib. Otherwise we just end up reinventing the wheel every time someone wants to formalize a game. And this is not to mention things like nimbers or surreals that are built on top of this.

[Tristan Figueroa-Reid]

Violeta Hernández said:

The basics of combinatorial games themselves should absolutely be a part of Mathlib. Otherwise we just end up reinventing the wheel every time someone wants to formalize a game. And this is not to mention things like nimbers or surreals that are built on top of this.

I'm so sorry for the misuse of words. I meant named combinatorial games. I do agree with keeping combinatorial games inside of Mathlib.

[Tristan Figueroa-Reid]

I remember discussing something about putting it in the Archive earlier.

[Violeta Hernández]

I think the real question we should be asking is, shouldn't the Archive be split into other repositories instead?

[Violeta Hernández]

For instance, an IMO repository would allow us math olympiad nerds to focus on problems more specifically (and would provide useful training material for all the fancy new AIs), while not taking as much time out of the Mathlib maintainers.

Arguably this already exists as compfiles, the difference would be that our version of it complies to Mathlib quality standards.

[Tristan Figueroa-Reid]

Violeta Hernández said:

I think the real question we should be asking is, shouldn't the Archive be split into other repositories instead?

Too many separate repositories for mathlib4 is going to lead to a lot of configuration duplication that would be annoying to update. It is quite nice to also be able to golf a tactic and immediately see results in Archive (since the Archive isn't just useful for AI training, but it gives a better peek into how end users might use mathlib4, which is very useful for testing user experience)

[Tristan Figueroa-Reid]

This is quite a strange problem: I think the end results of additive combinatorics are still useful enough to keep in mathlib4, but named combinatorial games are useless enough to be unused by essentially every single mathlib4 user, yet they still might have extra theory developed on them since a small but non-neglible amount of research is done on named combinatorial games.

I think something that would probably solve this is if Archive could be imported as a library: Archive contains a lot of end results and other non-essential extra problems (i.e. IMO), but I think for the small group of people that would be building on top of Archive outside of mathlib4, it makes sense for them to just import the entire folder instead of breaking it up into a series of submodules for maintainability reasons.

[Joseph Myers]

A monorepo works fine for mathlib at present (including niche topics), and probably for mathlib at ten times its present size given better infrastructure for only downloading/unpacking those oleans that are actually needed, so there's no hurry to get things working with multiple repositories. But it probably doesn't work well when we're 1000 times the present size.

Part of the infrastructure for multiple repositories would need to be automation to keep "configuration duplication" updated in sync for all repositories.

[Tristan Figueroa-Reid]

My only problem with keeping combinatorial games in a separate repository is that many combinatorial game theory tools are developed to analyze specific categories of games: it would make more sense if the entirety of combinatorial game theory were isolated or if games were in the Archive folder.

[Violeta Hernández]

Any updates on this? I've got #21003 in the oven and I'd like to know whether this is welcome in Mathilb or whether I should be moving it elsewhere.

[Patrick Massot]

I think we are waiting for you creating the repository.

[Yaël Dillies]

I thought it should live under leanprover-community?

[Kevin Buzzard]

historically I think things are often created elsewhere and then moved?

[Martin Dvořák]

Can you move a repository between two GitHub users without losing the commit history?

[Tristan Figueroa-Reid]

You can :+1:

[Yaël Dillies]

Should I then create YaelDillies/mathlib-add-combi?

[Violeta Hernández]

Hi! I'm sorry for completely forgetting about this for the past weeks. The semester hasn't been treating me so kindly...

What exactly is the scope here? Should I just copy over everything we already have on combinatorial games to this new repository, with the goal of deleting Mathlib's development altogether? Personally I'm not a fan of this since it would mean we'd have to get rid of our development of surreals as well, which are arguably relevant mathematics.

Or is the idea that we just copy over the "non-essential" things, i.e. the development of specific games like domineering or poset games?

[Damiano Testa]

As an external observer of the development, I see a lot of PRs and a lot of refactors going on.

[Damiano Testa]

My personal impression is that it would probably be simpler to excise what is currently being still thought about to a separate repository, where progress, tests and refactors can be done at "super Mathlib" speed.

[Damiano Testa]

Once things settle in the new repository, it is a good time to PR to mathlib.

[Damiano Testa]

By then, the formalisation would be more stable and it will be clearer to see what is in scope and what is better left on the side.

[Violeta Hernández]

I wouldn't classify the formalization as unstable, but there's certainly a lot of API that can be improved.

If that's the metric though, then we'd need to move the entirety of the Game and Surreal folders over, as these refactors involve the least common denominator file Game/PGame.

[Violeta Hernández]

(if we're going to take over surreal numbers too, then that could be an opportunity to finally get the surreal division PR merged somewhere)

[Violeta Hernández]

Is that what we want to do? If so, I'll publish the repo in a few hours and I'll copy over all of the relevant Mathlib PRs.

[Damiano Testa]

To me, this seems like a good idea. I would wait to see what the other maintainers also think.

[Patrick Massot]

I would move Game and Surreal.

[Patrick Massot]

unless there is some other part of Mathlib using anything from those folders.

[Patrick Massot]

In addition, a good data point is to look at files where you needed to systematically ping the maintainer team on Zulip because no maintainer was interested in the PR.

[Tristan Figueroa-Reid]

Damiano Testa said:

As an external observer of the development, I see a lot of PRs and a lot of refactors going on.

To clarify, the refactors are mainly to move to an IGame: the numerous PRs is because two PRs were made that were thousands of lines long about 2 years ago, and they're just now being split down, because reviewing those enormous PRs is hard. However, having IGame unlocks the ability for us to (nicely) formalize end results and open problems in combinatorial game theory, which would make this formalization a very good resource for real proof_wanteds.

[Violeta Hernández]

There's also the more minor refactor I've been doing of defining game relations generally on preorders, it's the source of some PRs but isn't really anything huge.

[Violeta Hernández]

Patrick Massot said:

In addition, a good data point is to look at files where you needed to systematically ping the maintainer team on Zulip because no maintainer was interested in the PR.

Yeah, that's the entire game folder, unfortunately.

[Tristan Figueroa-Reid]

Yeah - combinatorial game theory (I don't think) is used anywhere else in mathlib4. It helps a lot in developing utilities for dealing with classes and order theory (and it is probably the closest so far we have to reaching the end of a field other than additive combinatorics), but I think moving Game/Surreal out of mathlib4 would be permanent if it happens.

[Patrick Massot]

Violeta Hernández said:

Patrick Massot said:

In addition, a good data point is to look at files where you needed to systematically ping the maintainer team on Zulip because no maintainer was interested in the PR.

Yeah, that's the entire game folder, unfortunately.

You shouldn’t see that as unfortunate. It means you could move it all to the new repository and no longer have to beg for reviews.

[Violeta Hernández]

Speaking of, who would be the maintainers of the new repo? The Mathlib maintainers + me and Tristan?

[Kevin Buzzard]

I'm not sure I would like to be a maintainer for a new repo where I barely know the material -- I'm supposed to be proving Fermat's Last Theorem.

[Patrick Massot]

Kevin, I don’t think this would be so different from the situation in Mathlib. Nowadays no single maintainer understands all the math in Mathlib. You would ignore the game repo just like you ignore probability in Mathlib for instance (taking a topic that we are both ignorant about).

[Violeta Hernández]

I imagine the Mathlib maintainers wouldn't need to interact with the repo if they don't want to, but it'd still be nice to be able to rely on them on matters that relate to both repositories.

[Ruben Van de Velde]

Yeah, I don't think we should have "extended mathlib" repositories like this which the mathlib maintainers can't land things if needed

[Violeta Hernández]

The authority should carry over even if most of the responsibility need not be.

[Violeta Hernández]

Is there a way to only import part of Mathlib? Copying the relevant files just makes everything conflict with what's already there.

[Mario Carneiro]

? You just import part of mathlib

[Violeta Hernández]

Whoops you're right, I forgot to update the imports within the copied files.

[Violeta Hernández]

One last thing. I exchanged some DMs with @Yaël Dillies who recommended I wait for them to create a "Mathlib sublibrary" template before having the CGT repo go live, so we could have all of these future sublibraries under a common framework. Their suggestion was to start work on a preliminary repo, before copying everything over to a new repo built from this template. What do others think about this?

[Violeta Hernández]

(I personally think we could just start the repo without the template and update whatever relevant parameters we need later down the line as needed)

[Violeta Hernández]

Repo is up and running!
https://github.com/vihdzp/combinatorial-games

[Violeta Hernández]

Two questions

1. Is this going to be an "official" Mathlib repo? (as in, do I get to claim this is the official Mathlib combinatorial games library?)
2. How do I go about adding all the maintainers? Do I just send an invite to every Mathlib maintainer individually?

[Violeta Hernández]

Actually two further questions

3. What's the process for doing PRs going to be like in this new repo? I imagine every PR should still be approved by someone else; will we consider that as sufficient for merging?
4. What happens now within "core" Mathlib? I'll be moving over a bunch of relevant open PRs, but does that mean they get closed in Mathlib? Will we be deleting the Game / Surreal folders from Mathlib until further notice?

[Violeta Hernández]

5. Where can I find the Mathlib ruleset for branch protection and how can I implement it?

[Violeta Hernández]

6. Surely now that PGame is relegated to its own repository we don't need to put it in the ad hoc SetTheory namespace, right?

[Violeta Hernández]

7. What about deprecations? Since no one is going to be using this new repo yet, surely we can just do a purge of unsupported theorems?

[Kevin Buzzard]

Are you also going to take the Nimber directory?

[Violeta Hernández]

Great question. By Patrick's criterion I definitely should.

[Violeta Hernández]

Yeah, if I'm taking surreals then it only makes sense to take the other algebraic structure based on combinatorial games.

[Violeta Hernández]

Btw @Tristan Figueroa-Reid I sent you the invitation to be a collaborator

[Violeta Hernández]

Oh and

8. Should we announce the existence of this new repo at some point?

[Kevin Buzzard]

I would wait until you have moved the directories to the new repo and everything compiles and you've written a README with perhaps some future goals and a vision of where you're going, and then dump something in #announce (and remember to write "follow-up discussion here in #general" or whatever, so people don't start spamming #announce with responses which ping thousands of people)

Note that part of the reason that we're in this situation is that (IMNSHO) mathlib doesn't have a clear vision right now (and we seem to have recently decided "CGT is not for mathlib" after a long discussion). The vision initially for mathlib was "do math and grow", then "nail an undergraduate curriculum", then it became "grow in arbitrary directions with rate determined by density of whoever is active in the community" rather than any specific policy. If you start with a policy then it will hopefully make it very clear what you want (and more importantly what you don't want).

[Violeta Hernández]

I've moved the directories and everything compiles, so I guess that means it's README time.