feat: split Lean.Kernel.Environment from Lean.Environment#5145
Merged
Kha merged 1 commit intoleanprover:masterfrom Jan 18, 2025
Merged
feat: split Lean.Kernel.Environment from Lean.Environment#5145Kha merged 1 commit intoleanprover:masterfrom
Lean.Kernel.Environment from Lean.Environment#5145Kha merged 1 commit intoleanprover:masterfrom
Conversation
Contributor
|
Hi @Kha, this sounds exciting. I don't understand the appreciation (TCB); spelling it out may help others here. Most importantly, let me not distract you from your mission towards more parallelism in the lean compilation. It is exciting to see progress here. |
Contributor
|
I got it. TCB = Trusted Code Base |
ghost
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
Aug 26, 2024
ghost
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
Aug 27, 2024
4aebbe2 to
4ba7bdc
Compare
Member
Author
|
!bench |
Collaborator
|
Here are the benchmark results for commit 4ba7bdc. Benchmark Metric Change
=====================================================
- big_omega.lean MT task-clock 13.7% (12.0 σ)
- big_omega.lean MT wall-clock 13.7% (12.4 σ)
- bv_decide_mul branch-misses 2.0% (12.3 σ)
- bv_decide_realworld branch-misses 1.2% (31.5 σ)
- rbmap_fbip task-clock 4.1% (18.2 σ)
- rbmap_fbip wall-clock 4.1% (18.2 σ) |
ghost
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
Nov 8, 2024
ghost
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Nov 8, 2024
leodemoura
reviewed
Nov 12, 2024
leodemoura
reviewed
Nov 12, 2024
leodemoura
reviewed
Nov 12, 2024
leodemoura
reviewed
Nov 12, 2024
Member
|
@Kha This PR has update stage0 commits. So, squash should not be used, and the commit messages should be fixed. |
3d308a8 to
514ee09
Compare
Member
Author
|
!bench |
ghost
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
Nov 25, 2024
ghost
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Nov 25, 2024
e4759d2 to
a9fd0d1
Compare
a0a7047 to
3ca7e29
Compare
ghost
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
Jan 18, 2025
ghost
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Jan 18, 2025
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
4 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR splits the environment used by the kernel from that used by the elaborator, providing the foundation for tracking of asynchronously elaborated declarations, which will exist as a concept only in the latter.
Minor changes:
initQuotis moved from an environment header field to a direct environment as it is the only header field used by the kernel; this also makes the remaining header immutable after import