Skip to content
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

chore: exclude more symbols to get below Windows symbol limit #4746

Merged
merged 1 commit into from
Jul 15, 2024
Merged

chore: exclude more symbols to get below Windows symbol limit #4746

merged 1 commit into from
Jul 15, 2024

Conversation

Kha
Copy link
Member

@Kha Kha commented Jul 15, 2024

This is a short-term fix, a more principled fix is in the works

@Kha Kha requested a review from leodemoura as a code owner July 15, 2024 13:55
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc July 15, 2024 14:02 Inactive
@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, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase de96b6d8a71c50692f3589ad6a354546b58c57a1 --onto 5f70c1ca64a2c05a5866c47b9eb80a92034433ec. (2024-07-15 14:12:36)

@Kha Kha added the release-ci Enable all CI checks for a PR, like is done for releases label Jul 15, 2024
@Kha
Copy link
Member Author

Kha commented Jul 15, 2024

(needs a double-stage0 update to take effect)

@Kha Kha merged commit f167cfb into master Jul 15, 2024
22 of 24 checks passed
@Kha Kha deleted the exports-fewer-symbols branch July 15, 2024 21:19
Kha added a commit that referenced this pull request Jul 16, 2024
@Kha
chore: temporarily remove test broken by #4746
7aec6c9
Kha added a commit to Kha/lean4 that referenced this pull request Aug 29, 2024
@Kha
chore: revert "chore: temporarily remove test broken by leanprover#4746"
cc458b8 
This reverts commit 7aec6c9.
github-merge-queue bot pushed a commit that referenced this pull request Aug 29, 2024
@Kha
chore: revert "chore: temporarily remove test broken by #4746" (#5201)
5c61ad3 
This reverts commit 7aec6c9.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@leodemoura leodemoura Awaiting requested review from leodemoura leodemoura is a code owner

Assignees
No one assigned
Labels
release-ci Enable all CI checks for a PR, like is done for releases 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-mathlib4-bot