mathlib on windows

Stream: general

[Jeremy Avigad]

I am trying to install mathlib on a windows laptop. In mingw I set all the paths, but I get this:

$ leanpkg install https://github.com/leanprover/mathlib
> mkdir -p C:\msys64\home\aviga/.lean
> cd C:\msys64\home\aviga/.lean
fatal: not a git repository (or any of the parent directories): .git
fatal: not a git repository (or any of the parent directories): .git
mathlib: trying to update _target/deps/mathlib to revision lean-3.4.1
cannot find revision lean-3.4.1 in repository _target/deps/mathlib

What am I doing wrong? And -- out of curiosity -- why does it take so long for leanpkg to start up?

[Sebastian Ullrich]

Hi Jeremy! If leanpkg takes a while to start up, it's most likely not running from its .olean files. I don't know about the git error unfortunately

[Jeremy Avigad]

I suspected that, but I can't imagine why not. I installed the binary from leanprover.github.io, and the files are all there.
Maybe I'll ask Mario to help me on Monday.

[Andrew Ashworth]

Hmm, I use Lean on Windows. I've never installed mathlib user-wide. I know it works if you do leanpkg add per project.

[Jeremy Avigad]

Thanks for the suggestion. Indeed, using leanpkg add worked (modulo the problem with not using the .olean files).

[Sebastian Ullrich]

Heh, well, we do have the following source comment :) : https://github.com/leanprover/lean/blob/master/src/util/lean_path.cpp#L45

[Jeremy Avigad]

Thanks. Things seem to be ok now. Using lean --make in the library directory seems to have fixed the .olean problem. And deleting the .lean directory and running leanpkg install again seems to be working. It is building mathlib now.

[Sebastian Ullrich]

@Jeremy Avigad Now that I think about it, I'm surprised the .olean files haven't been a bigger issue before. We check the modification time of the .olean file against that of the corresponding .lean file. Extracting files from a zip file resets the modification time, so the result depends on the extraction order (at least in the zip file itself, .olean files are listed after their .lean files). And even then, Windows touches each downloaded file again to mark them as "potentially dangerous"

[Kevin Buzzard]

Just to remark that I am nowadays completely resigned to the fact that every invocation of leanpkg on a Windows machine begins with a 15 second wait during which nothing seems to happen other than me moaning about Windows.

[Kevin Buzzard]

A little test shows that on linux the tar command seems to preserve file timestamps. Is this just a problem with zip on Windows? And am I right in thinking I can fix on a user's Windows machine by somehow re-compiling leanpkg just once?

[Sebastian Ullrich]

elan seems to reset the modifications times even on Linux, though that's probably its own fault. Anyway, I've never had an issue with it on Linux, whereas I could reproduce the issue on Windows on the first try

[Sebastian Ullrich]

As Jeremy said, you should go into the library folder and call lean --make. You could do the same in leanpkg, but that's probably not the expensive part

[Jeremy Avigad]

An old post from Kevin (https://xenaproject.wordpress.com/2017/12/02/how-to-install-mathlib-and-keep-it-up-to-date/) suggests he has been struggling with this issue for a while.
Actually, for me, the situation is even more mysterious. When I do lean --make in the library folder, it compiles a bunch of files, say list A. If I type lean --make again, it compiles another bunch, say, list B. Then if I do it again, it then recompiles list A! If I keep doing it, it continues to cycle through those two. It is almost as though lean thinks there is a cyclic dependency, or there is some kind of funny race condition with timestamps. (I think the wait to start leanpkg became less painful only because I landed on the shorter side of the cycle.)
I'll be out all afternoon and the laptop is at home, but I'll experiment more later tonight.

[Sebastian Ullrich]

Oof, that doesn't sound good at all

[Sebastian Ullrich]

One good news, Lean 4 will have a trace option to debug why an .olean file wasn't imported...

[Bryan Gin-ge Chen]

This might be only tangentially related, but I experienced something like this when I ran leanpkg build inside _target/deps/mathlib in a package and then ran it from the base folder afterwards. I had also expected that once the .olean files were generated once, they didn't have to be rebuilt if nothing changed, but I guess that's not true.

[Mario Carneiro]

You should not run leanpkg inside the target folder, I think it gets confused

[Mario Carneiro]

you can just run lean --make instead

[Jeremy Avigad]

Update: deleting all the. olean files (del /s *.olean in library) and rebuilding (lean --make) seems to work fine. After that, lean --make does nothing. I had to go into the leanpkg directory and run lean --make there too. Now leanpkg runs instantaneously.

[Sebastian Ullrich]

I just released a new version of elan that seems to fix the issue