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.

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

refactor: move registration of namespaces on kernel add into elaborator #6214

Open
wants to merge 4 commits into
base: kernel-env-base
Choose a base branch
from

Conversation

Kha
Copy link
Member

@Kha Kha commented Nov 25, 2024

Kernel checking will be moved to a different thread but namespace registration should stay on the elaboration thread

Stacked on #5145

@Kha Kha requested review from leodemoura and tydeu as code owners November 25, 2024 17:13
@Kha Kha changed the base branch from master to kernel-env-base November 28, 2024 13:59
@Kha Kha force-pushed the push-vwrqzpymymss branch 2 times, most recently from 05ab0d9 to d52dfc2 Compare December 3, 2024 13:08
@Kha Kha force-pushed the push-vwrqzpymymss branch 2 times, most recently from d3312a6 to 2a59a24 Compare December 11, 2024 22:33
@Kha Kha force-pushed the push-vwrqzpymymss branch 4 times, most recently from cd7e0a1 to 4aaed4c Compare December 12, 2024 16:07
@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 Dec 12, 2024
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Dec 12, 2024

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase b862e2d25163584322bcca54e5e56d671da1f258 --onto 48be424eaa2ae06972e9cfec4d355906b532204d. (2024-12-12 16:33:10)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 48eb3084a0e0e15d6c22287d1c17072cbe9f1541 --onto dd6445515ddc71826c76b8020fe9e030579b432b. (2025-01-09 17:13:29)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase c7939cfb03c78820b069ba9c931900d44b11f58e --onto d2c4471cfa4611977bf4927b5cd849df1a4272b7. (2025-01-12 21:50:37)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase c7fd8733334bb0053e4e7ce39b4d241abe08f456 --onto a955708b6c5f25e7f9c9ae7b951f8f3d5aefe377. (2025-01-16 15:31:23)

@Kha Kha force-pushed the push-vwrqzpymymss branch from 4aaed4c to c23d6e9 Compare January 9, 2025 16:38
@Kha Kha requested a review from Vtec234 as a code owner January 9, 2025 16:38
@Kha Kha force-pushed the push-vwrqzpymymss branch 4 times, most recently from ffee8e5 to 44389a1 Compare January 16, 2025 14:51
@Kha Kha force-pushed the push-vwrqzpymymss branch from 44389a1 to a993476 Compare January 16, 2025 15:02
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
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