lake update not working

Stream: mathlib4

[Bolton Bailey]

In light of the recent change from Std to Batteries, I decided to try to update mathlib for my project just to make sure that I could do so without problems. I got the following error:

$ lake update
mathlib: updating repository './.lake/packages/mathlib' to revision '294ff6a495e19ae5a32188033d6e487ca42aded5'
Qq: updating repository './.lake/packages/Qq' to revision '53156671405fbbd5402ed17a79bd129b961bd8d6'
aesop: updating repository './.lake/packages/aesop' to revision '2225b0e4a3528da20499e2304b521e0c4c2a4563'
proofwidgets: updating repository './.lake/packages/proofwidgets' to revision 'e6b6247c61280c77ade6bbf0bc3c66a44fe2e0c5'
Cli: updating repository './.lake/packages/Cli' to revision 'a11566029bd9ec4f68a65394e8c3ff1af74c1a29'
error: ./.lake/packages/aesop/lakefile.toml:1:0: error: unexpected identifier; expected command
error: ./.lake/packages/aesop/lakefile.toml: package configuration has errors

My project only depends directly on Mathlib. Does this have anything to do with the migration, or is there another issue?

[Kim Morrison]

It looks more like it is due to aesop switching from lakefile.lean to a lakefile.toml.

[Kim Morrison]

I don't immediately see the problem. Could I look at the repository myself?

[Bolton Bailey]

Sure it's here https://github.com/BoltonBailey/formal-snarks-project

[Kim Morrison]

Oh, @Bolton Bailey, you are on leanprover/lean4:v4.4.0-rc1!

[Kim Morrison]

Please update your lean-toolchain to v4.8.0-rc1.

[Kim Morrison]

Running lake update will update Mathlib to the latest master, which relies on v4.8.0-rc1.

[Kim Morrison]

@Mac Malone, we really need something that makes it more obvious to the user what is going on here.

If nothing else, if the toolchain in an upstream repository after the update is more recent than the local toolchain, print a warning? Is there an issue covering this problem already?

[Bolton Bailey]

Ok I did the toolchain update and I am now getting
$ lake update
info: stderr:
fatal: Needed a single revision
error: external command 'git' exited with code 128

[Kim Morrison]

Hmm, can't reproduce locally. Do you want to try that again either with a fresh checkout, or after rm -rf .lake?

[Kim Morrison]

Also, your project is really not set up right. :-) lake build does nothing!

[Bolton Bailey]

Ok

[Kim Morrison]

@Mac Malone, I feel like this is sufficiently frequent (users set up their lake project with the main Project.lean having no imports, nor do they use globs), that we should detect for it and issue a warning in lake.

[Kim Morrison]

@Bolton Bailey, what do you usually do to build files in this project?

[Bolton Bailey]

It is usually the case that VSCode shows me whatever errors exist in my code

[Kim Morrison]

But don't you have to open all the files to verify that?

[Kim Morrison]

(No problem if that's what you're doing --- just trying to understand how we can make life easier. :-)

[Bolton Bailey]

Many of the files in this project do not build

[Bolton Bailey]

This has been the case ever since I tried to port this thing from mathlib3

[Bolton Bailey]

Even if they did build, it could possibly take hours for them to do so, that was my experience from the lean3 version.

[Kim Morrison]

Okay! Sorry about that. :-)

[Kim Morrison]

Did lake update after rm -rf .lake or a fresh checkout work for you?

[Bolton Bailey]

So it has not been a priority to get the project to build in its entirety. Instead I just build files one at a time by opening them, or running lake build with a specific name

[Bolton Bailey]

On a happier note, yes, your advice seems to have worked!

[Bolton Bailey]

(Now need to make compatible from a few months of Mathlib changes) Thanks a lot for your help!

[Mac Malone]

@Kim Morrison If you could make issues for these problems (with your feature suggestions), that would be great! :pray:

[Kim Morrison]

lean#4103 is a write-up of the problem here. @Bolton Bailey, perhaps you could check that it reflects what happened?

[Bolton Bailey]

Deja Vu: I am remebering now that all this has happened before here: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Get.20mathlib.20cache.20after.20updating.20mathlib.20dependency/near/392109769

[Bolton Bailey]

(Including someone having to tell me to change the toolchain)

[Kim Morrison]

@Bolton Bailey, you might find it easier to work if you explicitly comment out the as-yet-unported code, so that errors reflect breakages rather than just not-done-stuff.

[Kim Morrison]

Bolton Bailey said:

Deja Vu

Additional evidence we need to improve the tooling! :-)

[Bolton Bailey]

Yes, that issue looks like a good report of what happened, thanks for moving the ball forward on it

[Kim Morrison]

I've also created lean#4105 to track the problem of users not knowing that they either need to import things in Foo.lean, or use globs to tell lake build to build everything.

[Bolton Bailey]

lean4#4105?

[Bolton Bailey]

Wait, is it the case that if I import some files and not others in the MyProject.lean file of a Lean4 project, I can get the CI tools on GitHub to display if just the selected files built correctly?

[Kim Morrison]

Yes.

[Bolton Bailey]

That seems like useful information, thanks.

[Kim Morrison]

Currently you have to write/copy-paste your own github action around lake build, but @Austin Letson has been working on https://github.com/leanprover/lean-action which should make it very easy.

[Kim Morrison]

In fact, I think it is ready for use, and high on my list to test out. :-)

[Bolton Bailey]

I was not a big fan of the "comment everything out" suggestion since it seemed like a lot of mental overhead to uncomment and recomment everything I work on whenever I touch it. Including a subset of my files in the CI check seems much more appealing.

[Oliver Butterley]

What's the expected behaviour of lake update concerning lean-toolchain?

In February it swapped v4.6.0-rc1 to v4.6.0 and then in March it swapped v4.6.0 for v4.7.0-rc2. However it never swapped v4.7.0-rc2 to any of the newer versions.

Was the functionality modified? If so, is there a recommended way that we should update lean-toolchain to the latest apart from doing it manually?

[Mario Carneiro]

lake update never touches the lean-toolchain, however the mathlib post-update hook does, so if your project depends on mathlib then it will automatically be upgraded to the latest lean along with mathlib. Unfortunately this mechanism only works when lake doesn't have a breaking change, since in that case the old lake won't be able to read mathlib's lakefile which contains the definition of the post-update hook. So if you try to bump to the next stable you will frequently get stuck and have to copy the toolchain manually