v1.0.1 — SHA-pin actions/cache

Patch release. Single behavior-preserving change for supply-chain hygiene.

Change

• action.yml: actions/cache@v5 → actions/cache@27d5ce7f107fe9357f9df03efb73ab90386fccae # v5.0.5

Matches the SHA-pinning style sibling consumers use for their own
actions/cache references. Closes the supply-chain regression
introduced when the migration replaced their pinned actions/cache
with the floating @v5 reference.

No semantic change — v5.0.5 is the current v5 patch.

Upgrade

If you're on @v1, you're already on v1.0.1.

If you're SHA-pinned to v1.0.0 (@6bb3a2b...), bump to v1.0.1's SHA
or to @v1.0.1.

v1.0.0 — first stable release

First stable release of the Lean / Mathlib cache action.

Usage

```yaml

• uses: actions/checkout@v6
• uses: coproduct-opensource/lean-mathlib-cache@v1.0.0
  with:
  lean-project-dir: lean
  build-target: MyProject
  ```

Pin the patch (`@v1.0.0`) by default; `@v1` floats forward within the
major if you want auto-uptake of bugfixes.

What this action does

Packages the canonical 50-line elan + Lake + Mathlib boilerplate that
every Lean 4 project's CI currently reinvents:

1. Installs elan if not already cached
2. Caches `/.elan` + `/.lake` + `/.cache/mathlib`, keyed
   on `lean-toolchain` + `lakefile.{lean,toml}` + `lake-manifest.json`
3. Resolves the Lean toolchain from `lean-toolchain`
4. Runs `lake exe cache get` to hydrate prebuilt Mathlib oleans (turns
   a ~1h cold build into ~5 minutes)
5. Optionally runs `lake build `

Inputs

Input	Required	Default
`lean-project-dir`	yes	—
`build-target`	no	`''`
`fetch-mathlib-cache`	no	`'true'`
`cache-key-prefix`	no	`'lean'`
`fail-on-mathlib-cache-miss`	no	`'false'`

Outputs

• `cache-hit` — `'true'` if the cache key hit exactly
• `lean-version` — resolved Lean version string

Compatibility

• Runners: Ubuntu, macOS (any runner with curl + bash)
• `actions/checkout@v6` and `actions/cache@v5`
• Lean 4 (any version — toolchain is read from the consumer's `lean-toolchain` file)

Why this exists

The Lean 4 ecosystem has converged on a `lake exe cache get`-shaped
workflow for Mathlib, but nobody has packaged the surrounding cache
hygiene as a reusable Action. Every project either ships the 50-line
boilerplate at the top of each workflow, copies it from another project
(inheriting whatever bug that project hadn't found yet), or skips the
Mathlib cache and burns ~1h on cold runs. This action picks the fourth
option: a one-line `uses:` that codifies the canonical pattern.

See README.md
for the full cache-key strategy, multi-project setup, and related anti-patterns.

Sibling action

`coproduct-opensource/aeneas-ci`
— Aeneas-generated Lean tree freshness check; natural pairing for
Rust-to-Lean verified projects.