lean game maker

Stream: general

[Chris Birkbeck]

I'm trying to use the lean game maker and I'm having some trouble running it. I think I have managed to install it on my Windows pc using the Ubuntu WSL (but maybe I messed this up). In any case I can run make-lean-game in the directory and it does produce a html folder with some files, but the website I get is empty. It also doesn't create a zipped version of the olean files and no game_data file. The error I'm getting is Error: [Errno 2] No such file or directory: 'leanpkg' which is strange because there is such a file in the same directory where the game_config file is.

Does anyone have any idea what might be going wrong?

[Julian Berman]

I don't know about game maker (and don't have it nor windows in front of me to check), but that error condition in other contexts usually indicates a PATH issue -- does the error change or go away if you add the directory that leanpkg is in to your PATH explicitly?

[Marc Masdeu]

@Chris Birkbeck you may use the template at https://github.com/mmasdeu/topologygame to create your own game. It gets automatically served from github pages and has some custom additions (like wildcard expansion for levels, or show-source button).

[Chris Birkbeck]

Yes that's what I was trying to use. I'm at the point that if I run make-lean-game --nolib then it seems to create the right files, but since it doesn't create the library it doesn't work as a "game". I installed everything on the WSL now and if I run make-lean-game it now finds the leanpkg file, but its trying to build all of mathlib it seems. Is this normal? I thought it would only build the project.

[Marc Masdeu]

It should be getting the right oleans and thus not compile the whole library. Also be aware that it sometimes takes some time (read hours) for it to work. As far as I understood, it has nothing to do with compiling, it's just that some things get cached in your browser and/or servers and it takes time for them to get forgotten.

[Kevin Buzzard]

With NNG it would always compile mathlib, or at least enough of it to get the game running

[Chris Birkbeck]

Ok I got it working now. It seems there was some issues with finding the olean files. But making a new project and starting there seems to have worked. It now seems to not compile all of mathlib, but only the bits needed.

[Riccardo Brasca]

I hope this is for a number theory game!

[Chris Birkbeck]

That'll be the next one! I'm trying out a logic one since here at UCL they are running a summer course for students and I think it would be fun to try and make it into a game.

[Luisitoon]

Right, so I've made it through the library.zip document for my game in Lean. However, an error appears in the terminal: Error: [Errno 2] No such file or directory: "msguniq". Is solving this error indispensable to run the game ??