project doesn't accept mathlib oleans

Stream: maths

[Jakob von Raumer]

Does any know any troubleshooting suggestions for the case that the downloaded mathlib .oleans are just ignored and everytime leanpkg starts to rebuild mathlib instead?

[Patrick Massot]

Is that in mathlib itself or a project depending on mathlib?

[Jakob von Raumer]

A project depending on it. Freshly cloned and equipped with oleans by leanproject get-mathlib-cache

[Patrick Massot]

Then the simplest thing is probably to get rid of _target and start over without investigating

[Jakob von Raumer]

Did that already :confused:

[Jakob von Raumer]

I'll try changing the mathlib rev

[Jakob von Raumer]

That doesn't help either. It seems to believe that the current mathlib is older, for some reason:

mathlib: trying to update _target/deps/mathlib to revision a923261c6eb9e0b179ccaff22effe33e491a7cbc
> git checkout --detach a923261c6eb9e0b179ccaff22effe33e491a7cbc    # in directory _target/deps/mathlib
Previous HEAD position was 3c0061266f feat(data/{seq,stream}): cons_injective2 (#15832)
HEAD is now at a923261c6e feat(data/complex/module): add instance `complex.distrib_smul` (#17115)
> lean --make src

[Eric Wieser]

What do you mean by current?

[Eric Wieser]

That looks like the update was successful to me

[Jakob von Raumer]

After those lines it proceeds to build mathlib from scratch instead of using the oleans

[Eric Wieser]

If you run lean from the command line, which file does it build first?

[Jakob von Raumer]

You mean leanpkg build?

[Eric Wieser]

Or lean --make one_of_your_files

[Jakob von Raumer]

mathlib/src/tactic/core.lean is the first that gets built

[Floris van Doorn]

For some reason it look like it's skipping the "get mathlib olean cache" step. You should get some output

Looking for mathlib oleans for a923261c6e
  locally...
  remotely...
  Found remote mathlib oleans

Try running pip install -U mathlibtools?

[Floris van Doorn]

In the worst case, you can do cd _target/deps/mathlib/, make sure you're on the correct commit, leanproject get-cache and cd ../../... I've done that on old versions of leanproject to work around an issue it had.

[Eric Wieser]

What command is the output above from?

[Floris van Doorn]

In my case it was

vandoorn@pc93-178:~/projects/sphere-eversion(manifold_proper)$ leanproject up
mathlib: trying to update _target/deps/mathlib to revision 3b6552e051629f68c08f02b32339a8f53076a016
> git checkout --detach 3b6552e051629f68c08f02b32339a8f53076a016    # in directory _target/deps/mathlib
Previous HEAD position was 34c70db665 feat(geometry/euclidean/oriented_angle): oriented angles and betweenness (#16824)
HEAD is now at 3b6552e051 chore(linear_algebra/alternating): more lemmas about `curry_left` (#14844)
remote: Enumerating objects: 9954, done.
remote: Counting objects: 100% (7075/7075), done.
remote: Compressing objects: 100% (709/709), done.
remote: Total 9954 (delta 6591), reused 6701 (delta 6363), pack-reused 2879
Receiving objects: 100% (9954/9954), 6.02 MiB | 11.90 MiB/s, done.
Resolving deltas: 100% (7861/7861), completed with 1754 local objects.
From github.com:leanprover-community/mathlib
   40730f6ba8..97568f98eb  AD_barrels              -> origin/AD_barrels
[many lines of output omitted]
 * [new branch]            zorn_Ici                -> origin/zorn_Ici
configuring sphere_eversion 0.1
mathlib: trying to update _target/deps/mathlib to revision a923261c6eb9e0b179ccaff22effe33e491a7cbc
> git checkout --detach a923261c6eb9e0b179ccaff22effe33e491a7cbc    # in directory _target/deps/mathlib
Previous HEAD position was 3b6552e051 chore(linear_algebra/alternating): more lemmas about `curry_left` (#14844)
HEAD is now at a923261c6e feat(data/complex/module): add instance `complex.distrib_smul` (#17115)
Looking for mathlib oleans for a923261c6e
  locally...
  remotely...
  Found remote mathlib oleans
Located matching cache
  a923261c6e: 100%|███████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████| 80.6M/80.6M [00:18<00:00, 4.67MB/s]
Applying cache
  files extracted: 2783 [00:05, 519.62/s]

[Jakob von Raumer]

Thanks for the help, I'll try that after lunch :food:

[Jakob von Raumer]

Floris van Doorn said:

In the worst case, you can do cd _target/deps/mathlib/, make sure you're on the correct commit, leanproject get-cache and cd ../../... I've done that on old versions of leanproject to work around an issue it had.

That doesn't help either, it does the get-cache without issues and then in the base directory still wants to build mathlib whenever I open a file or do leanproject build

[Kevin Buzzard]

Are you on the most recent elan and leanproject? Do you see the "looking for mathlib oleans locally...remotely..." message? If they're being fetched locally then there's a chance they're corrupted; you can just remove the tar.xz file in ~/.mathlib and try again to get them remotely. If this still doesn't solve the problem there's a chance you accidentally edited core Lean; you can delete the version of Lean you're using in ~/.elan (this involves deleting two things) and then use elan to redownload lean and then leanproject to get mathlib ones.

[Jakob von Raumer]

I see the "looking for ..." when doing leanproject get-mathlib-cache or leanproject get-cache but not on leanproject build

[Jakob von Raumer]

elan update doesn't help either

[Kevin Buzzard]

You wouldn't expect it on leanproject build, that's just doing lean --make src.

[Kevin Buzzard]

elan self update updates elan, and some python command which I never remember updates leanproject.

[Kevin Buzzard]

If you think the problem is with your Lean version then you have to nuke things both in ~/.elan/toolchains and ~/.elan/update-hashes

[Kevin Buzzard]

If you accidentally add a space into a core Lean file then the main symptoms are what you are seeing by the way, and the fix is to delete the relevant files in those elan directories and then just open a file in VS Code in the project and it will redownload an uncorrupted Lean.

[Jakob von Raumer]

lean --make src doesn't show the "looking for..." either :thinking: I already tried deleting _target entirely, so it's not changed core files.

[Kevin Buzzard]

I don't understand why you would expect lean --make src, a command which builds lean files directly and has nothing to do with python, to print out a message which a python program prints out when attempting to access the internet to find olean files.

[Kevin Buzzard]

I am conjecturing that you have borked your lean installation

[Kevin Buzzard]

The "looking for" stuff is what the python front end is doing