Zulip Chat Archive

Stream: general

Topic: lean doesn't used files downloaded by update-mathlib

Floris van Doorn (Jun 20 2019 at 06:57):

Someone in the Hanoi formalabstracts group had the following issue. After running update-mathlib, Lean does not use the downloaded compiled files (the compilation time of logic.basic is instantaneous, but the compilation time is longer if we go further into mathlib, both in VSCode and running lean on the command line).

Does someone have an idea what could cause the issue? I attached a downloaded and compiled olean file from her laptop. There are some changes on the first line which might give a hint to someone who can read that line (@Mario Carneiro?).

Some notes: It is a Windows laptop, and elan was not installed on her laptop (is that a potential issue?).

basic.olean basic_downloaded.olean

Mario Carneiro (Jun 20 2019 at 06:58):

if there is a change in the first few lines of the olean file that's probably the checksum

Floris van Doorn (Jun 20 2019 at 07:00):

This is the checksum of the .lean file which is used to see if the file needs to be compiled again?

Floris van Doorn (Jun 20 2019 at 07:01):

was there a description of the meaning of the first line? I remember seeing that somewhere...

Mario Carneiro (Jun 20 2019 at 07:04):

oh no, it's the file length

Mario Carneiro (Jun 20 2019 at 07:05):

no I was right the first time, it's the checksum

Mario Carneiro (Jun 20 2019 at 07:05):

I suggest olean-rs for documentation on the olean format

Mario Carneiro (Jun 20 2019 at 07:06):

https://github.com/digama0/olean-rs/blob/master/olean.lean

Mario Carneiro (Jun 20 2019 at 07:12):

The olean dumps are identical though

Mario Carneiro (Jun 20 2019 at 07:13):

It's a checksum of the rest of the olean file

Mario Carneiro (Jun 20 2019 at 07:13):

And indeed the files are not byte for byte identical, there is a change somewhere in the middle but the dumps are the same suggesting it's not a semantic difference

Floris van Doorn (Jun 20 2019 at 07:23):

So any idea why these .olean files are not used by lean?

Mario Carneiro (Jun 20 2019 at 07:23):

they aren't the same, so yeah

Mario Carneiro (Jun 20 2019 at 07:24):

lean rejects it because it's changed

Mario Carneiro (Jun 20 2019 at 07:24):

I'm not sure what exactly has changed or why though

Floris van Doorn (Jun 20 2019 at 07:26):

Also, does your def read_olean read the checksum/whatever the difference is between the files on the first line?

I'll double check if she has the same version of Lean as me.

Mario Carneiro (Jun 20 2019 at 07:28):

The lean version of the olean reader ignores the checksum, but the rust version computes the real checksum and compares

Mario Carneiro (Jun 20 2019 at 07:29):

The lean version is stored in the olean file, and it's the same

Floris van Doorn (Jun 20 2019 at 07:30):

ah, I see, that's claimed_hash.

Floris van Doorn (Jun 20 2019 at 09:30):

In the end we just reinstalled Lean from scratch, which solved the issue.

Scott Morrison (Jun 20 2019 at 09:47):

Hopefully using elan this time. :-)

Floris van Doorn (Jun 20 2019 at 10:22):

Of course :)

Andrew Ashworth (Jun 20 2019 at 11:33):

I wonder if when Lean4 comes out there will be interest in binary package management

Andrew Ashworth (Jun 20 2019 at 11:34):

With the bigger focus on code extraction to C++, and people grousing about compile times for both languages, seems like it could be useful

Andrew Ashworth (Jun 20 2019 at 11:34):

I've been using Conan to manage my C++ build dependencies lately and I've been pretty impressed.

Simon Hudon (Jun 20 2019 at 11:49):

I've been thinking of adopting a solution like Nix for building snapshots of the Lean ecosystem and distributing the binaries. Unfortunately, we can't adopt Nix because of complications on Windows. But I'm looking different package management approaches for Lean 3 and @Sebastian Ullrich is looking at it for Lean 4

Johan Commelin (Jul 05 2019 at 11:43):

I'm also having problems now... on Linux.

Johan Commelin (Jul 05 2019 at 11:43):

I run update-mathlib in the perfectoid project, but Lean happily starts recompiling all the dependencies.

Kevin Buzzard (Jul 05 2019 at 11:50):

Check the timestamps of the olean files and see if they're strictly after the timestamps of the corresponding lean files.

Johan Commelin (Jul 05 2019 at 11:52):

Ok, let me try to do that...

Johan Commelin (Jul 05 2019 at 11:56):

-rw-rw-r-- 1 jmc jmc  4274 Jun 14 15:36 _target/deps/mathlib/src/tactic/squeeze.lean
-rw-rw-r-- 1 jmc jmc 19564 Jul  3 11:52 _target/deps/mathlib/src/tactic/squeeze.olean

Johan Commelin (Jul 05 2019 at 11:56):

Looks fine to me.

Johan Commelin (Jul 05 2019 at 12:01):

@Simon Hudon Any clue what could be the issue here?

Johan Commelin (Jul 05 2019 at 14:10):

find src | grep "[.]olean" | xargs touch has saved me quite a bit today

Simon Hudon (Jul 06 2019 at 22:42):

do you know what archive you're expanding? Try expanding it in a new directory and checking the time stamps of squeeze.[o]lean again

Kevin Kappelmann (Jul 31 2019 at 12:43):

Is there some URL that update-mathlib uses to download the latest mathlib + olean files? I'd like to use it for the proving is fun backend.

Kevin Kappelmann (Jul 31 2019 at 12:48):

I think I got it: https://github.com/leanprover-community/mathlib-nightly/releases

Floris van Doorn (Jul 31 2019 at 21:48):

I'm having these problems now myself. I downloaded today's archive - file name mathlib-olean-nightly-2019-07-31.tar.gz. However, if I make a single file, it seems to recompile a large chunk of the library.

In more detail:

I extract the archive I downloaded earlier today:

Floris@MSI MINGW64 /d/projects/mathlib ((badeb48b...))
$ cache-olean --fetch
Info: No github section found in 'git config', we will use GitHub with no authentication
Querying GitHub...
Reusing cached olean archive
... successfully extracted olean archive.

I check in more detail what's in the algebra folder:

Floris@MSI MINGW64 /d/projects/mathlib ((badeb48b...))
$ ls src/algebra/ -alt --time-style=full-iso
total 3973
drwxr-xr-x 1 Floris 197121      0 2019-07-31 05:24:01.000000000 -0400 ./
drwxr-xr-x 1 Floris 197121      0 2019-07-31 05:24:01.000000000 -0400 CommRing/
drwxr-xr-x 1 Floris 197121      0 2019-07-31 05:24:01.000000000 -0400 Mon/
drwxr-xr-x 1 Floris 197121      0 2019-07-31 05:23:59.000000000 -0400 group/
-rw-r--r-- 1 Floris 197121 470882 2019-07-31 05:14:21.000000000 -0400 direct_limit.olean
-rw-r--r-- 1 Floris 197121  48982 2019-07-30 03:28:45.000000000 -0400 direct_sum.olean
-rw-r--r-- 1 Floris 197121 240420 2019-07-30 03:25:53.000000000 -0400 pi_instances.olean
-rw-r--r-- 1 Floris 197121  23435 2019-07-30 03:24:39.000000000 -0400 punit_instances.olean
-rw-r--r-- 1 Floris 197121  46890 2019-07-30 03:22:47.000000000 -0400 char_p.olean
-rw-r--r-- 1 Floris 197121   2195 2019-07-30 03:22:01.000000000 -0400 default.olean
-rw-r--r-- 1 Floris 197121 194740 2019-07-30 03:22:00.000000000 -0400 module.olean
-rw-r--r-- 1 Floris 197121 115308 2019-07-30 03:20:25.000000000 -0400 pointwise.olean
-rw-r--r-- 1 Floris 197121 267084 2019-07-30 03:08:50.000000000 -0400 big_operators.olean
-rw-r--r-- 1 Floris 197121 228629 2019-07-30 03:07:36.000000000 -0400 gcd_domain.olean
-rw-r--r-- 1 Floris 197121 190155 2019-07-30 03:06:20.000000000 -0400 associated.olean
-rw-r--r-- 1 Floris 197121 144643 2019-07-30 03:05:46.000000000 -0400 archimedean.olean
-rw-r--r-- 1 Floris 197121  51843 2019-07-30 03:02:00.000000000 -0400 field_power.olean
-rw-r--r-- 1 Floris 197121 168299 2019-07-30 03:01:50.000000000 -0400 group_power.olean
-rw-r--r-- 1 Floris 197121 110312 2019-07-30 03:01:26.000000000 -0400 euclidean_domain.olean
-rw-r--r-- 1 Floris 197121  45067 2019-07-30 03:00:16.000000000 -0400 ordered_field.olean
-rw-r--r-- 1 Floris 197121  17108 2019-07-30 03:00:12.000000000 -0400 char_zero.olean
-rw-r--r-- 1 Floris 197121  51115 2019-07-30 03:00:10.000000000 -0400 field.olean
-rw-r--r-- 1 Floris 197121   8777 2019-07-30 03:00:05.000000000 -0400 field.lean
-rw-r--r-- 1 Floris 197121  27526 2019-07-30 03:00:05.000000000 -0400 group_power.lean
-rw-r--r-- 1 Floris 197121   9130 2019-07-30 03:00:05.000000000 -0400 ordered_field.lean
-rw-r--r-- 1 Floris 197121 306809 2019-07-29 12:26:57.000000000 -0400 ordered_ring.olean
-rw-r--r-- 1 Floris 197121  47613 2019-07-29 12:25:06.000000000 -0400 order_functions.olean
-rw-r--r-- 1 Floris 197121 298623 2019-07-29 12:25:05.000000000 -0400 ordered_group.olean
-rw-r--r-- 1 Floris 197121 269333 2019-07-29 12:22:18.000000000 -0400 free.olean
-rw-r--r-- 1 Floris 197121 180370 2019-07-29 12:21:26.000000000 -0400 ring.olean
-rw-r--r-- 1 Floris 197121  45015 2019-07-29 12:18:42.000000000 -0400 opposites.olean
-rw-r--r-- 1 Floris 197121  15325 2019-07-19 10:40:32.000000000 -0400 free.lean
-rw-r--r-- 1 Floris 197121  18757 2019-07-18 11:19:45.000000000 -0400 pi_instances.lean
-rw-r--r-- 1 Floris 197121  10353 2019-07-18 11:19:45.000000000 -0400 pointwise.lean
drwxr-xr-x 1 Floris 197121      0 2019-07-12 17:47:57.000000000 -0400 ../
-rw-r--r-- 1 Floris 197121  26082 2019-07-11 09:59:06.000000000 -0400 gcd_domain.lean
-rw-r--r-- 1 Floris 197121  30949 2019-07-11 06:13:21.000000000 -0400 big_operators.lean
-rw-r--r-- 1 Floris 197121  25098 2019-07-11 06:13:21.000000000 -0400 direct_limit.lean
-rw-r--r-- 1 Floris 197121   6126 2019-07-11 06:13:21.000000000 -0400 direct_sum.lean
-rw-r--r-- 1 Floris 197121  14904 2019-07-11 06:13:21.000000000 -0400 module.lean
-rw-r--r-- 1 Floris 197121   3561 2019-07-11 06:13:21.000000000 -0400 punit_instances.lean
-rw-r--r-- 1 Floris 197121  11805 2019-07-11 06:13:21.000000000 -0400 ring.lean
-rw-r--r-- 1 Floris 197121  18067 2019-07-11 00:19:32.000000000 -0400 ordered_ring.lean
-rw-r--r-- 1 Floris 197121  25188 2019-07-04 15:49:44.000000000 -0400 ordered_group.lean
-rw-r--r-- 1 Floris 197121  10197 2019-07-04 12:48:24.000000000 -0400 order_functions.lean
-rw-r--r-- 1 Floris 197121  15761 2019-06-14 21:30:47.000000000 -0400 archimedean.lean
-rw-r--r-- 1 Floris 197121  32748 2019-06-14 09:37:10.000000000 -0400 order.olean
-rw-r--r-- 1 Floris 197121  25505 2019-06-14 09:36:49.000000000 -0400 associated.lean
-rw-r--r-- 1 Floris 197121   8715 2019-06-14 09:36:49.000000000 -0400 char_p.lean
-rw-r--r-- 1 Floris 197121   3118 2019-06-14 09:36:49.000000000 -0400 char_zero.lean
-rw-r--r-- 1 Floris 197121    182 2019-06-14 09:36:49.000000000 -0400 default.lean
-rw-r--r-- 1 Floris 197121  13472 2019-06-14 09:36:49.000000000 -0400 euclidean_domain.lean
-rw-r--r-- 1 Floris 197121   6236 2019-06-14 09:36:49.000000000 -0400 field_power.lean
-rw-r--r-- 1 Floris 197121   4862 2019-06-14 09:36:49.000000000 -0400 opposites.lean
-rw-r--r-- 1 Floris 197121   9155 2019-06-14 09:36:49.000000000 -0400 order.lean

I build an arbitrary file, which seems to take longer than I would expect from compiling a single file:

Floris@MSI MINGW64 /d/projects/mathlib ((badeb48b...))
$ lean --make src/algebra/ring.lean

(continued in next message)

Floris van Doorn (Jul 31 2019 at 21:49):

I check the algebra folder again:

Floris@MSI MINGW64 /d/projects/mathlib ((badeb48b...))
$ ls src/algebra/ -alt --time-style=full-iso
total 3973
drwxr-xr-x 1 Floris 197121      0 2019-07-31 17:36:48.436140600 -0400 ./
-rw-r--r-- 1 Floris 197121 180253 2019-07-31 17:36:48.435177800 -0400 ring.olean
drwxr-xr-x 1 Floris 197121      0 2019-07-31 17:36:45.694285600 -0400 group/
-rw-r--r-- 1 Floris 197121  32746 2019-07-31 17:36:17.927331700 -0400 order.olean
drwxr-xr-x 1 Floris 197121      0 2019-07-31 05:24:01.000000000 -0400 CommRing/
drwxr-xr-x 1 Floris 197121      0 2019-07-31 05:24:01.000000000 -0400 Mon/
-rw-r--r-- 1 Floris 197121 470882 2019-07-31 05:14:21.000000000 -0400 direct_limit.olean
-rw-r--r-- 1 Floris 197121  48982 2019-07-30 03:28:45.000000000 -0400 direct_sum.olean
-rw-r--r-- 1 Floris 197121 240420 2019-07-30 03:25:53.000000000 -0400 pi_instances.olean
-rw-r--r-- 1 Floris 197121  23435 2019-07-30 03:24:39.000000000 -0400 punit_instances.olean
-rw-r--r-- 1 Floris 197121  46890 2019-07-30 03:22:47.000000000 -0400 char_p.olean
-rw-r--r-- 1 Floris 197121   2195 2019-07-30 03:22:01.000000000 -0400 default.olean
-rw-r--r-- 1 Floris 197121 194740 2019-07-30 03:22:00.000000000 -0400 module.olean
-rw-r--r-- 1 Floris 197121 115308 2019-07-30 03:20:25.000000000 -0400 pointwise.olean
-rw-r--r-- 1 Floris 197121 267084 2019-07-30 03:08:50.000000000 -0400 big_operators.olean
-rw-r--r-- 1 Floris 197121 228629 2019-07-30 03:07:36.000000000 -0400 gcd_domain.olean
-rw-r--r-- 1 Floris 197121 190155 2019-07-30 03:06:20.000000000 -0400 associated.olean
-rw-r--r-- 1 Floris 197121 144643 2019-07-30 03:05:46.000000000 -0400 archimedean.olean
-rw-r--r-- 1 Floris 197121  51843 2019-07-30 03:02:00.000000000 -0400 field_power.olean
-rw-r--r-- 1 Floris 197121 168299 2019-07-30 03:01:50.000000000 -0400 group_power.olean
-rw-r--r-- 1 Floris 197121 110312 2019-07-30 03:01:26.000000000 -0400 euclidean_domain.olean
-rw-r--r-- 1 Floris 197121  45067 2019-07-30 03:00:16.000000000 -0400 ordered_field.olean
-rw-r--r-- 1 Floris 197121  17108 2019-07-30 03:00:12.000000000 -0400 char_zero.olean
-rw-r--r-- 1 Floris 197121  51115 2019-07-30 03:00:10.000000000 -0400 field.olean
-rw-r--r-- 1 Floris 197121   8777 2019-07-30 03:00:05.000000000 -0400 field.lean
-rw-r--r-- 1 Floris 197121  27526 2019-07-30 03:00:05.000000000 -0400 group_power.lean
-rw-r--r-- 1 Floris 197121   9130 2019-07-30 03:00:05.000000000 -0400 ordered_field.lean
-rw-r--r-- 1 Floris 197121 306809 2019-07-29 12:26:57.000000000 -0400 ordered_ring.olean
-rw-r--r-- 1 Floris 197121  47613 2019-07-29 12:25:06.000000000 -0400 order_functions.olean
-rw-r--r-- 1 Floris 197121 298623 2019-07-29 12:25:05.000000000 -0400 ordered_group.olean
-rw-r--r-- 1 Floris 197121 269333 2019-07-29 12:22:18.000000000 -0400 free.olean
-rw-r--r-- 1 Floris 197121  45015 2019-07-29 12:18:42.000000000 -0400 opposites.olean
-rw-r--r-- 1 Floris 197121  15325 2019-07-19 10:40:32.000000000 -0400 free.lean
-rw-r--r-- 1 Floris 197121  18757 2019-07-18 11:19:45.000000000 -0400 pi_instances.lean
-rw-r--r-- 1 Floris 197121  10353 2019-07-18 11:19:45.000000000 -0400 pointwise.lean
drwxr-xr-x 1 Floris 197121      0 2019-07-12 17:47:57.000000000 -0400 ../
-rw-r--r-- 1 Floris 197121  26082 2019-07-11 09:59:06.000000000 -0400 gcd_domain.lean
-rw-r--r-- 1 Floris 197121  30949 2019-07-11 06:13:21.000000000 -0400 big_operators.lean
-rw-r--r-- 1 Floris 197121  25098 2019-07-11 06:13:21.000000000 -0400 direct_limit.lean
-rw-r--r-- 1 Floris 197121   6126 2019-07-11 06:13:21.000000000 -0400 direct_sum.lean
-rw-r--r-- 1 Floris 197121  14904 2019-07-11 06:13:21.000000000 -0400 module.lean
-rw-r--r-- 1 Floris 197121   3561 2019-07-11 06:13:21.000000000 -0400 punit_instances.lean
-rw-r--r-- 1 Floris 197121  11805 2019-07-11 06:13:21.000000000 -0400 ring.lean
-rw-r--r-- 1 Floris 197121  18067 2019-07-11 00:19:32.000000000 -0400 ordered_ring.lean
-rw-r--r-- 1 Floris 197121  25188 2019-07-04 15:49:44.000000000 -0400 ordered_group.lean
-rw-r--r-- 1 Floris 197121  10197 2019-07-04 12:48:24.000000000 -0400 order_functions.lean
-rw-r--r-- 1 Floris 197121  15761 2019-06-14 21:30:47.000000000 -0400 archimedean.lean
-rw-r--r-- 1 Floris 197121  25505 2019-06-14 09:36:49.000000000 -0400 associated.lean
-rw-r--r-- 1 Floris 197121   8715 2019-06-14 09:36:49.000000000 -0400 char_p.lean
-rw-r--r-- 1 Floris 197121   3118 2019-06-14 09:36:49.000000000 -0400 char_zero.lean
-rw-r--r-- 1 Floris 197121    182 2019-06-14 09:36:49.000000000 -0400 default.lean
-rw-r--r-- 1 Floris 197121  13472 2019-06-14 09:36:49.000000000 -0400 euclidean_domain.lean
-rw-r--r-- 1 Floris 197121   6236 2019-06-14 09:36:49.000000000 -0400 field_power.lean
-rw-r--r-- 1 Floris 197121   4862 2019-06-14 09:36:49.000000000 -0400 opposites.lean
-rw-r--r-- 1 Floris 197121   9155 2019-06-14 09:36:49.000000000 -0400 order.lean

Floris van Doorn (Jul 31 2019 at 21:51):

The interesting observations here are:

It did create a new compiled file ring.olean, so that's good
It also created a new compiled file order.olean, ~~but not for any other files imported by ring.lean~~ (ring.lean does indeed import order.olean via (among others) group.to_additive and tactic.push_neg)

Floris van Doorn (Jul 31 2019 at 21:52):

The compiled file order.olean is indeed different (e.g. it has 2 fewer bytes).

Floris van Doorn (Jul 31 2019 at 21:55):

So what does this mean?

Did Lean decide it had to re-generate order.olean, and therefore also had to compile all other files which imported order.lean? If so, why did this happen?
~~Is it expected that Lean doesn't generate olean files for the other intermediate files, even though order.olean changed? (Making ring.lean another time is almost immediate, so this seems fine.)~~ (see later message)

Floris van Doorn (Jul 31 2019 at 22:04):

One other (mostly unrelated) question:

When I run lean --make (or leanpkg build) I don't get output in the terminal while Lean is running. I think I saw that other users did get output when Lean was running, namely the file (and the line number?) it was compiling at the moment. Is the fact that I don't see this related to Windows? It is really frustrating, since it means I cannot see whether Lean is recompiling the whole library, when I expect it just to compile the file I've changed/added. Is there any way I can get this output (at this point, I would consider using a Linux VM if that would solve this issue)

Floris van Doorn (Jul 31 2019 at 22:10):

Oh, wait, I now see that ring.lean doesn't actually import any other file from this folder (I thought it would, but all the group files are now in a subfolder). Lean did generate olean files for all files imported by ring.lean.

Kevin Kappelmann (Jul 31 2019 at 22:11):

One other (mostly unrelated) question:

When I run lean --make (or leanpkg build) I don't get output in the terminal while Lean is running. I think I saw that other users did get output when Lean was running, namely the file (and the line number?) it was compiling at the moment. Is the fact that I don't see this related to Windows? It is really frustrating, since it means I cannot see whether Lean is recompiling the whole library, when I expect it just to compile the file I've changed/added. Is there any way I can get this output (at this point, I would consider using a Linux VM if that would solve this issue)

I do get that output using leanpkg build as well as lean --make but I am using Linux.

Floris van Doorn (Jul 31 2019 at 22:18):

Ok. Then there is probably something wrong on Windows (or possible specifically on my machine/terminal)

Kevin Buzzard (Aug 01 2019 at 06:45):

There has never been any output in Windows and I agree it's frustrating. Yes you can see both file and line number in Linux (at least in Ubuntu)

Floris van Doorn (Aug 02 2019 at 15:24):

I still have the same problem: Lean doesn't use the olean files downloaded from cache-olean --fetch. Any suggestions @Simon Hudon @Scott Morrison?

Johan Commelin (Aug 02 2019 at 15:26):

I use find to touch all the olean files

Johan Commelin (Aug 02 2019 at 15:26):

That updates the time stamps, and solves the problem for me.

Floris van Doorn (Aug 02 2019 at 15:27):

I'll try that.

Floris van Doorn (Aug 02 2019 at 15:29):

The time stamp problem is when an olean file is not newer than the corresponding lean file? I did try to search for such an olean file before, but couldn't find one. I'll try it anyway.

Kevin Buzzard (Aug 02 2019 at 15:37):

I am certainly not an expert here but I thought that Sebastian once told us that there would also be issues if an olean file relies on another olean file whose timestamp indicated that it had been created later on. In particular I thought that using find to touch all the olean files was risky business.

Johan Commelin (Aug 02 2019 at 15:38):

Well, it's been solving my issues so far.

Kevin Buzzard (Aug 02 2019 at 15:38):

I might be wrong.

Floris van Doorn (Aug 02 2019 at 15:38):

Thanks, @Johan Commelin, this fixes my issues like a charm!

Kevin Buzzard (Aug 02 2019 at 15:39):

I am clearly wrong :-)

Johan Commelin (Aug 02 2019 at 15:39):

Well, you xargs it to touch, and so I think all olean files will have exactly the same timestamp.

Johan Commelin (Aug 02 2019 at 15:40):

Maybe that's just on the right side of risky (-;

Kevin Buzzard (Aug 02 2019 at 15:40):

They don't end up with time stamps which are like 0.01 second apart or something? The reason I've always avoided this is that I didn't know how to touch them in the right order :-)

Floris van Doorn (Aug 02 2019 at 15:42):

I used find src/ -name '*.olean' -exec touch {} + and my timestamps are not the same (but within the same second). That didn't cause problems when importing files deep into mathlib...

Last updated: Dec 20 2023 at 11:08 UTC