Add Lean 4 ecosystem support

[jessealama]

What are you trying to accomplish?

Adds Dependabot support for the Lean 4 ecosystem, including:

1. Lean toolchain updates via lean-toolchain file
2. Lake package updates via lake-manifest.json (Lean's package manager lockfile)

Closes #13786

What's included?

Lean toolchain support:

• lean-toolchain is analogous to rust-toolchain.toml or .ruby-version—a single-line file specifying the compiler/language version
• Format: leanprover/lean4:v{version} (e.g., leanprover/lean4:v4.26.0)
• Fetches latest versions from GitHub releases at leanprover/lean4
• Handles release candidates (e.g., 4.27.0-rc1)

Lake package manager support:

• lake-manifest.json is analogous to Cargo.lock or package-lock.json—a lockfile tracking resolved dependency versions
• Lake packages are git-based (similar to git submodules), with each package pinned to a commit SHA
• Parses the manifest to extract package dependencies with their source URLs and branches
• Checks for updates using GitCommitChecker (finds newer commits on tracked branches)
• Updates package commit SHAs in the manifest
• Native helpers wrapping lake update for dependency resolution
• Dockerfile installs elan (Lean's toolchain manager, similar to rustup or nvm)

Anything you want to highlight for special attention from reviewers?

The toolchain implementation follows the rust_toolchain pattern. The Lake package support follows the git_submodules pattern for git-based dependency handling.

Lake packages use git commit SHAs as versions (not semver), with an inputRev field indicating the branch/tag being tracked (e.g., "main" or "v1.0.0"). The update checker finds the latest commit on that branch.

Inspired by the lean-update GitHub Action which also handles both lean-toolchain and lake-manifest.json updates.

How will you know you've accomplished your goal?

• All 72 unit tests pass
• Rubocop and Sorbet checks pass

Checklist

• I have run the complete test suite to ensure all tests and linters pass.
• I have thoroughly tested my code changes to ensure they work as expected, including adding additional tests for new functionality.
• I have written clear and descriptive commit messages.
• I have provided a detailed description of the changes in the pull request.
• I have ensured that the code is well-documented and easy to understand.

[jessealama]

I had some trouble with the CI because of rate limiting but it should be OK (many CI actions do pass).

[robaiken]

Hi @jessealama, Thank you for the contribution! We probably won't be able to review this PR until the new year. In the meantime, can you let me know if you are associated with the Lean ecosystem in any way?

[jessealama]

Hi @jessealama, Thank you for the contribution! We probably won't be able to review this PR until the new year. In the meantime, can you let me know if you are associated with the Lean ecosystem in any way?

No problem! Thanks for taking a look. There's no rush. I'm not associated with the Lean ecosysten in any official way; I'm just an enthusiastic user. Shall I try to get someone with a more official association with Lean to chime in?

[robaiken]

@jessealama The issue with adding new ecosystems is long-term support. We're trying to encourage more community ownership of ecosystems. Currently we have 3 community-maintained ecosystems.

We're hoping to add more where there's community willingness to support them long-term. If the Lean community is happy to help support their ecosystem updater, then we're happy to add support for it.

[jessealama]

@jessealama The issue with adding new ecosystems is long-term support. We're trying to encourage more community ownership of ecosystems. Currently we have 3 community-maintained ecosystems.

We're hoping to add more where there's community willingness to support them long-term. If the Lean community is happy to help support their ecosystem updater, then we're happy to add support for it.

Sounds good. I've set up a discussion in the Lean community (which uses Zulip) to gauge interest and interest in long-term support. I'll check back here in a while.

[javier-pm]

Hello!

Did you get some update from the community @jessealama?

[jessealama]

Hello!

Did you get some update from the community @jessealama?

I asked around and but some initial enthusiasm faded when it was pointed out to me that there's already a Lean-specific GitHub Action whose functionality overlaps with what Dependabot offers, and might potentially offer more features that make sense for Lean and the Lean community's expectations. It also seems that there's relatively little Ruby knowledge among the potential long-term maintainers in the community. I suppose we could close this PR, but I might suggest keeping the associated issue open in case things change. How does that sound?