manifest out of date

Stream: FLT

[Ruben Van de Velde]

I'm getting an odd lake warning I haven't seen before:

warning: manifest out of date: git revision of dependency 'mathlib' changed; use `lake update mathlib` to update it

[Ruben Van de Velde]

Doesn't seem to actually get in the way of anything

[Yaël Dillies]

This is because lean-toolchain in FLT doesn't agree with the lean-toolchainof the version of mathlib that lake update mathlib would bump FLT to

[Yaël Dillies]

The only way I know to get rid of it is to keep the rev = v4.19.0 line in the lakefile, rather than removing it once the bump is done locally

[Ruben Van de Velde]

Really? Everything seems to be on leanprover/lean4:v4.20.0-rc5

[Kevin Buzzard]

Yes I specifically bumped FLT to 20-rc5 in an attempt to get rid of this warning (and it didn't).

[Yaël Dillies]

Hmm then I am confused. Maybe lake now expects us to pin the commit too? As in rev = commithash

[Kevin Buzzard]

I'm sorry I'm so clueless about these things (I guess I'm picking stuff up as I go). Variables I don't understand are "inputRev" in lake-manifest.json (am I supposed to edit this manually?) and the various incantations that one can add to the lakefile.toml e.g. rev (not to be confused with "rev" in the json)

[Kevin Buzzard]

If I lake update mathlib then the diff in the json is

-   "rev": "4e685d14db58b1ab29024bb0761902a3615f3f14",
+   "rev": "33308ffdc0dc62f1437e76c5ce0857f52b7b3bfa",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.20.0-rc5",
+   "inputRev": null,

and the warning goes away (at least for now -- will it come back again if a PR to mathlib is merged?)

[Ruben Van de Velde]

Oh, did someone put inputRev in the lake manifest without putting it in the toml? That sounds plausible

[Kevin Buzzard]

Aah yes, we did do that.

So lemme get this straight. Are there two kinds of bumps?

1) mathlib does a lean version bump to lean v4.37; we then can, if we want, (and we should, esp if it's stable), choose to bump to the commit of mathlib tagged lean-v4.37, tag this FLT commit lean-4v.37 ourselves, so we're making an implicit promise that we're 100% compatible with everything else tagged lean-4v.37, and in this situation we add inputrev: "v4.37" to the json and also rev = [mathlib commit number for tag v4.37] in the toml

2) mathlib merges a theorem I want so I just decide to bump of my own accord, then I delete the rev from the toml if it's there, and make sure it says "inputrev": null in the json?

[Ruben Van de Velde]

What I've been doing for (1) is to add rev = "v4.17.0" to the toml, but then not commit that, and also not commit the change from null to "v4.17.0" in the json - but it's easy to miss that

[Kevin Buzzard]

Do you mean "what I've been doing for (2) is..."?

[Ruben Van de Velde]

No, for the bump to stable, so I end up on the v4.X.0 commit without leaving a reference to the tag in the toml

[Kevin Buzzard]

Oh so there are different systems for bump to stable and bump to rc?? Or do you mean "bump to mathlib lean-toolchain change" in general?

[Kim Morrison]

I'm confused why anyone is touching inputRev.

Just set the rev field in the toml to v4.20.0-rc5 (notice no "lean" prefix, @Kevin Buzzard), then run lake update (which will hopefully change your lean-toolchain to the toolchain Mathlib is using, or do this manually if that doesn't happen).

[Ruben Van de Velde]

The thing is - if you leave the rev key in the toml, then you need to remove it again to update mathlib to latest master (notably if you have automation to bump for you). So I add it when updating to a stable tag, but I don't commit that change, and leave inputRev as null

[Kevin Buzzard]

I am still unclear about whether there are two different algorithms for the two different kinds of bumps which I am half-convinced exist: bumps because I want a mathlib commit and bumps because reservoir or whatever wants a tagged commit saying "guaranteed to work with the v4.37 tag of mathlib".

[Ruben Van de Velde]

For the stable bump, you want to get the exact tagged revision of mathlib, so that acts as a synchronisation point for the ecosystem

[Kim Morrison]

It's not really clear to me that there is practical value in having everyone synchronize exactly. I think merely tagging the first commit of FLT when it was on the v4.X.Y toolchain would suffice.

Later we will have better automatic methods to do things like this, for now make your life easy!

[Ruben Van de Velde]

Hm, I don't see the point in synchronising if you don't do it exactly

[Kim Morrison]

Is there anyone depending on FLT + another downstream-of-Mathlib project? Hopefully there will be one day, but let's not make Kevin's life harder than it needs to be in the meantime.

[Yaël Dillies]

Kim, I don't understand what you are saying. inputRev is touched for us by lake update mathlib, and this is what's causing the warnings

[Yaël Dillies]

Kim Morrison said:

Is there anyone depending on FLT + another downstream-of-Mathlib project? Hopefully there will be one day, but let's not make Kevin's life harder than it needs to be in the meantime.

I wouldn't be surprised if that's the case, actually. A lot of AI companies are trying to automatically fill in sorries from various various projects in the ecosystem

[Ruben Van de Velde]

There's a bit of a chicken and egg too - if there's no compatible revisions, it's going to be hard to create such a project

[Kim Morrison]

I'm confused because I have never even noticed an inputRev field, because lake-manifest.json is not for human consumption. Never edit it by hand, never even read it! If there's a conflict nuke it and regenerate, and if that's not working ... #xy.

[Kim Morrison]

Ruben Van de Velde said:

There's a bit of a chicken and egg too - if there's no compatible revisions, it's going to be hard to create such a project

Agreed. Just make sure whatever workflows you set up here are not occupying Kevin's time when he's mean to be creating sorries for people. :-)

[Kevin Buzzard]

I am happy to bump often. We have a culture of bumping a lot in FLT because I remember what happened in perfectoid. We're currently on mathlib from 5 days ago. But usually I bump either because (a) I want a specific upstreamed commit which just landed in mathlib or (b) a bot opens an issue such as FLT#471 saying "you might want to consider updating because the naive algorithm just failed" (typically with errors of the form "this declaration already exists").

Auto-bumping to a new commit is very quick; the only hold-up is that it takes "two passes", one to make the trivial bump PR and then one an hour later once it's passed the interminable CI process which involves building all of the mathlib docs (it could be remarked that I literally never look at those docs or even the FLT docs, and I don't know anyone who does look at them, but they might). Manual bumping must be done manually but I don't mind doing that, I feel like mathlib itself is doing a good job of making sure that core changes aren't catastrophic, and this project is "more of the same" at the end of the day.

Anyway, the bottom line is that right now when I buid mathlib I get a "manifest out of date" warning despite having reviewed and merged the bump PR so I made a mistake. Is the mistake "don't ever have "inputRev": "v4.20.0-rc5", in lake-manifest.json"? Right now people have talked a lot on this thread but I still don't really feel I'm any closer to understanding the actual workflow.

Making a PR right now.

[Kevin Buzzard]

FLT#496

[Pietro Monticone]

I wasn't able to reproduce this warning:

warning: manifest out of date: git revision of dependency 'mathlib' changed; use `lake update mathlib` to update it

I have just tested the usual workflow in FLT by

1. Setting the rev = "v4.X" in the lakefile.toml file
2. Running lake update and getting the correct "inputRev": "v4.20.0-rc5" in the lake-manifest.json
3. Removing the rev = "v4.X" in the lakefile.toml file
4. Running lake update and getting the correct "inputRev": null in the lake-manifest.json

I'm not really sure there is any issue here, but I might have misunderstood something.

[Kevin Buzzard]

I merged FLT#497 which fixed the manifest problem. If you go back to a pre-497 commit you should be able to see the warning.

[Kevin Buzzard]

For me the usual workflow was "don't ever touch the toml, just type lake update"

[Pietro Monticone]

I virtually want back to a pre-497 just by setting the rev = "v4.20.0-rc5" in the lakefile.toml file and running lake update, right?

[Pietro Monticone]

The point is that I've never found necessary to run lake update mathlib so I'm asking if I'm doing something wrong.

[Yaël Dillies]

Pietro Monticone said:

I have just tested the usual workflow in FLT by

1. Setting the rev = "v4.X" in the lakefile.toml file
2. Running lake update and getting the correct "inputRev": "v4.20.0-rc5" in the lake-manifest.json
3. Removing the rev = "v4.X" in the lakefile.toml file
4. Running lake update and getting the correct "inputRev": null in the lake-manifest.json

The warning appears before you run step 4. Also I run lake update mathlib instead of lake update, but I doubt that changes anything

[Kevin Buzzard]

I didn't know that this was the workflow, when I've bumped because I wanted a commit, I've just typed either lake update or lake update mathlib randomly.

[Pietro Monticone]

@Yaël Dillies It doesn't seem to appear locally...

EDIT: Ok, now I see it. Sorry.

[Pietro Monticone]

Kevin Buzzard said:

I didn't know that this was the workflow, when I've bumped because I wanted a commit, I've just typed either lake update or lake update mathlib randomly.

I don't think lake update mathlib is ever needed in this case, but I can't be 100% sure.

[Pietro Monticone]

Kevin Buzzard said:

I didn't know that this was the workflow, when I've bumped because I wanted a commit, I've just typed either lake update or lake update mathlib randomly.

That is perfectly fine if you know that the toolchain isn't going to change when you run lake update (like in the latest bump FLT#497).

[Pietro Monticone]

In summary, the workflow should simply be: check whether a new version of lean-toolchain is available; If yes (e.g., v4.X), update the rev field in the lakefile.toml file to rev = "v4.X" and run lake update; else remove the rev field in the lakefile.toml file and run lake update.

The warning

warning: manifest out of date: git revision of dependency 'mathlib' changed; use `lake update mathlib` to update it

is exactly what you want in case the lakefile.toml doesn't specify a Mathlib rev (i.e. assuming master, I suppose) and you run lake build.

[Yaël Dillies]

So what you're saying is that bumps need to update the rev field?

[Pietro Monticone]

Yes.