Installing lean game maker

Stream: new members

[ZainAK283]

Has anyone installed Mohammad Pedramfar's Lean Game Maker in windows? ( https://github.com/mpedramfar/Lean-game-maker/blob/master/INSTALL.mdhttps://github.com/mpedramfar/Lean-game-maker/blob/master/INSTALL.md )

I managed to do the first git clone no problem

echo 'export PATH="$HOME/.pyenv/bin:$PATH"' >> ~/.bashrc
doesn't give any output, but I'm assuming that's what I'm supposed to see?

The main issue is when I try:
sudo apt install -y make build-essential libssl-dev zlib1g-dev libbz2-dev libreadline-dev libsqlite3-dev wget curl llvm libncurses5-dev libncursesw5-dev xz-utils tk-dev libffi-dev liblzma-dev python-openssl
I get:
bash: sudo: command not found

[Patrick Massot]

That sudo apt... line is definitely not Windows.

[Patrick Massot]

It's about Linux (and more precisely Debian-based Linux but you don't care about this).

[Patrick Massot]

However that while line is about getting python 3.7. So you can simply skip it if you already have a recent python

[Patrick Massot]

Otherwise go to python.org to see how to install python on Windows

[ZainAK283]

Thanks for the comment! I've installed a WSL ( https://ubuntu.com/wsl if it matters) and the install is mostly working I think,

at the end of https://github.com/mpedramfar/Lean-game-maker/blob/master/INSTALL.mdhttps://github.com/mpedramfar/Lean-game-maker/blob/master/INSTALL.md it says to "Clone the repository. ", what does this mean/how do I do this?

[Yakov Pechersky]

git clone https://github.com/mpedramfar/Lean-game-maker

[Luisitoon]

I am following the installation for lean-game-maker on"https://github.com/mmasdeu/Lean-game-maker/blob/master/INSTALL.md" and the second command is "echo 'export PATH="$HOME/.pyenv/bin:$PATH"' >> ~/.bashrc". I am not receiving any output by running this command on the terminal... Am I supposed to change the "PATH" and "HOME" terms or sth??

[Mauricio Collares]

This should only add a line to ~/.bashrc and is not intended to produce any output. Once you restart your terminal, the newly-added bashrc line should execute automatically and change your PATH for you

[Luisitoon]

I am about to finish the installation guide for the lean-game-maker... At the very end, it says: "Inside the virtual environment and in the root folder of the repository, type"

cd src/interactive_interface
npm install .
./node_modules/.bin/webpack --mode=production
cd ../..

pip3 install -e .

What does this mean?? I do not know how to proceed...

[Kevin Buzzard]

Which part don't you understand? I mean, it means "in the virtual environment (which you set up using python in an earlier stage) and in the root directory of the repository (i.e. the directory you just downloaded), type those things".

[Luisitoon]

I managed to type the code in the root directory of the repository by writing "cd Lean-game-maker" first. But how do I type the code for the virtual environment? What do I have to write before the code to activate the virtual environment in the terminal ???

[Julian Berman]

Type workon lean_env.

[Luisitoon]

I am getting this error:

bash: cd: src/interactive_interface: No such file or directory
npm ERR! code ENOENT
npm ERR! syscall open
npm ERR! path /home/lcastillo/package.json
npm ERR! errno -2
npm ERR! enoent ENOENT: no such file or directory, open '/home/lcastillo/package.json'
npm ERR! enoent This is related to npm not being able to find a file.
npm ERR! enoent

npm ERR! A complete log of this run can be found in:
npm ERR! /home/lcastillo/.npm/_logs/2022-08-09T13_35_08_176Z-debug-0.log
bash: ./node_modules/.bin/webpack: No such file or directory
Obtaining file:///
ERROR: file:/// does not appear to be a Python project: neither 'setup.py' nor 'pyproject.toml' found.

[Julian Berman]

You're in your home directory, but you're meant to be in the game maker directory

[Julian Berman]

(I'm not sure where you cloned it to so I can't tell you where to cd to, but that's the issue)

[Luisitoon]

Thank you!! I will take a closer look!!

[Luisitoon]

Right!! I've made it through the point in which I have my version of the game downloaded as library.zip document. How can I show the game on a web browser now ??

[Luisitoon]

I've made it through publishing a Lean game on my GitHub Page. However, an error appears referring to the format... so the game is not being displayed successfully... this is the repository:" https://github.com/luisscastillo/lean-game " ... any help ??

[Alex J. Best]

I don't know where you are seeing an error, but you probably need some sort of workflow file like https://github.com/alexjbest/CAP-game/blob/main/.github/workflows/game.yml to make github deploy your game properly

[Luisitoon]

Thank you, Alex!! I will take a look!!

[Luisitoon]

Hi, all!! My game is fully working. However, the goal does not appear on the right after deleting "sorry"... do you know where the error could come from??

You can check my current game if it's clearer for you to understand what I mean: https://luisscastillo.github.io/lean-game/

[Kevin Buzzard]

It's a 404 for me

[Luisitoon]

Sorry, @Kevin Buzzard , I was fixing some levels. Now it should be working...

[Kevin Buzzard]

More worryingly, trying to solve the first level with refl gives a red squiggle under refl.

[Kevin Buzzard]

Yeah you have red squiggles under sorries. I don't think that happens in NNG. Presumably you have it compiling locally?

[Luisitoon]

Locally, it is working. However, when running it on GitHub Actions, it gives me the error:

Error: Could not find the file "/home/runner/work/lean-game/lean-game/Lean-game-maker/src/interactive_interface/lean_server/leanprover-community/lean:3.45.0/lean_js_js.js" which is necessary to run Lean in the browser.

And this error prevents GitHub Actions from deploying the webpage to its fullest.

[Kevin Buzzard]

Clarification: Locally you have it working on a server? (i.e. you can play the game via a web browser, just not on the github website)? If so then you must be 99% of the way there! If so then why not put that file where github actions wants it?

[Kevin Buzzard]

@Chris Birkbeck do you remember anything about putting NNG onto a github page? I don't have a clue about the web stuff myself, I just wrote (most of) the Lean code, other people did the web stuff for me.

[Chris Birkbeck]

So if you have a look at https://github.com/CBirkbeck/natural_number_game you can see the files that I needed to host the mirror. Once I had those in the repo I just pointed the github pages at this and it automatically finds the index.html and generates the pages. I dont really understand the error, but you could go get those files from here: https://github.com/leanprover-community/lean/releases and put them in the repo and see if that works?

[Luisitoon]

Ok, I will now take a look. Thanks both!! The specific problem is that if I run "make-lean-game" on the terminal of my laptop, it works perfectly because I added the file "lean_js_js.js" to the "lean:3.45.0" folder, manually. However, GitHub Actions assumes that "lean_js_js.js" is not in "lean:3.45.0" folder because, by the time that mpedramfar uploaded his repository, lean:3.45.0 did not exist...

[Kevin Buzzard]

Do you have access to that file? If so then this isn't really a question for this forum.

[Luisitoon]

Ok, @Kevin Buzzard, you can now check that the website is fully working. If you don't mind, I write here the solution so as to help newcomers develop their own game :+1:

[Luisitoon]

MESSAGE FOR NEWCOMERS:

To those who may be willing to develop their own videogame by using Lean 3, such as the Natural Number Game from Kevin Buzzard, you need to know that there exists two ways in order to do it:

A) Follow Lean Game Maker guide from Mohammad Pedramfar or Marc Masdeu if you want to start from scratch.

https://github.com/mpedramfar/Lean-game-maker

In this case, you must follow the installation guide, which is not updated and requires some changes to make it work.

B) Use, as a template, Topology Game, from Marc Masdeu and Barcelona Lean Seminar.
https://github.com/mmasdeu/topologygame
In this case, it is not necessary to follow the installation guide from A), but you will have to adapt your work into your GitHub Account. For this reason, the usage guide from A) is recommended. Also, you may need to familiarize yourself with GitHub Actions, GitHub Pages and workflows, which will be required.

When it comes to the deployment of the website, you should consider these two aspects:

• Whenever you see the line

curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- -v -y

in the code, you must change it into

curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -v -y

which is the new version.

• Whenever you see the phrase “python-openssl”, you may need to change it into “python3-openssl”.

• Because the template from B) uses some snippets of code from A), you need to know that A) worked with Lean 3.4.1 and 3.4.2 versions at most, so these are not the latest now. For this reason, Marc Masdeu implemented “curl -s https://api.github.com/repos/leanprover-community/lean/releases/latest” in his code, which uses the files that are needed to deploy the website from the latest version of Lean. If you are you using that latest version, then it is straightforward. However, if you are using Lean 3.45.0, for example, which is in between the latest and the Lean 3.4.1 and 3.4.2 versions, then you will need to go to the file “leanpkg.toml” and change the Lean version, which is written in the code, into the latest which is available at the time of your deployment.

[Kevin Buzzard]

I have problems with level 5 of tutorial world:
level5.png

[Luisitoon]

Ok, thanks!! I’ll take a look tomorrow :+1:

[Luis Castillo]

The problem is that I am using files from Lean 3.45.0 while running the game on Lean 3.46.0, so the game levels that need to import files from mathlib are not working. I will try to solve the problem this week and share the solution with you :smile:

[Luis Castillo]

Right, so here is the solution to the above problem:

I had to change:

- name: Make game
run: |
cat leanpkg.path
make-lean-game --source_base_url=$source_base_url --web_editor_url=$web_editor_url

into:

name: Make game
run: |
make-lean-game --source_base_url=$source_base_url --web_editor_url=$web_editor_url

on the .yml GitHub file... :+1:

[Luis Castillo]

Can anyone check if Tutorial World Level 5 is now working on https://luisscastillo.github.io/lean-game/ ??

[Eric Wieser]

That change should make no difference at all other than printing less to the console

[Patrick Massot]

And indeed level 5 isn't working

[Luis Castillo]

Eric Wieser ha dicho:

That change should make no difference at all other than printing less to the console

Exactly!! That should not make any difference, but now Level 5 is working for me...

[Eric Wieser]

It works for me too, but I still don't believe those lines are relevant. Given it fails for Patrick, it sounds like it might just randomly work or fail

[Julian Berman]

(It doesn't work here, so it's 50/50 so far :)

[Eric Wieser]

Just to check, we're talking about https://luisscastillo.github.io/lean-game/?world=1&level=5, right?

[Eric Wieser]

And clicking straight to that page in a fresh tab rather than navigating through levels 1-4 first

[Julian Berman]

I went through the previous levels here

[Luis Castillo]

Excatly, Eric!! So you are wacthing the import file error on the right, Julian ??

[Eric Wieser]

I think there's a bug here: https://github.com/luisscastillo/lean-game/runs/7839500241?check_suite_focus=true#step:12:15

[Luis Castillo]

What do you mean?? Could it be solved or is it just irresolvable, Eric ??

[Eric Wieser]

It's trying to checkout a specific version of mathlib, failing, then continuing anyway

[Luis Castillo]

As far as I've been observing that deployment, what is nonsense to me is the fact that "Install elan" is using Lean v.3.46.0 (because it is latest) while all the other files are running on Lean v3.45.0, not sure if this is also problematic...

[Eric Wieser]

The bug is here:

https://github.com/mpedramfar/Lean-game-maker/blob/b875c60489e8d970fae31f6259b5f92f09eb1979/src/lean_game_maker/interactive_loader.py#L32

That doesn't actually check that leanpkg build succeeds

[Eric Wieser]

(it doesn't succeed, and so likely all the subsequent results are worthless)

[Luis Castillo]

Is there anything I could do to solve that ??

[Julian Berman]

I think that bug is obfuscating whatever the other bug in your repo is. Because yeah lean-game-maker shouldn't proceed if that fails, but that doesn't explain the actual error in the GH Action (i.e. how to get the command to succeed). Not sure if I know enough about game maker to know what that is, but let's see.

[Luis Castillo]

Definitely puzzling to me...

[Eric Wieser]

I opened https://github.com/mmasdeu/Lean-game-maker/pull/3 to stop that obfuscation

[Eric Wieser]

You should be able to checkout refs/pull/3/merge from that repo to get a version with my changes

[Julian Berman]

(Was finishing my last call of the day), though in the background running this from a fork of course produced a different result :D

[Julian Berman]

@Luis Castillo where did you get the lean_js_js.js file in your repo, and how'd you get them onto your gh-pages branch?

[Julian Berman]

Did you copy them from what Chris linked? EDIT: no seems not -- did you follow the compilation instructions from above then?

[Luis Castillo]

Julian Berman ha dicho:

Luis Castillo where did you get the lean_js_js.js file in your repo, and how'd you get them onto your gh-pages branch?

That file is just being downloaded by running "https://github.com/luisscastillo/lean-game/blob/main/.github/workflows/game.yml#L65"... Then, "https://github.com/luisscastillo/lean-game/blob/main/.github/workflows/game.yml#L78" just sends the docs to gh-pages.

[Julian Berman]

Ah sorry, missed that in the workflow, hrm why didn't that work on mine.

[Julian Berman]

The fact that you changed the workflow to hardcode 3.45.0 seems like it'd cause issues considering it seems to try to upgrade mathlib when it runs (and now mathlib is on 3.46.0, so the bot immediately pushes a commit moving it when it runs)

[Julian Berman]

I'm not sure that's related to the original issue but it's something I notice trying to run it myself

[Luis Castillo]

Thanks, Julian!! That's a good point!! Yet, I don't even have a clue why is working 50/50 at some times...

[Luis Castillo]

Can anyone check if Tutorial World Level 5 is working for you here (https://luisscastillo.github.io/lean-game/). Thanks!!

[Marc Masdeu]

Yes, it works for me, @Luis Castillo (nice to see you here, BTW!)