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.