Commit 2026-03-26 18:37 8af86740

View on Github ā†’

feat(scripts): add nightly-testing-checklist tool (#37196) This PR adds lake exe nightly-testing-checklist, a tool for monitoring and repairing the nightly-testing branches at Batteries and Mathlib. It checks toolchain freshness, upstream dependency versions (e.g. Batteries rev in Mathlib's lake-manifest.json), and CI status ā€” displaying failing jobs and Lean error messages inline. It can automatically fix "has already been declared" errors by using Lean's parser to identify and remove duplicate declarations, and bumps stale toolchains and dependencies. Flags:

  • --watch: wait for in-progress CI runs to complete (wakes on first job failure)
  • --fix: commit and push fixes (default is dry-run: generate .patch files)
  • --no-clone: report only, don't clone repos to /tmp
  • --no-build: clone and update deps, but don't build or fix errors The find_command_range.lean helper uses Lean.Parser.parseHeader + Lean.Parser.parseCommand to walk top-level commands and find byte ranges, including preceding attributes and doc comments. šŸ¤– Prepared with Claude Code

Estimated changes

added def main
added def ANSIColor.blue
added def ANSIColor.bold
added def ANSIColor.dim
added def ANSIColor.green
added def ANSIColor.red
added def ANSIColor.yellow
added structure BuildError
added structure CIRun
added structure FailingJob
added structure UpstreamDep
added def cloneRepo
added def commitAndPush
added def deployHelper
added def findCommandRange
added def fixLoop
added def generatePatch
added def getCIRun
added def getFailingJobs
added def getJobErrors
added def getLatestCommit
added def getLatestNightly
added def getManifestRev
added def ghRawFile
added def isOwnFile
added def madeProgress
added def main
added def parseBuildError
added def parseCIRun
added def removeByteRange
added def runCmd
added def runIdFromUrl
added def runShell
added def toolchainTag
added def watchRun