Zulip Chat Archive

Stream: new members

Topic: Windows Install Lean-game-maker


view this post on Zulip ZainAK283 (Jul 19 2020 at 01:43):

I'd like to install https://github.com/mpedramfar/Lean-game-maker/blob/master/INSTALL.md but I have a windows laptop, not linux, how do I go about doing this? In particular the command for:

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

view this post on Zulip Bryan Gin-ge Chen (Jul 19 2020 at 01:55):

I haven't tried it before, but maybe you could try https://github.com/pyenv-win/pyenv-win

view this post on Zulip Dan Stanescu (Jul 19 2020 at 02:01):

I tried to install it on a Mac and gave up. It will be even more difficult on Windows.
Installing pyenv is advised, but that line sudo apt ... is about installing all the dependencies for python.
I think one of the best bets is to install Anaconda, which puts just about everything on Windows and gives you an environment (currently it comes with python 3.7.6 I think).

view this post on Zulip Dan Stanescu (Jul 19 2020 at 02:03):

But even this will eventually require quite some experience with handling read/write permissions on Windows and so on.

view this post on Zulip Dan Stanescu (Jul 19 2020 at 02:08):

Then it'll be npm and gettext, the latter I have no idea how to get it on Windoze yet.

view this post on Zulip Dan Stanescu (Jul 19 2020 at 02:11):

It is usually installed with apt-get on Linux (although most of the time is pre-installed) and I'm not sure that GitBash will handle it.

view this post on Zulip Bryan Gin-ge Chen (Jul 19 2020 at 02:44):

We should probably tag @Mohammad Pedramfar.

view this post on Zulip Dan Stanescu (Jul 19 2020 at 14:01):

@ZainAK283 Just to clarify, I'm not saying it can't be done but it will need some work. It's difficult to provide instructions that will work for any scenario, but FWIW I'm willing to help in this chat so there's a record of it. The easiest way is to start by installing Anaconda (https://anaconda.org/). This should ideally take care of all the steps in the Python 3.7 section of the install page. Then also install nodejs using the link just following the start of the Install Lean-game-makersection in the instructions. Don't worry about pyenv for now, as Anaconda will create a python 3.7.6 environment anyway; it will be called base. You should be able install in that environment.

view this post on Zulip Reid Barton (Jul 19 2020 at 14:03):

What about WSL, e.g. https://ubuntu.com/wsl?

view this post on Zulip Dan Stanescu (Jul 19 2020 at 14:05):

Good question. I expected that to work, but AFAIK @ZainAK283 tried that path already, as per some of his earlier posts.

view this post on Zulip Reid Barton (Jul 19 2020 at 14:13):

I see. Maybe the easiest path is to use VMware or similar then.

view this post on Zulip Mohammad Pedramfar (Jul 19 2020 at 17:30):

I don't use windows, but I've been using anaconda for a while and it's great.

view this post on Zulip Mohammad Pedramfar (Jul 19 2020 at 17:31):

Dan Stanescu said:

I tried to install it on a Mac and gave up. It will be even more difficult on Windows.
Installing pyenv is advised, but that line sudo apt ... is about installing all the dependencies for python.
I think one of the best bets is to install Anaconda, which puts just about everything on Windows and gives you an environment (currently it comes with python 3.7.6 I think).

You can choose the python version by saying conda create -n myenv python=3.6 or any other version of python

view this post on Zulip Dan Stanescu (Jul 19 2020 at 17:39):

Oh great, I didn't know you could create environments newer than the python version Anaconda ships with.
But I'll advocate for using the default, currently 3.7.6, to start with. I had trouble with some newer versions (for 3.8.x I needed to upgrade setuptools etc.) which is not desirable for an initial install.

view this post on Zulip ZainAK283 (Jul 19 2020 at 19:54):

Thank you all for responding!
If a windows install won't work, then I can use a WSL. In which case, everything is fine up until the last section of https://github.com/mpedramfar/Lean-game-maker/blob/master/INSTALL.md

basically, I'm computer illiterate (my bad), so I'm not sure if I have nodejs and gettext, how to check if I do, or how to install in a WSL. I'm also not sure where the "virtual environment" i should type the last command

view this post on Zulip Dan Stanescu (Jul 19 2020 at 20:19):

@ZainAK283 Well, it appears there's some agreement that you could start by installing Anaconda, which has a very user-friendly Windows-like setup. Nodejs can also be installed in a similar way; just follow the links. Once that's done, we'll take it from there.

view this post on Zulip ZainAK283 (Jul 19 2020 at 20:51):

Got them! (I also installed chocolatey with nodejs just in case)
What next?

view this post on Zulip Kevin Buzzard (Jul 19 2020 at 21:30):

Hey Zain -- out of interest why do you want to install the game maker?

view this post on Zulip ZainAK283 (Jul 19 2020 at 21:33):

I think the games are a fantastic way to make Lean more accessible to beginners, especially those who are computer illiterate (even more than me!)
After playing with NNG, playing more games means that by the time you decide to install lean locally, you've got a seriously solid grasp of how to lean

view this post on Zulip ZainAK283 (Jul 19 2020 at 21:35):

I also really like the interface, showing the theorems and tactics on the side

view this post on Zulip Dan Stanescu (Jul 19 2020 at 21:59):

ZainAK283 said:

Got them! (I also installed chocolatey with nodejs just in case)
What next?

OK, let's just check npm. For this, open an Anaconda prompt.

view this post on Zulip Dan Stanescu (Jul 19 2020 at 21:59):

You should have the Anaconda prompt shortcut installed on the desktop.

view this post on Zulip Dan Stanescu (Jul 19 2020 at 22:01):

If not, search for it using the search menu. There should actually be two of them but leave the Power one aside for now.

view this post on Zulip ZainAK283 (Jul 19 2020 at 22:09):

image.png Is this what you mean?

view this post on Zulip Dan Stanescu (Jul 19 2020 at 22:12):

Totally. If everything were right (but it won't) you could just type the commands in the last section of the install page.
For now, remove the 0 just after the > and type "which npm" then enter. If that says nothing, try "whereis npm". I want to hope that the prompt interacts well with GitBash.

view this post on Zulip Dan Stanescu (Jul 19 2020 at 22:17):

You can do all this in the Lean-game-maker directory. You can go there by cd which means "change directory".
Like cd C:\Users\Zain\...
We may actually need to connect in a visual way, unfortunately this will be too difficult by just typing instructions.

view this post on Zulip Kevin Buzzard (Jul 19 2020 at 22:47):

Zain two remarks: if you want to collaborate to make a game I'd be more than happy (real number game and group theory game are slowly becoming viable, complex number game exists but not in browser form, people are thinking about category theory game on the Discord, filter game was suggested last week and I think it will fly, other games are possible, I think there's scope for a topology game). And secondly you don't have to get the game maker installed on Windows to actually make the games, you just need the game maker to compile them. If you collaborate with someone who has access to a Linux machine they can compile for you

view this post on Zulip ZainAK283 (Jul 20 2020 at 10:47):

Great!
Dan has offered to help, so I'll take him up on that - if that doesn't work, then I'll shove all the compiling worries on to someone else :)


Last updated: May 13 2021 at 17:42 UTC