lean4-samples/NaturalNumbers

Stream: lean4

[Scott Morrison]

Who, if anyone, "owns" https://github.com/leanprover/lean4-samples/tree/main/NaturalNumbers?

[Scott Morrison]

(and what is the relationship with other versions of the natural numbers game?)

[Scott Morrison]

@Kevin Buzzard

[Mario Carneiro]

I would assume @Chris Lovett , although I don't think he works on lean anymore

[Mario Carneiro]

see https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Port.20NNG.20to.20Lean.204/near/303965735

[Scott Morrison]

Okay, I see. I will wait to see what Kevin says.

We need at least a README.md in that directory explaining the connection to other versions of the NNG.

[Scott Morrison]

and then to decide if it needs either a maintainer or to be moved out of lean4-samples.

[Mario Carneiro]

what about the rest of lean4-samples? What is the status of this repository generally?

[Kevin Buzzard]

I'm not sure I've ever seen that before. @Jon Eugster ? @Patrick Massot ? Was this some early port?

[Mario Carneiro]

you did thumbs-up the announcement (linked above) :smiley:

[Kevin Buzzard]

Ok, so maybe I clicked on it once and then forgot about it?

[Scott Morrison]

The general status is that the repository has been rotting. I just made two PRs to at least restore meaningful CI to most of it.

[Scott Morrison]

An update: the new proposal is to delete this repo entirely. If anyone sees something there that is important to save, please let me know soon!

[Mario Carneiro]

Do we find the idea of a samples repository useful, independent of the particular examples in the repo now?

[Scott Morrison]

I mean, it's a nice idea, but given how this repo has been rotting for the past year, it's not clear that anyone is actually interested in doing it at this point.

[Scott Morrison]

I think we're definitely going to be removing this from the leanprover/ organisation.

[Scott Morrison]

• NaturalNumbers is just duplicative, and Kevin's new version is the future
• RubiksCube is redundant with the demo in the ProofWidgets repository
• the other directories are okay?

[Scott Morrison]

One possibility would be to migrate it to leanprover-community, and then either

• if there is a volunteer to take over maintaining it, give them the keys
• archive it at leanprover-community

Either of those choices allow for someone in the future doing something with it.

Another possibility is to simply delete it.

[Mario Carneiro]

Is archiving reversible?

[Scott Morrison]

Yes.

[Mario Carneiro]

I think migrating to community and archiving sounds reasonable then

[Kevin Buzzard]

Right, the version Jon and Alex got working following Patrick's work, and which I'm now trying to make even more accessible, is surely the version which will live on. Expect inequality world this weekend! And some new worlds also nearly ready for release...

[Chris Lovett]

Hi folks, yeah sorry haven't been able to maintain that code, but the idea of a lean4-samples repo was to provide a place to put interesting complete sample apps that go beyond what you'd find in the reference manual https://lean-lang.org/lean4/doc/examples.html and the clone of NaturalNumbers was designed to be something you could run inside VS code with no separate interactive UI just to reach devs that would be more inclined to learn about Lean's natural numbers and Proof capabilities that way, inside VS code (without the gamification - which is why I dropped Game from the title). But would be nice to keep it in sync, I wonder if Kevin's code could be layered in a way that serves both purposes. I also found the ListComprehension sample (originally posted in Zulip) very educational which is why I posted it in the samples repo. There was supposed to be a triggered CI build of the samples that reported any build breaks immediately.

[Scott Morrison]

I've just updated CI:

• ListComprehension was missing from CI
• everything was pointing at nightly releases of Lean, so the CI was potentially worthless

[Scott Morrison]

@Chris Lovett, the current proposal is:

• move from leanprover to leanprover-community, and then archive it (allowing for the possibility of someone adopting it later)

I think everyone would also be happy if you wanted it: i.e. transfer it to your github account.

[Chris Lovett]

Thanks Scott, If there's a possibility someone might adopt it over in leanprover-community that's fine with me, I won't have the time unfortunately.

[Jon Eugster]

On a similar note, should we finally transfer https://github.com/hhu-adam/NNG4 to leanprover-community, too?

[Scott Morrison]

Yes, I think we can do that! @Jon Eugster, who needs to be involved? I can grant the permissions required from the leanprover-community end.