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.

[Shreyas Srinivas]

@Mario Carneiro : My PR is still in the queue. Just wanted to remind you. It's a CI action that does regular toolchain updates

[Mario Carneiro]

I'm unsure about the change to the require Qq line from "v4.17.0" to "stable". I would like a second opinion on this from someone with dependency management expertise, cc: @Kim Morrison, is any other project using Qq as a dependency?

[Kim Morrison]

I think this should be okay. The relevant chunk of release_repos.yml, which determines what I do during releasing, says:

  - name: quote4
    url: https://github.com/leanprover-community/quote4
    toolchain-tag: true
    stable-branch: true
    branch: master
    dependencies: []

which in particular means the stable branch is kept up to date.

[Mario Carneiro]

well my question is whether it is better to use stable vs updating it along with the lean version

[Mario Carneiro]

I feel like using stable is more vague about which version is being referenced

[Kim Morrison]

My "promise" is that stable will be updated at approximately the same time Qq is updated and releases a new toolchain tag.

[Kim Morrison]

That's true.

[Kim Morrison]

The alternatives are essentially master, stable, or an explicit toolchain tag.

[Kim Morrison]

I'd prefer not the later, as that then requires human attention during updates, which won't happen.

[Mario Carneiro]

fair enough

[Shreyas Srinivas]

I changed the source of the lean-update action as requested by Kim

[Shreyas Srinivas]

I’ll now add the CI script to build the project in every PR

[Shreyas Srinivas]

The last update ran into trouble. Some manual intervention is needed : https://github.com/leanprover-community/iris-lean/issues/38

[Shreyas Srinivas]

Here's the PR for adding build CI

[Shreyas Srinivas]

https://github.com/leanprover-community/iris-lean/pull/40

[Shreyas Srinivas]

so basically all the errors in iris-lean#38 are about the missing field cofe

[Mario Carneiro]

there were a bunch more errors after that, they have to do with structure instances not allowing you to infer fields

[Shreyas Srinivas]

the build CI now uses lean-action

[Shreyas Srinivas]

The rest of the stuff is to check when the CI should run, add labels and remove labels

[Shreyas Srinivas]

lean-action doesn't provide that for us

[Mario Carneiro]

what are the paths for?

[Mario Carneiro]

the main branch is master in this repo

[Shreyas Srinivas]

It says "if these paths change"

[Shreyas Srinivas]

Run the CI

[Mario Carneiro]

but it should always run?

[Shreyas Srinivas]

you don't want it to run if you make changes to README.md

[Shreyas Srinivas]

or something similarly trivial

[Mario Carneiro]

I think I do

[Mario Carneiro]

or rather I don't want to be responsible for missing some relevant file in that list

[Mario Carneiro]

especially when the build is not so expensive

[Shreyas Srinivas]

okay then those paths can be deleted

[Mario Carneiro]

the labels too, I would prefer if they were added to lean-action

[Mario Carneiro]

I want the CI to look like https://github.com/leanprover/lean-action?tab=readme-ov-file#quick-setup

[Shreyas Srinivas]

That's literally just adding the awaiting-CI label to PRs and deleting it

[Mario Carneiro]

I can see that

[Mario Carneiro]

but iris-lean is a standard issue lean repo, it should not need custom config

[Shreyas Srinivas]

Labels are usually project specific, so I wouldn't expect lean-action to take on the task of manipulating repository PR labels

[Mario Carneiro]

if you are suggesting that every standard issue repo should be using awaiting CI tags, then that stuff should be moved to lean-action

[Mario Carneiro]

under an option

[Shreyas Srinivas]

It is simply convenient for us to know when the CI is running on a PR

[Shreyas Srinivas]

and it will come in handy when we decide to automate moving things to a review queue. Basically the CI would then check for this label and kick out PRs which have an awaiting-CI label

[Mario Carneiro]

I usually look at the :orange_circle: for that :rolling_eyes:

[Mario Carneiro]

it's better integrated with GHA to use this too

[Mario Carneiro]

I don't want iris-lean to be using experimental CI. It should use the standard issue stuff. Please experiment on projects that have more complex requirements

[Shreyas Srinivas]

Okay, in that case I have just pushed the standard stuff

[Shreyas Srinivas]

The only edit to the lean-action provided template is the name of the action

[Shreyas Srinivas]

But fwiw, it is not that experimental. We already did all the experimenting on equational theories

[Mario Carneiro]

if it's not experimental, then get it added to the standard issue template

[Shreyas Srinivas]

I think it's already part of the leanproject template. Neither Pietro nor I have pushed it further upstream for non-technical reasons (time basically)

[Mario Carneiro]

okay, that's fine. It can come to iris-lean once it is standard practice, there is no rush

[Mario Carneiro]

having green checkmarks pronto is good, the other stuff can wait

[Shreyas Srinivas]

Currently we are running the default config of lean-action. I don't see lean4checker running so I guess that needs some extra helpings of configuration

[Mario Carneiro]

I'm fine with setting options on the action to enable lean4checker

[Mario Carneiro]

although now that I come to think about it actually I don't think it's necessary, since iris-lean is a library and not really an endpoint project