dependabot / dependabot/dependabot-core

Add Lean 4 ecosystem support

Open
#13,786 0 comments 0 reactions 0 assignees View on GitHub
T: new-ecosystem
Dominant language
Ruby
Stars
5.8k
Forks
1.5k
Avg merge
2d 18h
Merged PRs (30d)
149

Description

### What is Lean?

[Lean 4](https://github.com/leanprover/lean4) is a functional programming language and interactive theorem prover. It's used for formal verification, mathematical proofs, and building verified software. Notable projects include [Mathlib](https://github.com/leanprover-community/mathlib4), the community-maintained library of formalized mathematics.

### The `lean-toolchain` file

Lean projects specify their toolchain version via a `lean-toolchain` file in the repository root. This is a single-line plain text file containing the toolchain identifier:

```
leanprover/lean4:v4.26.0
```

This tells [elan](https://github.com/leanprover/elan) (Lean's toolchain manager) which version of Lean to use. Keeping the toolchain up-to-date is important for security patches and compatibility with the broader ecosystem.

### Version format

Lean versions follow semver with support for release candidates:
- Stable: `4.26.0`, `4.27.0`, `4.28.0`
- Release candidates: `4.27.0-rc1`, `4.27.0-rc2`

Versions are published as [GitHub Releases](https://github.com/leanprover/lean4/releases).

### Desired behavior

- Projects on stable versions should only be offered stable updates
- Projects on RC versions should see both stable releases and newer RCs
- Stable versions should be considered newer than any RC of the same base version (e.g., `4.27.0 > 4.27.0-rc99`)

### Cooldown support

Release dates are available from the GitHub Releases API, enabling cooldown functionality.

### Scope

This ecosystem is similar in scope to `rust_toolchain`:
- Single manifest file (`lean-toolchain`)
- Single dependency (the Lean toolchain itself)
- No lockfiles
- No native helpers required

### Maintainer

I will serve as the responsible maintainer for this ecosystem.

Contributor guide

Open the contributing guide

Research direction

Start by locating the existing rust_toolchain ecosystem implementation and its tests, then trace how a lean-toolchain file and GitHub Releases API data enter the updater. Done means supporting stable and RC filtering, stable-over-RC ordering, and cooldowns for the single Lean toolchain dependency without lockfiles or native helpers.

Written by the indexing model from the issue text.

Assessment

Domain
tooling
Issue type
Feature
Difficulty
4/5
Estimated time
3-5 days
Activity status
Stale
Clarity
Mostly clear
Newbie friendliness
58/100

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.