installing natural number game in VS code

Stream: new members

[Mattia Bottoni]

Hi everybody!
I would like to install the natural number game on my VS code.

But when I use the command: leanproject get https://github.com/ImperialCollegeLondon/natural_number_game.git

I get the message: Cloning from https://github.com/ImperialCollegeLondon/natural_number_game.git
configuring natural_number_game 0.1
failed to start child process
Command '['leanpkg', 'configure']' returned non-zero exit status 1.

I then find a folder natural_number_game that I can open in VS code. But when I do so, I get the following error message: Lean: leanpkg.path does not exist

And when I click on: Run leanpkg configure.

I get the message: configuring natural_number_game 0.1
failed to start child process

• The terminal process "C:\Users\****\.elan\bin\leanpkg.exe 'configure'" terminated with exit code: 1.
• Terminal will be reused by tasks, press any key to close it

And I still cannot do the natural number game on VS code.

Does anybody know what the problem is? Do I need to install the natural number game differently?
Thank you all in advance for helping!

Best
Matt

[Patrick Massot]

You are not meant to install the natural number game, it's meant to be played online. That does not explain the errors you see, but you'll have a hard finding someone who wants to invest time debugging an installation issue for an obsolete version of Lean.

[Kevin Buzzard]

The Lean 4 repo is here https://github.com/hhu-adam/NNG4 , the branch I'm actively working on is here https://github.com/hhu-adam/NNG4/tree/level-rewrite , and in one month's time there will be a website running a new and improved NNG with more levels (even/odd numbers, prime numbers etc). It's my project for September to get this production-ready as I need it for teaching starting 1st October.

[Mattia Bottoni]

Thank you both for your answers :)

I am looking forward to seeing the NNG for Lean 4 :tada:

[Jerzy Kozera]

Kevin Buzzard said:

The Lean 4 repo is here https://github.com/hhu-adam/NNG4 , the branch I'm actively working on is here https://github.com/hhu-adam/NNG4/tree/level-rewrite , and in one month's time there will be a website running a new and improved NNG with more levels (even/odd numbers, prime numbers etc). It's my project for September to get this production-ready as I need it for teaching starting 1st October.

thank you for working on this! (and on NNG in general!) I've just finished NNG and was slightly disappointed that it used lean3 as I found out after finishing it. is there a version of Maths_Challenges (https://cocalc.com/share/public_paths/f014cd1885a22e8665a728be825e563fc79b7e1f) for lean4?

[Johan Commelin]

@Jerzy Kozera This version of NNG uses Lean 4: https://github.com/hhu-adam/NNG4

[Eric Wieser]

I believe that NNG4 *can* be run ~~from vscode~~ locally?

[Alex J. Best]

Eric Wieser said:

I believe that NNG4 *can* be run ~~from vscode~~ locally?

those look like instructions for devloping a game (by running it on a local webserver on your machine). This may not be what people are looking for when they want to play it in vscode though. Though it would work for someone who knows they will be without internet or something like that.