apply? cache corrupts when updating mathlib

Stream: mathlib4

[Floris van Doorn]

As mentioned in this thread I'm quite sure that updating mathlib corrupts the apply?cache. I managed to reproduce this as follows:

git clone git@github.com:fpvandoorn/LogicColloquiumTutorial.git
cd LogicColloquiumTutorial/
git checkout 4aa411059088049743ecd573653296d3c84ea3dc
lake exe cache get
lake update
cp lake-packages/mathlib/lean-toolchain .
lake exe cache get
code .

Now open LCTutorial.lean (or a new Lean file) and change the contents to

import Mathlib.Tactic.LibrarySearch

example (x y : ℕ) : x ≤ y := by
  apply?

This should cause a panic.

However, if you just make a new project with lake new test math && lake update && lake exe cache get then the same file will not panic.

[Mauricio Collares]

Interestingly, there are two copies of LibrarySearch.extra, one in build/lib/MathlibExtras (old) and one in lake-packages/mathlib/build/lib/MathlibExtras (new).

[Mauricio Collares]

Ah, this is probably due to #4838, which fixed the path for the library search cache

[Mauricio Collares]

Still annoying that an existing cache at the older location seems to take precedence for some mysterious reason

[Scott Morrison]

I'm not sure that is something I can control from the library_search end of things... It does seem that this is a transient issue that will pass once no one is using mathlib4 pre #4838.

[Yury G. Kudryashov]

Can lake exe cache unpack delete the old cache?

[Mario Carneiro]

I think the main issue here is the hacky way we are resolving what project files live in

[Floris van Doorn]

If this will not be an issue for upgrading mathlib in the future (i.e. past #4838), then it seems low priority to fix something like this.