updating Kevin's installation instructions

Stream: general

[Scott Morrison]

Hi @Kevin Buzzard, I'm thinking that since elan has now arrived and is pretty good, we should update your blog post.

If I wrote a guest post for you, could we put that up, and add a prominent link at the top of your old post?

[Kevin Buzzard]

Yes that would be fine. I have never used elan.

[Kevin Buzzard]

I also think we should plug the trivial way of getting Lean and Mathlib running on Windows 10: https://xenaproject.wordpress.com/getting-lean-and-mathlib-running-in-the-mlc/

[Kevin Buzzard]

There are no links to that page on the site because the system got changed again and now it's even easier for us at Imperial, we fire up VS Code and it's all there.

[Kevin Buzzard]

But on Thursday night one person with a win10 machine asked about installation and I said "I have just the link for you".

[Kevin Buzzard]

For those not clicking: the full installation procedure is " Download VS Code, now download this zip file (containing lean and mathlib lean and olean files and a leanpkg.path etc) and now tell VS Code where Lean is and now open this folder and it all works.". No git, no msys2, no command line

[Scott Morrison]

Okay! It would be good if we could arrange for creating that zip file automatically, so it doesn't become an ancient stranded artefact.

[Scott Morrison]

I think I am going to wait just a moment before writing that blog post --- Gabriel has just reviewed my PR to have the VS Code extension offer to install Lean, so it seems likely that will land soon, and this will make the instructions even easier.

[Kevin Buzzard]

Yes -- that link above suffered from document rot after about 3 days, when someone in ICT said "oh wow, is that what you're telling them? We can probably automate all of that". I thought they were crazy. We'll see. The reason I think they're crazy is that now when any undergraduate launches Visual Studio Code on a machine in the maths department, it starts off by default with a minimal Lean project open! The doc hence became obsolete. I can see this causing confusion for non-converts later down the line though...but I decided that this was not currently my problem.

[Gabriel Ebner]

Gabriel has just reviewed my PR to have the VS Code extension offer to install Lean, so it seems likely that will land soon

It should come to a vscode installation near you any moment now!

[Scott Morrison]

... and, it works!

[Scott Morrison]

If anyone wants to try deleting their Lean installation and trying it out, the VS Code extension now installs elan for you upon request! --- It took less than 2 minutes for me just now.

[Scott Morrison]

I will try to make a little video walk-through.

[Scott Morrison]

@Gabriel Ebner --- I was just thinking about making a "build all olean files" command in VS Code, as this is a common task. Do you think it is better to use the model of batch.ts, or to create a terminal and run the commands there?

[Scott Morrison]

(I haven't been able to get the batch mode to work.)

[Gabriel Ebner]

Have you seen ctrl+p task build? Should we package it up as a command as well?

[Scott Morrison]

No, I haven't. What is ctrl+p? On mac that doesn't seem to do anything.

[Scott Morrison]

Ah, under cmd-shift-p I get Tasks: Run Build Task

[Scott Morrison]

and under that leanpkg: configure and a few others.

[Scott Morrison]

Yes, putting lean --make _target && lean --make as a task under that would be a great solution.

[Scott Morrison]

I guess the lean --make is silly, that should just be leanpkg build.

[Scott Morrison]

But having some way to compile everything in the dependencies seems to be requested often.

[Gabriel Ebner]

Oh, on mac it is cmd+p task build then. BTW, your command is equivalent to lean --make.

[Scott Morrison]

Hmm... I guess so. :-)

[Scott Morrison]

There's no way to ask leanpkg to completely compile the dependencies, is there?

[Gabriel Ebner]

No.

[Scott Morrison]

It would be great to have leanpkg build-dependencies as well as leanpkg clean one day.

[Scott Morrison]

In the meantime, what do you think of adding lean --make as a build task? It would be a little awkward, as it probably belongs in leanpkg.ts, but isn't actually using leanpkg.

[Chris Hughes]

I have some error, related to the fact that I have a space in my username
C:\msys64\home\Christopher Hughes\mathlibs\exp>leanpkg build 'Hughes\.elan\toolchains\3.4.1\bin\..' is not recognized as an internal or external command, operable program or batch file. C:\Users\Christopher:1:0: error: file 'C:\Users\Christopher' not found <unknown>:1:1: error: file 'C:\Users\Christopher' not found

[Kevin Buzzard]

You have a space in "Christopher Hughes" and because of an irreparable flaw in Windows you are going to struggle.

[Kevin Buzzard]

If you can somehow change it to "Christopher_Hughes" this will change the behaviour of things.

[Scott Morrison]

Here's a short video I just made that shows a complete installation of Lean on a mac. Takes 3:40! (Well, with some time lapse for the downloads...)

[Scott Morrison]

https://www.youtube.com/watch?v=k8U6YOK7c0M&feature=youtu.be

[Scott Morrison]

(This uses the latest update to the VS Code extension, which now offers to install elan and Lean for you, if it can't find them.)

[Scott Morrison]

Sometime in the next few days I will try to make a windows video as well.

[Chris Hughes]

If you can somehow change it to "Christopher_Hughes" this will change the behaviour of things.

I think this will be more effort than it's worth. I'm going back to my old setup

[Kevin Buzzard]

I've noticed that kids these days far prefer video tutorials to reading boring old web pages.

[Ryan Smith]

I've been trying to get it working with elan on windows and this is not going well. I installed msys32 and elan, but when I try to run the package manager from the windows cmd line with leanpkg -v I get

'Smith\.elan\toolchains\stable\bin\..' is not recognized as an internal or external command,
operable program or batch file.

Seems like elan / msys32 / something doesn't understand spaces in windows filenames

[Ryan Smith]

I'm not fond of windows, but I do have to keep it on this computer for a reason.

[Bryan Gin-ge Chen]

This is a known issue and unfortunately I don't think there's an easy solution.

[Ryan Smith]

Ok, if stuck on windows is there a better general approach then?

[Bryan Gin-ge Chen]

@Chris Hughes might know. You can see he ran into the same problem earlier in the thread, and I think he has a working setup by some other means.

[Johan Commelin]

@Ryan Smith Looks like you have a space in your user name. This is known to break things.

[Ryan Smith]

Yeah I do. Is there a way around?

[Johan Commelin]

Dunno... haven't touched Windows in 15 years, and I don't use spaces in paths...

[Johan Commelin]

But Chris got it working

[Johan Commelin]

So to answer your question: Yes. There is a way around.

[Ryan Smith]

It's a dreadful system, been about as long for me. Somehow I thought it would have gotten better while I was away. Is macOS at least better supported right now?

[Johan Commelin]

How difficult is it to create a new user on Windows, and switch back and forth?

[Ryan Smith]

That would be doable if that's really the only blocking issue sure

[Johan Commelin]

What do you mean with "supported"? Support for Lean?

[Johan Commelin]

Lean on Mac seems to work pretty good.

[Ryan Smith]

Lean / elan since I was told things work better if you're using something to manage dependencies and stay up to date

[Johan Commelin]

Elan on Mac is a very smooth experience nowadays

[Ryan Smith]

Ok, cool. Will just switch off of my gf's computer and retry this on mac

[Johan Commelin]

1 sec

[Johan Commelin]

So, what you do:

[Johan Commelin]

(1) Install VScode, (2) Install the Lean extension in VScode, (3) Open a Lean file.

[Johan Commelin]

Afterwards, follow instructions, and it will install elan and lean for you

[Ryan Smith]

opening a lean file in vscode w/ extension does seem to call lean. I don't see anything about elan.

[Ryan Smith]

I'm a complete newbie trying to get a feel for how it works, so that's a good start if I can pull in mathlib

[Johan Commelin]

It will only install elan/lean if it cannot find them

[Johan Commelin]

Did you already have something installed?

[Ryan Smith]

I installed via msys32, I assumed it was screwed up because invoking the package manager from the command line fails

[Johan Commelin]

Is this still on windows?

[Ryan Smith]

yeah, waited when you said you had a solution

[Johan Commelin]

aah, sorry

[Johan Commelin]

That was the mac solution

[Johan Commelin]

sorry for the confusion

[Ryan Smith]

ah cool, so the vscode extension installs everything else?

[Johan Commelin]

I just wanted you to know it, before logging off

[Ryan Smith]

thx for the help :)

[Kevin Buzzard]

'Smith\.elan\toolchains\stable\bin\..' is not recognized as an internal or external command,
operable program or batch file.

Smith is half of your username, isn't it :-(

This is an issue with elan. Having a space in your username in Windows is a terrible idea; I know from personal experience that elan is not the only thing it breaks.

[Kevin Buzzard]

Cheap Windows hack: https://xenaproject.wordpress.com/getting-lean-and-mathlib-running-in-the-mlc/

[Kevin Buzzard]

I will update this blog page and turn it from old and out-of-date instructions on how to run Lean at Imperial to a clearly signposted hack for win10 in general.

[Kevin Buzzard]

https://xenaproject.wordpress.com/a-cheap-hack-to-get-lean-and-mathlib-running-on-a-windows-10-machine/

[Kevin Buzzard]

Summary: the correct elan method is causing problems for Windows 10 users with spaces in their file names. The link above might work better for them, and I'd be interested in feedback. @Ryan Smith if you still have not got things going, can you try this method?

[Scott Olson]

I've narrowed down the elan problems with spaces to leanpkg, actually. I'm 95% sure this bat file is the culprit: https://github.com/leanprover/lean/blob/master/bin/leanpkg.bat

The trouble comes with elan placing that in the homedir when the username has a space in it, but I believe it would also affect anyone who manually installed lean in any other path with a space in it.

[Scott Olson]

Now I'm trying to teach myself just enough .bat language to figure out why...

[Mario Carneiro]

not enough quotes?

[Scott Olson]

Almost surely, I just have no idea how .bat quoting works yet

[Kenny Lau]

Thanks @Scott Olson

[Mario Carneiro]

I think the last line should be

lean --run "%LIBDIR%\leanpkg\leanpkg\main.lean" %*

[Mario Carneiro]

I wonder if this is considered urgent enough to patch core

[Kenny Lau]

good luck getting those big guys patch it

[Scott Olson]

The IF NOT EXIST command also causes an error to print out

[Kenny Lau]

someone with much more threads than 4 can test if it works

[Scott Olson]

Quoting the --run arg and writing IF NOT EXIST "%LIBDIR%" seems to be enough

[Kenny Lau]

ok now then how to get the big guys to patch it

[Scott Olson]

lol I just noticed the commit that added leanpkg.bat was by a personal friend of mine. Maybe I'll start by asking them?

[Mario Carneiro]

If we can't patch core, the next best thing would be to store the patched file somewhere accessible from the tutorials "if you have problems with spaces, replace leanpkg.bat with this and try again"

[Mario Carneiro]

Pretty sure Corey doesn't have any magic access any more than we do

[Kenny Lau]

they'll say that this doesn't matter because half life 3 will soon be released

[Mario Carneiro]

I see @Gabriel Ebner is lurking, maybe he has magic access?

[Kenny Lau]

I mean, Lean 4

[Scott Olson]

Either way I'll make a PR after I double-check that I'm doing quoting the best way

[Scott Olson]

There's an open issue about it https://github.com/leanprover/lean/issues/1973

[Kevin Buzzard]

I guess Sebastian Ullrich might consider patching it -- he is interested in making this sort of infrastructure work, and there's a fair chance that this problem will still be there in Lean 4.

[Kenny Lau]

you mean Half Life 3

[Kevin Buzzard]

Half life 3 --- 1/8'th life.

[Gabriel Ebner]

I wouldn't count on a fix making it into a new Lean 3 release. A more brutal solution would be to include a patch in elan or the vscode extension. Given that Lean 3 is end-of-lifed, I'd accept a PR to the vscode extension that patches leanpkg.bat on windows.

[Scott Morrison]

oh, that's a good idea

[Scott Olson]

FYI I made the PR at https://github.com/leanprover/lean/pull/1976

[Ryan Smith]

@Johan Commelin Trying to install the lean plugin to vscode on macOS followed by opening a lean file does not install elan & lean, instead I just get file 'init' not found in the LEAN_PATH

[Bryan Gin-ge Chen]

@Scott Morrison is the author of that installation feature. He should be able to help.

[Bryan Gin-ge Chen]

Are you possibly running into this issue ? I think if you're getting that error you ought to have lean and elan on your system. Does lean --version in a console do anything?

[Ryan Smith]

Lean (version 3.4.1, commit 17fe3decaf8a, Release)
This time the plugin brought up an installation for elan, but when I'm trying to do a basic sanity check with Kevin's example of
import analysis.real
#check real
I'm not getting anything

[Bryan Gin-ge Chen]

Do you see orange bars on the side? If so, that means lean is busy processing the file and its imports.

[Ryan Smith]

I retract that: it took a very long time but it came back with \R! I think that means it's running and math lib import is ok?

[Bryan Gin-ge Chen]

Yes. To speed up this process in the future, you can run lean --make in your package directory.

[Ryan Smith]

Do you need to re run make if you edit your src files?

[Mario Carneiro]

vscode will automatically compile stuff in memory when you make edits, but they aren't saved when you quit

[Bryan Gin-ge Chen]

Running lean --make generates .olean files, which are object files that lean generates when it compiles the .lean source files. If you have lots of files that import each other then doing this lets the lean server in the VS code extension avoid re-compiling all of your imports when it starts up.

So if you're just editing small files that import only from mathlib, running lean --make again won't really be necessary. If you do want to run it, then as long as you haven't made changes to your package's copy of mathlib (e.g. by upgrading) or otherwise written / edited lots of files that you need to import, running lean --make after the first time will be much faster since it tries not to recompile files whose dependencies haven't changed.

[Ryan Smith]

Great, thanks

[Scott Morrison]

@Johan Commelin Trying to install the lean plugin to vscode on macOS followed by opening a lean file does not install elan & lean, instead I just get file 'init' not found in the LEAN_PATH

Hi @Ryan Smith, I'd like to understand what happened here. Did you have LEAN_PATH set already? That's likely to cause problems. It sounds like a moment later the plugin did work, and installed elan for you.

[Neil Strickland]

I am sorry to rant, but these complaints about spaces in user names are silly.

Allowing spaces in user names is a completely ordinary, benign design decision. It creates a need to escape strings in certain circumstances, but that is again a completely ordinary issue, which arises all over the place in software development in many different contexts. There are many, many thousands of programs that handle Windows paths correctly, and it does not take any magic to write them. If a certain program is broken by spaces in path names, that just means that the developers did not take the straightforward and standard steps necessary to avoid that problem.

[Johan Commelin]

@Neil Strickland I agree that it is not very user friendly. There have been efforts to figure out what is wrong, and people are trying to patch it up.

[Gabriel Ebner]

I feel like the last line was partly directed at me, so let me respond. Neither Leo, Sebastian, or me are using windows. I am sorry but I don't think any of us are aware of the "straightforward and standard steps" in windows cmd.exe programming. The windows-specific parts of the code base are in general less well tested. Now is probably not the ideal time, but in general feel free to submit fixes for these platform-specific bugs.

[Reid Barton]

This is a common problem for open-source projects: there are many fewer developers using Windows than Linux or OS X and Windows is fundamentally unfamiliar to users of Unix-type systems. The result is usually that Windows is not as well supported as it could be. We have this problem with the Haskell compiler (GHC) as well--we've recently got one (volunteer) developer who actually understands Windows who's got a ~20 year backlog of Windows-specific issues to work through, including stuff like the interpreter not crashing when it tries to print Unicode characters to the console. And GHC is a project with a far larger user and developer base than Lean. (It also happens to be another project whose primary developer is at MSR.)

[Reid Barton]

That said, the Unix-y equivalent of leanpkg.bat is also missing quotes in the same place. I guess nobody has spaces in their usernames on Unix-y systems :upside_down:

[Neil Strickland]

@Gabriel Ebner Thanks for the response. I think that the only cmd.exe related problem is probably resolved by Reid Barton's recent fix to leanpkg.bat. However, there are other issues caused by passing unescaped strings to CreateProcess() in src/library/process.cpp via exec_cmd and io.proc.spawn, and by using external processes to make or detect directories instead of calling CreateDirectory() and PathFileExists(). That is surely not the recommended approach even in POSIX systems. If I had an appropriate build environment then I would attempt to fix this myself, but I do not know how hard it would be to set that up.

[Johan Commelin]

That said, the Unix-y equivalent of leanpkg.bat is also missing quotes in the same place. I guess nobody has spaces in their usernames on Unix-y systems :upside_down:

Right. When you live in the shell, you quickly learn to use sane paths.

[Reid Barton]

(Not my fix, but @Scott Olson's)

[Reid Barton]

However, there are other issues caused by passing unescaped strings to CreateProcess() in src/library/process.cpp via exec_cmd and io.proc.spawn, and by using external processes to make or detect directories instead of calling CreateDirectory() and PathFileExists(). That is surely not the recommended approach even in POSIX systems.

I think @Keeley Hoek has a fork which fixes some issues like this for Windows.

[Reid Barton]

I didn't realize that Windows doesn't have an equivalent of the command-line argument list. I guess I knew that DOS worked that way...

[Scott Olson]

heh, yeah, I just learned that the other day when I went diving into elan's code and the Rust standard library to figure out how process creation worked on Windows