max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
40325 commits 1 branch 0 tags 5.3 GiB
Find a file
Kim Morrison 85d46c351f
chore: pin test-summary action to v2.4 SHA to unblock CI (#13686) 
This PR pins the `test-summary/action` GitHub Action to the immutable
commit SHA for `v2.4` to work around a broken upstream `v2` tag.
Upstream retagged `v2` to point at `v2.5`, which ships without the
bundled `index.js`, causing every job using the shared build template to
fail in the `Test Summary` post-step with `File not found:
'/home/runner/work/_actions/test-summary/action/v2/index.js'`, even when
all tests pass.

Pinning to the SHA (rather than another floating tag like `@v2.4`)
matches GitHub's [security
guidance](https://docs.github.com/en/actions/security-for-github-actions/security-guides/security-hardening-for-github-actions)
for third-party actions and avoids a repeat of this exact incident if
`v2.4` is later retagged. Dependabot is already configured for
`github-actions` updates in `.github/dependabot.yml`, so version bumps
remain low-cost.

Verification:
- `curl -sI
https://raw.githubusercontent.com/test-summary/action/v2/index.js`
returns 404
- `curl -sI
https://raw.githubusercontent.com/test-summary/action/31493c76ec9e7aa675f1585d3ed6f1da69269a86/index.js`
returns 200

The summary action is shared across every workflow that includes
`build-template.yml`, so this affects all CI Lake jobs, not just one.

🤖 Prepared with Claude Code

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
2026-05-08 10:38:53 +00:00
.claude chore: CLAUDE.md: test moddocs (#13662) 2026-05-06 14:03:06 +00:00
.github chore: pin test-summary action to v2.4 SHA to unblock CI (#13686) 2026-05-08 10:38:53 +00:00
.vscode chore: fixes from #13103 "enable separate codegen" (#13241) 2026-04-02 11:13:22 +00:00
doc doc: how to LLVM upgrade (#13656) 2026-05-06 10:03:53 +00:00
images
releases_drafts chore: remove stale release draft notes (#12518) 2026-02-17 19:56:23 +00:00
script chore: update release tooling and docs (#13631) 2026-05-04 15:33:36 +00:00
src feat: remove redundant deprecation warnings (#13595) 2026-05-07 15:43:34 +00:00
stage0 chore: update stage0 2026-05-05 18:38:42 +00:00
tests feat: remove redundant deprecation warnings (#13595) 2026-05-07 15:43:34 +00:00
.gitattributes chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
.gitignore chore: update release tooling and docs (#13631) 2026-05-04 15:33:36 +00:00
.gitpod.Dockerfile
.gitpod.yml chore: strip binaries only in release builds (#13208) 2026-03-31 17:18:43 +00:00
.ignore
AGENTS.md chore: add AGENTS.md symlink to CLAUDE.md (#13461) 2026-04-18 06:48:05 +00:00
CMakeLists.txt chore: use the lean-llvm LLVM for benchmarking (#13634) 2026-05-05 14:26:08 +00:00
CMakePresets.json chore: rename reldebug preset to more appropriate relwithassert (#13657) 2026-05-06 13:27:53 +00:00
CODEOWNERS chore: make @hargoniX code owner of the compiler (#10732) 2025-10-10 04:43:38 +00:00
CONTRIBUTING.md chore: migrate pkg tests (#12889) 2026-03-11 18:55:46 +00:00
flake.lock chore: update to c++20 (#12117) 2026-02-11 01:17:40 +00:00
flake.nix chore: add aarch64-darwin to flake (#12915) 2026-03-18 15:55:34 +00:00
lean-toolchain chore: relative lean-toolchains (#12652) 2026-02-25 10:23:35 +00:00
LICENSE
LICENSES feat: bundle leantar with Lean (#12822) 2026-03-09 20:10:59 +00:00
README.md doc: update URLs that are currently pointing to redirects (#10397) 2025-09-17 15:50:07 +00:00
RELEASES.md chore: updates to release_checklist.md (#7817) 2025-04-04 03:45:36 +00:00

README.md

This is the repository for Lean 4.

About

Installation

See Install Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean.