Dependabot support for Lean - call for co-maintainers

Stream: ecosystem infrastructure

[Jesse Alama]

Hi everyone,

I've been working on adding Lean 4 support to Dependabot, GitHub's automated dependency update service. The implementation is ready and a PR is open:

https://github.com/dependabot/dependabot-core/pull/13787

What this would enable:

• Automatic PRs to update your lean-toolchain file when new Lean versions are released
• Keep Lean projects up to date with minimal manual effort
• Works with GitHub's security and version update features

Current scope:
This initial version focuses on Lean toolchain updates only. It reads lean-toolchain and checks for new Lean releases. It does not (yet) handle Mathlib, CSLib, or other Lake dependencies — lake-manifest.json, lakefile.toml, and lakefile.lean aren't consulted in this version.

What's needed to move forward:
The Dependabot team supports a lot of languages and ecosystems, and they've found that community-maintained ecosystems work best when there's genuine community interest. They're (understandably) trying to avoid adding support for an ecosystem where there's only tepid interest, or where a single maintainer might disappear and leave them holding the bag. They currently have 3 community-maintained ecosystems and are asking for some community buy-in before merging this PR.

What I'm looking for:
I'm happy to take the lead here and handle any bugs or maintenance tasks that come up from upstream. What I'm really looking for is a second pair of eyes — someone to help review changes and sanity-check things occasionally.

Note that Dependabot is written in Ruby, so familiarity with Ruby would be helpful (though the Lean-specific logic is fairly straightforward).

If you're interested in helping out, or just want to express interest in having Dependabot support for Lean, please comment on the PR or reply here. Even just a "+1" on the PR helps show the Dependabot team that there's community interest.

Thanks!

[Kim Morrison]

I do like the idea of having Dependabot understand Lean4.

But isn't dependabot making suggestions to update the lean-toolchain, without also checking what needs to be done with lake dependencies, just going to cause pain to users?

I would be happy if the logic just said "if there are any library dependencies at all, I don't know what to do, so will be silent".

[Mac Malone]

I also quite like the idea of Dependabot support for Lean4 and agree with Kim's comments on the current PR.

As the maintainer of Lake and someone with signfiicant past experience with Ruby, this is something of great interest to me. However, I likely cannot give this a proper look until the new year. I suspect the timing may also be a general problem with gathering support for this now (e.g., the review of the PR was similarly delayed).

[Tobias Grosser]

Nice. I also like this idea quite a lot. We are using home-grown scripts to update to lean-nightlies. Dependabot seems like a great idea. Is there a way to try the dependabot script on our project before it is merged? I would be happy to give it a try.

[François G. Dorais]

I really need this and I'm willing to help.

[Jesse Alama]

Thanks for the feedback! It sounds like I'm not the only one who might benefit from this. I wonder if we might want to migrate the functionality contained in lean-update to Dependabot.

I'd love it if there could be something like npm outdated for Lean. In the Node.js world, this is a tool that fetches the state of one's dependencies and tells you what could be updated if one were to do npm update, without taking any further action. As far as I know, there's currently no such thing. Maybe we could add some equivalent functionality to lake update via, say, a --dry-run flag? Or we could add a new outdated command to lake that with a bit more functionality.

[Jesse Alama]

I've pinged the maintainers of the lean-update GitHub Action to get some more feedback.

[Jesse Alama]

Quick update: after playing around with lean-update, I was inspired to extend my Dependabot PR , which only handled lean-toolchain, to handle lake-manifest.json, too. Thus, Dependabot can track and update Lake package dependencies, not just Lean compiler version updates.

PR is here: https://github.com/dependabot/dependabot-core/pull/13787

[Asei Inoue]

@Jesse Alama Hi. I’m the maintainer of lean-update. First, thank you for letting me know about this. I’m glad to hear that someone else is interested in automatically updating in Lean projects. I hope your project goes well.

[Asei Inoue]

@Jesse Alama

It seems that you are looking for someone to become a maintainer of Lean Dependabot. Unfortunately, I can’t help with that. I’m currently starting a large-scale refactor of lean-update, and I’m planning to work on adding new features to it. Because of this, I don’t have the time. And I don’t think I’m qualified since I don’t have any knowledge of Ruby.

[Asei Inoue]

@Jesse Alama

If lean-update were to become unnecessary in the future thanks to Lean Dependabot, that would be welcome news for me as well. However, I suspect there are some differences in what can be done with a custome GitHub Action versus Dependabot, and I intend to continue maintaining lean-update.

[Asei Inoue]

By the way, to achieve something like npm outdated in Lean, Im wondering whether it would be sufficient to pass -wfail as an argument to lake build. What do you think?

[Jesse Alama]

Asei Inoue said:

Jesse Alama

It seems that you are looking for someone to become a maintainer of Lean Dependabot. Unfortunately, I can’t help with that. I’m currently starting a large-scale refactor of lean-update, and I’m planning to work on adding new features to it. Because of this, I don’t have the time. And I don’t think I’m qualified since I don’t have any knowledge of Ruby.

Looking forward to seeing the new lean-update work! I wonder if, given lean-update, something like Dependabot might be redundant. I agree that a custom GitHub Action gives one more freedom to add Lean-specific functionality and may well be a better solution.

@Tobias Grosser Could any of your custom scripts could be at least partially handled by the lean-update action?

[Asei Inoue]

At the moment, the lean-update action does not support updating to nightly versions at all. I was not aware that there was a need for such functionality. I have the desire to support it.

[Tobias Grosser]

Nice, that would be cool indeed.

[Tobias Grosser]

You can see the use of our scripts in https://github.com/opencompl/veir. I would be happy to beta-test lean-update.