GitHub · Where software is built

Labels Milestones New issue

`runLinter` should use lake to find and manage build artifacts

#1638

· thorimur opened

on Jan 27, 2026

RFC: Consider adding Alternative.{many,many1}

#1577

· 414owen opened

on Dec 27, 2025

Document what should live here, vs in mathlib

#1576

· 414owen opened

on Dec 27, 2025

Simple program causes Lean panic with `Batteries.CodeAction.Match` import

#1502

· mik-jozef opened

on Nov 8, 2025

Environment linters should remind users how to disable them

#1468

· bryangingechen opened

on Oct 19, 2025

Develop the `List.sum`, `List.prod` and related APIs

#1465

· fgdorais opened

on Oct 16, 2025

Verify Binary Heap

#1442

· fgdorais opened

on Oct 2, 2025

Mathlib CI cache not uploading

#1425

· linesthatinterlace opened

on Sep 22, 2025

batteries CI should run shake

#1356

· kim-em opened

on Jul 31, 2025

`trans` does not work on implicit arguments

#1222

· staroperator opened

on May 3, 2025

Run traced_repo = trace(repo) meet the error like KeyError: 'batteries'

#1160

· zx1384187 opened

on Mar 12, 2025

alias ignores noncomputable section

#1097

· YaelDillies opened

on Jan 21, 2025