Update and switch to lakefile.toml

Stream: iris-lean

[Shreyas Srinivas]

As the topic says, I'd like to try bringing iris-lean upto toolchain v4.17.0 and switch the lakefile.lean with lakefile.toml. Seems easier to do it earlier in a project

[Shreyas Srinivas]

Here's a PR : https://github.com/leanprover-community/iris-lean/pull/16

[Mario Carneiro]

As a general policy matter: Iris-lean works on the latest stable release, so updates to bump the lean version are usually rubber stamped. If someone could figure out how to set it up to use lean-action to do automatic version bumps I would be grateful

[Shreyas Srinivas]

There was just one array API change this time

[Shreyas Srinivas]

I think one source of confusion for me is that I am usually updating math repositories where pinning mathlib’s branch to stable is sufficient

[Shreyas Srinivas]

Then running lake update always jumps to the latest stable toolchain

[Shreyas Srinivas]

I am not sure how to get that behaviour in non math projects

[Shreyas Srinivas]

lean-action has something for regular updates. We used it in equational. But that’s a math project

[Shreyas Srinivas]

Here, I had to explicitly change lean-toolchain before running lake update to make it work

[Shreyas Srinivas]

I wonder if putting leanprover/lean4:stable in lean-toolchain will do the trick.

[Mario Carneiro]

no, changing the lean-toolchain file is exactly what you want

[Mario Carneiro]

but I thought there was a lean action bot that would do it for you

[Shreyas Srinivas]

There is a lean-action bot for checking a math project's toolchain and updating the project according to that

[Shreyas Srinivas]

but lake update behaves differently for math and other projects

[Shreyas Srinivas]

It won't, for example, fix the Qq dependency in iris which I had to manually update

[Shreyas Srinivas]

Also, the following lakefile.toml won't work because lake will complain that it is getting two different version of lake, so I can't keep the Qq dependency automatically up to date

name = "iris"
srcDir = "./src/"
defaultTargets = ["Iris"]

[[require]]
name = "Qq"
scope = "leanprover-community"
version = "git#stable"

[[lean_lib]]
name = "Iris"

[Shreyas Srinivas]

That's ofc because the stable in the dependency is the name of a github branch and the lean-toolchain inside reads leanprover/lean4:v4.17.0

[Shreyas Srinivas]

Same error if I leave the Qq dependency version at git#v4.17.0

[Shreyas Srinivas]

stable doesn't resolve to anything before lake checks for multiple toolchains

[Shreyas Srinivas]

which ... sounds like a bug to me

[Shreyas Srinivas]

It just performs a text comparison and throws

warning: toolchain not updated; multiple toolchain candidates:
  leanprover/lean4:stable
    from iris
  leanprover/lean4:v4.17.0
    from Qq

[Mario Carneiro]

why is anything asking for lean4:stable?

[Mario Carneiro]

you should never use that toolchain

[Shreyas Srinivas]

I experimented locally with changing the lean-toolchain to stable

[Shreyas Srinivas]

so that lake update automatically updates to the latest stable toolchain

[Shreyas Srinivas]

without tinkering with lean-toolchain

[Shreyas Srinivas]

based on a separate experiment below:

$ elan toolchain install leanprover/lean4:stable
error: 'leanprover/lean4:v4.17.0' is already installed

I conclude that lean4:stable is treated by elan as the latest stable toolchain

[Mario Carneiro]

yes which makes it a bad choice for usage in the project

[Mario Carneiro]

it's a reproducibility hazard, as it will not resolve to the same thing next month

[Mario Carneiro]

this is general advice for any library - if you put it on github it should not be using lean4:stable

[Mario Carneiro]

the update script should be aware that we want to update to the latest stable, but regular builds should use the lean version in the lean-toolchain file and that should be a stable identifier over time

[Shreyas Srinivas]

So the update action is not in lean-action
It is here :https://github.com/Seasawher/lean-update/

[Shreyas Srinivas]

Under the hood it uses the following js : https://github.com/Seasawher/lean-update/blob/main/scripts/getLatest.js

[Shreyas Srinivas]

This is mathlib independent. But it will almost certainly break because after replacing the toolchain, the action tries to simply run lake update.

[Shreyas Srinivas]

We also need to update all our dependencies

[Shreyas Srinivas]

This should work : https://github.com/leanprover-community/iris-lean/pull/19
Only admins and maintainers can test this CI action stuff afaik. So I can't test this directly. But the scripts are borrowed from equational_theories and simply call the lean-update action linked above. I changed the Qq dependency to point to stable so that we don't have to manually update its branch inside lakefile.toml

[Shreyas Srinivas]

@Mario Carneiro : The update CI PR is ready to be merged. We can similarly borrow other parts of the CI. Maybe even setup docs.