Leanblueprint for Windows

Stream: general

[Kajani Kaunda]

Is there a stable version for Patrick Massot's wonderful LeanBlueprint for windows 10 and above? It's ok if the answer is no, I will just have to go Linux ... :smile:

[Gareth Ma]

A non-answer: can you use docker to run leanblueprint?

[Kajani Kaunda]

Gareth Ma said:

A non-answer: can you use docker to run leanblueprint?

Well, if using the right O.S. is critical then Docker would work if it uses the right O.S. In my case, I guess I will just use a virtual machine. I will just spinnup a VMware Machine with UBUNTU or DEBIAN ... It should work. Once I get everything installed, then maybe I should share it. That way all that one has to do is download the machine, and your good to go! Do you think people would like that?

[Patrick Massot]

I don't understand the question. There is nothing depending on the OS here.

[Kajani Kaunda]

Patrick Massot said:

I don't understand the question. There is nothing depending on the OS here.

Ah. sorry I was not so clear...I just wanted to know if I can use the software on my Windows Machine... My apologies for not being clear...

[Yaël Dillies]

Patrick Massot said:

There is nothing depending on the OS here.

There is certainly some OS-dependent pain. As a matter of fact I still haven't managed to install leanblueprint on my Windows 10 :smiling:

[Kajani Kaunda]

Yaël Dillies said:

Patrick Massot said:

There is nothing depending on the OS here.

There is certainly some OS-dependent pain. As a matter of fact I still haven't managed to install leanblueprint on my Windows 10 :smiling:

Leanblueprint is great software!. So one way or the other we will get it to work and use it! :smile:

[Terence Tao]

I was just able (with a lot of assistance from @Pietro Monticone) set up lean blueprint on a Windows machine following the template instructions at https://github.com/pitmonticone/LeanProject . There were four vaguely Windows-related issues that came up, three of them minor:

1. In order to install lean blueprint, one must first install the PyGraphViz package in python. The instructions in https://pygraphviz.github.io/documentation/stable/install.html are slightly more complicated in Windows than in other OSes, but not too bad.
2. When I installed lean blueprint, the script directory that it was installed in was not in my PATH directory, so I had to manually add it there (or supply the full directory path for the executable).
3. My python build used different commands than "python3" or "pip3", but it was an easy matter to convert the template instructions to match the commands in my local python setup.
4. For some reason, my git setup suppressed the ".git" extension for the remote repository links (as reported in git remote -v). This confused the lean blueprint setup script, which relied in matching with a string ending in .git in order to guess the repository name. Hopefully this can be fixed in the next update of lean blueprint though. In the meantime there was a workaround, which was to use git remote set-url origin https://github.com/<user name>/<project name>.git to manually restore the .git extension.

[For the record: in case the leanblueprint setup goes awry, one should delete the blueprint and home_page directories from the repository, remove any items from lakefile.toml and lake-manifest.json that reference blueprint sites, and restart leanblueprint. We had to do this a couple times in the process of debugging issue #4.]

If anyone else wishes to try such a setup based on Pietro's template, please give @Pietro Monticone any feedback on your user experience (actually, it might be a good idea to share any such experiences directly on this thread). Once the kinks in the process are straightened out, this may well be the simplest way to get a blueprint up and running (in Windows or otherwise).

[Kajani Kaunda]

Terence Tao said:

I was just able (with a lot of assistance from Pietro Monticone) set up lean blueprint on a Windows machine following the template instructions at https://github.com/pitmonticone/LeanProject . There were four vaguely Windows-related issues that came up, three of them minor:

1. In order to install lean blueprint, one must first install the PyGraphViz package in python. The instructions in https://pygraphviz.github.io/documentation/stable/install.html are slightly more complicated in Windows than in other OSes, but not too bad.
2. When I installed lean blueprint, the script directory that it was installed in was not in my PATH directory, so I had to manually add it there (or supply the full directory path for the executable).
3. My python build used different commands than "python3" or "pip3", but it was an easy matter to convert the template instructions to match the commands in my local python setup.
4. For some reason, my git setup suppressed the ".git" extension for the remote repository links. This confused the lean blueprint setup script, which relied in matching with a string ending in .git in order to guess the repository name. Hopefully this can be fixed in the next update of lean blueprint though.

If anyone else wishes to try such a setup based on Pietro's template, please give Pietro Monticone any feedback on your user experience. Once the kinks in the process are straightened out, this may well be the simplest way to get a blueprint up and running (in Windows or otherwise).

Thank you very much. I will give it a try. I will surely give feedback.

[Pietro Monticone]

Thank you @Terence Tao for the summary.

I would just suggest to discuss this in the dedicated Zulip topic here https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Tutorial.3A.20Getting.20Started.20with.20Blueprint-Driven.20Projects/near/456633811

[Metin Ersin Arıcan]

You can use WSL (Windows Subsystem for Linux). It’s essentially a lightweight and easy-to-setup virtual machine.

[Kajani Kaunda]

Metin Ersin Arıcan said:

You can use WSL (Windows Subsystem for Linux). It’s essentially a lightweight and easy-to-setup virtual machine.

Oh!, Thats nice to know. We are soon going to get to the optimal configuration.

[Patrick Massot]

I see lots of things that are really about getting python to work on Windows but are not specific at all to leanblueprint. There isn’t much we can do about that. The WSL trick is basically: use a more friendly operating system (but embedded into Windows) and is indeed a very common solution to such issues. The story of the missing.git extension in the remote url is very surprising but it doesn’t cost much to try to work around it from our side. I’ll do that very soon.

[Kajani Kaunda]

Ok, following the tips from @Terence Tao and @Pietro Monticone, I happy I got a page! But it's the template page - because I cloned it to my local drive with the intention of changing it later. So now what I have to do is to update it with my own content and then figure out how to build the ".../blueprint" page or how it is built. Maybe it is as simple as just pointing it to a different project that has all of ones lean4 code etc. Example: https://my-git-name.github.io/my-lean4-project/. Let's see, ...

[Floris van Doorn]

Patrick Massot said:

I don't understand the question. There is nothing depending on the OS here.

There is also https://github.com/PatrickMassot/leanblueprint/pull/29 which is OS-dependent.

[Floris van Doorn]

Also, I just tried leanblueprint serve just now and it doesn't work for me. When running it, it gives no output and doesn't serve a webpage. after interrupting with ctrl-c it shows the message

Serving http://0.0.0.0:8000/
Press Ctrl-c to interrupt.

(and still doesn't serve the webpage)