Nightly Testing
Understanding the Lean/Mathlib nightly testing infrastructure. Use when working on toolchain bumps, adaptation PRs, or investigating nightly CI failures.
MCP get_skill({ skillId: "nightly-testing-fd543db9" })Use this skill with your agent
Create a free account and connect via MCP
# Nightly Testing Lean 4 publishes nightly toolchain builds from `master`. Batteries and Mathlib each have a `nightly-testing` branch that tracks these nightlies and runs CI against them. When CI passes, a `nightly-testing-YYYY-MM-DD` tag is created. When it fails, fixes are needed before the new toolchain can be adopted. ## The mathlib4-nightly-testing Fork Mathlib's nightly testing lives in a **separate fork**: `leanprover-community/mathlib4-nightly-testing`, not on the main `leanprover-community/mathlib4` repo. This keeps experimental toolchain branches out of the main repository. When Lean PRs affect Mathlib, `lean-pr-testing-NNNN` branches are created here automatically. ## Key Branches - **`nightly-testing`** — tracks the latest Lean nightly. CI runs here determine whether a nightly is usable. - **`nightly-with-mathlib`** — points to the latest nightly that passes Mathlib CI. Lean PRs that may affect downstream should base off this branch. - **`bump/v4.X.Y`** — accumulates reviewed adaptations for an upcoming Lean release. Adaptation PRs merge `nightly-testing` changes into this branch, and `master` is regularly merged in during release cycles. - **`lean-pr-testing-NNNN`** — created automatically to test specific Lean PRs against Mathlib. ## Zulip https://leanprover.zulipchat.com/#narrow/channel/nightly-testing has up-to-date status on nightly builds, failures, and adaptation work. ## Full Details The canonical reference for branch and tag conventions across lean4, Batteries, and Mathlib is: https://leanprover-community.github.io/contribute/tags_and_branches.html. If you are asked to work on nightly-testing, or lean-pr-testing-NNNN branches, you should read that page.
Related Skills
More skills in DevOps & Cloud
1password Skill
1password Skill linked from Juliano Barbosa Claude Code Skills, with the upstream skill instructions available on GitHub.
Actions Manager
GitHub Actions command center -- view workflow runs, read logs, re-run failed jobs, manage workflows, and debug CI failures entirely from the editor. Bypasses the deeply nested, visually-dependent Actions UI that is largely inaccessible to screen readers.
Airunway Aks Setup
Set up AI Runway on AKS — from bare cluster to running model. Covers cluster verification, controller install, GPU assessment, provider setup, and first deployment. WHEN: "setup AI Runway", "onboard AKS cluster", "install AI Runway", "airunway setup", "deploy model to AKS", "GPU inference on AKS", "KAITO setup on AKS", "run LLM on AKS", "vLLM on AKS", "set up model serving on AKS", "AI Runway controller".
Alz Accelerator
Deploy Azure Landing Zones using the ALZ Accelerator with AVM (Azure Verified Modules). Use this skill whenever the user mentions Azure Landing Zones, ALZ, Azure landing zone accelerator, AVM modules for landing zones, deploying management groups, hub-and-spoke networking, Virtual WAN, platform landing zones, or asks about Bicep vs Terraform for Azure infrastructure. Also trigger when the user wants to bootstrap CI/CD for Azure platform deployment, set up management groups hierarchy, or deploy connectivity/identity/management platform subscriptions.
Alz Accelerator Skill
Alz Accelerator Skill linked from Juliano Barbosa Claude Code Skills, with the upstream skill instructions available on GitHub.
Ansible Conventions and Best Practices
Ansible conventions and best practices
Explore Other Categories
Skills from other categories with shared topics
Lean Bisect
Bisect Lean toolchain versions to find where behavior changes. Use when trying to identify which Lean 4 commit caused a regression or behavior change.
Lean Mwe
Create minimal working examples (MWEs) from Lean errors for bug reports. Use when minimizing a Lean error, creating an MWE, or preparing a bug report for lean4 or mathlib4.
Lean PR
PR conventions for the leanprover/lean4 repository. Use when creating pull requests, writing commit messages, or following project conventions for Lean contributions.