Lean Game Maker JavaScript Lean server

Stream: general

[Nono]

Hello everyone,
I'm a student from Germany and I'm trying to create a Lean Game with the Lean Game Maker for a project. I was able to create the .zip file but I'm unsure about the next steps. The USAGE.md tells me to use a JavaScript Lean server and I tried to this as it is explained in this repository. I'm running into some issues however, so I was wondering if you guys did this before and could tell me where to go from here.

Also I'm using Ubuntu with WSL and often get the message UNC-Paths not supported which causes some problems, since it defaults to the windows directory. Should I use a virtual machine instead?

Sorry if I posted this in the wrong place!

[Jon Eugster]

It would be easier to help if you said what kind of problems you encountered, but following the last section of the manual you linked (USAGE.md) you download the file lean-3.50.3--browser.zip (or the one for the lean3 version you are using), unzip it and add the 3 files that are in this zip file into the folder YOURPROJECT/src/interactive_interface/lean_server/.
(i.e. I don't think there should be need to build anything manually using the second link you provided)

If you give a bit more details about what you're stuck on, I did set-up a lean3-game on ubuntu and macos recently, and could check what I did back then.

[Nono]

Thanks for the answer!
I already did what you mentioned and was able to use the Lean Game Maker on the Lean Game Skeleton to create a Lean Maze game-3.0.0-library.zip as it is explained in the "Making a game" section. But I'm unsure about the next steps. How can I run this in a browser now? I thought I would have to setup a Javascript Lean Server as it is mentioned in the "Lean Server" section. Is there an easier way to run this locally?

[Jon Eugster]

ok, so at that point you have everything you need in that folder with Lean Maze game-3.0.0-library.zip and a index.html and more stuff.

You just need the content of that folder be where your server finds it. If you don't have a server and run it locally you could do

cd THAT_FOLDER
python3 -m http.server

which should start a basic server that serves on http://localhost:8000 by default, which you can open in your browser. Does that work for you?

[Alex J. Best]

Personally I never worried about running locally, simply copying https://github.com/mmasdeu/topologygame and pushing to github was enough for me to develop a game (note the https://mmasdeu.github.io/topologygame/test/ test version can be updated independently of the main one)

[Jon Eugster]

That is indeed a very smooth option if you want your project on github.io :ok:

[Nono]

Jon Eugster schrieb:

ok, so at that point you have everything you need in that folder with Lean Maze game-3.0.0-library.zip and a index.html and more stuff.

You just need the content of that folder be where your server finds it. If you don't have a server and run it locally you could do

cd THAT_FOLDER
python3 -m http.server

which should start a basic server that serves on http://localhost:8000 by default, which you can open in your browser. Does that work for you?

My folder does not contain the index.html you mentioned. Do I have to create it myself? grafik.png this is the folder where the game library.zip is. If i start the server here as you explained i only get a directory listing for it.

[Nono]

Alex J. Best schrieb:

Personally I never worried about running locally, simply copying https://github.com/mmasdeu/topologygame and pushing to github was enough for me to develop a game (note the https://mmasdeu.github.io/topologygame/test/ test version can be updated independently of the main one)

Thanks, I created my repository with this template but how do I run this as a website like https://mmasdeu.github.io/topologygame/?

[Alex J. Best]

If you go the actions tab on github can you see any actions as having been run?

[Nono]

Just the inital commits.

[Alex J. Best]

If you click MakeGame on the left of the workflows tab, then the run workflow button (on the right), set production to true and manually run the workflow by clicking the green button it should build

[Nono]

Ah okay, I'll try that right now. Thank you!

[Alex J. Best]

The repo is a little out of date in terms of the lean files, so simplifying it a bit to get something building first is probably best (and you'll want to write your own content anyway of course!). So I'd edit game_config.toml to remove all the levels except set theory to get started or something

[Nono]

Makes sense. It seems the workflow will take some time but I think I can figure out the rest. Thank you for your help! @Alex J. Best @Jon Eugster

[Nono]

@Alex J. Best Actually it seems like the workflow fails at "upgrade Lean and dependencies" and and stops. Did you run into this aswell?

[Alex J. Best]

Oh I think so yes, that workflow has been broken for a few months unfortunately, and it was a bit overeager anyways.
Here is the workflow I'm actually using https://github.com/alexjbest/CAP-game/blob/main/.github/workflows/game.yml

[Alex J. Best]

This version also runs on every push, rather than having to be manually triggered

[Alex J. Best]

And will push to the test directory by default

[Alex J. Best]

@Marc Masdeu should we update your template perhaps?

[Nono]

Ok perfect. Thanks again!

[Nono]

It seems there is an error in leanpkg build

Run echo "::set-output name=started::true"
Warning: The `set-output` command is deprecated and will be disabled soon. Please upgrade to using Environment Files. For more information see: https://github.blog/changelog/2022-10-11-github-actions-deprecating-save-state-and-set-output-commands/
python: can't open file 'scripts/detect_errors.py': [Errno 2] No such file or directory
Error: Process completed with exit code 2.

[Alex J. Best]

I guess you'll need to copy https://github.com/alexjbest/CAP-game/blob/main/scripts/detect_errors.py across to your project too

[Nono]

Ok, I'll do that.

[Nono]

Unfortunatly I'm running into another error at "Deploy production":

remote: Write access to repository not granted.
fatal: unable to access 'https://github.com/Nono1337/Leantest.git/': The requested URL returned error: 403
Running post deployment cleanup jobs… 🗑️
/usr/bin/git checkout -B github-pages-deploy-action/mibtsw6pt
Reset branch 'github-pages-deploy-action/mibtsw6pt'
/usr/bin/git worktree remove github-pages-deploy-action-temp-deployment-folder --force
Error: The deploy step encountered an error: The process '/usr/bin/git' failed with exit code 128 ❌
Deployment failed! ❌

Do you have a solution to this as well?

[Alex J. Best]

Can you post more of the log? I don't recognise the error

[Nono]

Sure!

Run JamesIves/github-pages-deploy-action@4.1.5

    GitHub Pages Deploy Action 🚀

    🚀 Getting Started Guide: https://github.com/marketplace/actions/deploy-to-github-pages
    ❓ Discussions / Q&A: https://github.com/JamesIves/github-pages-deploy-action/discussions
    🔧 Report a Bug: https://github.com/JamesIves/github-pages-deploy-action/issues

    📣 Maintained by James Ives: https://jamesiv.es
    💖 Support: https://github.com/sponsors/JamesIves
Checking configuration and starting deployment… 🚦
Deploying using Deploy Token… 🔑
Configuring git…
/usr/bin/git config user.name Nono1337
/usr/bin/git config user.email Nono1337@users.noreply.github.com
/usr/bin/git config --local --unset-all http.https://github.com/.extraheader
/usr/bin/git remote rm origin
/usr/bin/git remote add origin ***github.com/Nono1337/Leantest.git
Git configured… 🔧
Starting to commit changes…
/usr/bin/git ls-remote --heads ***github.com/Nono1337/Leantest.git refs/heads/gh-pages
Creating worktree…
/usr/bin/git worktree add --no-checkout --detach github-pages-deploy-action-temp-deployment-folder
Preparing worktree (detached HEAD 1ca50cd)
/usr/bin/git checkout --orphan gh-pages
Switched to a new branch 'gh-pages'
Created the gh-pages branch… 🔧
/usr/bin/git reset --hard
/usr/bin/rsync -q -av --checksum --progress /home/runner/work/Leantest/Leantest/html/. github-pages-deploy-action-temp-deployment-folder --delete --exclude CNAME --exclude .nojekyll --exclude .ssh --exclude .git --exclude .github
/usr/bin/git add --all .
Checking if there are files to commit…
/usr/bin/git add --all .
/usr/bin/git checkout -b github-pages-deploy-action/mibtsw6pt
Switched to a new branch 'github-pages-deploy-action/mibtsw6pt'
/usr/bin/git commit -m Deploying to gh-pages from @ Nono1337/Leantest@1ca50cd69c1360d9e82c6f929fcda686807502ff 🚀 --quiet --no-verify
/usr/bin/git push --force ***github.com/Nono1337/Leantest.git github-pages-deploy-action/mibtsw6pt:gh-pages
remote: Write access to repository not granted.
fatal: unable to access 'https://github.com/Nono1337/Leantest.git/': The requested URL returned error: 403
Running post deployment cleanup jobs… 🗑️
/usr/bin/git checkout -B github-pages-deploy-action/mibtsw6pt
Reset branch 'github-pages-deploy-action/mibtsw6pt'
/usr/bin/git worktree remove github-pages-deploy-action-temp-deployment-folder --force
Error: The deploy step encountered an error: The process '/usr/bin/git' failed with exit code 128 ❌
Deployment failed! ❌

Warning: The `set-output` command is deprecated and will be disabled soon. Please upgrade to using Environment Files. For more information see: https://github.blog/changelog/2022-10-11-github-actions-deprecating-save-state-and-set-output-commands/

[Alex J. Best]

I'm not sure what the issue is, it could be something like https://github.com/JamesIves/github-pages-deploy-action/issues/1110#issuecomment-1117481234, or maybe that the repo is private?

[Nono]

Oh yes I made it private. I didn't know that would cause errors :man_facepalming: Thanks!

[Nono]

@Alex J. BestThe workflow finished and I was able to create the gh-pages branch but when I try to deploy it as a page it doesn't seem to work. I only get an empty page. I deployed the branch through github pages, should I use the workflow instead?

[Alex J. Best]

Hm that page is for your personal .github.io site, I would expect it to be something like https://nono1337.github.io/LeanTest/ . If you inspect the website it says that https://nono1337.github.io/game_data.json cannot be found, does some step of the workflow look like its adding that ok?

[Nono]

You were right, the game_data.json wasn't generated due to an error in the game_config.toml. It works now! Thank you very much for your help!