Skip to content

chore: check con-leche against the rebootstrapped toolchain - #16446

Merged
Kha merged 6 commits into
masterfrom
rebootstrap-con-leche
Nov 14, 2026
Merged

Kha merged 6 commits into
masterfrom
rebootstrap-con-leche

Conversation

@Kha

@Kha Kha commented Nov 13, 2026 •

Copy link
Copy Markdown
Member

This PR builds con-leche in the "Check rebootstrap" CI step so that its package test checks the rebootstrapped toolchain's exports with the pinned checker instead of skipping. It also installs elan once in a shared step for all jobs that use it.

This PR builds `lean-beam` in the primary Linux CI job at every check level instead of only in release builds, so that PRs breaking its plugin build or package test fail before reaching a nightly. Unstamped PR toolchains now bundle `lean-beam` like releases do.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@Kha
Kha requested a review from kim-em as a code owner November 13, 2026 12:56
@Kha Kha added the merge-ci Enable merge queue CI checks for PR. In particular, produce artifacts for all major platforms. label Nov 13, 2026
@Kha
Kha force-pushed the rebootstrap-con-leche branch from a38ad23 to 70b5d91 Compare November 13, 2026 12:58
@Kha Kha changed the title chore: check con-leche and lean-beam against the rebootstrapped toolchain chore: check con-leche against the rebootstrapped toolchain Nov 13, 2026
Kha and others added 2 commits November 13, 2026 13:03
The toolchain does not bundle libc headers, so `lean-beam`'s C sources fell back to the runner's `/usr/include`, which the self-hosted NixOS runner lacks. Point `C_INCLUDE_PATH` at the dev shell's `GLIBC_DEV`, the glibc release builds link against.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Install elan once in a dedicated step for the jobs that use it, now including the `lean-beam` package test, making it available to later steps through `GITHUB_PATH`, or through `/etc/profile.d` under msys2, which drops `GITHUB_PATH` entries.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@github-actions github-actions Bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Nov 13, 2026
@Kha
Kha force-pushed the rebootstrap-con-leche branch from 70b5d91 to 927e35a Compare November 13, 2026 15:59
Kha and others added 2 commits November 13, 2026 16:01
The rebootstrap tests require `lean-beam` like the main tests, and Beam rejects running under a compiler revision other than the one it was built against, so rebuild it with the rebootstrapped toolchain.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This PR builds `con-leche` in the "Check rebootstrap" CI step so that its package test checks the rebootstrapped toolchain's exports with the pinned checker instead of skipping.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@Kha
Kha force-pushed the rebootstrap-con-leche branch from 927e35a to 1febff3 Compare November 13, 2026 16:02
@Kha
Kha added this pull request to the merge queue Nov 14, 2026
Merged via the queue into master with commit 55a18a0 Nov 14, 2026
18 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

merge-ci Enable merge queue CI checks for PR. In particular, produce artifacts for all major platforms. toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants