Newly downloaded repo has errors

Stream: general

[Filippo A. E. Nuccio]

Since I was encountering problems with my local copy of lean-liquid, I have thrown it away and I have downloaded (leanproject get lean-liquid) a fresh new copy. Still, in one file I get errors (I have checked both online and with other colleagues, it properly compiles elsewhere). I do not know what to try any more... any suggestion?

[Mauricio Collares]

What errors? With no other information, my best guess is that you could have a corrupted olean cache in ~/.mathlib.

[Kevin Buzzard]

git pull (on master) then ./scripts/get-cache.sh and then leanproject build works for me -- no warnings or errors, and finishes quickly

[Filippo A. E. Nuccio]

Let me try

[Filippo A. E. Nuccio]

Is it normal that when I try to get the cache, it finds the local oleans for mathlib (and extracts the files), but says Trying to dowload project cache and returns No olean cache available?

[Oliver Nash]

@Filippo A. E. Nuccio Can you find your ~/./mathlib folder? Just blow away whatever is in there and I'll bet everything will just work.

[Filippo A. E. Nuccio]

No, unfortunately it does not; I have tried it several times already.

[Oliver Nash]

What happens if you type git rev-parse HEAD in your lean-liquid directory?

[Filippo A. E. Nuccio]

5618fc7844c798f00a0d29c3a70433d3d2e40f03

[Oliver Nash]

(One behind HEAD). Weird, that looks fine. In that case I'm stumped.

[Oliver Nash]

Although I do note it failed to build (though only because of linting). Maybe try git checkout 9fc85b0e58a2c9aa4752bcb9e073794b76ade06b and then try.

[Mauricio Collares]

What's the error message you're getting?

[Filippo A. E. Nuccio]

@Mauricio Collares Well, I have a lemma whose proof (which is a rfl) makes it unhappy, saying type mismatch, term rfl has type... as usual.

[Filippo A. E. Nuccio]

Oliver Nash said:

Although I do note it failed to build (though only because of linting). Maybe try git checkout 9fc85b0e58a2c9aa4752bcb9e073794b76ade06b and then try.

Trying it...

[Filippo A. E. Nuccio]

At any rate, is it normal that there are no project cache available? Or am I misunderstanding the error No olean cache available?

[Mauricio Collares]

If you want to check your Mathlib cache, the MD5 for ef51d2324e937c8883ac8d1781dfc9168668e451.tar.xz is 3bd64d96788c5b3f3fcf5ee2b3a1272f. But here ./scripts/get-cache.sh finds cached oleans for both mathlib and the project.

[Filippo A. E. Nuccio]

What do you mean by "here"?

[Filippo A. E. Nuccio]

On your pc?

[Mauricio Collares]

And the MD5 sum for the lean-liquid cache (5618fc7844c798f00a0d29c3a70433d3d2e40f03.tar.xz) is f6ab7e1db3179ee0eac82524fd1aaa24.

[Mauricio Collares]

Yes, I mean on my PC.

[Filippo A. E. Nuccio]

Oh, interesting. This means that for some reason my git repo is not dowloading the cache for the project, only for mathlib.

[Filippo A. E. Nuccio]

I have just unistalled and reinstalled both elan and mathtools...

[Eric Wieser]

for some reason my git repo is not dowloading the cache for the project, only for mathlib.

mathlibtools does not (yet) know how to download caches for things that aren't mathlib

[Filippo A. E. Nuccio]

Ah, but then how was @Mauricio Collares getting both cache?

[Mauricio Collares]

I ran ./scripts/get-cache.sh, which uses leanproject only for getting the mathlib cache (and wgets the project cache directly)

[Filippo A. E. Nuccio]

Kevin Buzzard said:

git pull (on master) then ./scripts/get-cache.sh and then leanproject build works for me -- no warnings or errors, and finishes quickly

@Kevin Buzzard When you do .scripts/get-cache.sh do you get Trying to dowload project cache and then No olean cache available?

[Filippo A. E. Nuccio]

Mauricio Collares said:

I ran ./scripts/get-cache.sh, which uses leanproject only for getting the mathlib cache (and wgets the project cache directly)

And have you also tried a leanproject build? Kevin says " it was ok pretty quickly" whereas to me it seems my PC is trying to take off quickly...

[Mauricio Collares]

I ran lean -j8 --make src without a project cache, just to be sure. It built the project in roughly half an hour.

[Filippo A. E. Nuccio]

WOW! Half an hour is fast, thanks.

[Filippo A. E. Nuccio]

And what is the -j8?

[Mauricio Collares]

I don't know if lean or leanproject uses multiple cores by default. This instructs lean to use 8 threads to compile (my CPU has 8 cores).

[Filippo A. E. Nuccio]

Ah, wow! Mine has one, so it will probably explain why your system is much faster.

[Kevin Buzzard]

@Filippo A. E. Nuccio here's what a fresh install looks like for me:

$ leanproject get lean-liquid
[normal git/leanproject download stuff]
$ cd lean-liquid/
$ ./scripts/get-cache.sh
Looking for lean-liquid oleans for ef51d2324e
  locally...
  Found local lean-liquid oleans
Located matching cache
Applying cache
  files extracted: 2351 [00:04, 516.21/s]
Trying to download project cache
Found oleans at https://oleanstorage.azureedge.net/mathlib/lean-liquid/
Extracted oleans into src and deleted archive
$ leanproject build
[small amount of git stuff and then a pause of a few seconds and then returns]

and I have oleans for everything in src and also for everything in _target/deps_mathlib.

[Filippo A. E. Nuccio]

@Kevin Buzzard Thanks! I see a (big) difference then: when it tries to dowload the project cache, it finds them in azureedge, and this fails on my side.

[Kevin Buzzard]

Are you on master branch?

[Filippo A. E. Nuccio]

I am

[Filippo A. E. Nuccio]

I am trying to manually add the lean-liquid part of the path to my url file, seeing if I get anywhere.

[Kevin Buzzard]

Do you have local work you need to save? What happens if you just nuke the repo and start again with leanproject get lean-liquid?

[Mauricio Collares]

@Filippo A. E. Nuccio Can you paste the output of get-cache.sh here?

[Filippo A. E. Nuccio]

@Kevin Buzzard No, I can throw everything away, but I have already tried severl times and I end up with the same problem.

[Filippo A. E. Nuccio]

$ ./scripts/get-cache.sh
Looking for mathlib oleans for ef51d2324e
  locally...
  Found local mathlib oleans
Located matching cache
Applying cache
  files extracted: 2351 [00:11, 213.47/s]
Trying to download project cache
No olean cache available

[Filippo A. E. Nuccio]

Can I ask you how your url file looks like?

[Filippo A. E. Nuccio]

The one in the ~/./mathlib folder

[Mauricio Collares]

It contains a single line: https://oleanstorage.azureedge.net/mathlib/.

[Kevin Buzzard]

~/.mathlib$ more url
https://oleanstorage.azureedge.net/mathlib/

[Mauricio Collares]

Can you download https://oleanstorage.azureedge.net/mathlib/lean-liquid/5618fc7844c798f00a0d29c3a70433d3d2e40f03.tar.xz from your browser, say? It should have 6548180 bytes.

[Filippo A. E. Nuccio]

Oh, identical to mine!

[Filippo A. E. Nuccio]

Mauricio Collares said:

Can you download https://oleanstorage.azureedge.net/mathlib/lean-liquid/5618fc7844c798f00a0d29c3a70433d3d2e40f03.tar.xz from your browser, say?

Are these the olean I should put in the ~/./mathlib folder?

[Kevin Buzzard]

I should think you should put them in the lean-liquid folder

[Mauricio Collares]

If you want to do it manually, you should extract those files at the lean-liquid root directory by running something like tar xvf ~/Downloads/5618fc7844c798f00a0d29c3a70433d3d2e40f03.tar.xz

[Filippo A. E. Nuccio]

Ok, let me try.

[Filippo A. E. Nuccio]

Done

[Filippo A. E. Nuccio]

In theory, leanproject build should now be quick, right?

[Kevin Buzzard]

and /src should look something like this:

$ ls -l
total 1348
-rw-rw-r-- 1 buzzard buzzard   9876 Apr 13 17:02 banach.lean
-rw-r--r-- 1 buzzard buzzard 106348 Apr 10 14:19 banach.olean
drwxrwxr-x 2 buzzard buzzard   4096 Apr 13 17:04 breen_deligne
-rw-rw-r-- 1 buzzard buzzard   1855 Apr 13 17:02 challenge.lean
-rw-rw-r-- 1 buzzard buzzard    690 Apr 13 17:02 challenge_notations.lean
-rw-r--r-- 1 buzzard buzzard   2833 Apr 11 20:37 challenge_notations.olean
-rw-r--r-- 1 buzzard buzzard  13274 Apr 13 16:22 challenge.olean
drwxrwxr-x 2 buzzard buzzard   4096 Apr 13 17:04 combinatorial_lemma
drwxrwxr-x 3 buzzard buzzard   4096 Apr 13 17:04 condensed
drwxrwxr-x 2 buzzard buzzard   4096 Apr 13 17:04 facts
drwxrwxr-x 9 buzzard buzzard   4096 Apr 13 17:04 for_mathlib
drwxrwxr-x 2 buzzard buzzard   4096 Apr 13 17:04 free_pfpng
drwxrwxr-x 2 buzzard buzzard   4096 Apr 13 17:04 hacks_and_tricks
drwxrwxr-x 2 buzzard buzzard   4096 Apr 13 17:04 invpoly
drwxrwxr-x 2 buzzard buzzard   4096 Apr 13 17:04 laurent_measures
drwxrwxr-x 2 buzzard buzzard   4096 Apr 13 17:04 Lbar
-rw-rw-r-- 1 buzzard buzzard   3923 Apr 13 17:02 liquid.lean
-rw-r--r-- 1 buzzard buzzard  16241 Apr 11 02:47 liquid.olean
drwxrwxr-x 2 buzzard buzzard   4096 Apr 13 17:04 locally_constant
drwxrwxr-x 2 buzzard buzzard   4096 Apr 13 17:04 normed_group
-rw-rw-r-- 1 buzzard buzzard  19812 Apr 13 17:02 normed_snake_dual.lean
-rw-r--r-- 1 buzzard buzzard 230539 Apr 10 14:38 normed_snake_dual.olean
-rw-rw-r-- 1 buzzard buzzard   7371 Apr 13 17:02 normed_snake.lean
-rw-r--r-- 1 buzzard buzzard 104440 Apr 10 14:23 normed_snake.olean
-rw-rw-r-- 1 buzzard buzzard  17649 Apr 13 17:02 normed_spectral.lean
-rw-r--r-- 1 buzzard buzzard 293048 Apr 10 14:49 normed_spectral.olean
-rw-rw-r-- 1 buzzard buzzard   1133 Apr 13 17:02 normed_to_cond.lean
-rw-r--r-- 1 buzzard buzzard   6990 Apr 13 16:20 normed_to_cond.olean
drwxrwxr-x 2 buzzard buzzard   4096 Apr 13 17:04 polyhedral_lattice
drwxrwxr-x 2 buzzard buzzard   4096 Apr 13 17:04 prop819
-rw-rw-r-- 1 buzzard buzzard  20178 Apr 13 17:02 prop819.lean
-rw-r--r-- 1 buzzard buzzard 404583 Apr 10 15:07 prop819.olean
drwxrwxr-x 2 buzzard buzzard   4096 Apr 13 17:04 prop_92
drwxrwxr-x 3 buzzard buzzard   4096 Apr 13 17:04 pseudo_normed_group
drwxrwxr-x 2 buzzard buzzard   4096 Apr 13 17:04 real_measures
drwxrwxr-x 2 buzzard buzzard   4096 Apr 13 17:04 rescale
-rw-rw-r-- 1 buzzard buzzard    763 Apr 13 17:02 statement.lean
-rw-r--r-- 1 buzzard buzzard   3350 Apr 11 02:40 statement.olean
drwxrwxr-x 2 buzzard buzzard   4096 Apr 13 17:04 system_of_complexes
drwxrwxr-x 3 buzzard buzzard   4096 Apr 13 17:04 thm95
$

[Kevin Buzzard]

and for a bonus point can someone tell me what definition of alphabetical order gives challenge.lean and then challenge_notations.lean and then challenge_notaitons.olean and then challenge.olean?

[Filippo A. E. Nuccio]

Well, quite similar

$ ls
banach.lean                normed_snake.lean
banach.olean               normed_snake.olean
breen_deligne/             normed_snake_dual.lean
challenge.lean             normed_snake_dual.olean
challenge.olean            normed_spectral.lean
challenge_notations.lean   normed_spectral.olean
challenge_notations.olean  normed_to_cond.lean
combinatorial_lemma/       normed_to_cond.olean
condensed/                 polyhedral_lattice/
facts/                     prop_92/
for_mathlib/               prop819/
free_pfpng/                prop819.lean
hacks_and_tricks/          prop819.olean
invpoly/                   pseudo_normed_group/
laurent_measures/          real_measures/
Lbar/                      rescale/
liquid.lean                statement.lean
liquid.olean               statement.olean
locally_constant/          system_of_complexes/
normed_group/              thm95/

[Kevin Buzzard]

this looks great

[Kevin Buzzard]

and does leanproject build work?

[Filippo A. E. Nuccio]

Oh, it finished!

[Filippo A. E. Nuccio]

And my laptop is still on the desk, not yet in the sky.

[Filippo A. E. Nuccio]

Let me try to open VSCode

[Kevin Buzzard]

There is still the question of what is going on because tomorrow you pull and then it doesn't work again :-/

[Mauricio Collares]

I wonder if you don't have wget installed

[Filippo A. E. Nuccio]

Ah

[Filippo A. E. Nuccio]

Well, first of all, even in VSCode it works! :tada: :octopus:

[Filippo A. E. Nuccio]

But now Kevin's point is crucial. How to avoid this tomorrow?

[Yaël Dillies]

Do not wake up

[Filippo A. E. Nuccio]

Indeed, I have a

$ wget
bash: wget: command not found

[Mauricio Collares]

(deleted)

[Mauricio Collares]

Ah!

[Kevin Buzzard]

Nice!

[Filippo A. E. Nuccio]

Ok, let me install wget and re-try everything.

[Filippo A. E. Nuccio]

YES!!!!

$ ./scripts/get-cache.sh
Looking for mathlib oleans for ef51d2324e
  locally...
  Found local mathlib oleans
Located matching cache
Applying cache
  files extracted: 2351 [00:11, 212.76/s]
Trying to download project cache
Found oleans at https://oleanstorage.azureedge.net/mathlib/lean-liquid/
Extracted oleans into src and deleted archive

[Filippo A. E. Nuccio]

Thank you so much @Mauricio Collares and @Kevin Buzzard

[Filippo A. E. Nuccio]

But now a final question: is it me that on a drunk evening decided to uninstall wget and don't have any recollection, or is it something that does not come with Win10? Perhaps @Patrick Massot has a clue?

[Ruben Van de Velde]

It seems likely that it would not come with Windows

[Ruben Van de Velde]

The failure mode is pretty poor, though

[Filippo A. E. Nuccio]

By "failure mode" you mean the way Win has not to inform the user of the problem?

[Bryan Gin-ge Chen]

We should probably add "install wget" to our installation instructions for windows, and possibly leanproject should mention the possibility that wget is missing in the error message.

[Mauricio Collares]

Kevin Buzzard said:

and for a bonus point can someone tell me what definition of alphabetical order gives challenge.lean and then challenge_notations.lean and then challenge_notaitons.olean and then challenge.olean?

ls uses your locale's collation rules (via LC_COLLATE), and I guess _ and . are considered equivalent? My locale has the same behaviour and I guess this is related to ISO/IEC 14651, but I don't want to buy the standard to discover why :) You can do LC_COLLATE=C ls -l to override it.

[Mauricio Collares]

Bryan Gin-ge Chen said:

We should probably add "install wget" to our installation instructions for windows, and possibly leanproject should mention the possibility that wget is missing in the error message.

It's not leanproject's fault, though: lean-liquid has a custom script which invokes wget. Leanproject uses Python's requests library.

[Bryan Gin-ge Chen]

Ah! I stand corrected then.

[Filippo A. E. Nuccio]

Mauricio Collares said:

Bryan Gin-ge Chen said:

We should probably add "install wget" to our installation instructions for windows, and possibly leanproject should mention the possibility that wget is missing in the error message.

It's not leanproject's fault, though: lean-liquid has a custom script which invokes wget. Leanproject uses Python's requests library.

@Johan Commelin We then need to add it to the LTE docs?

[Kevin Buzzard]

We just need to finish LTE :-)

[Patrick Massot]

Indeed this wget issue has nothing to do with leanproject. However avoiding Windows is still a great general purpose advice.

[Filippo A. E. Nuccio]

Thanks for the great general purpose advice! :rofl:

[Filippo A. E. Nuccio]

Yaël Dillies said:

Do not wake up

I woke up and it still works! :tada:

[Kevin Buzzard]

Yeah but now you have a git security issue ;-)