Lean Game Server

Stream: general

[Giovanni Mascellani]

Testing with both Firefox and Chromium under Debian and with Firefox under macOS, I can see the "main menu", but not get to the game. It displays a spinner for some time and then a blank windows with just one vertical ruler. Maybe too many people are already having fun.

[Henrik Böving]

Yes it did work for me before on Fedora Firefox but now spinner as well.

[Jon Eugster]

I wanted to update a level in the NNG and accidentally had some non-finished changes on it too :man_facepalming: Need to rebuild the docker containers of the games

[Alexander Bentkamp]

Ok, it's up and running again. Let's see how long it takes until we break it again :thinking:

[Adam Topaz]

Very cool! Do you have the code for the server on github somewhere?

[Giovanni Mascellani]

Now it works, nice! :-)

[Alexander Bentkamp]

@Adam Topaz The server is here: https://github.com/leanprover-community/lean4game, and the NNG game data is here: https://github.com/hhu-adam/NNG4

[Adam Topaz]

Thanks!

[Assaf Kfoury]

Jon Eugster said:

Alexander Bentkamp , Marcus Zibrowius and I are happy to announce that our
interactive game server for Lean 4 is up and running:

https://adam.math.hhu.de

Currently it mainly hosts the Natural Number Game for Lean 4, and we hope more games will be added and linked there in the future.

front.png
game.png

It is written in Lean itself, thanks to Patrick Massot 's prototype, which allows us to give direct feedback to game creators within their editor. However, documentation is still to be expanded. If you need help to create or modify a game, please don't hesitate to reach out!

As the server is in its beta phase, I'd like to note that it probably does not support more than ~20 users simultaneously for now. We also aim to further improve the interface and existing games over the next months, and we plan to add a functionality to load your own game through our server by simply providing a url to the game's github repo. For now, I will have to add games manually to appear on the page.

Many thanks to all who contributed to interactive game server for Lean4. I haven't yet tried all the parts of NNG4, but the little I saw and tried already is very good and promising. Excellent pedagogical tool!

[Assaf Kfoury]

Jon Eugster said:

Alexander Bentkamp , Marcus Zibrowius and I are happy to announce that our
interactive game server for Lean 4 is up and running:

https://adam.math.hhu.de

Currently it mainly hosts the Natural Number Game for Lean 4, and we hope more games will be added and linked there in the future.

front.png
game.png

It is written in Lean itself, thanks to Patrick Massot 's prototype, which allows us to give direct feedback to game creators within their editor. However, documentation is still to be expanded. If you need help to create or modify a game, please don't hesitate to reach out!

As the server is in its beta phase, I'd like to note that it probably does not support more than ~20 users simultaneously for now. We also aim to further improve the interface and existing games over the next months, and we plan to add a functionality to load your own game through our server by simply providing a url to the game's github repo. For now, I will have to add games manually to appear on the page.

Something that caught my attention only now: You say that the server probably does not support more than ~20 users simultaneously. So, NNG is not yet (should not yet be) available to a wider audience. When do you think this will be remedied? I would like to use NNG in a course in September 2023 with an enrollment of 25-35 students who, during the first two weeks of the course, will be playing NNG on their own before I start assigning homework exercises using the features of Lean they will have learned from NNG.

[Kevin Buzzard]

I would like to give NNG an update before people start talking about it publically; I just haven't found the time to do so yet, but now clearly the tools are available for me to be able to do this (I don't know anything about how the web part of it works but I can now edit the Lean code)

[Assaf Kfoury]

Kevin Buzzard said:

I would like to give NNG an update before people start talking about it publically; I just haven't found the time to do so yet, but now clearly the tools are available for me to be able to do this (I don't know anything about how the web part of it works but I can now edit the Lean code)

Ok, I will hold back, and make a decision on NNG3 vs NNG4 in mid-August.

[Wojciech Nawrocki]

When trying to inspect the type of a lemma in the sidebar, I see (missing):
Screenshot-2023-05-05-at-3.12.11-PM.png

[PCloud]

Assaf Kfoury said:

Jon Eugster said:

Alexander Bentkamp , Marcus Zibrowius and I are happy to announce that our
interactive game server for Lean 4 is up and running:

https://adam.math.hhu.de

Currently it mainly hosts the Natural Number Game for Lean 4, and we hope more games will be added and linked there in the future.

front.png
game.png

It is written in Lean itself, thanks to Patrick Massot 's prototype, which allows us to give direct feedback to game creators within their editor. However, documentation is still to be expanded. If you need help to create or modify a game, please don't hesitate to reach out!

As the server is in its beta phase, I'd like to note that it probably does not support more than ~20 users simultaneously for now. We also aim to further improve the interface and existing games over the next months, and we plan to add a functionality to load your own game through our server by simply providing a url to the game's github repo. For now, I will have to add games manually to appear on the page.

Something that caught my attention only now: You say that the server probably does not support more than ~20 users simultaneously. So, NNG is not yet (should not yet be) available to a wider audience. When do you think this will be remedied? I would like to use NNG in a course in September 2023 with an enrollment of 25-35 students who, during the first two weeks of the course, will be playing NNG on their own before I start assigning homework exercises using the features of Lean they will have learned from NNG.

If only we have a WASM build for Lean 4...

[Notification Bot]

14 messages were moved here from #announce > Lean Game Server by Johan Commelin.

[Jon Eugster]

exactly, so the lean3 game ran client-side in the browser, but since there isnt wasm available for lean4 (yet) we run this server-side, so capacity is limited by what resources the server has and by optimization of resource usage...

[Jon Eugster]

Wojciech Nawrocki said:

When trying to inspect the type of a lemma in the sidebar, I see (missing):
Screenshot-2023-05-05-at-3.12.11-PM.png

That's me being lazy typing documentation and the automated documentation not being implemented yet. :sweat_smile:

[Jon Eugster]

Assaf Kfoury said:

Ok, I will hold back, and make a decision on NNG3 vs NNG4 in mid-August.

That's probably a good timeframe to figure out how much improvements in the workflow increase the capacity and how much it just depends on the available RAM/CPU on the machines.

[Johan Commelin]

@Jon Eugster I don't know if this has come up before, but have there been ideas/discussions about i18n for the game framework?

[Alexander Bentkamp]

No, we haven't really thought about this yet, but it would probably be a good idea.

[Bulhwi Cha]

I'm willing to translate Lean 4 games into Korean.

[Matthew Ballard]

How good are LLMs for language to language translation?

[Scott Morrison]

I suspect for the low volume of text involved for a Lean game it's easier to do it by hand, in any case.

[Shreyas Srinivas]

Matthew Ballard said:

How good are LLMs for language to language translation?

Specifically how does it compare with deepl or google translate?

[Jon Eugster]

I think I would want to make the interface multilingual rarher soonish if there is demand for that. For the games themself, I wonder if it is simpler to just have an independent copy of the game in each language:thinking:
(nvm Patrick just explained to me how he thinks this should be done:sweat_smile:)

[Jon Eugster]

Bulhwi Cha said:

I'm willing to translate Lean 4 games into Korean.

Note however that Kevin got plans to refactor the NNG content significantly in the near future. Might be worth keeping an eye out for he progress on that

[Utensil Song]

Is it possible to host a series of Lean Games on https://game.lean-lang.org ?

[Jon Eugster]

Eventually it might be a plan to transfer the server at adam.math.hhu.de to lean-lang.org. However, that hasn't been discussed yet. So for now the best thing one can do is to create this "series of games" and have them published at adam.math.hhu.de

[Kevin Buzzard]

One game which I think would be interesting to make would be the British Natural Number Game. In this game, naturals start at 1 instead of 0. This means that none of these words like "additive monoid" or "commutative semiring" apply to the naturals, but suspect that this doesn't matter at all. My conjecture is that additive stuff gets harder to work with, but multiplicative stuff gets easier to work with because you don't have to keep saying $x\not=0$. For example we are currently working on theorems about divisibility and many of the lemmas don't work for 0, statements like $b\mid c\implies b\leq c$ is false for $0$, $a\leq a\times b$ is not true if $b=0$, $ax=ay\implies x=y$ is not true if $a=0$ and so on. When developing the new advanced multiplication world it really became clear to me that $0$ is a pain rather than being useful. In the British Natural Number Game you could imagine all the same levels, modified appropriately, and then you can ask where overall the proofs are shorter or longer, and I bet the answer is "longer for addition, shorter for multiplication, longer for $\leq$, shorter for divisibility". This would make a nice student project I think.

[Ruben Van de Velde]

The pnatural number game

[Kevin Buzzard]

I think that's how posh people say it in the UK

[loki der quaeler]

There's an odd text entry parsing issue where "\in" gets replaced with a lower case pi.
2023-11-25-19-12-26.2023-11-25-19_13_27.gif

[Mario Carneiro]

That symbol looks like \sqcap, my guess is that it is included as \inter and \in is missing for whatever reason

[Jon Eugster]

That's been a weird js-bug which is already fixed on the main branch.

[Miguel Marco]

I just translated the Set theory game to spanish. ChatGPT has been useful in some cases, but it should be used carefully, as it might mess with quotes, translate commands, or do other things that you have to correct by hand. At the end, I only used it to translate long paragraphs, and stick to manual translation of the short sentences that are embedded in the code (which is a significant part or the text that must be translated).

Would it be possible to host it in the server? The repo is this one.

[Jon Eugster]

Nice! I'll add it after I figured out how to deal with all the lake changes that came with v4.3.0:+1:

[Dan Velleman]

@Miguel Marco : Thanks for doing this! I have made quite a few changes to the game in the last day or two, and I'm still planning to add another world. So you might want to hold off a little bit before finalizing the Spanish version.

[Miguel Marco]

Dan Velleman said:

Miguel Marco : Thanks for doing this! I have made quite a few changes to the game in the last day or two, and I'm still planning to add another world. So you might want to hold off a little bit before finalizing the Spanish version.

Good to know. While I was translating it, I also considered that it would be nice to add some new worlds (dealing with sUnion, sInter, maybe maps, images and preimages....). But wanted to have the original game translated first, and then add slowly new stuff.

What world are you planning to add?

[Dan Velleman]

Yes, that's exactly what I'm adding. I've already added sInter, but that update hasn't made it to the server yet. I'm planning to add sUnion as well.

[Dan Velleman]

I've also made some small changes to earlier parts of the game, such as adding ext as a way to prove equality of sets.

[Miguel Marco]

Do you consider adding also images and preimages under maps? Or would that be off the intended scope?

[Dan Velleman]

I wasn't planning to do that, but I'll consider it. It would require introducing functions, which goes beyond my original intended scope. But you're right that theorems about image, preimage, one-to-one, and onto would make good game levels.

[Miguel Marco]

I have merged your last changes to my branch, to continue the translation, and it seems to fail when testing.

I get the following error in the lean4game execution:

[server] Listening on 8080
[server] [Sun Dec 03 2023 20:29:30 GMT+0100 (hora estándar de Europa central)] Socket opened - ::
[server] [Sun Dec 03 2023 20:29:30 GMT+0100 (hora estándar de Europa central)] Number of open sockets - 1
[server] [Sun Dec 03 2023 20:29:30 GMT+0100 (hora estándar de Europa central)] Free RAM - 52814 / 64251 MB
[server] CLIENT: {"jsonrpc":"2.0","id":0,"method":"initialize","params":{"processId":null,"clientInfo":{"name":"Monaco","version":"1.69.0"},"locale":"es-ES","rootPath":null,"rootUri":null,"capabilities":{"workspace":{"applyEdit":true,"workspaceEdit":{"documentChanges":true,"resourceOperations":["create","rename","delete"],"failureHandling":"textOnlyTransactional","normalizesLineEndings":true,"changeAnnotationSupport":{"groupsOnLabel":true}},"codeLens":{"refreshSupport":true},"executeCommand":{"dynamicRegistration":true},"workspaceFolders":true,"semanticTokens":{"refreshSupport":true},"inlayHint":{"refreshSupport":true},"diagnostics":{"refreshSupport":true}},"textDocument":{"publishDiagnostics":{"relatedInformation":true,"versionSupport":false,"tagSupport":{"valueSet":[1,2]},"codeDescriptionSupport":true,"dataSupport":true},"synchronization":{"dynamicRegistration":true},"completion":{"dynamicRegistration":true,"contextSupport":true,"completionItem":{"snippetSupport":true,"commitCharactersSupport":true,"documentationFormat":["markdown","plaintext"],"deprecatedSupport":true,"preselectSupport":true,"tagSupport":{"valueSet":[1]},"insertReplaceSupport":true,"resolveSupport":{"properties":["documentation","detail","additionalTextEdits"]},"insertTextModeSupport":{"valueSet":[1,2]},"labelDetailsSupport":true},"insertTextMode":2,"completionItemKind":{"valueSet":[1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25]},"completionList":{"itemDefaults":["commitCharacters","editRange","insertTextFormat","insertTextMode"]}},"hover":{"dynamicRegistration":true,"contentFormat":["markdown","plaintext"]},"signatureHelp":{"dynamicRegistration":true,"signatureInformation":{"documentationFormat":["markdown","plaintext"],"parameterInformation":{"labelOffsetSupport":true},"activeParameterSupport":true},"contextSupport":true},"definition":{"dynamicRegistration":true,"linkSupport":true},"references":{"dynamicRegistration":true},"documentHighlight":{"dynamicRegistration":true},"documentSymbol":{"dynamicRegistration":true,"symbolKind":{"valueSet":[1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26]},"hierarchicalDocumentSymbolSupport":true,"tagSupport":{"valueSet":[1]},"labelSupport":true},"codeAction":{"dynamicRegistration":true,"isPreferredSupport":true,"disabledSupport":true,"dataSupport":true,"resolveSupport":{"properties":["edit"]},"codeActionLiteralSupport":{"codeActionKind":{"valueSet":["","quickfix","refactor","refactor.extract","refactor.inline","refactor.rewrite","source","source.organizeImports"]}},"honorsChangeAnnotations":false},"codeLens":{"dynamicRegistration":true},"formatting":{"dynamicRegistration":true},"rangeFormatting":{"dynamicRegistration":true},"onTypeFormatting":{"dynamicRegistration":true},"rename":{"dynamicRegistration":true,"prepareSupport":true,"prepareSupportDefaultBehavior":1,"honorsChangeAnnotations":true},"documentLink":{"dynamicRegistration":true,"tooltipSupport":true},"typeDefinition":{"dynamicRegistration":true,"linkSupport":true},"implementation":{"dynamicRegistration":true,"linkSupport":true},"colorProvider":{"dynamicRegistration":true},"foldingRange":{"dynamicRegistration":true,"rangeLimit":5000,"lineFoldingOnly":true,"foldingRangeKind":{"valueSet":["comment","imports","region"]},"foldingRange":{"collapsedText":false}},"declaration":{"dynamicRegistration":true,"linkSupport":true},"selectionRange":{"dynamicRegistration":true},"semanticTokens":{"dynamicRegistration":true,"tokenTypes":["namespace","type","class","enum","interface","struct","typeParameter","parameter","variable","property","enumMember","event","function","method","macro","keyword","modifier","comment","string","number","regexp","operator","decorator"],"tokenModifiers":["declaration","definition","readonly","static","deprecated","abstract","async","modification","documentation","defaultLibrary"],"formats":["relative"],"requests":{"range":true,"full":{"delta":true}},"multilineTokenSupport":false,"overlappingTokenSupport":false,"serverCancelSupport":true,"augmentsSyntaxTokens":true},"linkedEditingRange":{"dynamicRegistration":true},"inlayHint":{"dynamicRegistration":true,"resolveSupport":{"properties":["tooltip","textEdits","label.tooltip","label.location","label.command"]}},"diagnostic":{"dynamicRegistration":true,"relatedDocumentSupport":false}},"window":{"showMessage":{"messageActionItem":{"additionalPropertiesSupport":true}},"showDocument":{"support":true}},"general":{"staleRequestSupport":{"cancel":true,"retryOnContentModified":["textDocument/semanticTokens/full","textDocument/semanticTokens/range","textDocument/semanticTokens/full/delta"]},"regularExpressions":{"engine":"ECMAScript","version":"ES2020"},"markdown":{"parser":"marked","version":"1.1.0"},"positionEncodings":["utf-16"]}},"initializationOptions":{"editDelay":200,"hasWidgets":true},"trace":"off","workspaceFolders":null}}
[server] Lean Server: libc++abi: terminating due to uncaught exception of type lean::exception: incomplete case
[server]
[server] [Sun Dec 03 2023 20:29:32 GMT+0100 (hora estándar de Europa central)] Socket closed - ::

Since the Lean version was updated, I did run lake clean, lake exe cache get and lake build -R, and in fact when i open the files of the game, I can see correctly the proof states. Any idea about what could the problem be?

[Miguel Marco]

nevermind, updating the server solved it.

[Dan Velleman]

@Miguel Marco : I just added some more levels to the Set Theory Game. I also made a few changes to the earlier levels. In particular, I decided to use obtain to get a witness for an existential assumption (rather than cases').

I don't have plans to add more levels at this point, so unless there are problems with the current version, I won't be making any changes for a little while.

[Miguel Marco]

Thanks. I had been porting your changes and now the spanish version is online. I will try to port your very last changes tomorrow.

I still think it would be nice to have something with images and preimages. Maybe a new game that works as a continuation of this one? (Set Theory Game returns). :rolling_on_the_floor_laughing:

[Steven Clontz]

What's the intent in level 1/7 of family union world? Of course the empty set is what's needed, but how is the player supposed to know how to find the contradiction from $x\in\emptyset$ (or am I missing something?)

[Dan Velleman]

The hints suggest using A rather than empty set (because you already have the theorem sub_ref). But you're right, the empty set would be another natural choice, and a player could get stuck if they make that choice. I'll have to think about how to deal with that.

[Dan Velleman]

Maybe I should just make the hint more explicit, to avoid the problem.

[Jon Eugster]

You could place a hint at the state after a user entered \empty either telling them what to do now or tell them to go back. something like:

Hint "use {A}"
Branch
   use empty
   Hint "this is a dead end, go back"
use A

[Dan Velleman]

Thanks Jon, good idea.

[Steven Clontz]

I like that hint idea as well. I guess I knew I had a mathematically valid answer, so I was fixated on making it work rather than backing up to consider other valid answers that I had the tools for.

[Miguel Marco]

One question: what would be the right way to use the calctactic in a game? Expect the user to provide the full calc block?
Or is there a nice way to stablish the chain of (in)equalities and then prove them one by one?

[Jon Eugster]

You can provide a Template (I think also an empty one) to force the user to use the editor for that level. The typewriter-like display is not designed for multi-line tactics

[Miguel Marco]

Where can I read documentation about writing such a template?

[Jon Eugster]

https://github.com/leanprover-community/lean4game/blob/main/doc/create_game.md#6-c-proof

(3rd point under 6c, if your device also doesnt scroll there on clicking the link)

There's a single paragraph about them here. I should extend that!