Zulip Chat Archive

I am trying to use the lean game maker to make a local version of the real number game. I think I downloaded everything correctly and when I make the game it seems to work. However, when everything finishes and I try to run the html file nothing pops up in the browser. I've tried a few things but at this point I am pretty stuck. Does anyone have any suggestions on what I can do?

Chris Birkbeck (Jun 21 2022 at 15:28):

I haven't managed to get the html to work like that. If you add it to a github repo and then create the github page using those files then it does generate the correct website.

David Talone (Jun 21 2022 at 15:41):

What files do I need to upload to github to generate the website?

Chris Birkbeck (Jun 21 2022 at 17:20):

If you run make-lean-game it will create a bunch of files in some folder (or make a folder called html). I just upload all of that into a repo and then point the github pages at that and it seems to work.

David Talone (Jun 21 2022 at 17:28):

Sorry for all the questions but what do you mean by saying point the github pages at the folder? I got the folder into github but I'm not sure what to do with it.

Chris Birkbeck (Jun 21 2022 at 18:11):

No problem! So if you go to settings and look at the pages tab then you can select a branch and then select between root or docs folder (I don't know how to get github to look for things in subfolders) . But if you have all the files in the main branch, say, then select this branch and then the root folder. It should then generate the pages for you from this.

If it helps you can look at what the mirror for the NNG looks like here: https://github.com/CBirkbeck/natural_number_game. If your repo looks like this then the above should work.

David Talone (Jun 21 2022 at 19:03):

I got it working. Thank you so Much!

David Talone (Jun 22 2022 at 14:02):

I got it working but now it says that lean is busy and it will never go away. Does anyone have any suggestions on what to do about this?

Kevin Buzzard (Jun 22 2022 at 14:09):

Allow cookies (some people couldn't play NNG because they had some browser paranoid settings on)

David Talone (Jun 22 2022 at 14:15):

I was able to run the NNG just fine but now that I'm trying this out it just says lean is busy. I turned on cookies anyway but it doesn't seem to have helped.

Chris Birkbeck (Jun 22 2022 at 14:21):

I had that problem, but for me it was because make-lean-game wasn't creating the mathlib olean files.

David Talone (Jun 22 2022 at 14:31):

How did you fix that problem?

Bart Michels (Jun 22 2022 at 14:34):

The game is built on a lean project right? So maybe the same way you would do for lean projects?
https://leanprover-community.github.io/leanproject.html#getting-mathlib-oleans

Chris Birkbeck (Jun 22 2022 at 14:53):

For me the issue was that when I ran make-lean-game I had an error saying Error: [Errno 2] No such file or directory: 'leanpkg'. It turned out that I just had a bad installation of the game maker, which once I installed properly, got rid of the error and then generated the correct files.

David Talone (Jun 22 2022 at 15:17):

Interesting, it doesn't seem like anything is working for me. It's not necessarily a big deal but it is a bit annoying.

David Talone (Jun 22 2022 at 15:29):

I figured out that it's only certain levels that aren't working but at least some of it is good.

Bart Michels (Jun 22 2022 at 17:22):

Are you on Windows? The latest update (KB5014697) introduced some network-related bugs, maybe it's that.

David Talone (Jun 22 2022 at 17:29):

No I'm on mac. For whatever reason everything seems to work now. I didn't really do anything but now it works.

Last updated: Dec 20 2023 at 11:08 UTC

leanprover-community / mathlib