Updating using lake again

Stream: lean4

[Patrick Massot]

We were discussing Heather's book in some other stream and I wanted to see whether some things changed in recent Lean versions. But I have not been able to update the project. I tried everything I could think of, changing the lakefile, deleting the manifest, deleting lake-packages, but nothing worked. @Mac Malone could you tell us how you would go from a fresh clone of https://github.com/hrmacbeth/math2001/ to a version that is setup to use current Mathlib master? Of course there would be build errors if things changed in Mathlib, but I'm very far away from that stage.

[Patrick Massot]

Everybody should feel free to play this challenge. Here is one recorded attempt:
lake.gif

[Patrick Massot]

By the way, I don't understand why cloning mathlib4 is so painfully slow, but lake not displaying anything doesn't help to know whether something is happening or the whole thing stopped.

[Kevin Buzzard]

Maybe update the mathlib git hash in the lakefile and then copy mathlib's lean-toolchain before the lake update?

[Kevin Buzzard]

Just tried -- still getting "warning: improperly formatted manifest: incompatible manifest version 4" and, like you, error: no such file or directory ../../../Math2001.lean

[Patrick Massot]

The error: no such file or directory ../../../Math2001.lean is not lake's fault, this project is indeed malformed from this perspective.

[Mac Malone]

@Patrick Massot You were right on track! All that was left to do was change the versions of mathlib (and maybe cs22-lean-autograder) mentioned in the lakefile (as @Kevin Buzzard suggested). Because they are currently fixed to a specific commit rather than a general branch (e.g., master for mathlib), lake update does not change them (it only updates to the latest revision on the branch specified). The most streamlined process would be:

1. Change mathlib4 and cs22-lean-autograder to be @ "master"
2. Run lake +leanprover-community/mathlib4:lean-toolchain update (it will fail because mathlib's configuration is too new, but you will get the updated toolchain)
3. Copy mathlib's lean-toolchain to math2001

In shell (tested on my Windows machine):

$ elan self update
$ git clone https://github.com/hrmacbeth/math2001
$ cd math2001
$ sed -i 's/@ .*/@ "master"/' lakefile.lean  # or sed -i '' 's/... on macOS
$ lake +leanprover-community/mathlib4:lean-toolchain update
$ cp lake-packages/mathlib/lean-toolchain .
$ lake exe cache get
$ lake build # will fail because of the missing file

Note that this will still produce an "incompatible manifest version" warning on the lake update because cs22-lean-autograder's latest manifest is still on that version.

[Kevin Buzzard]

What are we supposed to do about this incompatible manifest warning? I saw it when trying and failing to update another project recently.

[Kevin Buzzard]

I've just tried the above approach on another project and it's worked fine :tada: I had not previously understood the importance of having the lakefile version of mathlib set to master. In fact this also seems to work:

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git"

That was the state of the lakefile in my student's project (which must be the default because none of my students ever touch lakefile.lean).

So in more laymany terms, the process for upgrading mathlib on a repo which depends (only) on mathlib is:

1) check your lakefile doesn't point to specific mathlib commits. If it does, lake update won't do anything (and this is correct behaviour).
2) Manually copy some stupid text file from mathlib master for some reason
3) lake update, lake exe cache get, lake build.

We can clearly still do a little better here, but this is currently the workflow for updating a math-only project which depends on mathlib (the only use case that I or 99% of my students ever care about).

Note that in Lean 3, step 2 wasn't there and step 3 didn't have as many parts.

[Kevin Buzzard]

See also users failing to do (2) (despite the fact that it's in the docs)

[Mac Malone]

Kevin Buzzard said:

In fact this also seems to work:

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git"

Yep! Lake defaults a dependency's revision to master (the Git default) unless otherwise specified. This works great for mathlib, but not, for example, std4, whose default branch is main.

[Mac Malone]

Kevin Buzzard said:

What are we supposed to do about this incompatible manifest warning? I saw it when trying and failing to update another project recently.

The ideal solutions is for the maintainer of the dependency to update their package to the new version. Good news is the warning only shows up on lake update, not a regular lake build.

[Patrick Massot]

@Mac Malone thanks for your explanations. Of course I tried that modification of the lakefile in other attempts. The trick I was missing was the next step: lake +leanprover-community/mathlib4:lean-toolchain update.

[Patrick Massot]

And that magic line isn't so magic:

math2001$ lake +leanprover-community/mathlib4:lean-toolchain update
info: downloading component 'lean'
Error(Download(HttpStatus(404)), State { next_error: None, backtrace: InternalBacktrace { backtrace: None } })
error: could not download nonexistent lean version `leanprover-community-mathlib4-lean-toolchain`
info: caused by: could not download file from 'https://github.com/leanprover-community/mathlib4/releases/expanded_assets/lean-toolchain' to '/home/pmassot/.elan/tmp/vbdgprsl_06qst0e_file'
info: caused by: http request returned an unsuccessful status code: 404

[Mac Malone]

@Patrick Massot Ah, you may have an out-of-date elan, what does elan --version return? (It should be 3.0.0). I will add elan self update to the cheat sheet.

[Patrick Massot]

Ok, elan self update removes that error.

[Patrick Massot]

But that command still ends with warning: improperly formatted manifest: incompatible manifest version `4

[Mac Malone]

@Patrick Massot Yeah. That is because cs22-lean-autograder's latest manifest is still on that version. The update still properly completes, though.

[Patrick Massot]

It seems that warning can be ignored. So let's say we are talking about a project which already requires mathlib's master in its lakefile. The process to update to the latest Lean+Mathlib is to run from the project root:

elan self update
lake +leanprover-community/mathlib4:lean-toolchain update
cp lake-packages/mathlib/lean-toolchain .
lake exe cache get

and ignore all warnings along the way, right?

[Patrick Massot]

Do you then understand why users are baffled when they read "the FRO now wants to build crates.io for Lean" instead of reading "the FRO now wants to make sure you can update Mathlib by running a single command lake update_mathlib"?

[Patrick Massot]

We simply don't understand the rationale of priorities here.

[Patrick Massot]

@Heather Macbeth since all this is already quite a bit of work I opened a PR at https://github.com/hrmacbeth/math2001/pull/3 but I didn't fix anything else. In particular the first error is Qq related, so we may need some help.

[Eric Wieser]

I don't think we need lake update_mathlib, the behavior you're asking for should just be the behavior of lake update if we implement the mathlib-agnostic https://github.com/leanprover/lake/issues/180

[Patrick Massot]

The name I made up is my effort to not get in the way of people who don't care about Mathlib. But I'd be happy to have it called lake update of course.

[Julian Berman]

That would solve the middle 2 commands but still leave the first and last, no? (I +1'ed it though)

[Mac Malone]

@Eric Wieser, I am not sure if that meets @Patrick Massot's desires (but maybe he will correct it me?). It sounds like he wants lake update_mathlib to do all of these steps. lake#180 would just eliminate the toolchain copying (not the other steps).

[Eric Wieser]

The first one also seems like a bug; but you're right about the last one; update_mathlib could be update + exe cache get

[Eric Wieser]

What does the +leanprover-community/mathlib4:lean-toolchainmean in the second line, and why is it needed?

[Mac Malone]

Eric Wieser said:

What does the +leanprover-community/mathlib4:lean-toolchainmean in the second line, and why is it needed?

It is used to ensure the lake being used is the version from mathlib's lean-toolchain.

[Patrick Massot]

Mac, I don't understand why you seem unsure about my desires. What is difficult to understand in "I want to type only one command that is short and easy to remember and then things should simply work".

[Patrick Massot]

Also I'm not talking about science fiction. leanproject upgrade-mathlib used to do that in Lean 3.

[Mac Malone]

@Patrick Massot We certainly do want to simplify the process! lake#180 is high priority (eliminating the toolchain copy) and the crates.io clone is in part designed to facilitate a general integrated Lake cache (eliminating lake exe cache get). Also, I would note that even in Rust, which is a major inspiration, updating everything still takes at least three commands:

$ rustup update
$ cargo update
$ cargo build

[Arthur Paulino]

@Patrick Massot this is one of the instances of the "Lake doing specific mathlib things" vs "Lake is the package manager of a general purpose programming language" conflict that I've mentioned once

[Arthur Paulino]

My 2c: Mathlib is free to implement a lake run update_mathlib script (and much more)

[Patrick Massot]

Mac, I'm happy to learn than leanproject was better than the rust system, but I don't why it would mean we should regress that much compared to Lean 3.

[Mac Malone]

@Patrick Massot And I am still boggled as to why mathlib doesn't just make its convenient lake one-liners via custom code in its lakefile like @Arthur Paulino suggested (and I gave an example of in mathlib4#7282).

[Patrick Massot]

Arthur I really don't see why we need a conflict here. I don't why having a general purpose programming language prevents use with mathlib to be simple.

[Ruben Van de Velde]

(I don't think leanprover updated itself either, did it?)

[Patrick Massot]

Mac, that #7282 is labelled awaiting-author.

[Patrick Massot]

Ruben, it didn't but it was also backward compatible (and it was easy to update if you had a working python setup).

[Arthur Paulino]

Patrick Massot said:

Arthur I really don't see why we need a conflict here. I don't why having a general purpose programming language prevents use with mathlib to be simple.

It's all about API design. I don't think Lake should implement specific mathlib (or any other project) things because that can backfire pretty hard.
The role of Lake in this case is to provide everything any project needs to be as autonomous as possible. Lake already allows users to implement custom scripts like the one I suggested and even custom compiled binaries (like Cache)

[Arthur Paulino]

My suggestions in these scenarios are always empowering. Mathlib can run free, without relying on Mac/Lake implementations

[Mac Malone]

Patrick Massot said:

Mac, that #7282 is labelled awaiting-author.

Yes, it was made as an example to demonstrate these kinds of features could be done on the mathlib side. I sadly have too many other things requiring my attention to devote too much time making these tools myself (when someone else could do so). As @Arthur Paulino suggested, the goal of Lake is to make these things doable on the package side and only involve changes to Lake / core when such a thing is infeasible user-side.

[Julian Berman]

Not sure if "more ideas" are what's needed but has adding a post-update hook to lake been considered (i.e. something you can define in a lakefile which it calls post update)? And then mathlib could/would presumably want to run the cache getting in it, but users would still see it as running lake update same as any other general project -- to me it does seem a bit uncomfortable if the "biggest" project in the language has a totally different UI than others (because I think mathlib would be telling anyone contributing to it to essentially never run lake update)

[Julian Berman]

(This of course again recalls the situation in Python ~15 years ago, where it was common to override distutils commands to make them do more stuff...)

[Eric Wieser]

Mac Malone said:

Eric Wieser said:

What does the +leanprover-community/mathlib4:lean-toolchainmean in the second line, and why is it needed?

It is used to ensure the lake being used is the version from mathlib's lean-toolchain.

What version would be used otherwise?

[Eric Wieser]

And are you talking about the version of mathlib before the update or after the update?

[Eric Wieser]

Because I would expect the mathlib toolchain version before the update to be the same as the current project toolchain version

[Julian Berman]

Eric I think otherwise it'd use your own default toolchain locally the one from the current lean-toolchain file (and I think it tells elan to use the remote one, it's special syntax I think Sebastian added to address precisely this kind of issue if I followed the original thread correctly)

[Mac Malone]

Eric Wieser said:

What version would be used otherwise?

Either the project's lean-toolchain (if it has one, as you surmised) or the elan's default toolchain (whatever version that may happen to point to). Thus, for instructions like this it is worth fixing the one we want to use.

And are you talking about the version of mathlib before the update or after the update?

It uses the one directly from mathlib's master branch on GitHub.

[Mac Malone]

(TL;DR: exactly what Julian said :smile: )

[Mac Malone]

Julian Berman said:

Not sure if "more ideas" are what's needed but has adding a post-update hook to lake been considered

This is a great idea that could potentially solve all this and is rather easy to implement! :tada: Would you mind making an issue for it?

[Eric Wieser]

Can lake bootstrap itself as follows?

• Looking at the dependencies it was asked to update
• Getting the newest among all the toolchains
• Re-running the new version of itself at that toolchain

[Eric Wieser]

The fact that old lake can't update to a project that uses new lake seems pretty unfortunate

[Arthur Paulino]

@Patrick Massot let me try to be explicit about why Lake being too specific about Mathlib is a bad general design decision and not just poor willingness.

Mathlib is a Lean 4 project that uses Lake as the package manager and build tool. So Mathlib depends on the API that Lake provides. If Lake starts making assumptions about specific needs of Mathlib, it's easy to imagine a situation of incompatibility: Mathlib changes while maintaining the same Lake version and then the Lake API fails due to wrong assumptions.

Here's an example: Lake currently assumes a hardcoded URL for the mathlib4 repo (lake new foo math). If that URL changes (say the community migrates away from GitHub due to some evil decision from Microsoft or something), then we have a generation of cursed Lake versions

[Julian Berman]

Mac Malone said:

Julian Berman said:

Not sure if "more ideas" are what's needed but has adding a post-update hook to lake been considered

This is a great idea that could potentially solve all this and is rather easy to implement! :tada: Would you mind making an issue for it?

Done at https://github.com/leanprover/lake/issues/185 with a tiny bit more detail

[Kyle Miller]

@Arthur Paulino I think you're responding mostly to Patrick's suggestion of "lake update_mathlib" right? His primary desire isn't for Lake to be made mathlib-specific, but rather that there is some single command (ideally lake update even) that does what's necessary to update dependencies and the toolchain. He mentions "lake update_mathlib" as an "I'd accept this alternative if somehow that's what it takes to get this."

Having Lake be a package manager of a general purpose programming language doesn't mean the basic interaction for things like updating dependencies has to be inconvenient. Just like how it's not good making something general cater to a specific project, it's also not good if every project needs to add their own custom scripts to fill in common missing user-friendliness. This I think is what Patrick is getting at.

There just seems to be some miscommunication here, and I hope I'm accurate in how I'm representing Patrick.

[Arthur Paulino]

I agree that lake update UX is strange. My impression is that it boils down to Lean 4 project versions not having explicit semantics about an order. For example, cargo update works nicely because packages use semantic versioning rather than a git hash (and cargo knows about this ordering)

[Arthur Paulino]

For example, Suppose my project depends on packages A and B. And both of them depend on C.
C has two versions: C1 and C2.
A depends on C1 and is incompatible with C2. B would work with either.
What should lake update do? How would it know that using C2 is not allowed?

[Ruben Van de Velde]

In 99.9% of cases involving mathematicians, your project does not depend on such packages

[Ruben Van de Velde]

The goal is to have a foolproof interface for people who don't paint themselves in a corner like that

[Eric Wieser]

Arthur Paulino said:

For example, Suppose my project depends on packages A and B. And both of them depend on C.
C has two versions: C1 and C2.
A depends on C1 and is incompatible with C2. B would work with either.
What should lake update do? How would it know that using C2 is not allowed?

Note that the current issues people are facing with lake update are not caused by version mismatches in dependent packages; they're caused by version mismatches in the version of lean itself, which to make matters worse is linked to the version of the package manager metadata

[Arthur Paulino]

In my experience managing Lean 4 packages, I've always set it all up so that lake update is a no-op

[Eric Wieser]

I don't see how that can possibly be the intended way to use lake

[Arthur Paulino]

It's the only way I found to avoid headaches of this kind

[Kevin Buzzard]

Patrick Massot said:

It seems that warning can be ignored. So let's say we are talking about a project which already requires mathlib's master in its lakefile. The process to update to the latest Lean+Mathlib is to run from the project root:

elan self update
lake +leanprover-community/mathlib4:lean-toolchain update
cp lake-packages/mathlib/lean-toolchain .
lake exe cache get

and ignore all warnings along the way, right?

This cp lake-packages/mathlib/lean-toolchain . might fail if your local version of mathlib is not up to date with origin/master, right? When I was experimenting earlier I pulled mathlib master from origin locally.

Or is this what lake +leanprover-community/mathlib4:lean-toolchain update does? I have no understanding of that line.

[Eric Wieser]

+leanprover-community/mathlib4:lean-toolchain means "before you run lake update, let me manually tell you which version of lake you will need in order to do the update"

[Mac Malone]

Julian Berman said:

Done at https://github.com/leanprover/lake/issues/185 with a tiny bit more detail

And a simple implementation is now at lean4#2603. :grinning_face_with_smiling_eyes:

[Eric Wieser]

I think there are three pieces and they're all currently separate:

1. Update the dependent packages in a project (the stuff in lake-packages). I think this all just works now, but was painful before
2. Update the lean-toolchain of the project to match the things that were updated (lake#180)
3. Using a suitable lean-toolchain to run lake itself such that it can actually understand how to do step 1

[Kevin Buzzard]

Arthur Paulino said:

In my experience managing Lean 4 packages, I've always set it all up so that lake update is a no-op

Arthur you are a very savvy Lean user. What Patrick and I are desperate to get is something which just works for all of e.g. my summer project users, every single one of which (apart from one) just has a default lakefile.lean which they never opened and have no understanding of, and which just has one dependency which is mathlib master. What we're trying to stress is that in practice right now quite possibly the majority of Lean projects which exist currently actually do look like this, and even if Lean gets popular in other areas it will still be the case that for years and years any mathematics student doing a summer project or an MSc project or a BSc project or any other project will 99 times out of 100 be in exactly the same situation: one project, depends on mathlib, depends on nothing else. Support for updating these project which does not involve "now copy a text file from mathlib which you don't even have installed" or "now run curl on the command line which curl doesn't work on and you have no idea why" is what those of us actively teaching in the mathematics community would really like to have. Copying a text file is much harder than you think. Let me stress this. I work with people who have no idea what a directory is.

[Arthur Paulino]

I'm not claiming that you should do the same as me. I'm just expressing a pain point which made me avoid lake update altogether. Or at least make it harmless.
I'm not a fan of the manual cp workaround either

[Mac Malone]

Kevin Buzzard said:

Copying a text file is much harder than you think. Let me stress this. I work with people who have no idea what a directory is.

Now this suggests to me that the Lake CLI might not be the best place to simplify the process then. For such users, I imagine handling this in the IDE (i.e., via the VSCode extension) would be the most preferable place. A topic which I believe has already broached in a different thread (and some such features Marc suggested could already be coming soon).

[Kevin Buzzard]

Yeah I would love to get mathematician users away from the command line completely! :-) But given that we're stuck with it for now I'd like them to have to type as little as possible :-)

[Mario Carneiro]

and in particular, not for certain things they type to make it much harder to undo with the right thing

[Adam Topaz]

While I generally agree that it would be nice to make the UX as nice as possible for mathematicians who don't want to use a command line, at some point I think we need to expect people to know how to use a computer.

[Mario Carneiro]

in my experience, there is always a really short list of things you have to type to get a working setup. It's just that what precisely that is seems to change every once in a while, and you have to add more things to it depending on how much you trust your configuration (i.e. are we needing to reinstall lake here? elan? windows?)

[Kevin Buzzard]

You don't need to know about concepts such as directories to use a computer any more. This is a relatively recent development.

[Adam Topaz]

Yeah, I guess the definition of "computer" has changed. Personally I think we should invest more into online solutions that don't require any installation whatsoever, since people who don't know what a directory is are probably most comfortable in a browser anyway

[Eric Wieser]

Especially based on my LftCM experience where local installation was broken for many people due to their antivirus trying to protect them, which I don't think we can do much about

[Patrick Massot]

@Mac Malone, thanks a lot for trying to improve on this. I'm sorry I disappeared from the discussion, I'm very busy since the end of this morning.

[Mario Carneiro]

Does lake have a way to turn off the post-update hook? This is causing major problems for mathport, which now frequently runs out of space in CI: https://github.com/leanprover-community/mathport/actions/workflows/build.yml

[Mario Carneiro]

@Mac Malone

[Mac Malone]

@Mario Carneiro Sadly, no. I am little confused as to what is doing wrong. It was my understanding that mathlib always needed a fetched cache? One fix would be to add an fetchCacheOnUpdate config flag to mathlib.

[Mario Carneiro]

I am still investigating, but I think the mathport CI is using lake update to update the manifest without building (and hence it has no need for oleans)

[Mario Carneiro]

The lean-toolchain copy is good, but the lake exe cache get is unwanted at update time

[Mario Carneiro]

that should be a pre-build step, not a post-update step

[Mario Carneiro]

Yes, here's the update script: https://github.com/leanprover-community/lean3port/blob/master/update.sh

Notice that it runs lake update but not lake build

[Mario Carneiro]

CI runs out of space while running it

[Mario Carneiro]

I'm wondering whether we should just have a custom version of lake update hacked together with jq instead, because it is difficult to keep these scripts working if lake update does arbitrary things

[Mac Malone]

@Mario Carneiro Pre-install and post-install hooks are a very common property of package managers, so yes I think you should expect lake update to do arbitrary things.

[Mac Malone]

Lake could have a configuration option to turn them off, though.

[Mario Carneiro]

How do I just update though?

[Mac Malone]

Mario Carneiro said:

The lean-toolchain copy is good, but the lake exe cache get is unwanted at update time

One of the main motivations of the post-update hook was to call lake exe cache get after lake update and such was specifically requested higher up in this same thread.

[Mario Carneiro]

only lake knows how to do that properly

[Mario Carneiro]

I'm aware of that, but the appropriateness of this is unsurprisingly context dependent

[Mario Carneiro]

actually, could you point to where someone asked for lake update to run lake exe cache get? I don't see it from a cursory reading

[Mac Malone]

@Mario Carneiro In Julian's original proposal, he did suggest named post-update hooks and a --without-hook option to solve this, which may appeal to you. I felt that starting with the simplest approach first and building up from there was best for this kind of very customizable feature.

[Mario Carneiro]

I think an important part of having these hooks is being able to disable them

[Mac Malone]

There is:

Eric Wieser said:

The first one also seems like a bug; but you're right about the last one; update_mathlib could be update + exe cache get

[Mario Carneiro]

because otherwise you have removed the ability to do lake update

[Mario Carneiro]

That is not asking update to do lake exe cache get

[Mario Carneiro]

it's asking update_mathlib to do so

[Mac Malone]

And there is:

Patrick Massot said:

It seems that warning can be ignored. So let's say we are talking about a project which already requires mathlib's master in its lakefile. The process to update to the latest Lean+Mathlib is to run from the project root:

elan self update
lake +leanprover-community/mathlib4:lean-toolchain update
cp lake-packages/mathlib/lean-toolchain .
lake exe cache get

and ignore all warnings along the way, right?

Patrick Massot said:

Do you then understand why users are baffled when they read "the FRO now wants to build crates.io for Lean" instead of reading "the FRO now wants to make sure you can update Mathlib by running a single command lake update_mathlib"?

Which struck me as a desire for an all-in-one as well.

[Mac Malone]

The update_mathlib command then became the post-update hook with this suggestion:

Julian Berman said:

Not sure if "more ideas" are what's needed but has adding a post-update hook to lake been considered (i.e. something you can define in a lakefile which it calls post update)? And then mathlib could/would presumably want to run the cache getting in it, but users would still see it as running lake update same as any other general project -- to me it does seem a bit uncomfortable if the "biggest" project in the language has a totally different UI than others (because I think mathlib would be telling anyone contributing to it to essentially never run lake update)

[Mario Carneiro]

In any case, this is a critical issue which I would like to get into the next RC. Should I write up a PR for --without-hooks support in lake update?

[Mario Carneiro]

Hopefully cache can be better integrated into build such that it can be moved from post-update to pre-build, and then this won't be an issue (for mathlib, at least)

[Mario Carneiro]

but keeping them as separate steps is also not unreasonable; you still have to run lake exe cache get when switching branches

[Mario Carneiro]

removing the mathlib post-update hook would also solve this issue

[Patrick Massot]

A compromise could be to have lake update not getting cache but lake build and, much more importantly, opening the project in VSCode would get the cache (with a message explaining why the user need to wait in the VSCode case).

[Mario Carneiro]

#8448 makes lake update -KnoCacheOnUpdate work to avoid the lake exe cache get step

[Mario Carneiro]

@Patrick Massot I'm not sure I would even call that a compromise, that's the intended goal state

[Patrick Massot]

No it isn't. After the lake update commands succeeds I expect my project to be usable. With that plan it is not yet usable. So I need to wait for lake update then open VSCode and wait again instead of waiting only once.

[Patrick Massot]

In case you run lake build there is no difference. The waiting time is distributed differently but there are not more oscillation between acting and waiting.

[Mario Carneiro]

Actually #8448 doesn't work, apparently the -K flags are not honored? @Mac Malone

[Joachim Breitner]

Did you delete lakefile.olean?

[Mario Carneiro]

FFFF

[Mario Carneiro]

..ahem

[Mario Carneiro]

but also no that doesn't help

[Mario Carneiro]

Patrick Massot said:

No it isn't. After the lake update commands succeeds I expect my project to be usable. With that plan it is not yet usable. So I need to wait for lake update then open VSCode and wait again instead of waiting only once.

After lake update your project will still not be usable, because your project hasn't been compiled yet, nor any other projects besides mathlib

[Mario Carneiro]

you actually do want to run lake build, we just need to make this command not unusable for mathlib-depending projects

[Mario Carneiro]

Using the with syntax in require works to set -K options but I guess there is no other way to pass -K options in the top level project to mathlib

[Mario Carneiro]

I think I will just use environment variables instead of -K options in #8448

[Mac Malone]

Mario Carneiro said:

Using the with syntax in require works to set -K options but I guess there is no other way to pass -K options in the top level project to mathlib

Yeah, configuration options are not currently inherited by upstream packages.

[Mac Malone]

(I have been thinking about changing this.)

[Johan Commelin]

❯ lake update
updating lake-packages/mathlib to revision 81e04e3518080a288dfa9a490c048e08ab890cb0
error: ./lake-packages/mathlib/lakefile.lean:28:2: error: 'weakLeanArgs' is not a field of structure 'Lake.PackageConfig'
error: ./lake-packages/mathlib/lakefile.lean:68:2: error: 'srcDir' is not a field of structure 'Lake.LeanExeConfig'
error: ./lake-packages/mathlib/lakefile.lean:84:0: error: expected 'abbrev', 'add_decl_doc', 'axiom', 'builtin_initialize', 'class', 'custom_data', 'declare_opaque_type', 'declare_simp_like_tactic', 'declare_syntax_cat', 'def',
'elab', 'elab_rules', 'example', 'extern_lib', 'family_def', 'inductive', 'infix', 'infixl', 'infixr', 'initialize', 'instance', 'lean_exe', 'lean_lib', 'library_data', 'library_facet', 'macro', 'macro_rules', 'module_data', 'module_facet', 'notation', 'opaque', 'package', 'package_data', 'package_facet', 'postfix', 'prefix', 'register_builtin_option', 'register_option', 'script', 'structure', 'syntax', 'target', 'target_data', 'theorem' or 'unif_hint'
error: ./lake-packages/mathlib/lakefile.lean: package configuration has errors

Did I do something stupid?

[Ruben Van de Velde]

Did you update the lean toolchain before that?

[Johan Commelin]

Nope

[Johan Commelin]

I haven't updated a lean project in 6 months or so. What is the sequence of incantations that I should utter?

[Johan Commelin]

lake -h update didn't instruct me to do anything else beforehand

[Ruben Van de Velde]

https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency#updating-mathlib4 probably

[Johan Commelin]

Aha! That seems to do something different

[Johan Commelin]

Ok, now I need to fix the build. But at least the update seems to work