Running lake cache without updating the lean toolchain

Stream: general

[Shreyas Srinivas]

For some reason, lake exe cache get is off-late upgrading my toolchain. This is an issue because until now, if I did not like or want a toolchain upgrade, all I had to do was change the lean-toolchain file, and remove the manifest file and build folder. Calling lake exe cache get would simply get the mathlib cache of that toolchain.

[Shreyas Srinivas]

How do I compel cache to not update the toolchain

[Shreyas Srinivas]

These are the lines in the output of lake exe cache get show that cache is indeed updating the toolchain:

info: mathlib: cloning https://github.com/leanprover-community/mathlib4.git
info: updating toolchain to 'leanprover/lean4:v4.18.0-rc1'

[Shreyas Srinivas]

In a way that makes the cache get command redundant since, lake update does the same thing. I currently just want to get the cache for the toolchain I set.

[Kim Morrison]

Can you point us to a repro? i.e. a commit of some repository where lake exe cache get has this behaviour?

[Shreyas Srinivas]

clone equational theories.

[Shreyas Srinivas]

then try lake update and it will fail to build. Delete ./.lake, lake-manifest.json and change lean-toolchain to v4.14.0-rc3 ( which is what I want to revert to).

[Shreyas Srinivas]

run lake exe cache get

[Kim Morrison]

Oh, that is ancient. :-)

[Shreyas Srinivas]

Yeah, but the non-updating behaviour has been around for at least a year if not more. Why would 4.14.0-rc3 be different?

[Shreyas Srinivas]

Here's a partial command transcript:

shreyas@vonNeumann:~/Projects/temporary/equational_theories$ rm -Rf ./.lake/
shreyas@vonNeumann:~/Projects/temporary/equational_theories$ nano lean-toolchain
shreyas@vonNeumann:~/Projects/temporary/equational_theories$ cat lean-toolchain
leanprover/lean4:v4.14.0-rc3
shreyas@vonNeumann:~/Projects/temporary/equational_theories$ rm lake-manifest.json
rm: cannot remove 'lake-manifest.json': No such file or directory
shreyas@vonNeumann:~/Projects/temporary/equational_theories$ lake exe cache get
info: equational_theories: no previous manifest, creating one from scratch
info: doc-gen4: cloning https://github.com/leanprover/doc-gen4
info: doc-gen4: checking out revision '1b489cdbe4bc57a6acdddb9a5dc5699acacdecdd'
info: checkdecls: cloning https://github.com/PatrickMassot/checkdecls.git
info: mathlib: cloning https://github.com/leanprover-community/mathlib4.git
info: updating toolchain to 'leanprover/lean4:v4.18.0-rc1'
...

[Shreyas Srinivas]

Interestingly, if I don't try the whole update attempt (meaning I run lake exe cache get on a fresh clone from github), this update step doesn't happen

[Eric Wieser]

I don't think deleting the manifest is a supported workflow?

[Shreyas Srinivas]

Not deleting the manifest means that lake downloads the commits of the dependencies recorded in it

[Eric Wieser]

Yes, that is how it is supposed to work

[Shreyas Srinivas]

which means when I am downgrading, the manifest will make lake download invalid versions

[Eric Wieser]

lake update can downgrade too

[Shreyas Srinivas]

In any case "delete manifest and ./.lake" has been the default nuclear option if lake cache or lake update fails

[Shreyas Srinivas]

It has always worked well for me

[Shreyas Srinivas]

and deleting the manifest has not caused cache to automatically update toolchains in the past

[Eric Wieser]

"nukes have always worked for me, says user struggling with nuclear fallout" is not the best stance...

[Shreyas Srinivas]

point is, this behaviour has changed.

[Eric Wieser]

What happens if you go back to a clean version and just change the mathlib tag in the lakefile, and do lake update?

[Shreyas Srinivas]

In this case, the last clean version was on toolchain v4.14.0-rc3

[Shreyas Srinivas]

So going back to that toolchain, the first step, is already the problem I am describing

[Eric Wieser]

By "clean" I mean "don't delete the manifest"

[Eric Wieser]

And also, don't edit the toolchain. Only edit the lakefile

[Shreyas Srinivas]

rror: ././.lake/packages/mathlib: revision not found 'v4.14.0-rc3'

[Eric Wieser]

Ok, so pick a revision that exists

[Eric Wieser]

You can either go though the mathlib history and pick a commit SHA, or pick something more stable like the non-rc version

[Shreyas Srinivas]

Dependency Mathlib uses a different lean-toolchain
  Project uses leanprover/lean4:v4.18.0-rc1
  Mathlib uses leanprover/lean4:v4.17.0

The cache will not work unless your project's toolchain matches Mathlib's toolchain
This can be achieved by copying the contents of the file `././.lake/packages/mathlib/././lean-toolchain`
into the `lean-toolchain` file at the root directory of your project
You can use `cp ././.lake/packages/mathlib/././lean-toolchain ./lean-toolchain`
error: mathlib: failed to fetch cache

[Eric Wieser]

Is that after picking a git rev that exists?

[Shreyas Srinivas]

This method also used to work btww

Eric Wieser said:

And also, don't edit the toolchain. Only edit the lakefile

Didn't edit the toolchain in the above. Only lakefile.toml

[Eric Wieser]

I don't think toml files existed in 4.13.0, though I'm not certain

[Shreyas Srinivas]

yes. That's where this must come from : Mathlib uses leanprover/lean4:v4.17.0

[Shreyas Srinivas]

this is v4.17.0

[Eric Wieser]

So you wrote 4.17.0 in the toml?

[Shreyas Srinivas]

name = "equational_theories"
defaultTargets = ["equational_theories"]

[leanOptions]
pp.unicode.fun = true
autoImplicit = false
relaxedAutoImplicit = false

[[require]]
name = "mathlib"
git = "https://github.com/leanprover-community/mathlib4.git"
rev = "v4.17.0"

[[require]]
name = "checkdecls"
git = "https://github.com/PatrickMassot/checkdecls.git"

[[require]]
name = "«doc-gen4»"
git = "https://github.com/leanprover/doc-gen4"

[Shreyas Srinivas]

I only changed the rev of mathlib

[Eric Wieser]

Eric Wieser said:

And also, don't edit the toolchain. Only edit the lakefile

I'll refine this suggestion to "only edit the toolchain if lake tells you to"

[Shreyas Srinivas]

Eric Wieser said:

Eric Wieser said:

And also, don't edit the toolchain. Only edit the lakefile

I'll refine this suggestion to "only edit the toolchain if lake tells you to"

Having done that:

info: updating toolchain to 'leanprover/lean4:v4.18.0-rc1'
info: restarting Lake via Elan
info: toolchain not updated; already up-to-date
info: mathlib: running post-update hooks
Dependency Mathlib uses a different lean-toolchain
  Project uses leanprover/lean4:v4.18.0-rc1
  Mathlib uses leanprover/lean4:v4.17.0

[Eric Wieser]

Can you give the full list of commands you ran, from a clean state?

[Shreyas Srinivas]

that's difficult

[Eric Wieser]

Well in that case, can you make a fresh clone of the repo and trigger the same issue?

[Shreyas Srinivas]

Yes. I am currently showing you this issue on such a clone

[Eric Wieser]

It's fine for your commands to include # edit the lakefile with blah

[Eric Wieser]

Why is it hard to tell us the list of commands you ran? This is #mwe, but for the command line instead of Lean

[Shreyas Srinivas]

The sequence is as I described above:

1. Clone equational theories.
2. Make a branch if you like
3. run lake update
4. run lake build and it will almost certainly fail
   (more coming up)

[Eric Wieser]

That sequence doesn't mention modifying the lakefile, but you did modify it

[Shreyas Srinivas]

Please wait

5. change lean-toolchain to 4.14.0-rc3

[Shreyas Srinivas]

6. delete lake-manifest and ./.lake
7. run lake exe cache get

[Shreyas Srinivas]

Shreyas Srinivas said:

Here's a partial command transcript:

shreyas@vonNeumann:~/Projects/temporary/equational_theories$ rm -Rf ./.lake/
shreyas@vonNeumann:~/Projects/temporary/equational_theories$ nano lean-toolchain
shreyas@vonNeumann:~/Projects/temporary/equational_theories$ cat lean-toolchain
leanprover/lean4:v4.14.0-rc3
shreyas@vonNeumann:~/Projects/temporary/equational_theories$ rm lake-manifest.json
rm: cannot remove 'lake-manifest.json': No such file or directory
shreyas@vonNeumann:~/Projects/temporary/equational_theories$ lake exe cache get
info: equational_theories: no previous manifest, creating one from scratch
info: doc-gen4: cloning https://github.com/leanprover/doc-gen4
info: doc-gen4: checking out revision '1b489cdbe4bc57a6acdddb9a5dc5699acacdecdd'
info: checkdecls: cloning https://github.com/PatrickMassot/checkdecls.git
info: mathlib: cloning https://github.com/leanprover-community/mathlib4.git
info: updating toolchain to 'leanprover/lean4:v4.18.0-rc1'
...

This brings us up to this point

[Eric Wieser]

This sequence has gone wrong in step 4, you should rewind to step 2

[Shreyas Srinivas]

equational theories doesn't build on 4.18.0-rc1. That's an entirely different issue

[Eric Wieser]

Yes, but that told you that step 3 was a mistake

[Shreyas Srinivas]

I am simply trying to get my local repo back to 4.14.0-rc3 which is the last toolchain it passed CI on

[Shreyas Srinivas]

Eric Wieser said:

Yes, but that told you that step 3 was a mistake

Yes, but at that stage lean-toolchain had already changed to v4.18.0-rc1

[Eric Wieser]

Great, so undo it

[Shreyas Srinivas]

And the cache had been dowloaded

[Shreyas Srinivas]

for v4.18.0-rc1

[Shreyas Srinivas]

And it is in undoing it that i first tried steps 5 to 7

[Eric Wieser]

git reset --hard is your undo button

[Shreyas Srinivas]

My undo solution was simpler. To clone the repo and checkout the relevant PR branch again

[Eric Wieser]

Sure, whatever. Did you then edit the lakefile from that clean state?

[Shreyas Srinivas]

No, because that repository was already in v4.14.0-rc3

[Shreyas Srinivas]

there was no need to downgrade it

[Eric Wieser]

What did you do instead of step 3 above?

[Shreyas Srinivas]

My question is, how do I go back to 4.14.0-rc3 after an update to 4.18.0 without making a fresh clone or git reset

[Eric Wieser]

You can't, because the information that told you exactly what 4.14.0rc3 meant was in the manifest you deleted / overwrote

[Shreyas Srinivas]

Previously, cleaning the manifest and build folder and fixing lean-toolchain or mathlib's revision did the trick

[Shreyas Srinivas]

Eric Wieser said:

You can't, because the information that told you exactly what 4.14.0rc3 meant was in the manifest you deleted / overwrote

that manifest was already overwritten by lake update

[Eric Wieser]

Yes, I attribute the overwriting to you because you ran lake update

[Shreyas Srinivas]

yes

[Shreyas Srinivas]

So how do I get it back to the revisions of dependencies for v4.14.0-rc3?

[Eric Wieser]

git checkout pr-commit -- lake-manifest.json

[Shreyas Srinivas]

It used to be that lake would correctly regenerate a deleted manifest according to the toolchain in lean-toolchain

[Eric Wieser]

It is impossible for it to regenerate the same one you started with

[Shreyas Srinivas]

Eric Wieser said:

git checkout pr-commit -- lake-manifest.json

why do I need to tinker with manifests and pick them in the first place when I am downgrading?

[Eric Wieser]

Which version of mathlib are you expecting lake to pick?

[Shreyas Srinivas]

When generating a fresh manifest for <insert toolchain> lake used to be able to pick the correct revisions.

[Shreyas Srinivas]

I know this because I have used this trick several times.

[Eric Wieser]

Are you sure? I think it only ever picked the newest revisions (for the branch specified in the lakefile)

[Eric Wieser]

This is indistinguishable from the "correct" revision if you're on the latest version already

[Shreyas Srinivas]

I have downgraded toolchains before.

[Eric Wieser]

Eric Wieser said:

Which version of mathlib are you expecting lake to pick?

[Shreyas Srinivas]

the version in the rev parameter of mathlib in lakefile?

[Shreyas Srinivas]

Step 8. I changed the rev of mathlib to "v4.14.0-rc3". Ran lake exe cache get. The toolchain file was not modified.

[Shreyas Srinivas]

I took your advice and created a fresh clone

[Eric Wieser]

Shreyas Srinivas said:

the version in the rev parameter of mathlib in lakefile?

Which is "main", right?

[Shreyas Srinivas]

Just now

[Shreyas Srinivas]

1614  gh repo clone teorth/equational_theories
 1615  cd ./equational_theories/
 1616  nano lakefile.toml
 1617  lake update
 1618  history | tail -n 5

[Shreyas Srinivas]

In 1616, I modified lakefile.toml to add rev=v4.17.0 for mathlib

[Shreyas Srinivas]

This is the result:

Dependency Mathlib uses a different lean-toolchain
  Project uses leanprover/lean4:v4.18.0-rc1
  Mathlib uses leanprover/lean4:v4.17.0

The cache will not work unless your project's toolchain matches Mathlib's toolchain
This can be achieved by copying the contents of the file `././.lake/packages/mathlib/././lean-toolchain`
into the `lean-toolchain` file at the root directory of your project
You can use `cp ././.lake/packages/mathlib/././lean-toolchain ./lean-toolchain`
error: mathlib: failed to fetch cache

[Eric Wieser]

Great, do what it told you and now you're done

[Shreyas Srinivas]

It worked to update to v4.17.0. But when I did the same to downgrade to v4.14.0, it failed

[Eric Wieser]

Probably because the toml format didn't exist

[Eric Wieser]

I recommend going back one at a time

[Shreyas Srinivas]

I am sure it did

[Shreyas Srinivas]

We have been using the toml file since before that toolchain

[Shreyas Srinivas]

The issue was, cache said I should run lake update to update the manifest

[Shreyas Srinivas]

So I ran lake update

[Shreyas Srinivas]

Which decided that I need v4.18.0-rc1

[Shreyas Srinivas]

back to square one.

[Eric Wieser]

That sounds like your lakefile didn't pin something

[Shreyas Srinivas]

[[require]]
name = "mathlib"
git = "https://github.com/leanprover-community/mathlib4.git"
rev = "v4.14.0"

[[require]]
name = "checkdecls"
git = "https://github.com/PatrickMassot/checkdecls.git"

[[require]]
name = "«doc-gen4»"
git = "https://github.com/leanprover/doc-gen4"
rev = "main"

[[lean_lib]]
name = "equational_theories"

[[lean_exe]]
name = "extract_implications"
root = "scripts.extract_implications"
supportInterpreter = true

[[lean_exe]]
name = "export_equations"
root = "scripts.export_equations"
supportInterpreter = true

[[lean_exe]]
name = "generate_lifting_magma_family_counterexamples"
root = "equational_theories.LiftingMagmaFamiliesCounterexamples"
supportInterpreter = true

[Shreyas Srinivas]

It pinned mathlib

[Jon Eugster]

you'll need to specify explicit revs for all dependencies

[Eric Wieser]

You probably need to pin doc-gen too

[Eric Wieser]

Or only ask to update mathlib

[Shreyas Srinivas]

$ lake update mathlib
info: updating toolchain to 'leanprover/lean4:v4.18.0-rc1'

[Shreyas Srinivas]

This time I changed the rev of both mathlib and doc-gen. Something strange:

nano lakefile.toml
shreyas@vonNeumann:~/Projects/temporary/equational_theories$ nano lean-toolchain
shreyas@vonNeumann:~/Projects/temporary/equational_theories$ lake update
info: doc-gen4: checking out revision '0a8cd7afb471bb1fdd335118bf1e253a38a2af53'
info: updating toolchain to 'leanprover/lean4:v4.15.0-rc1'

[Shreyas Srinivas]

both revs were set to v4.14.0

[Shreyas Srinivas]

but :

$  cat lean-toolchain
leanprover/lean4:v4.14.0

[Shreyas Srinivas]

which contradicts : info: updating toolchain to 'leanprover/lean4:v4.15.0-rc1'

[Shreyas Srinivas]

I need to leave now, but it is clear that lake has some very confusing behaviour when trying to downgrade toolchains