feat: split `Lean.Kernel.Environment` from `Lean.Environment` #5145

Kha · 2024-08-23T15:47:56Z

This PR clarifies Lean's Trusted Code Base (TCB) by splitting the data used by the kernel from the data used by general elaboration and code generation, and in the future asynchronously elaborated declarations.

kernel diagnostics are moved from an environment extension to a direct environment as they are the only extension used by the kernel
initQuot is 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
the status of native reduction as a TCB extension is made explicit in the code by moving it into an optional callback the kernel uses to call into the richer environment with access to the interpreter. This would also allow us to correctly forward Options to the interpreter such as preferNative (not implemented yet).

tobiasgrosser · 2024-08-25T05:44:51Z

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.

tobiasgrosser · 2024-08-25T08:40:12Z

I got it. TCB = Trusted Code Base

Kha · 2024-11-08T15:41:53Z

!bench

leanprover-bot · 2024-11-08T16:02:27Z

Here are the benchmark results for commit 4ba7bdc.
There were significant changes against commit c779f3a:

  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 σ)

src/Lean/Message.lean

src/Lean/Environment.lean

leodemoura · 2024-11-12T02:06:12Z

@Kha This PR has update stage0 commits. So, squash should not be used, and the commit messages should be fixed.

Kha · 2024-11-19T16:22:59Z

!bench

This PR adds less-than and less-than-or-equal-to relations to `UInt32`, consistent with the other `UIntN` types.

This PR implements `Std.Net.Addr` which contains structures around IP and socket addresses. While we could implement our own parser instead of going through the `addr_in`/`addr_in6` route we will need to implement these conversions to make proper system calls anyway. Hence this is likely the approach with the least amount of non trivial code overall. The only thing I am uncertain about is whether `ofString` should return `Option` or `Except`, unfortunately `libuv` doesn't hand out error messages on IP parsing.

…ver#6595) This PR improves the theorems used to justify the steps performed by the inequality offset module. See new test for examples of how they are going to be used.

This PR adds support for the `simp?` and `dsimp?` tactics in conversion mode. Closes leanprover#6164

This PR adds a `toFin` and `msb` lemma for unsigned bitvector division. We *don't* have `toInt_udiv`, since the only truly general statement we can make does no better than unfolding the definition, and it's not uncontroversially clear how to unfold `toInt` (see `toInt_eq_msb_cond`/`toInt_eq_toNat_cond`/`toInt_eq_toNat_bmod` for a few options currently provided). Instead, we do have `toInt_udiv_of_msb` that's able to provide a more meaningful rewrite given an extra side-condition (that `x.msb = false`). This PR also upstreams a minor `Nat` theorem (`Nat.div_le_div_left`) needed for the above from Mathlib. --------- Co-authored-by: Kim Morrison <[email protected]>

… types (leanprover#6587) This PR adds decidable instances for the `LE` and `LT` instances for the `Offset` types defined in `Std.Time`.

…nprover#6347) This PR adds `BitVec.toNat_rotateLeft` and `BitVec.toNat_rotateLeft`. --------- Co-authored-by: Kim Morrison <[email protected]>

This PR adds a `toFin` and `msb` lemma for unsigned bitvector modulus. Similar to leanprover#6402, we don't provide a general `toInt_umod` lemmas, but instead choose to provide more specialized rewrites, with extra side-conditions. --------- Co-authored-by: Kim Morrison <[email protected]>

…prover#6599) The FFI description didn't mention Int or signed integers. This PR adds `Int` and signed integers to the FFI document.

Users have requested toolchain tags on `lean4-cli`, so let's add it to the release checklist to make sure these get added regularly. Previously, `lean4-cli` has used more complicated tags, but going forward we're going to just use the simple `v4.16.0` style tags, with no repository-specific versioning. --------- Co-authored-by: Markus Himmel <[email protected]>

This PR fixes a bug in the pattern selection in the `grind`.

This PR adds support for case-splitting on `<->` (and `@Eq Prop`) in the `grind` tactic.

This PR fixes a bug in the `simp_arith` tactic. See new test.

This PR improves the case-split heuristic used in grind, prioritizing case-splits with fewer cases.

This PR fixes a bug in the `grind` core module responsible for merging equivalence classes and propagating constraints.

This PR fixes one of the sanity check tests used in `grind`.

This PR adds lemmas about `Array.append`, improving alignment with the `List` API.

This PR improves the case split heuristic used in the `grind` tactic, ensuring it now avoids unnecessary case-splits on `Iff`.

This PR improves the usability of the `[grind =]` attribute by automatically handling forbidden pattern symbols. For example, consider the following theorem tagged with this attribute: ``` getLast?_eq_some_iff {xs : List α} {a : α} : xs.getLast? = some a ↔ ∃ ys, xs = ys ++ [a] ``` Here, the selected pattern is `xs.getLast? = some a`, but `Eq` is a forbidden pattern symbol. Instead of producing an error, this function converts the pattern into a multi-pattern, allowing the attribute to be used conveniently.

This PR allows the dot ident notation to resolve to the current definition, or to any of the other definitions in the same mutual block. Existing code that uses dot ident notation may need to have `nonrec` added if the ident has the same name as the definition. Closes leanprover#6601

) This PR implements support for offset constraints in the `grind` tactic. Several features are still missing, such as constraint propagation and support for offset equalities, but `grind` can already solve examples like the following: ```lean example (a b c : Nat) : a ≤ b → b + 2 ≤ c → a + 1 ≤ c := by grind example (a b c : Nat) : a ≤ b → b ≤ c → a ≤ c := by grind example (a b c : Nat) : a + 1 ≤ b → b + 1 ≤ c → a + 2 ≤ c := by grind example (a b c : Nat) : a + 1 ≤ b → b + 1 ≤ c → a + 1 ≤ c := by grind example (a b c : Nat) : a + 1 ≤ b → b ≤ c + 2 → a ≤ c + 1 := by grind example (a b c : Nat) : a + 2 ≤ b → b ≤ c + 2 → a ≤ c := by grind ``` --------- Co-authored-by: Kim Morrison <[email protected]>

github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Aug 26, 2024

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Aug 26, 2024

Update lean-toolchain for testing leanprover/lean4#5145

c431416

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Aug 27, 2024

Trigger CI for leanprover/lean4#5145

593e074

Kha marked this pull request as ready for review August 27, 2024 11:32

Kha requested review from mhuisi, kim-em and leodemoura as code owners August 27, 2024 11:32

Kha force-pushed the kernel-env branch 2 times, most recently from 4aebbe2 to 4ba7bdc Compare November 8, 2024 15:41

Kha requested a review from tydeu as a code owner November 8, 2024 15:41

Kha added the changelog-language Language features, tactics, and metaprograms label Nov 8, 2024

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Nov 8, 2024

Trigger CI for leanprover/lean4#5145

a7a9d0c

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 8, 2024

Update lean-toolchain for testing leanprover/lean4#5145

b16708d

leanprover-community-bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Nov 8, 2024

leodemoura reviewed Nov 12, 2024

View reviewed changes

src/Lean/Message.lean Outdated Show resolved Hide resolved

leodemoura reviewed Nov 12, 2024

View reviewed changes

src/Lean/Environment.lean Show resolved Hide resolved

leodemoura reviewed Nov 12, 2024

View reviewed changes

src/Lean/Environment.lean Outdated Show resolved Hide resolved

leodemoura reviewed Nov 12, 2024

View reviewed changes

src/Lean/Environment.lean Outdated Show resolved Hide resolved

leodemoura closed this Nov 12, 2024

leodemoura reopened this Nov 12, 2024

Kha force-pushed the kernel-env branch 2 times, most recently from 3d308a8 to 514ee09 Compare November 19, 2024 15:56

Kha changed the base branch from master to nightly-with-mathlib November 19, 2024 16:05

Kha force-pushed the kernel-env branch from 514ee09 to e0353ed Compare November 19, 2024 16:08

david-christiansen and others added 2 commits January 9, 2025 07:01

feat: add UInt32.{lt, le} (leanprover#6591)

1b42728

This PR adds less-than and less-than-or-equal-to relations to `UInt32`, consistent with the other `UIntN` types.

Kha force-pushed the kernel-env branch from a9fd0d1 to c710e55 Compare January 9, 2025 16:38

Kha requested a review from Vtec234 as a code owner January 9, 2025 16:38

Kha force-pushed the kernel-env branch from c710e55 to 1faefa6 Compare January 9, 2025 16:47

feat: improve inequality offset support theorems for grind (leanpro…

d369976

…ver#6595) This PR improves the theorems used to justify the steps performed by the inequality offset module. See new test for examples of how they are going to be used.

Kha force-pushed the kernel-env branch from 1faefa6 to 0d778d8 Compare January 9, 2025 21:15

jrr6 and others added 22 commits January 10, 2025 01:42

feat: add simp? and dsimp? in conversion mode (leanprover#6593)

c07948a

This PR adds support for the `simp?` and `dsimp?` tactics in conversion mode. Closes leanprover#6164

feat: add decidable instances for comparison operation of time offset…

ed309dc

… types (leanprover#6587) This PR adds decidable instances for the `LE` and `LT` instances for the `Offset` types defined in `Std.Time`.

feat: BitVec.toNat theorems for rotateLeft and rotateRight (lea…

0b5d977

…nprover#6347) This PR adds `BitVec.toNat_rotateLeft` and `BitVec.toNat_rotateLeft`. --------- Co-authored-by: Kim Morrison <[email protected]>

chore: update stage0

58cd011

doc: update FFI description for Int and signed fixed-width ints (lean…

03081a5

…prover#6599) The FFI description didn't mention Int or signed integers. This PR adds `Int` and signed integers to the FFI document.

fix: pattern selection for local lemmas (leanprover#6606)

acad587

This PR fixes a bug in the pattern selection in the `grind`.

feat: add support for splitting on <-> to grind (leanprover#6607)

7ea5504

This PR adds support for case-splitting on `<->` (and `@Eq Prop`) in the `grind` tactic.

fix: simp_arith (leanprover#6608)

4636091

This PR fixes a bug in the `simp_arith` tactic. See new test.

feat: improve case-split heuristic used in grind (leanprover#6609)

5119528

This PR improves the case-split heuristic used in grind, prioritizing case-splits with fewer cases.

fix: bug in the grind propagator (leanprover#6610)

c5c1278

This PR fixes a bug in the `grind` core module responsible for merging equivalence classes and propagating constraints.

fix: checkParents in grind (leanprover#6611)

ce1ff03

This PR fixes one of the sanity check tests used in `grind`.

feat: lemmas about Array.append (leanprover#6612)

8b1aabb

This PR adds lemmas about `Array.append`, improving alignment with the `List` API.

feat: improve case split heuristic used in grind (leanprover#6613)

5419025

This PR improves the case split heuristic used in the `grind` tactic, ensuring it now avoids unnecessary case-splits on `Iff`.

feat: split Lean.Kernel.Environment from Lean.Environment

7818f9b

chore: update stage0

136e93a

chore: clean up after update-stage0

a46ba58

Kha force-pushed the kernel-env branch from 0d778d8 to a46ba58 Compare January 12, 2025 21:27

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: split `Lean.Kernel.Environment` from `Lean.Environment` #5145

feat: split `Lean.Kernel.Environment` from `Lean.Environment` #5145

Kha commented Aug 23, 2024 •

edited

Loading

tobiasgrosser commented Aug 25, 2024

tobiasgrosser commented Aug 25, 2024

Kha commented Nov 8, 2024

leanprover-bot commented Nov 8, 2024

leodemoura commented Nov 12, 2024

Kha commented Nov 19, 2024

feat: split Lean.Kernel.Environment from Lean.Environment #5145

Are you sure you want to change the base?

feat: split Lean.Kernel.Environment from Lean.Environment #5145

Conversation

Kha commented Aug 23, 2024 • edited Loading

tobiasgrosser commented Aug 25, 2024

tobiasgrosser commented Aug 25, 2024

Kha commented Nov 8, 2024

leanprover-bot commented Nov 8, 2024

leodemoura commented Nov 12, 2024

Kha commented Nov 19, 2024

feat: split `Lean.Kernel.Environment` from `Lean.Environment` #5145

feat: split `Lean.Kernel.Environment` from `Lean.Environment` #5145

Kha commented Aug 23, 2024 •

edited

Loading