Content-Length: 286102 | pFad | http://github.com/leanprover/lean4/pull/9104

64 chore: lake: re-enable tests in CI by tydeu · Pull Request #9104 · leanprover/lean4 · GitHub
Skip to content

chore: lake: re-enable tests in CI #9104

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
Draft
wants to merge 3 commits into
base: master
Choose a base branch
from
Draft

chore: lake: re-enable tests in CI #9104

wants to merge 3 commits into from

Conversation

tydeu
Copy link
Member

@tydeu tydeu commented Jun 30, 2025 •
edited
Loading

This PR re-enables Lake tests in the CI. The most likely cause of the previous issues was memory limits that have since been fixed.

This also fixes some issues with the tests on macOS and corrects the properly avoids downloading Mathlib in the init test after changes to the math-lax template in #8866.

@tydeu tydeu added the changelog-no Do not include this PR in the release changelog label Jun 30, 2025
@tydeu tydeu marked this pull request as draft June 30, 2025 15:47
@tydeu tydeu force-pushed the lake/enable-tests branch from 51dea31 to a9ceda5 Compare July 14, 2025 23:46
@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 Jul 15, 2025
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2025-07-14 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2025-07-15 03:05:06)

@leanprover-bot
Copy link
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-07-14 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-07-15 03:05:08)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
changelog-no Do not include this PR in the release changelog 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.
3 participants
@tydeu @leanprover-community-bot @leanprover-bot








ApplySandwichStrip

pFad - (p)hone/(F)rame/(a)nonymizer/(d)eclutterfier!      Saves Data!


--- a PPN by Garber Painting Akron. With Image Size Reduction included!

Fetched URL: http://github.com/leanprover/lean4/pull/9104

Alternative Proxies:

Alternative Proxy

pFad Proxy

pFad v3 Proxy

pFad v4 Proxy