beer reward

Stream: general

[Patrick Massot]

Starting on January 14th, I'll be teaching my Lean-powered undergraduate course again. Last year I was so afraid of the installation procedure on Windows that I didn't tell my students to try to install Lean at home. But this turned out to be a huge issue. So I'm offering as much beer as you can drink during Fomm2020 to anyone contributing to a download-and-click-only install of Lean+VScode+plugin+update-mathlib on Windows which then allows to download and unzip a project containing a compiled mathlib and use it without recompiling or typing any command in a shell. Ideally this should work on any version of Windows that my students could have, but having the main current version covered would already be nice. Useful starting points could include: https://github.com/NeilStrickland/lean_installer and https://dzone.com/articles/making-a-stand-alone-executable-from-a-python-scri or similar (one can only assume students will have an installation of python fighting Lean, not helping it). Let me ping potential windows users: @Rob Lewis, @Mario Carneiro, @Floris van Doorn, @Neil Strickland

[Andrew Ashworth]

Would an installer be necessary? It seems to me you could just make a zip file. Some combination of VSCode portable mode https://code.visualstudio.com/docs/editor/portable, configuring the VSCode settings file, and bundling Lean and Mathlib.

[Patrick Massot]

I don't know about installer. I only know students are not able to follow a list of instructions if is has more than two items or if one of the item is not "download" or "click".

[Patrick Massot]

And also I have no access to Windows so I can't try anything.

[Andrew Ashworth]

Ahh. Windows 10 has unlimited trial versions for development, in case you end up needing to do your own troubleshooting: https://developer.microsoft.com/en-us/windows/downloads/virtual-machines

[Rob Lewis]

If you really want them to just download and unzip a project containing compiled mathlib, then installing update-mathlib should be unnecessary, right?

[Rob Lewis]

That should let you skip all the Python nonsense.

[Rob Lewis]

If that's the case, I agree with Andrew, throw everything in one zip with a configured portable VSCode. Maybe wrap it in a script that adds a shortcut or executable or something to open the right directory in VSCode.

[Patrick Massot]

I cheated a bit by mixing my lecture requirements with the general case. But I shouldn't have done that. What is urgent indeed doesn't need update-mathlib.

[Patrick Massot]

@Simon Hudon Will your current IO api work allow to code update-mathlib in Lean?

[Patrick Massot]

But I still don't know how the portable VScode thing will find Lean.

[Simon Hudon]

I still don’t have support for processes but once I have that it should be doable and more portable than a Lean 3 solution

[Bryan Gin-ge Chen]

But I still don't know how the portable VScode thing will find Lean.

You might be able to include in your bundle a settings.json with a line that sets lean.executablePath to an appropriate relative path.

[Patrick Massot]

I will probably try such hacks since nobody seems interested by beer. But it would be nice to offer a full solution.

[Andrew Ashworth]

The latest versions of CMake allow easier installer creation. When Lean4 rolls around I will investigate it if I have time, I recently had to do a lot of this kind of thing for work so I have some familiarity with it. It's a little arcane.

[Kevin Buzzard]

I was thinking about this (for the same sort of reasons) a month or two ago, and it seemed to me to be reasonable to say to the students "download VS Code by clicking here" but then I decided that the holy grail would be for them never to have to type a command into a command line, so ideally one would want one click which says "tell me a directory where you want to put your Lean stuff" and then installs lean (somewhere) + a tutorial repo with compiled mathlib (in the directory they chose) and also, ideally, installs the Lean extension for VS Code.

[Simon Hudon]

@Andrew Ashworth What do you mean by "rolls around"? The source code is available and it can be built so you can already use it

[Andrew Ashworth]

I tried to build Lean 4 in... November? The CMake build on Windows with Clang + Mingw wasn't working for me. There was some issue with the bootstrap procedure (I don't really remember what it was, because I only spent ~30 minutes investigating). Perhaps the Windows build works now? I have not tested it since then.

[Simon Hudon]

The CI system builds a Windows version, maybe you should look at it

[Andrew Ashworth]

Yeah. I knew going in it was going to be a semi-pain, since Nix doesn't run on Windows at all. Maybe I will try again this weekend.

[Patrick Massot]

I think I just managed to boot the Windows VM pointed out by Andrew!

[Patrick Massot]

So I'm now exploring that portable mode in VScode. I manage to "install" VScode + lean plugin in user space. Now I can download lean and put it in the same folder. But I need to choose the right Lean executable path. @Gabriel Ebner or @Bryan Gin-ge Chen do you have any idea how I could use a path relative to the VScode executable here?

[Patrick Massot]

I don't even know whether I should use Windows backward path separator here.

[Patrick Massot]

It seems that giving a full absolute path with backward separators works in the sense that it doesn't complain about lauching Lean. But then #check nat takes forever. I'll continue investigating tomorrow. But this is pointless if we can't solve that relative path issue.

[Bryan Gin-ge Chen]

Just now I set up a portable vscode on my Mac, but I couldn't get the extension to find Lean whenever I used any relative path (even ~/path/to/lean didn't work). There's a semi-related issue here that I found after googling for "VS Code relative paths" (long story short, a keyword to use in settings paths that would stand for the location of the executable doesn't exist yet).

Maybe we could hack something in vscode-lean (or a fork?). Apparently, we can get the absolute path to the vscode-lean extension with vscode.extensions.getExtension ("jroesch.lean").extensionPath. Since the folder structure for the portable VS Code that you provide should be predictable, we should be able to use this method to give an absolute path to Lean?

I'll experiment with this a little bit more tonight, but no promises.

[Bryan Gin-ge Chen]

OK, here's a fork of vscode-lean which allows you to use %extensionPath% in the lean.executablePath and lean.leanpkgPath settings as a placeholder for the absolute path to the extension. You then can specify a relative path on top of that and hopefully that's enough for your needs. To test it out:

• Clone the repo and then bundle it with vsce package to get a .vsix file. Or if you trust me, you can download the attached file: lean-0.14.8.vsix.
• Open the extensions tab in your portable version of VS Code and then click the three dots at the top right to "Install from VSIX".
• Now open the settings and edit lean.executablePath and lean.leanpkgPath (the 2nd most likely doesn't matter since your students are not likely to use the leanpkg integration). The string should begin with %extensionPath% and then include a relative path from the extension folder inside the "portable data" folder to the Lean executable you want to use. E.g. I think %extensionPath%/../../../lean will point to lean in the same directory as the Visual Studio Code executable.

I only did some minimal testing, so I'm not sure if you need to use forward slashes or back slashes on Windows.

@Gabriel Ebner If you think this would be valuable for the main extension I can add some more documentation and PR this.

[Gabriel Ebner]

@Bryan Gin-ge Chen The % variable interpolation syntax looks very much like 90s Windows. :confused: But lexical syntax aside, please submit a PR!

[Patrick Massot]

Thank you very much Bryan! I'll try that.

[Patrick Massot]

I confirm that Bryan's version of the extension works as advertised (at least for the lean executable path).

[Bryan Gin-ge Chen]

Great! Here's the PR. I'm not so wedded to the syntax, so if anyone feels like bikeshedding, feel free to comment there.

[Tim Daly]

Make a docker image containing the full install and run docker on windows.

[Tim Daly]

Here are the instructions I wrote to make an Axiom docker image:
https://github.com/daly/axiom/blob/master/Dockerfile.howto

It should be similar if you swap out the Axiom specific parts for Lean.
Docker runs on windows.

[Tim Daly]

Once you create the docker image your students only need to type
docker run -i -t Massot/Lean Lean
(the last Lean being whatever command starts your lean development environment)

PS: I prefer Irish Stout, yaknow, the nasty, warm, sticky stuff with various forms of pond life.

[Tim Daly]

It would, in general, if the various releases of Lean were available as docker images.
This will be especially true when Lean 4 drops. That way it would be possible to run Lean3 in one image and Lean4 in another at the same time.

[Tim Daly]

I will be at the Formal Methods / Lean Together conference if you need help.

[Tim Daly]

@Patrick Massot Can you tell me what version of Ubuntu and what sequence of steps are needed to get a running environment? I can try to build a docker image for it.

[Patrick Massot]

Thanks Tim, but I don't really see the advantage of a docker image over the lighter "portable VScode + lean" solution. None of those will really give you a native fully working environment and the docker solution looks much heavier (embarking a Linux distribution).

[Bryan Gin-ge Chen]

The just-released vscode-lean 0.14.9 contains the %extensionPath% feature, so no need to use the custom version of the extension any more.

[Patrick Massot]

I'm coming back to the issue of trying to use Lean in windows. After some tests in Pittsburgh, I thought it was possible to distribute a zip file containing VScode, its lean extension, Lean and mathlib. But my students told me it doesn't work (Lean is constantly recompiling thousands of files). Indeed I now have a virtual machine with Win10 and it doesn't work. Does anyone know how to ask Lean why it's compiling?

[Patrick Massot]

I tried downloading a mathlib nightly (from before the Lean 3.5.0 switch) and ask Lean if it's ok. But it always want to compile.

[Patrick Massot]

I would be very grateful if some windows user here could download https://www.math.u-psud.fr/~pmassot/enseignement/math114/bundles/math114_win.zip, unzip it and launch math114.bat and tell me why Lean is compiling stuff.

[Rob Lewis]

I think it's a time stamp thing. I saw the recompiling behavior. Then I ran the standard touch olean incantation, restarted the server, and it was fine. Trying again from scratch to test.

[Patrick Massot]

I tried the touch olean incantations so many times...

[Rob Lewis]

BTW, something seems funny with your .bat script, it didn't terminate even after quitting VSCode. It was keeping a lock on the files so I couldn't delete the directory.

[Patrick Massot]

That was the first bat file I wrote since 1998.

[Patrick Massot]

I can believe it is funny.

[Rob Lewis]

I don't know what the cmd shell version of the touch olean script should be. (I did it from Git Bash before.) cmd has a different find and no grep by default.

[Patrick Massot]

I tried from git bash

[Patrick Massot]

Life is hard enough on Windows without using cmd

[Rob Lewis]

But presumably your students wont' be using git bash, right?

[Rob Lewis]

If they're just double clicking the .bat script it's going through cmd?

[Patrick Massot]

No, but I mean: even when I touch olean using git bash I still can't get VScode to open my exercises without trying to compile thousands of lean files

[Patrick Massot]

Did you managed to achieve that?

[Rob Lewis]

Yes. I unzipped the files, ran the .bat, opened 00_appercu.lean, saw the recompiling behavior. Restarted the server a bunch, same behavior. Closed VSCode. in Git Bash, find . | grep "[.]olean$" | xargs touch. Ran the bat again. 00_appercu.lean opened and everything is compiled.

1 goal
f : ℝ → ℝ,
u : ℕ → ℝ,
x₀ : ℝ,
hu : limite_suite u x₀,
hf : continue_en f x₀
⊢ limite_suite (f ∘ u) (f x₀)

[Patrick Massot]

Where did you ran that find command?

[Patrick Massot]

in which folder?

[Rob Lewis]

The root of your archive, same directory as the bat.

[Patrick Massot]

What if you know zip that folder, move it somewhere else, unzip and run the bat?

[Rob Lewis]

Uh, there are tons of tiny files in that archive, it takes a long time to zip and unzip. I can try. But I think that will overwrite the timestamps. Everything was stamped to the time I unzipped it before.

[Rob Lewis]

It's possible it depends on the zip/unzip tool, I have no idea.

[Gabriel Ebner]

I also tried the zip file. Directly after unzipping, lean tries to compile everything. After touch `find` in git bash, everything works as expected (i.e., no compiling).

[Patrick Massot]

Windows world is so crazy :-(

[Sebastien Gouezel]

OK, I just tried it, and it works out of the box for me.

[Rob Lewis]

I mean, I don't really see what's crazy? There are olean time stamp issues on Linux too. It's not unreasonable to consider a file created at the moment it's unzipped, is it?

[Gabriel Ebner]

So I've just tried two things on windows:

[Gabriel Ebner]

If I extract the zip file via drag-and-drop, then the files get the current timestamp.

[Patrick Massot]

I never had any olean time stamp issues on Linux.

[Sebastien Gouezel]

I mean, I unzipped it, I executed the bat file, then I opened 01egalites, it didn't recompile anything and I could start proving stuff right away.

[Gabriel Ebner]

If I extract the file via "extract all...", then they have the old timestamp.

[Gabriel Ebner]

@Sebastien Gouezel How did you unzip them?

[Sebastien Gouezel]

I used an unzipper called 7-zip.

[Sebastien Gouezel]

The timestamps are the original ones.

[Rob Lewis]

Haha, okay. I zipped my copy with the updated time stamps, moved it to a new folder, and unzipped it, both using the built in Windows 10 unzip tool. It kept the time stamps and works immediately.

[Rob Lewis]

I never had any olean time stamp issues on Linux.

I have, using cache-olean/update-mathlib.

[Patrick Massot]

I couldn't do anything with Gabriel's method but installing 7-zip worked.

[Patrick Massot]

Thank you very much Rob, Gabriel and Sébastien!

[Gabriel Ebner]

https://devblogs.microsoft.com/oldnewthing/20110504-00/?p=10743

[Gabriel Ebner]

Apparently windows helpfully resets the timestamp when you extract zip files. But only for zip files that you've downloaded!

[Gabriel Ebner]

The fix seems to be to check Unblock in the properties dialog...

[Patrick Massot]

Indeed that Unblock checkbox also does the trick! Thank you very much for investigating this Gabriel!