Skip to content

chore: CI: make "Linux Lake" primary PR CI job #8739

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
Kha merged 7 commits into from
Jun 13, 2025
Merged

chore: CI: make "Linux Lake" primary PR CI job #8739

Kha merged 7 commits into from
Jun 13, 2025

Conversation

@Kha
Copy link
Member

@Kha Kha commented Jun 12, 2025 •
edited
Loading

Comes with .olean caching and module system-powered short-circuiting

@Kha Kha requested a review from kim-em as a code owner June 12, 2025 08:27
@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 Jun 12, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Jun 12, 2025 •
edited
Loading

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase faffe863343211d03d07d4ef19d90a2aa9d6fc8c --onto 0a9c24649767dea857a388e5385b7ae94bfd0185. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-12 08:58:00)
  • ❗ Batteries CI can not be attempted yet, as the nightly-testing-2025-06-12 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Batteries CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-12 10:37:54)

@Kha Kha force-pushed the push-rlqrzovkwlmk branch from aca24a1 to 63ab706 Compare June 12, 2025 10:07
@Kha Kha added the release-ci Enable all CI checks for a PR, like is done for releases label Jun 12, 2025
@Kha Kha removed the release-ci Enable all CI checks for a PR, like is done for releases label Jun 12, 2025
@Kha Kha force-pushed the push-rlqrzovkwlmk branch 2 times, most recently from 6846b51 to d0bfe80 Compare June 13, 2025 11:21
@Kha Kha enabled auto-merge June 13, 2025 11:21
@Kha Kha added this pull request to the merge queue Jun 13, 2025
Merged via the queue into leanprover:master with commit 121ce56 Jun 13, 2025
13 checks passed
@Kha Kha deleted the push-rlqrzovkwlmk branch June 13, 2025 13:03
nomeata added a commit that referenced this pull request Jun 16, 2025
@nomeata
chore: Run “Linux release” for PRs as secondary job
644f57a 
This PR reifnes #8739 to make sure we get a linux release in the PR
release.
@nomeata nomeata mentioned this pull request Jun 16, 2025
Merged
github-merge-queue bot pushed a commit that referenced this pull request Jun 16, 2025
@nomeata
chore: Run “Linux release” for PRs as secondary job (#8817)
5568e06 
This PR reifnes #8739 to make sure we get a linux release in the PR
release.
algebraic-dev pushed a commit to algebraic-dev/lean4 that referenced this pull request Jun 18, 2025
@Kha @algebraic-dev
chore: CI: make "Linux Lake" primary PR CI job (leanprover#8739)
b073974 
Comes with .olean caching and module system-powered short-circuiting
algebraic-dev pushed a commit to algebraic-dev/lean4 that referenced this pull request Jun 18, 2025
@nomeata @algebraic-dev
chore: Run “Linux release” for PRs as secondary job (leanprover#8817)
578a171 
This PR reifnes leanprover#8739 to make sure we get a linux release in the PR
release.
wkrozowski pushed a commit to wkrozowski/lean4 that referenced this pull request Jun 24, 2025
@Kha @wkrozowski
chore: CI: make "Linux Lake" primary PR CI job (leanprover#8739)
8702572 
Comes with .olean caching and module system-powered short-circuiting
wkrozowski pushed a commit to wkrozowski/lean4 that referenced this pull request Jun 24, 2025
@nomeata @wkrozowski
chore: Run “Linux release” for PRs as secondary job (leanprover#8817)
f847e81 
This PR reifnes leanprover#8739 to make sure we get a linux release in the PR
release.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@kim-em kim-em Awaiting requested review from kim-em kim-em is a code owner

Assignees

No one assigned

Labels

toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@Kha @leanprover-community-bot