## Stream: general

### Topic: mathlib on windows

#### Jeremy Avigad (Sep 16 2018 at 00:34):

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 (Sep 16 2018 at 00:42):

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 (Sep 16 2018 at 00:58):

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 (Sep 16 2018 at 01:01):

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 (Sep 16 2018 at 01:21):

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

#### Sebastian Ullrich (Sep 16 2018 at 02:03):

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

#### Jeremy Avigad (Sep 16 2018 at 02:09):

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 (Sep 16 2018 at 06:04):

@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 (Sep 16 2018 at 07:35):

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 (Sep 16 2018 at 08:30):

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 (Sep 16 2018 at 16:41):

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 (Sep 16 2018 at 16:42):

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 (Sep 16 2018 at 19:38):

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 (Sep 16 2018 at 19:49):

Oof, that doesn't sound good at all

#### Sebastian Ullrich (Sep 16 2018 at 19:49):

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

#### Bryan Gin-ge Chen (Sep 16 2018 at 19:53):

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 (Sep 16 2018 at 19:57):

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

#### Mario Carneiro (Sep 16 2018 at 19:57):

you can just run lean --make instead

#### Jeremy Avigad (Sep 17 2018 at 01:28):

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 (Sep 17 2018 at 02:02):

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

Last updated: May 16 2021 at 05:21 UTC