elan on windows

Stream: general

[Scott Morrison]

@Sebastian Ullrich,

[Scott Morrison]

I'm trying to work on installation procedures.

[Scott Morrison]

Yesterday two students very successfully used the following technique:

[Scott Morrison]

1. Install Git for Windows

[Scott Morrison]

2. Install VS Code

[Scott Morrison]

3. In a git bash terminal, install Elan

[Scott Morrison]

When I'm trying it again today on a virtualised copy of windows 10, I'm getting the error message:

[Scott Morrison]

info: downloading installer
Archive:  elan-init.zip
  inflating: elan-init.exe
elan-init.exe: error while loading shared libraries: api-ms-win-crt-locale-l1-1-0.dll: cannot open shared object file: No such file or directory

[Scott Morrison]

Do you (or anyone else) have an idea of why this is a problem for me, but wasn't a problem for them yesterday?

[Scott Morrison]

Presumably it is just that they had already installed something that provided this dll...?

[Scott Morrison]

Could we perhaps just bundle it in elan-init.zip?

[Scott Morrison]

It seems this file (and about 8 others) are all available as a separate download at https://www.microsoft.com/en-au/download/details.aspx?id=48145

[Scott Morrison]

However they are only tiny files, and they are all redistributable, so we could just package them with the elan download.

[Scott Morrison]

Hmm, I've been looking at the build script for Elan, and can't make head or tail or it, so I think I might be stuck in this direction. I guess for the best available instructions for Elan on windows will have to be to install this extra set of DLLs by hand. :-(

[Kevin Buzzard]

[off-topic -- related but not the same -- Scott -- if you have a virtual windows 10 machine around, can you be bothered to try my easy install method ? (1) download and uncompress http://wwwf.imperial.ac.uk/~buzzard/xena/Xena.zip [lean + mathlib + sample project with path and toml files + all .olean files made] (2) install VS Code and Lean extension, and edit lean.executablePath (3) File -> Open Folder -> open "my_project" (4) that's it. I am interested to know how the .olean files perform. Try importing data.real.basic or whatever.]

[Scott Morrison]

Hi Kevin,

[Scott Morrison]

I got stuck at the "edit lean.executablePath step, because I don't understand windows.

[Scott Morrison]

That zip file ended up in a "Downloads" directory, but ... where is that? :-)

[Scott Morrison]

The built-in folder viewer in Windows doesn't seem to want to admit that there is some notion of absolute path :-)

[Scott Morrison]

And the VS Code settings editor doesn't want to give me a file picker. :-)

[Kevin Buzzard]

meh

[Kevin Buzzard]

Try C:/Users/my_userid/Downloads

[Scott Morrison]

Ah, the problem is that the zip file wasn't actually uncompressed!

[Scott Morrison]

In the file viewer I clicked on it and it showed me the contents, but it is just showing me the inside of a zip file without decompressing.

[Kevin Buzzard]

oh yeah, Windows just opens them when you click on them :-/

[Kevin Buzzard]

right click on it to uncompress it maybe

[Kevin Buzzard]

7-zip or winzip or something

[Mario Carneiro]

there is a "extract all" button in explorer when you open a zip file

[Kevin Buzzard]

are you good at computers?

[Kevin Buzzard]

Thanks :-)

[Mario Carneiro]

was that directed at me?

[Kevin Buzzard]

Someone with a mac and someone using linux on the other side of the world trying to figure out how to uncompress a file in Windows :-)

[Kevin Buzzard]

We just needed someone who was good at computers to come along

[Sean Leather]

I recently looked at a Windows computer for the first time in a long time. I was surprised things had changed so much, and not in a good way. But, fortunately for my brother-in-law, I could still figure out how to clean up his task bar and make bookmarks in Edge.

[Scott Morrison]

Ok, I unzipped on the terminal, eventually worked out the path to use for lean.executablePath, and it works

[Scott Morrison]

It was about a 15 second delay watching a yellow bar before your test.lean finished.

[Scott Morrison]

I'm not sure what that says about the olean files, however.

[Scott Morrison]

I think this virtual machine is still set to only use one core.

[Kevin Buzzard]

Doesnt VS code always take some time sorting stuff out when it starts up? What happens if you import analysis.real?

[Scott Morrison]

I've just updated the mathlib documentation on using elan.

[Scott Morrison]

Hopefully it is all correct, and works on ubuntu / macOS / windows 10.

[Scott Morrison]

I probably ought to create brand new virtual machines for each and try them out once more...

[Scott Morrison]

But I think once that PR gets merged, this may be a better set of starting instructions than Kevin's blog post.

[Scott Morrison]

https://github.com/leanprover/mathlib/pull/371 if anyone wants to try it out.

[Patrick Massot]

At the end of scenario 1, I read "If you want to play more, it's better to compile all your dependencies once and for all. You can do this by going into my_playground and running leanpkg build." But this is already what is written in the previous paragraph. I guess this was meant to explain how to fully compile mathlib. For this I think you need to go to _target/deps/mathlib and run lean --make (or leanpkg build?)

[Reid Barton]

Running leanpkg build inside the dependencies can cause lean to get confused, I recall. But I think lean --make in the dependencies is probably okay and recently I tried lean --make _target/deps/mathlib from the project directory and as far as I can tell it worked fine.

[Reid Barton]

See https://github.com/leanprover/mathlib/issues/308 where this paragraph is discussed

[Reid Barton]

I was hoping that some expert would come along and tell me whether my suggestion is OK, but at this point I guess I should just PR it

[Scott Morrison]

This sounds good to me. lean --make _target/deps/mathlib works for me, and I think should be the canonical advice if you want the entire thing precompiled. I'm not convinced anyone should want that, but okay. :-)

[Patrick Massot]

I want that. I don't want my workflow to break each time I add a new import in a Lean file

[Scott Morrison]

okay!

[Scott Morrison]

In other installation news, my PR to vscode-lean at <https://github.com/leanprover/vscode-lean/pull/91> seems to be working now on all operating systems, and means that the vscode extension will offer to install elan for you if it can't find a copy of Lean already.

[Scott Morrison]

I think I now have 7 outstanding PRs across 3 repos. :-) Maybe I'll go do some maths for a while.

[Scott Morrison]

And then there were 6!

[Scott Morrison]

Thanks @Sebastian Ullrich for merging that. I think Gabriel is away still, but it would be great if you wanted to have a look at <https://github.com/leanprover/vscode-lean/pull/91>, my PR to vscode-lean which will automatically offer to install elan if it can't find Lean.

[Scott Morrison]

If we can find a mechanism that is reliable, I think this will really soften the installation problem for beginners.

[Sebastian Ullrich]

@Scott Morrison Looks fine to me, but I'm not sure I want to find out how to do a vscode-lean release right now

[Sebastian Ullrich]

You may want to tidy up the commit history a bit

[Scott Morrison]

Will do, thanks. I'll wait to see what Gabriel says.

[Scott Morrison]

Okay, commit history fixed!

[Neil Strickland]

The new procedure looks promising, but it does not work correctly when the user's home directory has spaces in (which is a common pattern, eg C:\Users\Neil Strickland). Specifically, when trying to run leanpkg --help in a Git bash terminal embedded in VS Code, I see

'Strickland\.elan\toolchains\stable\bin\..' is not recognized as an internal or external command,
operable program or batch file.
C:\Users\Neil:1:0: error: file 'C:\Users\Neil' not found
<unknown>:1:1: error: file 'C:\Users\Neil' not found

which indicates that something somewhere is using the path C:\Users\Neil Strickland\.elan\toolchains\stable\bin and not escaping it correctly.

This is a bit mysterious to me. Running "which leanpkg" reports "/c/Users/Neil Strickland/.elan/bin/leanpkg". Note that this is not the path that is causing trouble above. I think that leanpkg is actually starting and producing the above error message. However, looking at https://github.com/leanprover/lean/blob/master/leanpkg/leanpkg/main.lean suggests that "leanpkg --help" should always run correctly without needing to resolve any paths. On the other hand, it is strange that /c/Users/Neil Strickland/.elan/bin/ contains four executables (lean.exe, elan.exe, leanpkg.exe and leanchecker.exe) which cmp tells me are byte-for-byte identical. So probably that leanpkg.exe involves some kind of wrapper that is producing the error message.

I have not been able to work out where leanpkg is getting the bad path from. I looked in various places under /c/Users/Neil Strickland/.elan and /c/Users/Neil Strickland/.vscode and /c/Users/Neil Strickland/AppData/Roaming/Visual Studio Code without success. Running "env" under Git bash also does not enlighten me.

In general, the problem with spaces in paths in Lean seems to arise as follows. The only Windows system call anywhere in the Lean code seems to be a CreateProcess() at line 221 of https://github.com/leanprover/lean/blob/master/src/library/process.cpp. On lines 70,74,77 of https://github.com/leanprover/lean/blob/master/leanpkg/leanpkg/resolve.lean there are calls to exec_cmd which end up using the above system call to start Git. This is probably appropriate, but the arguments should be escaped properly. However, in various other places in resolve.lean and main.lean the functions exec_cmd and io.proc.spawn are used to create directories and check for the existence of files and directories. These could again be fixed by escaping the arguments properly but it would be much more appropriate and robust to refactor the code to use the system calls CreateDirectory() and PathFileExists() (and their POSIX equivalents) directly.

Probably some of the above commentary should be converted to issues on github. But I am not yet properly familiar with how everything fits together.

[Reid Barton]

The issue is in leanpkg.bat: https://github.com/leanprover/lean/pull/1976/files
I'm not sure whether just modifying your local copy will confuse elan, but it's worth a try

[Reid Barton]

(There could be other issues, I suppose, but this is one known one.)

[Neil Strickland]

I don't believe that that is correct. Other methods of installing Lean give me a file leanpkg.bat which is a wrapper to the executable leanpkg.exe. However, using elan via VS Code installs the lean executables in C:\Users\Neil Strickland\.elan\bin, and there is a leanpkg.exe there but no leanpkg.bat. Moreover, leanpkg is invoked from Git bash which would ignore any .bat file anyway. When starting Git bash inside VS Code in the obvious way, the environment variables LEANDIR, LIBDIR and LEAN_PATH are not set, but the PATH variable includes C:\Users\Neil Strickland\.elan\bin, and "which leanpkg" reports that that is where leanpkg is found.

[Bryan Gin-ge Chen]

I'm pinging @Scott Olson, who wrote the patch to leanpkg.bat mentioned by Reid. Since he's already looked into this issue, he may be well-equipped to follow up on Neil's post above.

[Scott Olson]

I made a PR at lean#1976. These errors are from leanpkg.bat:

'Strickland\.elan\toolchains\stable\bin\..' is not recognized as an internal or external command,
operable program or batch file.
C:\Users\Neil:1:0: error: file 'C:\Users\Neil' not found
<unknown>:1:1: error: file 'C:\Users\Neil' not found

Specifically the first line comes from the IF NOT EXIST line and the latter two come from the lean line since it's getting passed

lean --run "C:\Users\Neil" "Strickland\.elan\toolchains\stable\bin\..\lib\lean\leanpkg\leanpkg\main.lean"

instead of

lean --run "C:\Users\Neil Strickland\.elan\toolchains\stable\bin\..\lib\lean\leanpkg\leanpkg\main.lean"

[Reid Barton]

I think the leanpkg in .elan/bin (which is really elan itself) invokes leanpkg in (for example) .elan/toolchains/3.4.1/bin/, which should be leanpkg.bat on Windows. I would have to defer to someone who has a Windows machine though.

[Scott Olson]

Oh yes, I looked into that before and Reid is correct. I forgot the step where elan has its own leanpkg wrapper binary.

[Scott Olson]

I originally spent quite a while thinking elan's code contained the bug until I figured out it was invoking leanpkg.bat...

[Scott Olson]

Also, for the curious, the elan binaries are not just byte-for-byte identical, but actually hardlinked:

C:\Users\Scott>fsutil hardlink list .elan\bin\leanpkg.exe
\Users\Scott\.elan\bin\lean.exe
\Users\Scott\.elan\bin\leanpkg.exe
\Users\Scott\.elan\bin\leanchecker.exe
\Users\Scott\.elan\bin\elan.exe

Meaning the filesystem only stores one file which these 4 paths all point to

[Neil Strickland]

This seems to be correct: C:\Users\Neil Strickland\.elan\bin\leanpkg.exe invokes C:\Users\Neil Strickland\.elan\toolchains\*\leanpkg.bat via cmd.exe even when we start with Git bash, which is all pretty convoluted. Editing leanpkg.bat by hand at least allows be to run leanpkg --help successfully. I have not yet tried to do anything more useful.

[Scott Olson]

.elan\bin\leanpkg.exe is just a normal windows program so it can invoke a .bat file regardless of being invoked from git bash or anything else

[Neil Strickland]

Certainly it can; that doesn't mean that it should. You probably need to call CreateProcess() to invoke leanpkg and if necessary you can supply the required environment variables as an argument to CreateProcess() as documented at https://docs.microsoft.com/en-us/windows/desktop/api/processthreadsapi/nf-processthreadsapi-createprocessa instead of going through leanpkg.bat.

[Scott Olson]

elan could certainly invoke lean itself without going through leanpkg.bat, which we should probably do anyway because then it will work regardless of whether we get leanpkg.bat fixed, and for older versions

[Scott Olson]

elan is written in Rust so we probably don't need to think about the exact Windows API calls, but it should be possible to make the wrapper invoke lean with the extra --run <path to leanpkg> args and the environment variables

[Scott Olson]

I posted an issue to the elan repo: https://github.com/Kha/elan/issues/16