perf: eliminate checkSystemInterval overhead when disabled

Skip the FFI call to lean_check_system_interval entirely when LEAN_CHECK_SYSTEM_INTERVAL_MS is unset by checking a builtin_initialize'd Bool flag inline. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Merge master into joachim/checkSystemTime
2026-04-14 08:04:07 +00:00 · 2026-04-06 18:14:34 +00:00 · 2026-04-06 14:19:13 +00:00 · 2026-04-06 10:14:43 +00:00 · 2026-04-06 10:10:56 +00:00 · 2026-04-06 09:00:16 +00:00
167 changed files with 408 additions and 1060 deletions
--- a/.github/workflows/build-template.yml
+++ b/.github/workflows/build-template.yml
@@ -131,7 +131,7 @@ jobs:
          [ -d build ] || mkdir build
          cd build
          # arguments passed to `cmake`
-          OPTIONS=(-DWFAIL=ON)
+          OPTIONS=(-DLEAN_EXTRA_MAKE_OPTS=-DwarningAsError=true)
          if [[ -n '${{ matrix.release }}' ]]; then
            # this also enables githash embedding into stage 1 library, which prohibits reusing
            # `.olean`s across commits, so we don't do it in the fast non-release CI
@@ -201,7 +201,6 @@ jobs:
        if: matrix.name == 'Linux Lake' && !cancelled() && (github.event_name != 'pull_request' || github.event.pull_request.head.repo.full_name == github.repository)
        run: |
          curl --version
-          cat build/stage1/lib/lean/Leanc.trace
          cd src
          time ../build/stage0/bin/lake build -o ../build/lake-mappings.jsonl
          time ../build/stage0/bin/lake cache put ../build/lake-mappings.jsonl --repo=${{ github.repository }}
--- a/.github/workflows/update-stage0.yml
+++ b/.github/workflows/update-stage0.yml
@@ -77,7 +77,7 @@ jobs:
      # sync options with `Linux Lake` to ensure cache reuse
      run: |
        mkdir -p build
-        cmake --preset release -B build -DWFAIL=ON
+        cmake --preset release -B build -DLEAN_EXTRA_MAKE_OPTS=-DwarningAsError=true
      shell: 'nix develop -c bash -euxo pipefail {0}'
    - if: env.should_update_stage0 == 'yes'
      run: |
--- a/.gitignore
+++ b/.gitignore
@@ -34,4 +34,3 @@ wdErr.txt
 wdIn.txt
 wdOut.txt
 downstream_releases/
-.claude/worktrees/
--- a/script/release_repos.yml
+++ b/script/release_repos.yml
@@ -28,14 +28,6 @@ repositories:
    branch: main
    dependencies: []

-  - name: leansqlite
-    url: https://github.com/leanprover/leansqlite
-    toolchain-tag: true
-    stable-branch: false
-    branch: main
-    dependencies:
-      - plausible
-
  - name: verso
    url: https://github.com/leanprover/verso
    toolchain-tag: true
@@ -108,7 +100,7 @@ repositories:
    toolchain-tag: true
    stable-branch: false
    branch: main
-    dependencies: [lean4-cli, BibtexQuery, mathlib4, leansqlite]
+    dependencies: [lean4-cli, BibtexQuery, mathlib4]

  - name: cslib
    url: https://github.com/leanprover/cslib
--- a/script/release_steps.py
+++ b/script/release_steps.py
@@ -481,9 +481,11 @@ def execute_release_steps(repo, version, config):
        run_command("lake update", cwd=repo_path, stream_output=True)
    elif repo_name == "verso":
        # verso has nested Lake projects in test-projects/ that each have their own
-        # lake-manifest.json with a subverso pin and their own lean-toolchain.
-        # After updating the root manifest via `lake update`, sync the de-modulized
-        # subverso rev into all sub-manifests, and update their lean-toolchain files.
+        # lake-manifest.json with a subverso pin. After updating the root manifest via
+        # `lake update`, sync the de-modulized subverso rev into all sub-manifests.
+        # The sub-projects use an old toolchain (v4.21.0) that doesn't support module/prelude
+        # syntax, so they need the de-modulized version (tagged no-modules/<root-rev>).
+        # The "SubVerso version consistency" CI check accepts either the root or de-modulized rev.
        run_command("lake update", cwd=repo_path, stream_output=True)
        print(blue("Syncing de-modulized subverso rev to test-project sub-manifests..."))
        sync_script = (
@@ -496,15 +498,6 @@ def execute_release_steps(repo, version, config):
        )
        run_command(sync_script, cwd=repo_path)
        print(green("Synced de-modulized subverso rev to all test-project sub-manifests"))
-        # Update all lean-toolchain files in test-projects/ to match the root
-        print(blue("Updating lean-toolchain files in test-projects/..."))
-        find_result = run_command("find test-projects -name lean-toolchain", cwd=repo_path)
-        for tc_path in find_result.stdout.strip().splitlines():
-            if tc_path:
-                tc_file = repo_path / tc_path
-                with open(tc_file, "w") as f:
-                    f.write(f"leanprover/lean4:{version}\n")
-                print(green(f"  Updated {tc_path}"))
    elif dependencies:
        run_command(f'perl -pi -e \'s/"v4\\.[0-9]+(\\.[0-9]+)?(-rc[0-9]+)?"/"' + version + '"/g\' lakefile.*', cwd=repo_path)
        run_command("lake update", cwd=repo_path, stream_output=True)
@@ -666,61 +659,56 @@ def execute_release_steps(repo, version, config):
        # Fetch latest changes to ensure we have the most up-to-date nightly-testing branch
        print(blue("Fetching latest changes from origin..."))
        run_command("git fetch origin", cwd=repo_path)
-
-        # Check if nightly-testing branch exists on origin (use local ref after fetch for exact match)
-        nightly_check = run_command("git show-ref --verify --quiet refs/remotes/origin/nightly-testing", cwd=repo_path, check=False)
-        if nightly_check.returncode != 0:
-            print(yellow("No nightly-testing branch found on origin, skipping merge"))
-        else:
-            try:
-                print(blue("Merging origin/nightly-testing..."))
-                run_command("git merge origin/nightly-testing", cwd=repo_path)
-                print(green("Merge completed successfully"))
-            except subprocess.CalledProcessError:
-                # Merge failed due to conflicts - check which files are conflicted
-                print(blue("Merge conflicts detected, checking which files are affected..."))
-
-                # Get conflicted files using git status
-                status_result = run_command("git status --porcelain", cwd=repo_path)
-                conflicted_files = []
-
-                for line in status_result.stdout.splitlines():
-                    if len(line) >= 2 and line[:2] in ['UU', 'AA', 'DD', 'AU', 'UA', 'DU', 'UD']:
-                        # Extract filename (skip the first 3 characters which are status codes)
-                        conflicted_files.append(line[3:])
-
-                # Filter out allowed files
-                allowed_patterns = ['lean-toolchain', 'lake-manifest.json']
-                problematic_files = []
-
+        
+        try:
+            print(blue("Merging origin/nightly-testing..."))
+            run_command("git merge origin/nightly-testing", cwd=repo_path)
+            print(green("Merge completed successfully"))
+        except subprocess.CalledProcessError:
+            # Merge failed due to conflicts - check which files are conflicted
+            print(blue("Merge conflicts detected, checking which files are affected..."))
+            
+            # Get conflicted files using git status
+            status_result = run_command("git status --porcelain", cwd=repo_path)
+            conflicted_files = []
+            
+            for line in status_result.stdout.splitlines():
+                if len(line) >= 2 and line[:2] in ['UU', 'AA', 'DD', 'AU', 'UA', 'DU', 'UD']:
+                    # Extract filename (skip the first 3 characters which are status codes)
+                    conflicted_files.append(line[3:])
+            
+            # Filter out allowed files
+            allowed_patterns = ['lean-toolchain', 'lake-manifest.json']
+            problematic_files = []
+            
+            for file in conflicted_files:
+                is_allowed = any(pattern in file for pattern in allowed_patterns)
+                if not is_allowed:
+                    problematic_files.append(file)
+            
+            if problematic_files:
+                # There are conflicts in non-allowed files - fail
+                print(red("❌ Merge failed!"))
+                print(red(f"Merging nightly-testing resulted in conflicts in:"))
+                for file in problematic_files:
+                    print(red(f"  - {file}"))
+                print(red("Please resolve these conflicts manually."))
+                return
+            else:
+                # Only allowed files are conflicted - resolve them automatically
+                print(green(f"✅ Only allowed files conflicted: {', '.join(conflicted_files)}"))
+                print(blue("Resolving conflicts automatically..."))
+                
+                # For lean-toolchain and lake-manifest.json, keep our versions
                for file in conflicted_files:
-                    is_allowed = any(pattern in file for pattern in allowed_patterns)
-                    if not is_allowed:
-                        problematic_files.append(file)
-
-                if problematic_files:
-                    # There are conflicts in non-allowed files - fail
-                    print(red("❌ Merge failed!"))
-                    print(red(f"Merging nightly-testing resulted in conflicts in:"))
-                    for file in problematic_files:
-                        print(red(f"  - {file}"))
-                    print(red("Please resolve these conflicts manually."))
-                    return
-                else:
-                    # Only allowed files are conflicted - resolve them automatically
-                    print(green(f"✅ Only allowed files conflicted: {', '.join(conflicted_files)}"))
-                    print(blue("Resolving conflicts automatically..."))
-
-                    # For lean-toolchain and lake-manifest.json, keep our versions
-                    for file in conflicted_files:
-                        print(blue(f"Keeping our version of {file}"))
-                        run_command(f"git checkout --ours {file}", cwd=repo_path)
-
-                    # Complete the merge
-                    run_command("git add .", cwd=repo_path)
-                    run_command("git commit --no-edit", cwd=repo_path)
-
-                    print(green("✅ Merge completed successfully with automatic conflict resolution"))
+                    print(blue(f"Keeping our version of {file}"))
+                    run_command(f"git checkout --ours {file}", cwd=repo_path)
+                
+                # Complete the merge
+                run_command("git add .", cwd=repo_path)
+                run_command("git commit --no-edit", cwd=repo_path)
+                
+                print(green("✅ Merge completed successfully with automatic conflict resolution"))

    # Build and test (skip for Mathlib)
    if repo_name not in ["mathlib4"]:
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -116,19 +116,11 @@ option(CHECK_OLEAN_VERSION "Only load .olean files compiled with the current ver
 option(USE_LAKE "Use Lake instead of lean.mk for building core libs from language server" ON)
 option(USE_LAKE_CACHE "Use the Lake artifact cache for stage 1 builds (requires USE_LAKE)" OFF)

-set(LEAN_EXTRA_OPTS "" CACHE STRING "extra options to lean (via lake or make)")
-set(LEAN_EXTRA_MAKE_OPTS "" CACHE STRING "extra options to leanmake")
+set(LEAN_EXTRA_MAKE_OPTS "" CACHE STRING "extra options to lean --make")
 set(LEANC_CC ${CMAKE_C_COMPILER} CACHE STRING "C compiler to use in `leanc`")

 # Temporary, core-only flags. Must be synced with stdlib_flags.h.
-string(APPEND LEAN_EXTRA_OPTS " -Dbackward.do.legacy=false")
-
-# option used by the CI to fail on warnings
-option(WFAIL "Fail build if warnings are emitted by Lean" ON)
-if(WFAIL MATCHES "ON")
-  string(APPEND LAKE_EXTRA_ARGS " --wfail")
-  string(APPEND LEAN_EXTRA_MAKE_OPTS " -DwarningAsError=true")
-endif()
+string(APPEND LEAN_EXTRA_MAKE_OPTS " -Dbackward.do.legacy=false")

 if(LAZY_RC MATCHES "ON")
  set(LEAN_LAZY_RC "#define LEAN_LAZY_RC")
@@ -206,7 +198,7 @@ set(CMAKE_ARCHIVE_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}/lib/lean")

 # OSX default thread stack size is very small. Moreover, in Debug mode, each new stack frame consumes a lot of extra memory.
 if((MULTI_THREAD MATCHES "ON") AND (CMAKE_SYSTEM_NAME MATCHES "Darwin"))
-  string(APPEND LEAN_EXTRA_OPTS " -s40000")
+  string(APPEND LEAN_EXTRA_MAKE_OPTS " -s40000")
 endif()

 # We want explicit stack probes in huge Lean stack frames for robust stack overflow detection
@@ -678,9 +670,6 @@ else()
  set(LEAN_PATH_SEPARATOR ":")
 endif()

-# inherit genral options for lean.mk.in and stdlib.make.in
-string(APPEND LEAN_EXTRA_MAKE_OPTS " ${LEAN_EXTRA_OPTS}")
-
 # Version
 configure_file("${LEAN_SOURCE_DIR}/version.h.in" "${LEAN_BINARY_DIR}/include/lean/version.h")
 if(STAGE EQUAL 0)
@@ -1065,7 +1054,7 @@ string(REPLACE "ROOT" "${CMAKE_BINARY_DIR}" LEANC_CC "${LEANC_CC}")
 string(REPLACE "ROOT" "${CMAKE_BINARY_DIR}" LEANC_INTERNAL_FLAGS "${LEANC_INTERNAL_FLAGS}")
 string(REPLACE "ROOT" "${CMAKE_BINARY_DIR}" LEANC_INTERNAL_LINKER_FLAGS "${LEANC_INTERNAL_LINKER_FLAGS}")

-toml_escape("${LEAN_EXTRA_OPTS}" LEAN_EXTRA_OPTS_TOML)
+toml_escape("${LEAN_EXTRA_MAKE_OPTS}" LEAN_EXTRA_OPTS_TOML)

 if(CMAKE_BUILD_TYPE MATCHES "Debug|Release|RelWithDebInfo|MinSizeRel")
  set(CMAKE_BUILD_TYPE_TOML "${CMAKE_BUILD_TYPE}")
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@@ -1085,17 +1085,6 @@ Examples:
 def sum {α} [Add α] [Zero α] : Array α → α :=
  foldr (· + ·) 0

-/--
-Computes the product of the elements of an array.
-
-Examples:
- * `#[a, b, c].prod = a * (b * (c * 1))`
- * `#[1, 2, 5].prod = 10`
-/
-@[inline, expose]
-def prod {α} [Mul α] [One α] : Array α → α :=
-  foldr (· * ·) 1
-
 /--
 Counts the number of elements in the array `as` that satisfy the Boolean predicate `p`.

--- a/src/Init/Data/Array/Int.lean
+++ b/src/Init/Data/Array/Int.lean
@@ -7,7 +7,6 @@ module

 prelude
 public import Init.Data.List.Int.Sum
-public import Init.Data.List.Int.Prod
 public import Init.Data.Array.MinMax
 import Init.Data.Int.Lemmas

@@ -75,17 +74,4 @@ theorem sum_div_length_le_max_of_max?_eq_some_int {xs : Array Int} (h : xs.max?
  simpa [List.max?_toArray, List.sum_toArray] using
    List.sum_div_length_le_max_of_max?_eq_some_int (by simpa using h)

-@[simp] theorem prod_replicate_int {n : Nat} {a : Int} : (replicate n a).prod = a ^ n := by
-  rw [← List.toArray_replicate, List.prod_toArray]
-  simp
-
-theorem prod_append_int {as₁ as₂ : Array Int} : (as₁ ++ as₂).prod = as₁.prod * as₂.prod := by
-  simp [prod_append]
-
-theorem prod_reverse_int (xs : Array Int) : xs.reverse.prod = xs.prod := by
-  simp [prod_reverse]
-
-theorem prod_eq_foldl_int {xs : Array Int} : xs.prod = xs.foldl (init := 1) (· * ·) := by
-  simp only [foldl_eq_foldr_reverse, Int.mul_comm, ← prod_eq_foldr, prod_reverse_int]
-
 end Array
--- a/src/Init/Data/Array/Lemmas.lean
+++ b/src/Init/Data/Array/Lemmas.lean
@@ -4380,47 +4380,6 @@ theorem sum_eq_foldl [Zero α] [Add α] [Std.Associative (α := α) (· + ·)]
    xs.sum = xs.foldl (init := 0) (· + ·) := by
  simp [← sum_toList, List.sum_eq_foldl]

-/-! ### prod -/
-
-@[simp, grind =] theorem prod_empty [Mul α] [One α] : (#[] : Array α).prod = 1 := rfl
-theorem prod_eq_foldr [Mul α] [One α] {xs : Array α} :
-    xs.prod = xs.foldr (init := 1) (· * ·) :=
-  rfl
-
-@[simp, grind =]
-theorem prod_toList [Mul α] [One α] {as : Array α} : as.toList.prod = as.prod := by
-  cases as
-  simp [Array.prod, List.prod]
-
-@[simp, grind =]
-theorem prod_append [One α] [Mul α] [Std.Associative (α := α) (· * ·)]
-    [Std.LawfulLeftIdentity (α := α) (· * ·) 1]
-    {as₁ as₂ : Array α} : (as₁ ++ as₂).prod = as₁.prod * as₂.prod := by
-  simp [← prod_toList, List.prod_append]
-
-@[simp, grind =]
-theorem prod_singleton [Mul α] [One α] [Std.LawfulRightIdentity (· * ·) (1 : α)] {x : α} :
-    #[x].prod = x := by
-  simp [Array.prod_eq_foldr, Std.LawfulRightIdentity.right_id x]
-
-@[simp, grind =]
-theorem prod_push [Mul α] [One α] [Std.Associative (α := α) (· * ·)]
-    [Std.LawfulIdentity (· * ·) (1 : α)] {xs : Array α} {x : α} :
-    (xs.push x).prod = xs.prod * x := by
-  simp [Array.prod_eq_foldr, Std.LawfulRightIdentity.right_id, Std.LawfulLeftIdentity.left_id,
-    ← Array.foldr_assoc]
-
-@[simp, grind =]
-theorem prod_reverse [One α] [Mul α] [Std.Associative (α := α) (· * ·)]
-    [Std.Commutative (α := α) (· * ·)]
-    [Std.LawfulLeftIdentity (α := α) (· * ·) 1] (xs : Array α) : xs.reverse.prod = xs.prod := by
-  simp [← prod_toList, List.prod_reverse]
-
-theorem prod_eq_foldl [One α] [Mul α] [Std.Associative (α := α) (· * ·)]
-    [Std.LawfulIdentity (· * ·) (1 : α)] {xs : Array α} :
-    xs.prod = xs.foldl (init := 1) (· * ·) := by
-  simp [← prod_toList, List.prod_eq_foldl]
-
 theorem foldl_toList_eq_flatMap {l : List α} {acc : Array β}
    {F : Array β → α → Array β} {G : α → List β}
    (H : ∀ acc a, (F acc a).toList = acc.toList ++ G a) :
--- a/src/Init/Data/Array/Nat.lean
+++ b/src/Init/Data/Array/Nat.lean
@@ -8,7 +8,6 @@ module
 prelude
 public import Init.Data.Array.MinMax
 import Init.Data.List.Nat.Sum
-import Init.Data.List.Nat.Prod
 import Init.Data.Array.Lemmas

 public section
@@ -82,24 +81,4 @@ theorem sum_div_length_le_max_of_max?_eq_some_nat {xs : Array Nat} (h : xs.max?
  simpa [List.max?_toArray, List.sum_toArray] using
    List.sum_div_length_le_max_of_max?_eq_some_nat (by simpa using h)

-protected theorem prod_pos_iff_forall_pos_nat {xs : Array Nat} : 0 < xs.prod ↔ ∀ x ∈ xs, 0 < x := by
-  simp [← prod_toList, List.prod_pos_iff_forall_pos_nat]
-
-protected theorem prod_eq_zero_iff_exists_zero_nat {xs : Array Nat} :
-    xs.prod = 0 ↔ ∃ x ∈ xs, x = 0 := by
-  simp [← prod_toList, List.prod_eq_zero_iff_exists_zero_nat]
-
-@[simp] theorem prod_replicate_nat {n : Nat} {a : Nat} : (replicate n a).prod = a ^ n := by
-  rw [← List.toArray_replicate, List.prod_toArray]
-  simp
-
-theorem prod_append_nat {as₁ as₂ : Array Nat} : (as₁ ++ as₂).prod = as₁.prod * as₂.prod := by
-  simp [prod_append]
-
-theorem prod_reverse_nat (xs : Array Nat) : xs.reverse.prod = xs.prod := by
-  simp [prod_reverse]
-
-theorem prod_eq_foldl_nat {xs : Array Nat} : xs.prod = xs.foldl (init := 1) (· * ·) := by
-  simp only [foldl_eq_foldr_reverse, Nat.mul_comm, ← prod_eq_foldr, prod_reverse_nat]
-
 end Array
--- a/src/Init/Data/List/Basic.lean
+++ b/src/Init/Data/List/Basic.lean
@@ -2056,20 +2056,6 @@ def sum {α} [Add α] [Zero α] : List α → α :=
@[simp, grind =] theorem sum_cons [Add α] [Zero α] {a : α} {l : List α} : (a::l).sum = a + l.sum := rfl
 theorem sum_eq_foldr [Add α] [Zero α] {l : List α} : l.sum = l.foldr (· + ·) 0 := rfl

-/--
-Computes the product of the elements of a list.
-
-Examples:
- * `[a, b, c].prod = a * (b * (c * 1))`
- * `[1, 2, 5].prod = 10`
-/
-def prod {α} [Mul α] [One α] : List α → α :=
-  foldr (· * ·) 1
-
-@[simp, grind =] theorem prod_nil [Mul α] [One α] : ([] : List α).prod = 1 := rfl
-@[simp, grind =] theorem prod_cons [Mul α] [One α] {a : α} {l : List α} : (a::l).prod = a * l.prod := rfl
-theorem prod_eq_foldr [Mul α] [One α] {l : List α} : l.prod = l.foldr (· * ·) 1 := rfl
-
 /-! ### range -/

 /--
--- a/src/Init/Data/List/Int.lean
+++ b/src/Init/Data/List/Int.lean
@@ -7,4 +7,3 @@ module

 prelude
 public import Init.Data.List.Int.Sum
-public import Init.Data.List.Int.Prod
--- a/src/Init/Data/List/Int/Prod.lean
+++ b/src/Init/Data/List/Int/Prod.lean
@@ -1,31 +0,0 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kim Morrison
-/
-module
-
-prelude
-import Init.Data.List.Lemmas
-import Init.Data.Int.Lemmas
-public import Init.Data.Int.Pow
-public import Init.Data.List.Basic
-
-public section
-
-set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
-set_option linter.indexVariables true -- Enforce naming conventions for index variables.
-
-namespace List
-
-@[simp]
-theorem prod_replicate_int {n : Nat} {a : Int} : (replicate n a).prod = a ^ n := by
-  induction n <;> simp_all [replicate_succ, Int.pow_succ, Int.mul_comm]
-
-theorem prod_append_int {l₁ l₂ : List Int} : (l₁ ++ l₂).prod = l₁.prod * l₂.prod := by
-  simp [prod_append]
-
-theorem prod_reverse_int (xs : List Int) : xs.reverse.prod = xs.prod := by
-  simp [prod_reverse]
-
-end List
--- a/src/Init/Data/List/Lemmas.lean
+++ b/src/Init/Data/List/Lemmas.lean
@@ -1878,24 +1878,6 @@ theorem sum_reverse [Zero α] [Add α] [Std.Associative (α := α) (· + ·)]
    simp_all [sum_append, Std.Commutative.comm (α := α) _ 0,
      Std.LawfulLeftIdentity.left_id, Std.Commutative.comm]

-@[simp, grind =]
-theorem prod_append [Mul α] [One α] [Std.LawfulLeftIdentity (α := α) (· * ·) 1]
-    [Std.Associative (α := α) (· * ·)] {l₁ l₂ : List α} : (l₁ ++ l₂).prod = l₁.prod * l₂.prod := by
-  induction l₁ generalizing l₂ <;> simp_all [Std.Associative.assoc, Std.LawfulLeftIdentity.left_id]
-
-@[simp, grind =]
-theorem prod_singleton [Mul α] [One α] [Std.LawfulRightIdentity (· * ·) (1 : α)] {x : α} :
-    [x].prod = x := by
-  simp [List.prod_eq_foldr, Std.LawfulRightIdentity.right_id x]
-
-@[simp, grind =]
-theorem prod_reverse [One α] [Mul α] [Std.Associative (α := α) (· * ·)]
-    [Std.Commutative (α := α) (· * ·)]
-    [Std.LawfulLeftIdentity (α := α) (· * ·) 1] (xs : List α) : xs.reverse.prod = xs.prod := by
-  induction xs <;>
-    simp_all [prod_append, Std.Commutative.comm (α := α) _ 1,
-      Std.LawfulLeftIdentity.left_id, Std.Commutative.comm]
-
 /-! ### concat

 Note that `concat_eq_append` is a `@[simp]` lemma, so `concat` should usually not appear in goals.
@@ -2802,11 +2784,6 @@ theorem sum_eq_foldl [Zero α] [Add α] [Std.Associative (α := α) (· + ·)]
    xs.sum = xs.foldl (init := 0) (· + ·) := by
  simp [sum_eq_foldr, foldl_eq_apply_foldr, Std.LawfulLeftIdentity.left_id]

-theorem prod_eq_foldl [One α] [Mul α] [Std.Associative (α := α) (· * ·)]
-    [Std.LawfulIdentity (· * ·) (1 : α)] {xs : List α} :
-    xs.prod = xs.foldl (init := 1) (· * ·) := by
-  simp [prod_eq_foldr, foldl_eq_apply_foldr, Std.LawfulLeftIdentity.left_id]
-
 -- The argument `f : α₁ → α₂` is intentionally explicit, as it is sometimes not found by unification.
 theorem foldl_hom (f : α₁ → α₂) {g₁ : α₁ → β → α₁} {g₂ : α₂ → β → α₂} {l : List β} {init : α₁}
    (H : ∀ x y, g₂ (f x) y = f (g₁ x y)) : l.foldl g₂ (f init) = f (l.foldl g₁ init) := by
--- a/src/Init/Data/List/Nat.lean
+++ b/src/Init/Data/List/Nat.lean
@@ -13,7 +13,6 @@ public import Init.Data.List.Nat.Sublist
 public import Init.Data.List.Nat.TakeDrop
 public import Init.Data.List.Nat.Count
 public import Init.Data.List.Nat.Sum
-public import Init.Data.List.Nat.Prod
 public import Init.Data.List.Nat.Erase
 public import Init.Data.List.Nat.Find
 public import Init.Data.List.Nat.BEq
--- a/src/Init/Data/List/Nat/Prod.lean
+++ b/src/Init/Data/List/Nat/Prod.lean
@@ -1,50 +0,0 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kim Morrison
-/
-module
-
-prelude
-import Init.Data.List.Lemmas
-public import Init.BinderPredicates
-public import Init.NotationExtra
-import Init.Data.Nat.Lemmas
-
-public section
-
-set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
-set_option linter.indexVariables true -- Enforce naming conventions for index variables.
-
-namespace List
-
-protected theorem prod_eq_zero_iff_exists_zero_nat {l : List Nat} : l.prod = 0 ↔ ∃ x ∈ l, x = 0 := by
-  induction l with
-  | nil => simp
-  | cons x xs ih =>
-    simp [Nat.mul_eq_zero, ih, eq_comm (a := (0 : Nat))]
-
-protected theorem prod_pos_iff_forall_pos_nat {l : List Nat} : 0 < l.prod ↔ ∀ x ∈ l, 0 < x := by
-  induction l with
-  | nil => simp
-  | cons x xs ih =>
-    simp only [prod_cons, mem_cons, forall_eq_or_imp, ← ih]
-    constructor
-    · intro h
-      exact ⟨Nat.pos_of_mul_pos_right h, Nat.pos_of_mul_pos_left h⟩
-    · exact fun ⟨hx, hxs⟩ => Nat.mul_pos hx hxs
-
-@[simp]
-theorem prod_replicate_nat {n : Nat} {a : Nat} : (replicate n a).prod = a ^ n := by
-  induction n <;> simp_all [replicate_succ, Nat.pow_succ, Nat.mul_comm]
-
-theorem prod_append_nat {l₁ l₂ : List Nat} : (l₁ ++ l₂).prod = l₁.prod * l₂.prod := by
-  simp [prod_append]
-
-theorem prod_reverse_nat (xs : List Nat) : xs.reverse.prod = xs.prod := by
-  simp [prod_reverse]
-
-theorem prod_eq_foldl_nat {xs : List Nat} : xs.prod = xs.foldl (init := 1) (· * ·) := by
-  simp only [foldl_eq_foldr_reverse, Nat.mul_comm, ← prod_eq_foldr, prod_reverse_nat]
-
-end List
--- a/src/Init/Data/List/Perm.lean
+++ b/src/Init/Data/List/Perm.lean
@@ -606,13 +606,6 @@ theorem sum_nat {l₁ l₂ : List Nat} (h : l₁ ~ l₂) : l₁.sum = l₂.sum :
  | swap => simpa [List.sum_cons] using Nat.add_left_comm ..
  | trans _ _ ih₁ ih₂ => simp [ih₁, ih₂]

-theorem prod_nat {l₁ l₂ : List Nat} (h : l₁ ~ l₂) : l₁.prod = l₂.prod := by
-  induction h with
-  | nil => simp
-  | cons _ _ ih => simp [ih]
-  | swap => simpa [List.prod_cons] using Nat.mul_left_comm ..
-  | trans _ _ ih₁ ih₂ => simp [ih₁, ih₂]
-
 theorem all_eq {l₁ l₂ : List α} {f : α → Bool} (hp : l₁.Perm l₂) : l₁.all f = l₂.all f := by
  rw [Bool.eq_iff_iff]; simp [hp.mem_iff]

@@ -622,9 +615,6 @@ theorem any_eq {l₁ l₂ : List α} {f : α → Bool} (hp : l₁.Perm l₂) : l
 grind_pattern Perm.sum_nat => l₁ ~ l₂, l₁.sum
 grind_pattern Perm.sum_nat => l₁ ~ l₂, l₂.sum

-grind_pattern Perm.prod_nat => l₁ ~ l₂, l₁.prod
-grind_pattern Perm.prod_nat => l₁ ~ l₂, l₂.prod
-
 end Perm

 end List
--- a/src/Init/Data/List/ToArray.lean
+++ b/src/Init/Data/List/ToArray.lean
@@ -213,9 +213,6 @@ theorem forM_toArray [Monad m] (l : List α) (f : α → m PUnit) :
@[simp, grind =] theorem sum_toArray [Add α] [Zero α] (l : List α) : l.toArray.sum = l.sum := by
  simp [Array.sum, List.sum]

-@[simp, grind =] theorem prod_toArray [Mul α] [One α] (l : List α) : l.toArray.prod = l.prod := by
-  simp [Array.prod, List.prod]
-
@[simp, grind =] theorem append_toArray (l₁ l₂ : List α) :
    l₁.toArray ++ l₂.toArray = (l₁ ++ l₂).toArray := by
  apply ext'
--- a/src/Init/Data/String/Decode.lean
+++ b/src/Init/Data/String/Decode.lean
@@ -363,7 +363,7 @@ theorem toBitVec_eq_of_parseFirstByte_eq_threeMore {b : UInt8} (h : parseFirstBy
 public def isInvalidContinuationByte (b : UInt8) : Bool :=
  b &&& 0xc0 != 0x80

-theorem isInvalidContinuationByte_eq_false_iff {b : UInt8} :
+theorem isInvalidContinutationByte_eq_false_iff {b : UInt8} :
    isInvalidContinuationByte b = false ↔ b &&& 0xc0 = 0x80 := by
  simp [isInvalidContinuationByte]

--- a/src/Init/Data/Vector/Basic.lean
+++ b/src/Init/Data/Vector/Basic.lean
@@ -506,16 +506,6 @@ Examples:
@[inline, expose] def sum [Add α] [Zero α] (xs : Vector α n) : α :=
  xs.toArray.sum

-/--
-Computes the product of the elements of a vector.
-
-Examples:
- * `#v[a, b, c].prod = a * (b * (c * 1))`
- * `#v[1, 2, 5].prod = 10`
-/
-@[inline, expose] def prod [Mul α] [One α] (xs : Vector α n) : α :=
-  xs.toArray.prod
-
 /--
 Pad a vector on the left with a given element.

--- a/src/Init/Data/Vector/Int.lean
+++ b/src/Init/Data/Vector/Int.lean
@@ -30,16 +30,4 @@ theorem sum_reverse_int (xs : Vector Int n) : xs.reverse.sum = xs.sum := by
 theorem sum_eq_foldl_int {xs : Vector Int n} : xs.sum = xs.foldl (b := 0) (· + ·) := by
  simp only [foldl_eq_foldr_reverse, Int.add_comm, ← sum_eq_foldr, sum_reverse_int]

-@[simp] theorem prod_replicate_int {n : Nat} {a : Int} : (replicate n a).prod = a ^ n := by
-  simp [← prod_toArray, Array.prod_replicate_int]
-
-theorem prod_append_int {as₁ as₂ : Vector Int n} : (as₁ ++ as₂).prod = as₁.prod * as₂.prod := by
-  simp [← prod_toArray]
-
-theorem prod_reverse_int (xs : Vector Int n) : xs.reverse.prod = xs.prod := by
-  simp [prod_reverse]
-
-theorem prod_eq_foldl_int {xs : Vector Int n} : xs.prod = xs.foldl (b := 1) (· * ·) := by
-  simp only [foldl_eq_foldr_reverse, Int.mul_comm, ← prod_eq_foldr, prod_reverse_int]
-
 end Vector
--- a/src/Init/Data/Vector/Lemmas.lean
+++ b/src/Init/Data/Vector/Lemmas.lean
@@ -278,12 +278,6 @@ theorem toArray_mk {xs : Array α} (h : xs.size = n) : (Vector.mk xs h).toArray
@[simp, grind =] theorem sum_toArray [Add α] [Zero α] {xs : Vector α n} :
    xs.toArray.sum = xs.sum := rfl

-@[simp] theorem prod_mk [Mul α] [One α] {xs : Array α} (h : xs.size = n) :
-    (Vector.mk xs h).prod = xs.prod := rfl
-
-@[simp, grind =] theorem prod_toArray [Mul α] [One α] {xs : Vector α n} :
-    xs.toArray.prod = xs.prod := rfl
-
@[simp] theorem eq_mk : xs = Vector.mk as h ↔ xs.toArray = as := by
  cases xs
  simp
@@ -557,10 +551,6 @@ theorem toArray_toList {xs : Vector α n} : xs.toList.toArray = xs.toArray := rf
    xs.toList.sum = xs.sum := by
  rw [← toList_toArray, Array.sum_toList, sum_toArray]

-@[simp, grind =] theorem prod_toList [Mul α] [One α] {xs : Vector α n} :
-    xs.toList.prod = xs.prod := by
-  rw [← toList_toArray, Array.prod_toList, prod_toArray]
-
@[simp] theorem getElem_toList {xs : Vector α n} {i : Nat} (h : i < xs.toList.length) :
    xs.toList[i] = xs[i]'(by simpa using h) := by
  cases xs
@@ -3144,39 +3134,3 @@ theorem sum_eq_foldl [Zero α] [Add α]
    {xs : Vector α n} :
    xs.sum = xs.foldl (b := 0) (· + ·) := by
  simp [← sum_toList, List.sum_eq_foldl]
-
-/-! ### prod -/
-
-@[simp, grind =] theorem prod_empty [Mul α] [One α] : (#v[] : Vector α 0).prod = 1 := rfl
-theorem prod_eq_foldr [Mul α] [One α] {xs : Vector α n} :
-    xs.prod = xs.foldr (b := 1) (· * ·) :=
-  rfl
-
-@[simp, grind =]
-theorem prod_append [One α] [Mul α] [Std.Associative (α := α) (· * ·)]
-    [Std.LeftIdentity (α := α) (· * ·) 1] [Std.LawfulLeftIdentity (α := α) (· * ·) 1]
-    {as₁ as₂ : Vector α n} : (as₁ ++ as₂).prod = as₁.prod * as₂.prod := by
-  simp [← prod_toList, List.prod_append]
-
-@[simp, grind =]
-theorem prod_singleton [Mul α] [One α] [Std.LawfulRightIdentity (· * ·) (1 : α)] {x : α} :
-    #v[x].prod = x := by
-  simp [← prod_toList, Std.LawfulRightIdentity.right_id x]
-
-@[simp, grind =]
-theorem prod_push [Mul α] [One α] [Std.Associative (α := α) (· * ·)]
-    [Std.LawfulIdentity (· * ·) (1 : α)] {xs : Vector α n} {x : α} :
-    (xs.push x).prod = xs.prod * x := by
-  simp [← prod_toArray]
-
-@[simp, grind =]
-theorem prod_reverse [One α] [Mul α] [Std.Associative (α := α) (· * ·)]
-    [Std.Commutative (α := α) (· * ·)]
-    [Std.LawfulLeftIdentity (α := α) (· * ·) 1] (xs : Vector α n) : xs.reverse.prod = xs.prod := by
-  simp [← prod_toList, List.prod_reverse]
-
-theorem prod_eq_foldl [One α] [Mul α]
-    [Std.Associative (α := α) (· * ·)] [Std.LawfulIdentity (· * ·) (1 : α)]
-    {xs : Vector α n} :
-    xs.prod = xs.foldl (b := 1) (· * ·) := by
-  simp [← prod_toList, List.prod_eq_foldl]
--- a/src/Init/Data/Vector/Nat.lean
+++ b/src/Init/Data/Vector/Nat.lean
@@ -37,23 +37,4 @@ theorem sum_reverse_nat (xs : Vector Nat n) : xs.reverse.sum = xs.sum := by
 theorem sum_eq_foldl_nat {xs : Vector Nat n} : xs.sum = xs.foldl (b := 0) (· + ·) := by
  simp only [foldl_eq_foldr_reverse, Nat.add_comm, ← sum_eq_foldr, sum_reverse_nat]

-protected theorem prod_pos_iff_forall_pos_nat {xs : Vector Nat n} : 0 < xs.prod ↔ ∀ x ∈ xs, 0 < x := by
-  simp [← prod_toArray, Array.prod_pos_iff_forall_pos_nat]
-
-protected theorem prod_eq_zero_iff_exists_zero_nat {xs : Vector Nat n} :
-    xs.prod = 0 ↔ ∃ x ∈ xs, x = 0 := by
-  simp [← prod_toArray, Array.prod_eq_zero_iff_exists_zero_nat]
-
-@[simp] theorem prod_replicate_nat {n : Nat} {a : Nat} : (replicate n a).prod = a ^ n := by
-  simp [← prod_toArray, Array.prod_replicate_nat]
-
-theorem prod_append_nat {as₁ as₂ : Vector Nat n} : (as₁ ++ as₂).prod = as₁.prod * as₂.prod := by
-  simp [← prod_toArray]
-
-theorem prod_reverse_nat (xs : Vector Nat n) : xs.reverse.prod = xs.prod := by
-  simp [prod_reverse]
-
-theorem prod_eq_foldl_nat {xs : Vector Nat n} : xs.prod = xs.foldl (b := 1) (· * ·) := by
-  simp only [foldl_eq_foldr_reverse, Nat.mul_comm, ← prod_eq_foldr, prod_reverse_nat]
-
 end Vector
--- a/src/Init/System/IO.lean
+++ b/src/Init/System/IO.lean
@@ -1880,12 +1880,3 @@ lead to undefined behavior.
 -/
@[extern "lean_runtime_forget"]
 def Runtime.forget (a : α) : BaseIO Unit := return
-
-set_option linter.unusedVariables false in
-/--
-Ensures `a` remains at least alive until the call site by holding a reference to `a`. This can be useful
-for unsafe code (such as an FFI) that relies on a Lean object not being freed until after some point
-in the program. At runtime, this will be a no-op as the C compiler will optimize away this call.
-/
-@[extern "lean_runtime_hold"]
-def Runtime.hold (a : @& α) : BaseIO Unit := return
--- a/src/Lean/Compiler/LCNF/InferBorrow.lean
+++ b/src/Lean/Compiler/LCNF/InferBorrow.lean
@@ -67,7 +67,7 @@ structure ParamMap where
  The set of fvars that were already annotated as borrowed before arriving at this pass. We try to
  preserve the annotations here if possible.
  -/
-  annotatedBorrows : Std.HashSet FVarId := {}
+  annoatedBorrows : Std.HashSet FVarId := {}

 namespace ParamMap

@@ -95,7 +95,7 @@ where
        modify fun m =>
          { m with
            map := m.map.insert (.decl decl.name) (initParamsIfNotExported exported decl.params),
-            annotatedBorrows := decl.params.foldl (init := m.annotatedBorrows) fun acc p =>
+            annoatedBorrows := decl.params.foldl (init := m.annoatedBorrows) fun acc p =>
              if p.borrow then acc.insert p.fvarId else acc
          }
        goCode decl.name code
@@ -116,7 +116,7 @@ where
      modify fun m =>
        { m with
          map := m.map.insert (.jp declName decl.fvarId) (initParams decl.params),
-          annotatedBorrows := decl.params.foldl (init := m.annotatedBorrows) fun acc p =>
+          annoatedBorrows := decl.params.foldl (init := m.annoatedBorrows) fun acc p =>
            if p.borrow then acc.insert p.fvarId else acc
        }
      goCode declName decl.value
@@ -286,7 +286,7 @@ where

  ownFVar (fvarId : FVarId) (reason : OwnReason) : InferM Unit := do
    unless (← get).owned.contains fvarId do
-      if !reason.isForced && (← get).paramMap.annotatedBorrows.contains fvarId then
+      if !reason.isForced && (← get).paramMap.annoatedBorrows.contains fvarId then
        trace[Compiler.inferBorrow] "user annotation blocked owning {← PP.run <| PP.ppFVar fvarId}: {← reason.toString}"
      else
        trace[Compiler.inferBorrow] "own {← PP.run <| PP.ppFVar fvarId}: {← reason.toString}"
--- a/src/Lean/CoreM.lean
+++ b/src/Lean/CoreM.lean
@@ -446,6 +446,24 @@ Note that the value of `ctx.initHeartbeats` is ignored and replaced with `IO.get
@[inline] def CoreM.toIO' (x : CoreM α) (ctx : Context) (s : State) : IO α :=
  (·.1) <$> x.toIO ctx s

+/--
+Record a check-in for the `LEAN_CHECK_SYSTEM_INTERVAL_MS` monitoring.
+When that env var is set, warns on stderr if too much CPU time has elapsed since
+the last check-in from either the C++ `check_system` or this function.
+-/
+@[extern "lean_check_system_interval"]
+private opaque checkSystemIntervalImpl (componentName : @& String) : BaseIO Unit
+
+@[extern "lean_check_system_interval_is_enabled"]
+private opaque checkSystemIntervalIsEnabled : Unit → Bool
+
+private builtin_initialize checkSystemIntervalEnabled : Bool ←
+  pure (checkSystemIntervalIsEnabled ())
+
+@[inline] def checkSystemInterval (componentName : @& String) : BaseIO Unit := do
+  if checkSystemIntervalEnabled then
+    checkSystemIntervalImpl componentName
+
 /--
 Throws an internal interrupt exception if cancellation has been requested. The exception is not
 caught by `try catch` but is intended to be caught by `Command.withLoggingExceptions` at the top
@@ -456,6 +474,7 @@ Like `checkSystem` but without the global heartbeat check, for callers that have
 heartbeat tracking (e.g. `SynthInstance`).
 -/
@[inline] def checkInterrupted : CoreM Unit := do
+  checkSystemInterval "Lean elaborator"
  if let some tk := (← read).cancelTk? then
    if (← tk.isSet) then
      throwInterruptException
--- a/src/Lean/Elab/Deriving/Basic.lean
+++ b/src/Lean/Elab/Deriving/Basic.lean
@@ -233,41 +233,27 @@ def processDefDeriving (view : DerivingClassView) (decl : Expr) (isNoncomputable
        finally
          Core.setMessageLog (msgLog ++ (← Core.getMessageLog))
  let env ← getEnv
-  let isPropType ← isProp result.type
-  if isPropType then
-    let decl ← mkThmOrUnsafeDef {
-      name := instName, levelParams := result.levelParams.toList,
-      type := result.type, value := result.value
-    }
-    addDecl decl
+  let hints := ReducibilityHints.regular (getMaxHeight env result.value + 1)
+  let decl ← mkDefinitionValInferringUnsafe instName result.levelParams.toList result.type result.value hints
+  -- Pre-check: if the instance value depends on noncomputable definitions and the user didn't write
+  -- `noncomputable`, give an actionable error with a `Try this:` suggestion.
+  unless isNoncomputable || (← read).isNoncomputableSection || (← isProp result.type) do
+    let noncompRef? := preNormValue.foldConsts none fun n acc =>
+      acc <|> if Lean.isNoncomputable (asyncMode := .local) env n then some n else none
+    if let some noncompRef := noncompRef? then
+      if let some cmdRef := cmdRef? then
+        if let some origText := cmdRef.reprint then
+          let newText := (origText.replace "deriving instance " "deriving noncomputable instance ").trimAscii
+          logInfoAt cmdRef m!"Try this: {newText}"
+      throwError "failed to derive instance because it depends on \
+        `{.ofConstName noncompRef}`, which is noncomputable"
+  if isNoncomputable || (← read).isNoncomputableSection then
+    addDecl <| Declaration.defnDecl decl
+    modifyEnv (addNoncomputable · instName)
  else
-    let hints := ReducibilityHints.regular (getMaxHeight env result.value + 1)
-    let decl ← mkDefinitionValInferringUnsafe instName result.levelParams.toList result.type result.value hints
-    -- Pre-check: if the instance value depends on noncomputable definitions and the user didn't write
-    -- `noncomputable`, give an actionable error with a `Try this:` suggestion.
-    unless isNoncomputable || (← read).isNoncomputableSection do
-      let noncompRef? := preNormValue.foldConsts none fun n acc =>
-        acc <|> if Lean.isNoncomputable (asyncMode := .local) env n then some n else none
-      if let some noncompRef := noncompRef? then
-        if let some cmdRef := cmdRef? then
-          if let some origText := cmdRef.reprint then
-            let newText := (origText.replace "deriving instance " "deriving noncomputable instance ").trimAscii
-            logInfoAt cmdRef m!"Try this: {newText}"
-        throwError "failed to derive instance because it depends on \
-          `{.ofConstName noncompRef}`, which is noncomputable"
-    if isNoncomputable || (← read).isNoncomputableSection then
-      addDecl <| Declaration.defnDecl decl
-      modifyEnv (addNoncomputable · instName)
-    else
-      addAndCompile <| Declaration.defnDecl decl
+    addAndCompile <| Declaration.defnDecl decl
  trace[Elab.Deriving] "Derived instance `{.ofConstName instName}`"
-  -- For Prop-typed instances (theorems), skip `implicit_reducible` since reducibility hints are
-  -- irrelevant for theorems. This matches the behavior of the handwritten `instance` command
-  -- (see `MutualDef.lean`).
-  if isPropType then
-    addInstance instName AttributeKind.global (eval_prio default)
-  else
-    registerInstance instName AttributeKind.global (eval_prio default)
+  registerInstance instName AttributeKind.global (eval_prio default)
  addDeclarationRangesFromSyntax instName (← getRef)

 end Term
--- a/src/Lean/Linter.lean
+++ b/src/Lean/Linter.lean
@@ -18,4 +18,3 @@ public import Lean.Linter.List
 public import Lean.Linter.Sets
 public import Lean.Linter.UnusedSimpArgs
 public import Lean.Linter.Coe
-public import Lean.Linter.GlobalAttributeIn
--- a/src/Lean/Linter/GlobalAttributeIn.lean
+++ b/src/Lean/Linter/GlobalAttributeIn.lean
@@ -1,59 +0,0 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Wojciech Różowski
-/
-module
-
-prelude
-public import Lean.Elab.Command
-public import Lean.Linter.Basic
-
-
-namespace Lean.Linter
-open Elab.Command
-
-private structure TopDownSkipQuot where
-  stx : Syntax
-
-def topDownSkipQuot (stx : Syntax) : TopDownSkipQuot := ⟨stx⟩
-
-partial instance [Monad m] : ForIn m TopDownSkipQuot Syntax where
-  forIn := fun ⟨stx⟩ init f => do
-    let rec @[specialize] loop stx b [Inhabited (type_of% b)] := do
-      if stx.isQuot then return ForInStep.yield b
-      match (← f stx b) with
-      | ForInStep.yield b' =>
-        let mut b := b'
-        if let Syntax.node _ _ args := stx then
-          for arg in args do
-            match (← loop arg b) with
-            | ForInStep.yield b' => b := b'
-            | ForInStep.done b'  => return ForInStep.done b'
-        return ForInStep.yield b
-      | ForInStep.done b => return ForInStep.done b
-    match (← @loop stx init ⟨init⟩) with
-    | ForInStep.yield b => return b
-    | ForInStep.done b  => return b
-
-def getGlobalAttributesIn? : Syntax → Option (Ident × Array (TSyntax `attr))
-  | `(attribute [$x,*] $id in $_) =>
-    let xs := x.getElems.filterMap fun a => match a.raw with
-      | `(Parser.Command.eraseAttr| -$_) => none
-      | `(Parser.Term.attrInstance| local $_attr:attr) => none
-      | `(Parser.Term.attrInstance| scoped $_attr:attr) => none
-      | `(attr| $a) => some a
-    (id, xs)
-  | _ => default
-
-def globalAttributeIn : Linter where run := withSetOptionIn fun stx => do
-  for s in topDownSkipQuot stx do
-    if let some (id, nonScopedNorLocal) := getGlobalAttributesIn? s then
-      for attr in nonScopedNorLocal do
-        logErrorAt attr
-          m!"Despite the `in`, the attribute {attr} is added globally to {id}\n\
-          please remove the `in` or make this a `local {attr}`"
-
-builtin_initialize addLinter globalAttributeIn
-
-end Lean.Linter
--- a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
+++ b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
@@ -242,6 +242,7 @@ def ppSimpTheorem [Monad m] [MonadEnv m] [MonadError m] (s : SimpTheorem) : m Me
 instance : BEq SimpTheorem where
  beq e₁ e₂ := e₁.proof == e₂.proof

+
 /--
 Configuration for `MetaM` used to process global simp theorems
 -/
@@ -255,6 +256,8 @@ def simpGlobalConfig : ConfigWithKey :=
@[inline] def withSimpGlobalConfig : MetaM α → MetaM α :=
  withConfigWithKey simpGlobalConfig

+
+
 private partial def isPerm : Expr → Expr → MetaM Bool
  | .app f₁ a₁, .app f₂ a₂ => isPerm f₁ f₂ <&&> isPerm a₁ a₂
  | .mdata _ s, t => isPerm s t
@@ -367,32 +370,11 @@ private def mkSimpTheoremKeys (type : Expr) (noIndexAtArgs : Bool) : MetaM (Arra
    | some (_, lhs, rhs) => pure (← DiscrTree.mkPath lhs noIndexAtArgs, ← isPerm lhs rhs)
    | none => throwError "Unexpected kind of simp theorem{indentExpr type}"

-register_builtin_option simp.rfl.checkTransparency: Bool := {
-  defValue := false
-  descr    := "if true, Lean generates a warning if the left and right-hand sides of the `[simp]` equation are not definitionally equal at the restricted transparency level used by `simp` "
-}
-
-private def mkSimpTheoremCore (origin : Origin) (e : Expr) (levelParams : Array Name) (proof : Expr)
-    (post : Bool) (prio : Nat) (noIndexAtArgs : Bool) : MetaM SimpTheorem := do
+private def mkSimpTheoremCore (origin : Origin) (e : Expr) (levelParams : Array Name) (proof : Expr) (post : Bool) (prio : Nat) (noIndexAtArgs : Bool) : MetaM SimpTheorem := do
  assert! origin != .fvar ⟨.anonymous⟩
  let type ← instantiateMVars (← inferType e)
  let (keys, perm) ← mkSimpTheoremKeys type noIndexAtArgs
-  let rfl ← isRflProof proof
-  if rfl && simp.rfl.checkTransparency.get (← getOptions) then
-    forallTelescopeReducing type fun _ type => do
-      let checkDefEq (lhs rhs : Expr) := do
-        unless (← withTransparency .instances <| isDefEq lhs rhs) do
-          logWarning m!"`{origin.key}` is a `rfl` simp theorem, but its left-hand side{indentExpr lhs}\n\
-            is not definitionally equal to the right-hand side{indentExpr rhs}\n\
-            at `.instances` transparency. Possible solutions:\n\
-            1- use `id rfl` as the proof\n\
-            2- mark constants occurring in the lhs and rhs as `[implicit_reducible]`"
-      match_expr type with
-      | Eq _ lhs rhs => checkDefEq lhs rhs
-      | Iff lhs rhs => checkDefEq lhs rhs
-      | _ =>
-        logWarning m!"'{origin.key}' is a 'rfl' simp theorem, unexpected resulting type{indentExpr type}"
-  return { origin, keys, perm, post, levelParams, proof, priority := prio, rfl }
+  return { origin, keys, perm, post, levelParams, proof, priority := prio, rfl := (← isRflProof proof) }

 /--
 Creates a `SimpTheorem` from a global theorem.
--- a/src/include/lean/lean.h
+++ b/src/include/lean/lean.h
@@ -3168,10 +3168,6 @@ static inline lean_obj_res lean_manual_get_root(lean_obj_arg _unit) {
    return lean_mk_string(LEAN_MANUAL_ROOT);
 }

-static inline lean_obj_res lean_runtime_hold(b_lean_obj_arg a) {
-    return lean_box(0);
-}
-
 #ifdef LEAN_EMSCRIPTEN
 #define LEAN_SCALAR_PTR_LITERAL(b1, b2, b3, b4, b5, b6, b7, b8) (lean_object*)((uint32_t)b1 | ((uint32_t)b2 << 8) | ((uint32_t)b3 << 16) | ((uint32_t)b4 << 24)), (lean_object*)((uint32_t)b5 | ((uint32_t)b6 << 8) | ((uint32_t)b7 << 16) | ((uint32_t)b8 << 24))
 #else
--- a/src/lake/Lake/Build/InitFacets.lean
+++ b/src/lake/Lake/Build/InitFacets.lean
@@ -19,7 +19,7 @@ import Lake.Build.InputFile
 namespace Lake

 /-- The initial set of Lake facets. -/
-public def initFacetConfigs : FacetConfigMap :=
+public def initFacetConfigs : DNameMap FacetConfig :=
  DNameMap.empty
  |> insert Module.initFacetConfigs
  |> insert Package.initFacetConfigs
@@ -30,4 +30,4 @@ public def initFacetConfigs : FacetConfigMap :=
  |> insert InputDir.initFacetConfigs
 where
  insert {k} (group : DNameMap (KFacetConfig k)) map :=
-    group.foldl (init := map) fun m _ v => m.insert v.toFacetConfig
+    group.foldl (init := map) fun m k v => m.insert k v.toFacetConfig
--- a/src/lake/Lake/Config/FacetConfig.lean
+++ b/src/lake/Lake/Config/FacetConfig.lean
@@ -27,20 +27,6 @@ public structure FacetConfig (name : Name) : Type where
  memoize : Bool := true
  deriving Inhabited

-/-- A mapping of facet names to the configuration for that name. -/
-public abbrev FacetConfigMap := DNameMap FacetConfig
-
-/--
-Tries to retrieve the facet configuration for the given {lean}`name`,
-returning {lean}`none` if no such mapping is present.
-/
-public nonrec def FacetConfigMap.get? (name : Name) (self : FacetConfigMap) : Option (FacetConfig name) :=
-  self.get? name -- specializes `get?`
-
-/-- Inserts the facet configuration {lean}`cfg` into the map (overwriting any existing configuration). -/
-public nonrec def FacetConfigMap.insert {name} (cfg : FacetConfig name) (self : FacetConfigMap) : FacetConfigMap :=
-  self.insert name cfg -- specializes `insert`
-
 public protected abbrev FacetConfig.name (_ : FacetConfig name) := name

 public structure KFacetConfig (k : Name) (name : Name) extends FacetConfig name where
@@ -84,9 +70,6 @@ public structure NamedConfigDecl (β : Name → Type u) where
  name : Name
  config : β name

-/-- A facet declaration from a configuration file. -/
-public abbrev FacetDecl := NamedConfigDecl FacetConfig
-
 /-- A module facet's declarative configuration. -/
 public abbrev ModuleFacetConfig := KFacetConfig Module.facetKind

--- a/src/lake/Lake/Config/LakefileConfig.lean
+++ b/src/lake/Lake/Config/LakefileConfig.lean
@@ -1,53 +0,0 @@
-/-
-Copyright (c) 2025 Mac Malone. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mac Malone
-/
-module
-
-prelude
-public import Lake.Config.Script
-public import Lake.Config.Dependency
-public import Lake.Config.PackageConfig
-public import Lake.Config.FacetConfig
-public import Lake.Config.TargetConfig
-
-set_option doc.verso true
-
-open Lean
-
-namespace Lake
-
-/-- The configuration defined by a Lake configuration file (e.g., {lit}`lakefile.(lean|toml)`). -/
-public structure LakefileConfig where
-  /-- The package deceleration of the configuration file. -/
-  pkgDecl : PackageDecl
-  /-- Depdency configurations in the order declared by the configuration file.  -/
-  depConfigs : Array Dependency := #[]
-  /-- Facet configurations in the order declared by the configuration file. -/
-  facetDecls : Array FacetDecl := {}
-  /-- Target configurations in the order declared by the configuration file. -/
-  targetDecls : Array (PConfigDecl pkgDecl.keyName) := #[]
-  /-- Name-declaration map of target configurations declared in the configuration file. -/
-  targetDeclMap : DNameMap (NConfigDecl pkgDecl.keyName) :=
-    targetDecls.foldl (fun m d => m.insert d.name (.mk d rfl)) {}
-  /-- The names of targets declared via {lit}`@[default_target]`. -/
-  defaultTargets : Array Name := #[]
-  /-- Scripts declared in the configuration file. -/
-  scripts : NameMap Script := {}
-  /-- The names of the scripts declared via {lit}`@[default_script]`. -/
-  defaultScripts : Array Script := #[]
-  /-- {lit}`post_update` hooks in the order declared by the configuration file.. -/
-  postUpdateHooks : Array (OpaquePostUpdateHook pkgDecl.keyName) := #[]
-  /--
-  The name of the configuration file's test driver.
-
-  It is either  declared via {lit}`@[test_driver]` or derived from {lean}`PackageConfig.testDriver`.
-  -/
-  testDriver : String := pkgDecl.config.testDriver
-  /--
-  The name of the configuration file's test driver.
-
-  It is either declared via {lit}`@[lint_driver]` or derived from {lean}`PackageConfig.lintDriver`.
-  -/
-  lintDriver : String := pkgDecl.config.lintDriver
--- a/src/lake/Lake/Config/Package.lean
+++ b/src/lake/Lake/Config/Package.lean
@@ -45,7 +45,7 @@ public structure Package where
  /-- The path to the package's configuration file (relative to `dir`). -/
  relConfigFile : FilePath
  /-- The path to the package's JSON manifest of remote dependencies (relative to `dir`). -/
-  relManifestFile : FilePath
+  relManifestFile : FilePath := defaultManifestFile
  /-- The package's scope (e.g., in Reservoir). -/
  scope : String
  /-- The URL to this package's Git remote. -/
--- a/src/lake/Lake/Config/PackageConfig.lean
+++ b/src/lake/Lake/Config/PackageConfig.lean
@@ -336,16 +336,11 @@ public configuration PackageConfig (p : Name) (n : Name) extends WorkspaceConfig
 deriving Inhabited

 /-- The package's name as specified by the author. -/
-@[deprecated "Deprecated without replacement" (since := "2025-12-10")]
 public abbrev PackageConfig.origName (_ : PackageConfig p n) := n

 /-- A package declaration from a configuration written in Lean. -/
 public structure PackageDecl where
-  baseName : Name
-  keyName : Name
+  name : Name
  origName : Name
-  config : PackageConfig keyName origName
+  config : PackageConfig name origName
  deriving TypeName
-
-@[deprecated PackageDecl.keyName (since := "2025-12-10")]
-public abbrev PackageDecl.name := @keyName
--- a/src/lake/Lake/Config/Workspace.lean
+++ b/src/lake/Lake/Config/Workspace.lean
@@ -22,17 +22,15 @@ open Lean (Name LeanOptions)

 namespace Lake

-/--
-**For internal use only.**
-Computes the cache to use for the package based on the environment.
-/
+/-- **For internal use only.** Computes the cache to use for the package based on the environment. -/
 public def computeLakeCache (pkg : Package) (lakeEnv : Lake.Env) : Cache :=
  if pkg.bootstrap then
    lakeEnv.lakeSystemCache?.getD ⟨pkg.lakeDir / "cache"⟩
  else
    lakeEnv.lakeCache?.getD ⟨pkg.lakeDir / "cache"⟩

-public structure Workspace.Raw : Type where
+/-- A Lake workspace -- the top-level package directory. -/
+public structure Workspace : Type where
  /-- The root package of the workspace. -/
  root : Package
  /-- The detected {lean}`Lake.Env` of the workspace. -/
@@ -51,25 +49,14 @@ public structure Workspace.Raw : Type where
  The packages within the workspace
  (in {lit}`require` declaration order with the root coming first).
  -/
-  packages : Array Package := #[]
+  packages : Array Package := {}
  /-- Name-package map of packages within the workspace. -/
  packageMap : DNameMap NPackage := {}
  /-- Configuration map of facets defined in the workspace. -/
-  facetConfigs : FacetConfigMap := {}
-  deriving Nonempty
+  facetConfigs : DNameMap FacetConfig := {}

-public structure Workspace.Raw.WF (ws : Workspace.Raw) : Prop where
-  packages_wsIdx : ∀ (h : i < ws.packages.size), (ws.packages[i]'h).wsIdx = i
-
-/-- A Lake workspace -- the top-level package directory. -/
-public structure Workspace extends raw : Workspace.Raw, wf : raw.WF
-
-public instance : Nonempty Workspace := .intro {
-  lakeEnv := default
-  lakeConfig := Classical.ofNonempty
-  root := Classical.ofNonempty
-  packages_wsIdx h := by simp at h
-}
+public instance : Nonempty Workspace :=
+  ⟨by constructor <;> exact Classical.ofNonempty⟩

 public hydrate_opaque_type OpaqueWorkspace Workspace

@@ -188,20 +175,9 @@ This is configured through {lit}`cache.service` entries in the system Lake confi
@[inline] public def packageOverridesFile (self : Workspace) : FilePath :=
  self.lakeDir / "package-overrides.json"

-/-- **For internal use only.** Add a well-formed package to the workspace. -/
-@[inline] public def addPackage' (pkg : Package) (self : Workspace) (h : pkg.wsIdx = self.packages.size) : Workspace :=
-  {self with
-    packages := self.packages.push pkg
-    packageMap := self.packageMap.insert pkg.keyName pkg
-    packages_wsIdx {i} i_lt := by
-      cases Nat.lt_add_one_iff_lt_or_eq.mp <| Array.size_push .. ▸ i_lt with
-      | inl i_lt => simpa [Array.getElem_push_lt i_lt] using self.packages_wsIdx i_lt
-      | inr i_eq => simpa [i_eq] using h
-  }
-
 /-- Add a package to the workspace. -/
-@[inline] public def addPackage (pkg : Package) (self : Workspace) : Workspace :=
-  self.addPackage' {pkg with wsIdx := self.packages.size} rfl
+public def addPackage (pkg : Package) (self : Workspace) : Workspace :=
+  {self with packages := self.packages.push pkg, packageMap := self.packageMap.insert pkg.keyName pkg}

 /-- Returns the unique package in the workspace (if any) that is identified by  {lean}`keyName`. -/
@[inline] public protected def findPackageByKey? (keyName : Name) (self : Workspace) : Option (NPackage keyName) :=
@@ -275,15 +251,15 @@ public def findTargetDecl? (name : Name) (self : Workspace) : Option ((pkg : Pac
  self.packages.findSome? fun pkg => pkg.findTargetDecl? name <&> (⟨pkg, ·⟩)

 /-- Add a facet to the workspace. -/
-@[inline] public def addFacetConfig {name} (cfg : FacetConfig name) (self : Workspace) : Workspace :=
-  {self with facetConfigs := self.facetConfigs.insert cfg}
+public def addFacetConfig {name} (cfg : FacetConfig name) (self : Workspace) : Workspace :=
+  {self with facetConfigs := self.facetConfigs.insert name cfg}

 /-- Try to find a facet configuration in the workspace with the given name. -/
-@[inline] public def findFacetConfig? (name : Name) (self : Workspace) : Option (FacetConfig name) :=
+public def findFacetConfig? (name : Name) (self : Workspace) : Option (FacetConfig name) :=
  self.facetConfigs.get? name

 /-- Add a module facet to the workspace. -/
-@[inline] public def addModuleFacetConfig (cfg : ModuleFacetConfig name) (self : Workspace) : Workspace :=
+public def addModuleFacetConfig (cfg : ModuleFacetConfig name) (self : Workspace) : Workspace :=
  self.addFacetConfig cfg.toFacetConfig

 /-- Try to find a module facet configuration in the workspace with the given name. -/
@@ -291,7 +267,7 @@ public def findModuleFacetConfig? (name : Name) (self : Workspace) : Option (Mod
  self.findFacetConfig? name |>.bind (·.toKind? Module.facetKind)

 /-- Add a package facet to the workspace. -/
-@[inline] public def addPackageFacetConfig (cfg : PackageFacetConfig name) (self : Workspace) : Workspace :=
+public def addPackageFacetConfig (cfg : PackageFacetConfig name) (self : Workspace) : Workspace :=
  self.addFacetConfig cfg.toFacetConfig

 /-- Try to find a package facet configuration in the workspace with the given name. -/
@@ -299,7 +275,7 @@ public def findPackageFacetConfig? (name : Name) (self : Workspace) : Option (Pa
  self.findFacetConfig? name |>.bind (·.toKind? Package.facetKind)

 /-- Add a library facet to the workspace. -/
-@[inline] public def addLibraryFacetConfig (cfg : LibraryFacetConfig name) (self : Workspace) : Workspace :=
+public def addLibraryFacetConfig (cfg : LibraryFacetConfig name) (self : Workspace) : Workspace :=
  self.addFacetConfig cfg.toFacetConfig

 /-- Try to find a library facet configuration in the workspace with the given name. -/
--- a/src/lake/Lake/DSL/Package.lean
+++ b/src/lake/Lake/DSL/Package.lean
@@ -26,18 +26,17 @@ def elabPackageCommand : CommandElab := fun stx => do
  let configId : Ident ← `(pkgConfig)
  let id ← mkConfigDeclIdent nameStx?
  let origName := Name.quoteFrom id id.getId
-  let ⟨wsIdx, name⟩ := nameExt.getState (← getEnv)
-  let baseName := match name with
+  let ⟨idx, name⟩ := nameExt.getState (← getEnv)
+  let name := match name with
    | .anonymous => origName
    | name => Name.quoteFrom id name
-  let wsIdx := quote wsIdx
-  let keyName := Syntax.mkCApp ``Name.num #[baseName, wsIdx]
-  let ty := Syntax.mkCApp ``PackageConfig #[keyName, origName]
+  let name := Syntax.mkCApp ``Name.num #[name, quote idx]
+  let ty := Syntax.mkCApp ``PackageConfig #[name, origName]
  elabConfig ``PackageConfig configId ty cfg
  let attr ← `(Term.attrInstance| «package»)
  let attrs := #[attr] ++ expandAttrs attrs?
  let id := mkIdentFrom id packageDeclName
-  let decl ← `({baseName := $baseName, origName := $origName, keyName := $keyName, config := $configId})
+  let decl ← `({name := $name, origName := $origName, config := $configId})
  let cmd ← `($[$doc?]? @[$attrs,*] abbrev $id : PackageDecl := $decl)
  withMacroExpansion stx cmd <| elabCommand cmd
  let nameId := mkIdentFrom id <| packageDeclName.str "name"
--- a/src/lake/Lake/Load/Config.lean
+++ b/src/lake/Lake/Load/Config.lean
@@ -7,7 +7,6 @@ module

 prelude
 public import Lake.Config.Env
-public import Lake.Config.Lang
 public import Lake.Config.LakeConfig
 public import Lake.Load.Manifest

@@ -42,16 +41,8 @@ public structure LoadConfig where
  pkgDir : FilePath := wsDir / relPkgDir
  /-- The package's Lake configuration file (relative to its directory). -/
  relConfigFile : FilePath := defaultConfigFile
-  /-- The full path to the loaded package's Lake configuration file. -/
+    /-- The full path to the loaded package's Lake configuration file. -/
  configFile : FilePath := pkgDir / relConfigFile
-  /-
-  The format of the package's configuration file.
-
-  If {lean}`none`, the format will be determined by the file's extension.
-  -/
-  configLang? : Option ConfigLang := none
-  /-- The package's Lake manifest file (relative to its directory). -/
-  relManifestFile : FilePath := defaultManifestFile
  /-- Additional package overrides for this workspace load. -/
  packageOverrides : Array PackageEntry := #[]
  /-- A set of key-value Lake configuration options (i.e., {lit}`-K` settings). -/
@@ -64,7 +55,6 @@ public structure LoadConfig where
  updateDeps : Bool := false
  /--
  Whether to update the workspace's {lit}`lean-toolchain` when dependencies are updated.
-
  If {lean}`true` and a toolchain update occurs, Lake will need to be restarted.
  -/
  updateToolchain : Bool := true
--- a/src/lake/Lake/Load/Lean.lean
+++ b/src/lake/Lake/Load/Lean.lean
@@ -7,7 +7,6 @@ module

 prelude
 public import Lake.Config.Package
-public import Lake.Config.LakefileConfig
 public import Lake.Load.Config
 import Lake.Load.Lean.Elab
 import Lake.Load.Lean.Eval
@@ -22,7 +21,22 @@ open Lean

 namespace Lake

-/-- Elaborate a Lake configuration file written in Lean and extract the Lake configuration.  -/
-public def loadLeanConfig  (cfg : LoadConfig) : LogIO LakefileConfig := do
+/--
+Elaborate a Lean configuration file into a `Package`.
+The resulting package does not yet include any dependencies.
+-/
+public def loadLeanConfig (cfg : LoadConfig) : LogIO (Package × Environment) := do
  let configEnv ← importConfigFile cfg
-  LakefileConfig.loadFromEnv configEnv cfg.leanOpts
+  let ⟨keyName, origName, config⟩ ← IO.ofExcept <| PackageDecl.loadFromEnv configEnv cfg.leanOpts
+  let baseName := if cfg.pkgName.isAnonymous then origName else cfg.pkgName
+  let pkg : Package := {
+    wsIdx := cfg.pkgIdx
+    baseName, keyName, origName, config
+    dir := cfg.pkgDir
+    relDir := cfg.relPkgDir
+    configFile := cfg.configFile
+    relConfigFile := cfg.relConfigFile
+    scope := cfg.scope
+    remoteUrl := cfg.remoteUrl
+  }
+  return (← pkg.loadFromEnv configEnv cfg.leanOpts, configEnv)
--- a/src/lake/Lake/Load/Lean/Eval.lean
+++ b/src/lake/Lake/Load/Lean/Eval.lean
@@ -7,7 +7,6 @@ module

 prelude
 public import Lake.Config.Workspace
-public import Lake.Config.LakefileConfig
 import Lean.DocString
 import Lake.DSL.AttributesCore

@@ -76,38 +75,39 @@ private def mkOrdTagMap
    return map.insert declName <| ← f declName

 /-- Load a `PackageDecl` from a configuration environment. -/
-private def PackageDecl.loadFromEnv
+public def PackageDecl.loadFromEnv
  (env : Environment) (opts := Options.empty)
 : Except String PackageDecl := do
  let declName ←
    match packageAttr.getAllEntries env |>.toList with
    | [] => error s!"configuration file is missing a `package` declaration"
-    | [keyName] => pure keyName
+    | [name] => pure name
    | _ => error s!"configuration file has multiple `package` declarations"
  evalConstCheck env opts _ declName

-/-- Load a Lake configuration from a configuration file's environment. -/
-public def LakefileConfig.loadFromEnv
-  (env : Environment) (opts : Options)
-: LogIO LakefileConfig := do
-
-  -- load package declaration
-  let pkgDecl ← IO.ofExcept <| PackageDecl.loadFromEnv env opts
-  let prettyName := pkgDecl.baseName.toString (escape := false)
-  let keyName := pkgDecl.keyName
+/--
+Load the optional elements of a `Package` from the Lean environment.
+This is done after loading its core configuration but before resolving
+its dependencies.
+-/
+public def Package.loadFromEnv
+  (self : Package) (env : Environment) (opts : Options)
+: LogIO Package := do

  -- load target, script, hook, and driver configurations
  let constTargetMap ← IO.ofExcept <| mkOrdTagMap env targetAttr fun name => do
    evalConstCheck env opts ConfigDecl name
  let targetDecls ← constTargetMap.toArray.mapM fun decl => do
-    if h : decl.pkg = keyName then
+    if h : decl.pkg = self.keyName then
      return .mk decl h
    else
-      error s!"target '{decl.name}' was defined in package '{decl.pkg}', \
-        but registered under '{keyName}'"
+      error s!"\
+        target '{decl.name}' was defined in package '{decl.pkg}', \
+        but registered under '{self.keyName}'"
  let targetDeclMap ← targetDecls.foldlM (init := {}) fun m decl => do
    if let some orig := m.get? decl.name then
-      error s!"{prettyName}: target '{decl.name}' was already defined as a '{orig.kind}', \
+      error s!"\
+        {self.prettyName}: target '{decl.name}' was already defined as a '{orig.kind}', \
        but then redefined as a '{decl.kind}'"
    else
      return m.insert decl.name (.mk decl rfl)
@@ -116,7 +116,8 @@ public def LakefileConfig.loadFromEnv
    if let some exeConfig := decl.config? LeanExe.configKind then
      let root := exeConfig.root
      if let some origExe := exeRoots.get? root then
-        error s!"{prettyName}: executable '{decl.name}' has the same root module '{root}' \
+        error s!"\
+          {self.prettyName}: executable '{decl.name}' has the same root module '{root}' \
          as executable '{origExe}'"
      else
        return exeRoots.insert root decl.name
@@ -124,78 +125,80 @@ public def LakefileConfig.loadFromEnv
      return exeRoots
  let defaultTargets ← defaultTargetAttr.getAllEntries env |>.mapM fun name =>
    if let some decl := constTargetMap.find? name then pure decl.name else
-      error s!"{prettyName}: package is missing target '{name}' marked as a default"
+      error s!"{self.prettyName}: package is missing target '{name}' marked as a default"
  let scripts ← mkTagMap env scriptAttr fun scriptName => do
-    let name := prettyName ++ "/" ++ scriptName.toString (escape := false)
+    let name := self.prettyName ++ "/" ++ scriptName.toString (escape := false)
    let fn ← IO.ofExcept <| evalConstCheck env opts ScriptFn scriptName
    return {name, fn, doc? := ← findDocString? env scriptName : Script}
  let defaultScripts ← defaultScriptAttr.getAllEntries env |>.mapM fun name =>
    if let some script := scripts.get? name then pure script else
-      error s!"{prettyName}: package is missing script '{name}' marked as a default"
+      error s!"{self.prettyName}: package is missing script '{name}' marked as a default"
  let postUpdateHooks ← postUpdateAttr.getAllEntries env |>.mapM fun name =>
    match evalConstCheck env opts PostUpdateHookDecl name with
    | .ok decl =>
-      if h : decl.pkg = keyName then
-        return OpaquePostUpdateHook.mk ⟨cast (by rw [h]) decl.fn⟩
+      if h : decl.pkg = self.keyName then
+        return OpaquePostUpdateHook.mk ⟨cast (by rw [h, keyName]) decl.fn⟩
      else
-        error s!"post-update hook was defined in '{decl.pkg}', but was registered in '{keyName}'"
+        error s!"post-update hook was defined in '{decl.pkg}', but was registered in '{self.keyName}'"
    | .error e => error e
  let depConfigs ← IO.ofExcept <| packageDepAttr.getAllEntries env |>.mapM fun name =>
    evalConstCheck env opts Dependency name
  let testDrivers ← testDriverAttr.getAllEntries env |>.mapM fun name =>
    if let some decl := constTargetMap.find? name then
-      return decl.name
+      pure decl.name
    else if scripts.contains name then
-      return name
+      pure name
    else
-      error s!"{prettyName}: package is missing script or target '{name}' marked as a test driver"
-  let testDriver ← id do
+      error s!"{self.prettyName}: package is missing script or target '{name}' marked as a test driver"
+  let testDriver ←
    if testDrivers.size > 1 then
-      error s!"{prettyName}: only one script, executable, or library can be tagged @[test_driver]"
+      error s!"{self.prettyName}: only one script, executable, or library can be tagged @[test_driver]"
    else if h : testDrivers.size > 0 then
-      if pkgDecl.config.testDriver.isEmpty then
-        return (testDrivers[0]'h |>.toString)
+      if self.config.testDriver.isEmpty then
+        pure (testDrivers[0]'h |>.toString)
      else
-        error s!"{prettyName}: cannot both set testDriver and use @[test_driver]"
+        error s!"{self.prettyName}: cannot both set testDriver and use @[test_driver]"
    else
-      return pkgDecl.config.testDriver
+      pure self.config.testDriver
  let lintDrivers ← lintDriverAttr.getAllEntries env |>.mapM fun name =>
    if let some decl := constTargetMap.find? name then
-      return decl.name
+      pure decl.name
    else if scripts.contains name then
-      return name
+      pure name
    else
-      error s!"{prettyName}: package is missing script or target '{name}' marked as a lint driver"
-  let lintDriver ← id do
+      error s!"{self.prettyName}: package is missing script or target '{name}' marked as a lint driver"
+  let lintDriver ←
    if lintDrivers.size > 1 then
-      error s!"{prettyName}: only one script or executable can be tagged @[lint_driver]"
+      error s!"{self.prettyName}: only one script or executable can be tagged @[lint_driver]"
    else if h : lintDrivers.size > 0 then
-      if pkgDecl.config.lintDriver.isEmpty then
-        return (lintDrivers[0]'h |>.toString)
+      if self.config.lintDriver.isEmpty then
+        pure (lintDrivers[0]'h |>.toString)
      else
-        error s!"{prettyName}: cannot both set lintDriver and use @[lint_driver]"
+        error s!"{self.prettyName}: cannot both set lintDriver and use @[lint_driver]"
    else
-      return pkgDecl.config.lintDriver
-
-  -- load facets
-  let facetDecls ← IO.ofExcept do
-    let mut decls : Array FacetDecl := #[]
-    for name in moduleFacetAttr.getAllEntries env do
-      let decl ← evalConstCheck env opts ModuleFacetDecl name
-      decls :=  decls.push {decl with config := decl.config.toFacetConfig}
-    for name in packageFacetAttr.getAllEntries env do
-      let decl ← evalConstCheck env opts PackageFacetDecl name
-      decls := decls.push  {decl with config := decl.config.toFacetConfig}
-    for name in libraryFacetAttr.getAllEntries env do
-      let decl ← evalConstCheck env opts LibraryFacetDecl name
-      decls := decls.push  {decl with config := decl.config.toFacetConfig}
-    return decls
+      pure self.config.lintDriver

  -- Fill in the Package
-  return {
-    pkgDecl, depConfigs, facetDecls,
-    targetDecls, targetDeclMap, defaultTargets,
-    scripts, defaultScripts,
-    testDriver, lintDriver,
-    postUpdateHooks,
+  return {self with
+    depConfigs, targetDecls, targetDeclMap
+    defaultTargets, scripts, defaultScripts
+    testDriver, lintDriver,  postUpdateHooks
  }
+
+/--
+Load module/package facets into a `Workspace` from a configuration environment.
+-/
+public def Workspace.addFacetsFromEnv
+  (env : Environment) (opts : Options) (self : Workspace)
+: Except String Workspace := do
+  let mut ws := self
+  for name in moduleFacetAttr.getAllEntries env do
+    let decl ← evalConstCheck env opts ModuleFacetDecl name
+    ws := ws.addModuleFacetConfig decl.config
+  for name in packageFacetAttr.getAllEntries env do
+    let decl ← evalConstCheck env opts PackageFacetDecl name
+    ws := ws.addPackageFacetConfig decl.config
+  for name in libraryFacetAttr.getAllEntries env do
+    let decl ← evalConstCheck env opts LibraryFacetDecl name
+    ws := ws.addLibraryFacetConfig decl.config
+  return ws
--- a/src/lake/Lake/Load/Manifest.lean
+++ b/src/lake/Lake/Load/Manifest.lean
@@ -94,9 +94,6 @@ public structure PackageEntry where

 namespace PackageEntry

-@[inline] public def prettyName (entry : PackageEntry) : String :=
-  entry.name.toString (escape := false)
-
 public protected def toJson (entry : PackageEntry) : Json :=
  let fields := [
    ("name", toJson entry.name),
--- a/src/lake/Lake/Load/Materialize.lean
+++ b/src/lake/Lake/Load/Materialize.lean
@@ -10,7 +10,6 @@ public import Lake.Config.Env
 public import Lake.Load.Manifest
 public import Lake.Config.Package
 import Lake.Util.Git
-import Lake.Util.IO
 import Lake.Reservoir

 open System Lean
@@ -88,8 +87,6 @@ def materializeGitRepo
    cloneGitPkg name repo url rev?

 public structure MaterializedDep where
-  /-- Absolute path to the materialized package. -/
-  pkgDir : FilePath
  /-- Path to the materialized package relative to the workspace's root directory. -/
  relPkgDir : FilePath
  /--
@@ -108,31 +105,16 @@ namespace MaterializedDep
@[inline] public def name (self : MaterializedDep) : Name :=
  self.manifestEntry.name

-@[inline] public def prettyName (self : MaterializedDep) : String :=
-  self.manifestEntry.name.toString (escape := false)
-
@[inline] public def scope (self : MaterializedDep) : String :=
  self.manifestEntry.scope

-/-- Path to the dependency's manfiest file (relative to `relPkgDir`). -/
-@[inline] public def relManifestFile? (self : MaterializedDep) : Option FilePath :=
+/-- Path to the dependency's configuration file (relative to `relPkgDir`). -/
+@[inline] public def manifestFile? (self : MaterializedDep) : Option FilePath :=
  self.manifestEntry.manifestFile?

-/-- Path to the dependency's manfiest file (relative to `relPkgDir`). -/
-@[inline] public def relManifestFile (self : MaterializedDep) : FilePath :=
-  self.relManifestFile?.getD defaultManifestFile
-
-/-- Absolute path to the dependency's manfiest file. -/
-@[inline] public def manifestFile (self : MaterializedDep) : FilePath :=
-  self.pkgDir / self.relManifestFile
-
 /-- Path to the dependency's configuration file (relative to `relPkgDir`). -/
-@[inline] public def relConfigFile (self : MaterializedDep) : FilePath :=
-  self.manifestEntry.configFile
-
-/-- Absolute path to the dependency's configuration file. -/
@[inline] public def configFile (self : MaterializedDep) : FilePath :=
-  self.pkgDir / self.relConfigFile
+  self.manifestEntry.configFile

 public def fixedToolchain (self : MaterializedDep) : Bool :=
  match self.manifest? with
@@ -175,11 +157,10 @@ public def Dependency.materialize
  (lakeEnv : Env) (wsDir relPkgsDir relParentDir : FilePath)
 : LoggerIO MaterializedDep := do
  if let some src := dep.src? then
-    let sname := dep.name.toString (escape := false)
    match src with
    | .path dir =>
      let relPkgDir := relParentDir / dir
-      mkDep sname relPkgDir "" (.path relPkgDir)
+      mkDep (wsDir / relPkgDir) relPkgDir "" (.path relPkgDir)
    | .git url inputRev? subDir? => do
      let sname := dep.name.toString (escape := false)
      let repoUrl := Git.filterUrl? url |>.getD ""
@@ -227,19 +208,16 @@ public def Dependency.materialize
    | _ => error s!"{pkg.fullName}: Git source not found on Reservoir"
 where
  materializeGit name relPkgDir gitUrl remoteUrl inputRev? subDir? : LoggerIO MaterializedDep := do
-    let gitDir := wsDir / relPkgDir
-    let repo := GitRepo.mk gitDir
+    let pkgDir := wsDir / relPkgDir
+    let repo := GitRepo.mk pkgDir
    let gitUrl := lakeEnv.pkgUrlMap.find? dep.name |>.getD gitUrl
    materializeGitRepo name repo gitUrl inputRev?
    let rev ← repo.getHeadRevision
    let relPkgDir := if let some subDir := subDir? then relPkgDir / subDir else relPkgDir
-    mkDep name relPkgDir remoteUrl <| .git gitUrl rev inputRev? subDir?
-  @[inline] mkDep name relPkgDir remoteUrl src : LoggerIO MaterializedDep := do
-    let pkgDir := wsDir / relPkgDir
-    let some pkgDir ← resolvePath? pkgDir
-      | error s!"{name}: package directory not found: {pkgDir}"
+    mkDep pkgDir relPkgDir remoteUrl <| .git gitUrl rev inputRev? subDir?
+  @[inline] mkDep pkgDir relPkgDir remoteUrl src : LoggerIO MaterializedDep := do
    return {
-      pkgDir, relPkgDir, remoteUrl,
+      relPkgDir, remoteUrl
      manifest? :=  ← Manifest.load (pkgDir / defaultManifestFile) |>.toBaseIO
      manifestEntry := {name := dep.name, scope := dep.scope, inherited, src}
    }
@@ -253,9 +231,9 @@ public def PackageEntry.materialize
 : LoggerIO MaterializedDep :=
  match manifestEntry.src with
  | .path (dir := relPkgDir) .. =>
-    mkDep relPkgDir ""
+    mkDep (wsDir / relPkgDir) relPkgDir ""
  | .git (url := url) (rev := rev) (subDir? := subDir?) .. => do
-    let sname := manifestEntry.prettyName
+    let sname := manifestEntry.name.toString (escape := false)
    let relGitDir := relPkgsDir / sname
    let gitDir := wsDir / relGitDir
    let repo := GitRepo.mk gitDir
@@ -276,15 +254,12 @@ public def PackageEntry.materialize
      let url := lakeEnv.pkgUrlMap.find? manifestEntry.name |>.getD url
      cloneGitPkg sname repo url rev
    let relPkgDir := match subDir? with | .some subDir => relGitDir / subDir | .none => relGitDir
-    mkDep relPkgDir (Git.filterUrl? url |>.getD "")
+    mkDep gitDir relPkgDir (Git.filterUrl? url |>.getD "")
 where
-  @[inline] mkDep relPkgDir remoteUrl : LoggerIO MaterializedDep := do
-    let pkgDir := wsDir / relPkgDir
-    let some pkgDir ← resolvePath? pkgDir
-      | error s!"{manifestEntry.prettyName}: package directory not found: {pkgDir}"
+  @[inline] mkDep pkgDir relPkgDir remoteUrl : LoggerIO MaterializedDep := do
    let manifest? ← id do
      if let some manifestFile := manifestEntry.manifestFile? then
        Manifest.load (pkgDir / manifestFile) |>.toBaseIO
      else
        return .error (.noFileOrDirectory "" 0 "")
-    return {pkgDir, relPkgDir, remoteUrl, manifest?, manifestEntry}
+    return {relPkgDir, remoteUrl, manifest?, manifestEntry}
--- a/src/lake/Lake/Load/Package.lean
+++ b/src/lake/Lake/Load/Package.lean
@@ -8,13 +8,10 @@ module
 prelude
 public import Lake.Load.Config
 public import Lake.Config.Package
-public import Lake.Config.LakefileConfig
 import Lake.Util.IO
 import Lake.Load.Lean
 import Lake.Load.Toml

-set_option doc.verso true
-
 /-! # Package Loader

 This module contains the main definitions to load a package
@@ -26,38 +23,6 @@ open System (FilePath)

 namespace Lake

-/--
-**For interal use only.**
-
-Constructs a package from the configuration defined in its Lake configuration file
-and the load configuaration.
-/
-public def mkPackage
-  (loadCfg : LoadConfig) (fileCfg : LakefileConfig) (wsIdx := loadCfg.pkgIdx)
-: Package :=
-  let {
-    pkgDir := dir, relPkgDir := relDir,
-    configFile, relConfigFile, relManifestFile,
-    scope, remoteUrl, ..} := loadCfg
-  let {
-    depConfigs, defaultTargets, scripts, defaultScripts, testDriver, lintDriver
-    -- destructing needed for type-correctness
-    pkgDecl, targetDecls, targetDeclMap, postUpdateHooks,
-    ..} := fileCfg
-  let {baseName, keyName, origName, config} := pkgDecl
-  {
-    wsIdx, baseName, keyName, origName, config
-    dir, relDir, configFile, relConfigFile, relManifestFile
-    scope, remoteUrl
-    depConfigs
-    targetDecls, targetDeclMap, defaultTargets
-    scripts, defaultScripts
-    testDriver, lintDriver
-    postUpdateHooks
-  }
-
-public theorem wsIdx_mkPackage : (mkPackage l f i).wsIdx = i := by rfl
-
 /--
 Return whether a configuration file with the given name
 and/or a supported extension exists.
@@ -84,25 +49,21 @@ public def realConfigFile (cfgFile : FilePath) : BaseIO FilePath := do
      resolvePath (cfgFile.addExtension "toml")

 /--
-**For internal use only.**
-
-Resolves a relative configuration file path in {lean}`cfg` and
-detects its configuration language (if necessary).
+Loads a Lake package configuration (either Lean or TOML).
+The resulting package does not yet include any dependencies.
 -/
-public def resolveConfigFile
+public def loadPackageCore
  (name : String) (cfg : LoadConfig)
-: LogIO {cfg : LoadConfig // cfg.configLang?.isSome} := do
-  if h : cfg.configLang?.isSome then
-    let some configFile ← resolvePath? cfg.configFile
-      | error s!"{name}: configuration file not found: {cfg.configFile}"
-    return ⟨{cfg with configFile}, h⟩
-  else if let some ext := cfg.relConfigFile.extension then
-    let some configFile ← resolvePath? cfg.configFile
-      | error s!"{name}: configuration file not found: {cfg.configFile}"
+: LogIO (Package × Option Environment) := do
+  if let some ext := cfg.relConfigFile.extension then
+    let cfg ←
+      if let some configFile ← resolvePath? cfg.configFile then
+        pure {cfg with configFile}
+      else error s!"{name}: configuration file not found: {cfg.configFile}"
    match ext with
-    | "lean" => return ⟨{cfg with configFile, configLang? := some .lean}, rfl⟩
-    | "toml" => return ⟨{cfg with configFile, configLang? := some .toml}, rfl⟩
-    | _ => error s!"{name}: configuration has unsupported file extension: {configFile}"
+    | "lean" => (·.map id some) <$> loadLeanConfig cfg
+    | "toml" => ((·,none)) <$> loadTomlConfig cfg
+    | _ => error s!"{name}: configuration has unsupported file extension: {cfg.configFile}"
  else
    let relLeanFile := cfg.relConfigFile.addExtension "lean"
    let relTomlFile := cfg.relConfigFile.addExtension "toml"
@@ -111,28 +72,18 @@ public def resolveConfigFile
    if let some configFile ← resolvePath? leanFile then
      if (← tomlFile.pathExists) then
        logInfo s!"{name}: {relLeanFile} and {relTomlFile} are both present; using {relLeanFile}"
-      return ⟨{cfg with configFile, relConfigFile := relLeanFile, configLang? := some .lean}, rfl⟩
-    else if let some configFile ← resolvePath? tomlFile then
-      return ⟨{cfg with configFile, relConfigFile := relTomlFile, configLang? := some .toml}, rfl⟩
+       let cfg := {cfg with configFile, relConfigFile := relLeanFile}
+      let (pkg, env) ← loadLeanConfig cfg
+      return (pkg, some env)
    else
-      error s!"{name}: no configuration file with a supported extension:\n{leanFile}\n{tomlFile}"
-
-/--
-**For internal use only.**
-Reads the configuration of a Lake configuration file.
-
-The load configuration {lean}`cfg` is assumed to already have an absolute path in
-{lean}`cfg.configFile` and that the proper configuratin langauge for it is in
-{lean}`cfg.configLang?`. This can be ensured through {lean}`resolveConfigFile`.
-/
-public def loadConfigFile (cfg : LoadConfig) (h : cfg.configLang?.isSome) : LogIO LakefileConfig := do
-  match cfg.configLang?.get h with
-  | .lean => loadLeanConfig cfg
-  | .toml => loadTomlConfig cfg
+      if let some configFile ← resolvePath? tomlFile then
+        let cfg := {cfg with configFile, relConfigFile := relTomlFile}
+        let pkg ← loadTomlConfig cfg
+        return (pkg, none)
+      else
+        error s!"{name}: no configuration file with a supported extension:\n{leanFile}\n{tomlFile}"

 /-- Loads a Lake package as a single independent object (without dependencies). -/
-public def loadPackage (cfg : LoadConfig) : LogIO Package := do
-  Lean.searchPathRef.set cfg.lakeEnv.leanSearchPath
-  let ⟨cfg, h⟩ ← resolveConfigFile "[root]" cfg
-  let fileCfg ← loadConfigFile cfg h
-  return mkPackage cfg fileCfg
+public def loadPackage (config : LoadConfig) : LogIO Package := do
+  Lean.searchPathRef.set config.lakeEnv.leanSearchPath
+  (·.1) <$> loadPackageCore "[root]" config
--- a/src/lake/Lake/Load/Resolve.lean
+++ b/src/lake/Lake/Load/Resolve.lean
@@ -25,43 +25,37 @@ This module contains definitions for resolving the dependencies of a package.

 namespace Lake

-/-- Returns the load configuration of a materialized dependency. -/
-@[inline] def mkDepLoadConfig
-  (ws : Workspace) (dep : MaterializedDep)
-  (lakeOpts : NameMap String) (leanOpts : Options) (reconfigure : Bool)
-: LoadConfig where
-  lakeEnv := ws.lakeEnv
-  wsDir := ws.dir
-  pkgIdx := ws.packages.size
-  pkgName := dep.name
-  pkgDir := dep.pkgDir
-  relPkgDir := dep.relPkgDir
-  relConfigFile := dep.relConfigFile
-  relManifestFile := dep.relManifestFile
-  lakeOpts; leanOpts; reconfigure
-  scope := dep.scope
-  remoteUrl := dep.remoteUrl
-
-def Workspace.addFacetDecls (decls : Array FacetDecl) (self : Workspace) : Workspace :=
-  decls.foldl (·.addFacetConfig ·.config) self
-
 /--
 Loads the package configuration of a materialized dependency.
-Adds the package and the facets defined within it to the `Workspace`.
+Adds the facets defined in the package to the `Workspace`.
 -/
-def addDepPackage
+def loadDepPackage
+  (wsIdx : Nat)
  (dep : MaterializedDep)
  (lakeOpts : NameMap String)
  (leanOpts : Options) (reconfigure : Bool)
 : StateT Workspace LogIO Package := fun ws => do
-  let wsIdx := ws.packages.size
-  let loadCfg := mkDepLoadConfig ws dep lakeOpts leanOpts reconfigure
-  let ⟨loadCfg, h⟩ ← resolveConfigFile dep.prettyName loadCfg
-  let fileCfg ← loadConfigFile loadCfg h
-  let pkg := mkPackage loadCfg fileCfg wsIdx
-  let ws := ws.addPackage' pkg wsIdx_mkPackage
-  let ws := ws.addFacetDecls fileCfg.facetDecls
-  return (pkg, ws)
+  let name := dep.name.toString (escape := false)
+  let pkgDir := ws.dir / dep.relPkgDir
+  let some pkgDir ← resolvePath? pkgDir
+    | error s!"{name}: package directory not found: {pkgDir}"
+  let (pkg, env?) ← loadPackageCore name {
+    lakeEnv := ws.lakeEnv
+    wsDir := ws.dir
+    pkgIdx := wsIdx
+    pkgName := dep.name
+    pkgDir
+    relPkgDir := dep.relPkgDir
+    relConfigFile := dep.configFile
+    lakeOpts, leanOpts, reconfigure
+    scope := dep.scope
+    remoteUrl := dep.remoteUrl
+  }
+  if let some env := env? then
+    let ws ← IO.ofExcept <| ws.addFacetsFromEnv env leanOpts
+    return (pkg, ws)
+  else
+    return (pkg, ws)

 /--
 The resolver's call stack of dependencies.
@@ -106,7 +100,7 @@ abbrev ResolveT m := DepStackT <| StateT Workspace m
 /-
 Recursively visits each node in a package's dependency graph, starting from
 the workspace package `root`. Each dependency missing from the workspace is
-added to the workspace using the `resolve` function.
+resolved using the `load` function and added into the workspace.

 Recursion occurs breadth-first. Each direct dependency of a package is
 resolved in reverse order before recursing to the dependencies' dependencies.
@@ -114,10 +108,9 @@ resolved in reverse order before recursing to the dependencies' dependencies.
 See `Workspace.updateAndMaterializeCore` for more details.
 -/
@[inline] private def Workspace.resolveDepsCore
-  [Monad m] [MonadError m] [MonadLiftT LogIO m] (ws : Workspace)
-  (resolve : Package → Dependency → Workspace → m MaterializedDep)
+  [Monad m] [MonadError m] (ws : Workspace)
+  (load : Package → Dependency → Nat → StateT Workspace m Package)
  (root : Package := ws.root) (stack : DepStack := {})
-  (leanOpts : Options := {}) (reconfigure := true)
 : m Workspace := do
  ws.runResolveT go root stack
 where
@@ -130,8 +123,8 @@ where
        return -- already handled in another branch
      if pkg.baseName = dep.name then
        error s!"{pkg.prettyName}: package requires itself (or a package with the same name)"
-      let matDep ← resolve pkg dep (← getWorkspace)
-      discard <| addDepPackage matDep dep.opts leanOpts reconfigure
+      let depPkg ← load pkg dep ws.packages.size
+      modifyThe Workspace (·.addPackage depPkg)
    -- Recursively load the dependencies' dependencies
    (← getWorkspace).packages.forM recurse start

@@ -178,17 +171,17 @@ private def reuseManifest
    logWarning s!"{rootName}: ignoring previous manifest because it failed to load: {e}"

 /-- Add a package dependency's manifest entries to the update state. -/
-private def addDependencyEntries (dep : MaterializedDep) : UpdateT LoggerIO PUnit := do
-  match (← Manifest.load dep.manifestFile |>.toBaseIO) with
+private def addDependencyEntries (pkg : Package) (matDep : MaterializedDep) : UpdateT LoggerIO PUnit := do
+  match matDep.manifest? with
  | .ok manifest =>
    manifest.packages.forM fun entry => do
      unless (← getThe (NameMap PackageEntry)).contains entry.name do
-        let entry := entry.setInherited.inDirectory dep.relPkgDir
+        let entry := entry.setInherited.inDirectory pkg.relDir
        store entry.name entry
  | .error (.noFileOrDirectory ..) =>
-    logWarning s!"{dep.prettyName}: ignoring missing manifest:\n  {dep.manifestFile}"
+    logWarning s!"{pkg.prettyName}: ignoring missing manifest '{pkg.manifestFile}'"
  | .error e =>
-    logWarning s!"{dep.prettyName}: ignoring manifest because it failed to load: {e}"
+    logWarning s!"{pkg.prettyName}: ignoring manifest because it failed to load: {e}"

 /-- Materialize a single dependency, updating it if desired. -/
 private def updateAndMaterializeDep
@@ -363,6 +356,7 @@ def Workspace.updateAndMaterializeCore
  (updateToolchain := true)
 : LoggerIO (Workspace × NameMap PackageEntry) := UpdateT.run do
  reuseManifest ws toUpdate
+  let ws := ws.addPackage ws.root
  if updateToolchain then
    let deps := ws.root.depConfigs.reverse
    let matDeps ← deps.mapM fun dep => do
@@ -371,18 +365,21 @@ def Workspace.updateAndMaterializeCore
    ws.updateToolchain matDeps
    let start := ws.packages.size
    let ws ← (deps.zip matDeps).foldlM (init := ws) fun ws (dep, matDep) => do
-      addDependencyEntries matDep
-      let (_, ws) ← addDepPackage matDep dep.opts leanOpts true ws
+      let (depPkg, ws) ← loadUpdatedDep ws.packages.size dep matDep ws
+      let ws := ws.addPackage depPkg
      return ws
    ws.packages.foldlM (init := ws) (start := start) fun ws pkg =>
-      ws.resolveDepsCore updateAndAddDep pkg [ws.root.baseName] leanOpts true
+      ws.resolveDepsCore (stack := [ws.root.baseName]) updateAndLoadDep pkg
  else
-    ws.resolveDepsCore updateAndAddDep (leanOpts := leanOpts) (reconfigure := true)
+    ws.resolveDepsCore updateAndLoadDep
 where
-  @[inline] updateAndAddDep pkg dep ws := do
-    let matDep ← updateAndMaterializeDep ws pkg dep
-    addDependencyEntries matDep
-    return matDep
+  @[inline] updateAndLoadDep pkg dep wsIdx := do
+    let matDep ← updateAndMaterializeDep (← getWorkspace) pkg dep
+    loadUpdatedDep wsIdx dep matDep
+  @[inline] loadUpdatedDep wsIdx dep matDep : StateT Workspace (UpdateT LoggerIO) Package  := do
+    let depPkg ← loadDepPackage wsIdx matDep dep.opts leanOpts true
+    addDependencyEntries depPkg matDep
+    return depPkg

 /-- Write package entries to the workspace manifest. -/
 def Workspace.writeManifest
@@ -474,9 +471,12 @@ public def Workspace.materializeDeps
  if pkgEntries.isEmpty && !ws.root.depConfigs.isEmpty then
    error "missing manifest; use `lake update` to generate one"
  -- Materialize all dependencies
-  ws.resolveDepsCore (leanOpts := leanOpts) (reconfigure := reconfigure) fun pkg dep ws => do
+  let ws := ws.addPackage ws.root
+  ws.resolveDepsCore fun pkg dep wsIdx => do
+    let ws ← getWorkspace
    if let some entry := pkgEntries.find? dep.name then
-      entry.materialize ws.lakeEnv ws.dir relPkgsDir
+      let result ← entry.materialize ws.lakeEnv ws.dir relPkgsDir
+      loadDepPackage wsIdx result dep.opts leanOpts reconfigure
    else
      if pkg.isRoot then
        error <|
--- a/src/lake/Lake/Load/Toml.lean
+++ b/src/lake/Lake/Load/Toml.lean
@@ -7,12 +7,10 @@ module

 prelude
 public import Lake.Config.Package
-public import Lake.Config.LakefileConfig
 public import Lake.Load.Config
 public import Lake.Toml.Decode
 import Lake.Toml.Load
 import Lean.Parser.Extension
-import Lake.Build.Infos
 import Init.Omega
 meta import Lake.Config.LakeConfig
 meta import Lake.Config.InputFileConfig
@@ -426,15 +424,14 @@ private def decodeTargetDecls
  (pkg : Name) (prettyName : String) (t : Table)
 : DecodeM (Array (PConfigDecl pkg) × DNameMap (NConfigDecl pkg)) := do
  let r : DecodeTargetState pkg := {}
-  let r ← go r LeanLib.keyword LeanLib.configKind LeanLibConfig.decodeToml (by simp)
-  let r ← go r LeanExe.keyword LeanExe.configKind LeanExeConfig.decodeToml (by simp)
-  let r ← go r InputFile.keyword InputFile.configKind InputFileConfig.decodeToml (by simp)
-  let r ← go r InputDir.keyword InputDir.configKind InputDirConfig.decodeToml (by simp)
+  let r ← go r LeanLib.keyword LeanLib.configKind LeanLibConfig.decodeToml
+  let r ← go r LeanExe.keyword LeanExe.configKind LeanExeConfig.decodeToml
+  let r ← go r InputFile.keyword InputFile.configKind InputFileConfig.decodeToml
+  let r ← go r InputDir.keyword InputDir.configKind InputDirConfig.decodeToml
  return (r.decls, r.map)
 where
  go (r : DecodeTargetState pkg) kw kind
-      (decode : {n : Name} → Table → DecodeM (ConfigType kind pkg n))
-      (h : DataType kind = OpaqueConfigTarget kind) := do
+      (decode : {n : Name} → Table → DecodeM (ConfigType kind pkg n)) := do
    let some tableArrayVal := t.find? kw | return r
    let some vals ← tryDecode? tableArrayVal.decodeValueArray | return r
    vals.foldlM (init := r) fun r val => do
@@ -449,10 +446,8 @@ where
      else
        let config ← @decode name t
        let decl : NConfigDecl pkg name :=
-          -- Safety: By definition, for declarative configurations, the type of a package target
-          -- is its configuration's data kind (i.e., `CustomData pkg name = DataType kind`).
-          -- In the equivalent Lean configuration, this would hold by type family axiom.
-          unsafe {pkg, name, kind, config, wf_data := fun _ => ⟨lcProof, h⟩}
+          -- Safety: By definition, config kind = facet kind for declarative configurations.
+          unsafe {pkg, name, kind, config, wf_data := lcProof}
        -- Check that executables have distinct root module names
        let exeRoots ← id do
          if h : kind = LeanExe.configKind then
@@ -474,8 +469,8 @@ where

 /-! ## Root Loader -/

-/-- Load a Lake configuration from a file written in TOML. -/
-public def loadTomlConfig (cfg : LoadConfig) : LogIO LakefileConfig := do
+/-- Load a `Package` from a Lake configuration file written in TOML. -/
+public def loadTomlConfig (cfg: LoadConfig) : LogIO Package := do
  let input ← IO.FS.readFile cfg.configFile
  let ictx := mkInputContext input cfg.relConfigFile.toString
  match (← loadToml ictx |>.toBaseIO) with
@@ -487,12 +482,21 @@ public def loadTomlConfig (cfg : LoadConfig) : LogIO LakefileConfig := do
      let keyName := baseName.num wsIdx
      let prettyName := baseName.toString (escape := false)
      let config ← @PackageConfig.decodeToml keyName origName table
-      let pkgDecl := {baseName, keyName, origName, config : PackageDecl}
      let (targetDecls, targetDeclMap) ← decodeTargetDecls keyName prettyName table
      let defaultTargets ← table.tryDecodeD `defaultTargets #[]
      let defaultTargets := defaultTargets.map stringToLegalOrSimpleName
      let depConfigs ← table.tryDecodeD `require #[]
-      return {pkgDecl, depConfigs, targetDecls, targetDeclMap, defaultTargets}
+      return {
+        wsIdx, baseName, keyName, origName
+        dir := cfg.pkgDir
+        relDir := cfg.relPkgDir
+        configFile := cfg.configFile
+        relConfigFile := cfg.relConfigFile
+        scope := cfg.scope
+        remoteUrl := cfg.remoteUrl
+        config, depConfigs, targetDecls, targetDeclMap
+        defaultTargets
+      }
    if errs.isEmpty then
      return pkg
    else
--- a/src/lake/Lake/Load/Workspace.lean
+++ b/src/lake/Lake/Load/Workspace.lean
@@ -31,21 +31,18 @@ Does not resolve dependencies.
 public def loadWorkspaceRoot (config : LoadConfig) : LogIO Workspace := do
  Lean.searchPathRef.set config.lakeEnv.leanSearchPath
  let lakeConfig ← loadLakeConfig config.lakeEnv
-  let config := {config with pkgIdx := 0}
-  let ⟨config, h⟩ ← resolveConfigFile "[root]" config
-  let fileCfg ← loadConfigFile config h
-  let root := mkPackage config fileCfg 0
-  let facetConfigs := fileCfg.facetDecls.foldl (·.insert ·.config) initFacetConfigs
+  let (root, env?) ← loadPackageCore "[root]" {config with pkgIdx := 0}
  let ws : Workspace := {
    root
    lakeEnv := config.lakeEnv
    lakeConfig
    lakeArgs? := config.lakeArgs?
-    facetConfigs
-    packages_wsIdx h := by simp at h
+    facetConfigs := initFacetConfigs
  }
-  let ws := ws.addPackage' root wsIdx_mkPackage
-  return ws
+  if let some env := env? then
+    IO.ofExcept <| ws.addFacetsFromEnv env config.leanOpts
+  else
+    return ws

 /--
 Load a `Workspace` for a Lake package by
--- a/src/lakefile.toml.in
+++ b/src/lakefile.toml.in
@@ -41,6 +41,7 @@ leanLibDir = "lib/lean"
 nativeLibDir = "lib/lean"

 # Additional options derived from the CMake configuration
+# For example, CI will set `-DwarningAsError=true` through this
 moreLeanArgs = [${LEAN_EXTRA_OPTS_TOML}]

 # Uncomment to limit number of reported errors further in case of overwhelming cmdline output
--- a/src/runtime/interrupt.cpp
+++ b/src/runtime/interrupt.cpp
@@ -5,6 +5,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <limits>
+#include <cstdlib>
+#include <ctime>
+#include <execinfo.h>
 #include "runtime/thread.h"
 #include "runtime/interrupt.h"
 #include "runtime/exception.h"
@@ -16,6 +19,68 @@ namespace lean {
 LEAN_THREAD_VALUE(size_t, g_max_heartbeat, 0);
 LEAN_THREAD_VALUE(size_t, g_heartbeat, 0);

+// --- check_system interval monitoring ---
+//
+// When LEAN_CHECK_SYSTEM_INTERVAL_MS=N is set, warn on stderr if check_system
+// is not called within N milliseconds of CPU time on the current thread.
+// Uses CLOCK_THREAD_CPUTIME_ID so that IO waits do not count towards the interval.
+// Zero overhead when env var is unset.
+
+// 0 = disabled
+static unsigned g_check_system_interval_ms = 0;
+static bool g_check_system_interval_initialized = false;
+
+static unsigned get_check_system_interval_ms() {
+    if (!g_check_system_interval_initialized) {
+        g_check_system_interval_initialized = true;
+        if (const char * env = std::getenv("LEAN_CHECK_SYSTEM_INTERVAL_MS")) {
+            g_check_system_interval_ms = std::atoi(env);
+        }
+    }
+    return g_check_system_interval_ms;
+}
+
+static uint64_t thread_cpu_time_ns() {
+    struct timespec ts;
+    clock_gettime(CLOCK_THREAD_CPUTIME_ID, &ts);
+    return static_cast<uint64_t>(ts.tv_sec) * 1000000000ULL + static_cast<uint64_t>(ts.tv_nsec);
+}
+
+// Thread-local: last CPU time when check_system was called on this thread.
+LEAN_THREAD_VALUE(uint64_t, g_last_check_system_ns, 0);
+
+static void check_system_interval(char const * component_name) {
+    unsigned interval_ms = get_check_system_interval_ms();
+    if (interval_ms > 0) {
+        uint64_t now_ns = thread_cpu_time_ns();
+        uint64_t last_ns = g_last_check_system_ns;
+        g_last_check_system_ns = now_ns;
+        if (last_ns != 0) {
+            uint64_t elapsed_ms = (now_ns - last_ns) / 1000000;
+            if (elapsed_ms > interval_ms) {
+                fprintf(stderr,
+                    "[check_system] WARNING: %llu ms CPU time since last check_system call "
+                    "(component: %s)\n",
+                    (unsigned long long)elapsed_ms, component_name);
+                void * bt_buf[64];
+                int nptrs = backtrace(bt_buf, 64);
+                backtrace_symbols_fd(bt_buf, nptrs, 2); // fd 2 = stderr
+                // Reset timer after printing to avoid backtrace overhead cascading
+                g_last_check_system_ns = thread_cpu_time_ns();
+            }
+        }
+    }
+}
+
+extern "C" LEAN_EXPORT obj_res lean_check_system_interval(b_lean_obj_arg component_name) {
+    check_system_interval(lean_string_cstr(component_name));
+    return lean_io_result_mk_ok(lean_box(0));
+}
+
+extern "C" LEAN_EXPORT uint8_t lean_check_system_interval_is_enabled(lean_obj_arg /* unit */) {
+    return get_check_system_interval_ms() > 0;
+}
+
 extern "C" LEAN_EXPORT obj_res lean_internal_get_default_max_heartbeat() {
 #ifdef LEAN_DEFAULT_MAX_HEARTBEAT
    return lean_box(LEAN_DEFAULT_MAX_HEARTBEAT);
@@ -71,6 +136,7 @@ void check_interrupted() {
 }

 void check_system(char const * component_name, bool do_check_interrupted) {
+    check_system_interval(component_name);
    check_stack(component_name);
    check_memory(component_name);
    if (do_check_interrupted) {
--- a/src/runtime/thread.h
+++ b/src/runtime/thread.h
@@ -181,11 +181,9 @@ public:
 template<typename T> class unique_lock {
 public:
    unique_lock(T const &) {}
-    unique_lock(T const &, std::adopt_lock_t) {}
    ~unique_lock() {}
    void lock() {}
    void unlock() {}
-    T * release() { return nullptr; }
 };
 inline unsigned hardware_concurrency() { return 1; }
 }
--- a/src/runtime/uv/dns.cpp
+++ b/src/runtime/uv/dns.cpp
@@ -173,7 +173,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_dns_get_name(b_obj_arg addr) {
 #else

 // Std.Internal.IO.Async.DNS.getAddrInfo (host service : @& String) (family : UInt8) : IO (IO.Promise (Except IO.Error (Array IPAddr)))
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_dns_get_info(b_obj_arg name, b_obj_arg service, uint8_t family) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_dns_get_info(b_obj_arg name, b_obj_arg service, uint8_t family, int8_t protocol) {
    lean_always_assert(
        false && ("Please build a version of Lean4 with libuv to invoke this.")
    );
--- a/stage0/src/CMakeLists.txt
+++ b/stage0/src/CMakeLists.txt
--- a/stage0/src/include/lean/lean.h
+++ b/stage0/src/include/lean/lean.h
--- a/stage0/src/lakefile.toml.in
+++ b/stage0/src/lakefile.toml.in
--- a/stage0/src/runtime/thread.h
+++ b/stage0/src/runtime/thread.h
--- a/stage0/src/runtime/uv/dns.cpp
+++ b/stage0/src/runtime/uv/dns.cpp
--- a/stage0/stdlib/Init/Data/Array/Basic.c
+++ b/stage0/stdlib/Init/Data/Array/Basic.c
--- a/stage0/stdlib/Init/Data/Array/Int.c
+++ b/stage0/stdlib/Init/Data/Array/Int.c
--- a/stage0/stdlib/Init/Data/Array/Nat.c
+++ b/stage0/stdlib/Init/Data/Array/Nat.c
--- a/stage0/stdlib/Init/Data/List/Basic.c
+++ b/stage0/stdlib/Init/Data/List/Basic.c
--- a/stage0/stdlib/Init/Data/List/Int.c
+++ b/stage0/stdlib/Init/Data/List/Int.c
--- a/stage0/stdlib/Init/Data/List/Int/Prod.c
+++ b/stage0/stdlib/Init/Data/List/Int/Prod.c
--- a/stage0/stdlib/Init/Data/List/Nat.c
+++ b/stage0/stdlib/Init/Data/List/Nat.c
--- a/stage0/stdlib/Init/Data/List/Nat/Prod.c
+++ b/stage0/stdlib/Init/Data/List/Nat/Prod.c
--- a/stage0/stdlib/Init/Data/Vector/Basic.c
+++ b/stage0/stdlib/Init/Data/Vector/Basic.c
--- a/stage0/stdlib/Init/System/IO.c
+++ b/stage0/stdlib/Init/System/IO.c
--- a/stage0/stdlib/Lake/Build/Common.c
+++ b/stage0/stdlib/Lake/Build/Common.c
--- a/stage0/stdlib/Lake/Build/Index.c
+++ b/stage0/stdlib/Lake/Build/Index.c
--- a/stage0/stdlib/Lake/Build/InitFacets.c
+++ b/stage0/stdlib/Lake/Build/InitFacets.c
--- a/stage0/stdlib/Lake/Build/Library.c
+++ b/stage0/stdlib/Lake/Build/Library.c
--- a/stage0/stdlib/Lake/Build/Module.c
+++ b/stage0/stdlib/Lake/Build/Module.c
--- a/stage0/stdlib/Lake/Build/Package.c
+++ b/stage0/stdlib/Lake/Build/Package.c
--- a/stage0/stdlib/Lake/Build/Run.c
+++ b/stage0/stdlib/Lake/Build/Run.c
--- a/stage0/stdlib/Lake/Build/Target/Fetch.c
+++ b/stage0/stdlib/Lake/Build/Target/Fetch.c
--- a/stage0/stdlib/Lake/CLI/Build.c
+++ b/stage0/stdlib/Lake/CLI/Build.c
--- a/stage0/stdlib/Lake/CLI/Init.c
+++ b/stage0/stdlib/Lake/CLI/Init.c
--- a/stage0/stdlib/Lake/CLI/Main.c
+++ b/stage0/stdlib/Lake/CLI/Main.c
--- a/stage0/stdlib/Lake/Config/FacetConfig.c
+++ b/stage0/stdlib/Lake/Config/FacetConfig.c
--- a/stage0/stdlib/Lake/Config/LakefileConfig.c
+++ b/stage0/stdlib/Lake/Config/LakefileConfig.c
--- a/stage0/stdlib/Lake/Config/PackageConfig.c
+++ b/stage0/stdlib/Lake/Config/PackageConfig.c
--- a/stage0/stdlib/Lake/Config/Workspace.c
+++ b/stage0/stdlib/Lake/Config/Workspace.c
--- a/stage0/stdlib/Lake/DSL/Package.c
+++ b/stage0/stdlib/Lake/DSL/Package.c
--- a/stage0/stdlib/Lake/Load/Config.c
+++ b/stage0/stdlib/Lake/Load/Config.c
--- a/stage0/stdlib/Lake/Load/Lean.c
+++ b/stage0/stdlib/Lake/Load/Lean.c
--- a/stage0/stdlib/Lake/Load/Lean/Elab.c
+++ b/stage0/stdlib/Lake/Load/Lean/Elab.c
--- a/stage0/stdlib/Lake/Load/Lean/Eval.c
+++ b/stage0/stdlib/Lake/Load/Lean/Eval.c
--- a/stage0/stdlib/Lake/Load/Manifest.c
+++ b/stage0/stdlib/Lake/Load/Manifest.c
--- a/stage0/stdlib/Lake/Load/Materialize.c
+++ b/stage0/stdlib/Lake/Load/Materialize.c
--- a/stage0/stdlib/Lake/Load/Package.c
+++ b/stage0/stdlib/Lake/Load/Package.c
--- a/stage0/stdlib/Lake/Load/Resolve.c
+++ b/stage0/stdlib/Lake/Load/Resolve.c
--- a/stage0/stdlib/Lake/Load/Toml.c
+++ b/stage0/stdlib/Lake/Load/Toml.c
--- a/stage0/stdlib/Lake/Load/Workspace.c
+++ b/stage0/stdlib/Lake/Load/Workspace.c
--- a/stage0/stdlib/Lean/Compiler/LCNF/InferBorrow.c
+++ b/stage0/stdlib/Lean/Compiler/LCNF/InferBorrow.c
--- a/stage0/stdlib/Lean/Compiler/LCNF/PassManager.c
+++ b/stage0/stdlib/Lean/Compiler/LCNF/PassManager.c
--- a/stage0/stdlib/Lean/Compiler/LCNF/Simp/Main.c
+++ b/stage0/stdlib/Lean/Compiler/LCNF/Simp/Main.c
--- a/stage0/stdlib/Lean/Compiler/LCNF/ToDecl.c
+++ b/stage0/stdlib/Lean/Compiler/LCNF/ToDecl.c
--- a/stage0/stdlib/Lean/CoreM.c
+++ b/stage0/stdlib/Lean/CoreM.c
--- a/stage0/stdlib/Lean/Elab/Deriving/Basic.c
+++ b/stage0/stdlib/Lean/Elab/Deriving/Basic.c
--- a/stage0/stdlib/Lean/Elab/PreDefinition/Basic.c
+++ b/stage0/stdlib/Lean/Elab/PreDefinition/Basic.c
--- a/stage0/stdlib/Lean/Elab/PreDefinition/Main.c
+++ b/stage0/stdlib/Lean/Elab/PreDefinition/Main.c
--- a/Show More
+++ b/Show More
Author	SHA1	Message	Date
Joachim Breitner	7234d6477f	perf: eliminate checkSystemInterval overhead when disabled Skip the FFI call to lean_check_system_interval entirely when LEAN_CHECK_SYSTEM_INTERVAL_MS is unset by checking a builtin_initialize'd Bool flag inline. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>	2026-04-06 18:14:34 +00:00
Joachim Breitner	f3348db41a	Merge master into joachim/checkSystemTime	2026-04-06 14:19:13 +00:00
Joachim Breitner	ca28d0719b	chore: remove non-instrumentation changes from branch Keep only the checkSystemInterval FFI and its call in checkInterrupted. The withIncRecDepth+checkInterrupted change belongs in a separate PR. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>	2026-04-06 10:14:43 +00:00
Joachim Breitner	9d90cb957a	Merge branch 'master' of https://github.com/leanprover/lean4 into joachim/checkSystemTime	2026-04-06 10:10:56 +00:00
Joachim Breitner	e8836ac7a2	chore: remove perf_event_open, amortize LCNF simp checkSystem to % 128 Remove instruction-count mode (perf_event_open) from check_system interval monitoring — keep only the simpler CPU-time mode (LEAN_CHECK_SYSTEM_INTERVAL_MS). The perf_event_open code can be re-added later if needed. Also amortize LCNF simp checkSystem to every 128 visits (unconditional was +0.44% on big_do.lean per CI benchmarks). Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>	2026-04-06 09:00:16 +00:00
Joachim Breitner	0a0aca5db4	feat: add instruction-count mode to check_system interval monitoring Adds `LEAN_CHECK_SYSTEM_INTERVAL_INSN=N` env var (N in millions of instructions) using perf_event_open on Linux. This is deterministic and load-independent, unlike the existing CPU-time mode. Instruction count mode takes priority over `LEAN_CHECK_SYSTEM_INTERVAL_MS` when both are set. Also includes LCNF checkSystem calls (simp + per-declaration) for testing gap coverage. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>	2026-04-05 11:47:20 +00:00
Joachim Breitner	555e957bbd	Merge branch 'master' of https://github.com/leanprover/lean4 into joachim/checkSystemTime	2026-04-04 21:28:48 +00:00
Joachim Breitner	1581f29df7	Merge remote-tracking branch 'origin/master' into joachim/checkSystemTime	2026-04-04 07:12:07 +00:00
Joachim Breitner	bf3743ef12	Merge branch 'master' of https://github.com/leanprover/lean4 into joachim/checkSystemTime	2026-04-03 21:15:00 +00:00
Joachim Breitner	6ba4b30109	fix: improve check_system interval monitoring Move the timer reset in check_system_interval to after the backtrace, so that backtrace overhead doesn't inflate the next gap measurement. Also fix merge: restore withIncRecDepth calling checkInterrupted (from #13258) which was lost during the merge with master. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>	2026-04-03 20:33:36 +00:00
Joachim Breitner	d1af3f6b07	Merge remote-tracking branch 'origin/joachim/inferType-checkSystem' into joachim/checkSystemTime	2026-04-03 06:39:10 +00:00
Joachim Breitner	1de717dc1a	Merge branch 'master' of https://github.com/leanprover/lean4 into joachim/checkSystemTime	2026-04-03 06:38:42 +00:00
Joachim Breitner	623b027952	perf: add checkInterrupted to inferType cache miss path This adds a `Core.checkInterrupted` call in `checkInferTypeCache` on cache miss, allowing cancellation to be detected during large type inference traversals. Previously, `inferTypeImp` could run for >100ms without any interruption check when processing large expressions (e.g. BVDecide proof terms), making IDE cancellation unresponsive. The check is only on cache miss (actual computation), so cache hits have zero overhead. `checkInterrupted` is used instead of the heavier `checkSystem` to minimize performance impact. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>	2026-04-02 12:51:21 +00:00
Joachim Breitner	92108472e5	revert: remove ineffective check_heartbeat amortization check_heartbeat is only ever called from check_system, so amortizing check_system calls from within check_heartbeat has no effect on the kernel type checker gaps. Remove the amortization to avoid unnecessary CI regression. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>	2026-04-02 11:42:08 +00:00
Joachim Breitner	480b2bffc5	perf: increase check_heartbeat amortization interval to 1024 Reduce overhead of the amortized check_system in check_heartbeat by checking every 1024 heartbeats instead of 256. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>	2026-04-02 10:55:35 +00:00
Joachim Breitner	908b647be9	perf: amortize check_system via check_heartbeat Add an amortized check_system call every 256 heartbeats inside check_heartbeat. This ensures periodic stack, memory, and monitoring interval checks for any code path that uses heartbeats, including the kernel type checker. Also fix backtrace cascade in check_system_interval monitoring by resetting the timer after printing the warning, and remove the redundant per-call checkSystem in LCNF simp (keeping only the amortized one). Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>	2026-04-02 09:59:28 +00:00
Joachim Breitner	9beb4dad84	Merge remote-tracking branch 'origin/master' into joachim/checkSystemTime	2026-04-02 07:57:47 +00:00
Joachim Breitner	29bd37591c	fix: add amortized checkSystem to LCNF simp This PR adds a periodic `checkSystem` call to the LCNF simplifier's recursive traversal, checking every 512 visited nodes. This breaks up multi-second gaps (observed up to 2.3s on `big_do.lean`) without measurable performance regression — the amortized cost is effectively zero on benchmarks like `big_do` and `simp_local`. An unconditional `checkSystem` on every node caused a 0.4% instruction count regression, which is why the amortized approach is used instead. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>	2026-04-01 14:14:18 +00:00
Joachim Breitner	e2937ad233	fix: add checkSystem calls to long-running elaboration paths This PR adds `checkSystem` calls to several code paths that can run for extended periods without checking for cancellation, heartbeat limits, or stack overflow. This improves responsiveness of the cancellation mechanism in the language server. Affected paths: - `simp` rewrite candidate loops (`Rewrite.lean`) - `simpAppUsingCongr` argument traversal (`Types.lean`) - `synthesizeSyntheticMVarsStep` mvar loop (`SyntheticMVars.lean`) - `abstractNestedProofs` visitor (`AbstractNestedProofs.lean`) - `transform`/`transformWithCache` visitors (`Transform.lean`) - LCNF compiler pass runner loop (`Main.lean`) - LCNF checker recursive traversal (`Check.lean`) - LCNF simplifier recursive traversal (`Simp/Main.lean`) - `whnfCore` recursive reduction loop (`WHNF.lean`) With these changes, at a 50ms monitoring threshold across the full test suite, the only remaining Lean-side elaborator gaps are: - bv_decide pure computation wrapped in `IO.lazyPure` (architectural) - Single deep `whnf` reductions from the `constructorNameAsVariable` linter (~100-180ms) Remaining C++ gaps (type checker, interpreter module init) are tracked separately. Found using `LEAN_CHECK_SYSTEM_INTERVAL_MS` monitoring from #13218. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>	2026-04-01 12:56:03 +00:00
Joachim Breitner	66924cc4ac	fix: add checkSystem calls to long-running elaboration paths This PR adds `checkSystem` calls to several code paths that can run for extended periods without checking for cancellation, heartbeat limits, or stack overflow. This improves responsiveness of the cancellation mechanism in the language server. Affected paths: - `simp` rewrite candidate loops (`Rewrite.lean`) - `simpAppUsingCongr` argument traversal (`Types.lean`) - `synthesizeSyntheticMVarsStep` mvar loop (`SyntheticMVars.lean`) - `abstractNestedProofs` visitor (`AbstractNestedProofs.lean`) - `transform`/`transformWithCache` visitors (`Transform.lean`) - LCNF compiler pass runner loop (`Main.lean`) - LCNF checker recursive traversal (`Check.lean`) - LCNF simplifier recursive traversal (`Simp/Main.lean`) - `whnfCore` recursive reduction loop (`WHNF.lean`) With these changes, at a 50ms monitoring threshold across the full test suite, the only remaining Lean-side elaborator gaps are: - bv_decide pure computation wrapped in `IO.lazyPure` (architectural) - Single deep `whnf` reductions from the `constructorNameAsVariable` linter (~100-180ms) Remaining C++ gaps (type checker, interpreter module init) are tracked separately. Found using `LEAN_CHECK_SYSTEM_INTERVAL_MS` monitoring from #13218. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>	2026-04-01 09:12:33 +00:00
Joachim Breitner	7488a1f712	feat: share check_system interval timer between C++ and Lean Factor the interval monitoring into a standalone `check_system_interval` function exposed to Lean via `@[extern "lean_check_system_interval"]`. Call it from both the C++ `check_system` and the Lean-level `Core.checkInterrupted`, so that CPU time spent in Lean elaboration (e.g. simp) is properly tracked and attributed. Previously the timer only fired from C++ kernel code, so gaps caused by Lean-level elaboration were misleadingly attributed to the kernel component that happened to call `check_system` next. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>	2026-03-31 16:28:36 +00:00
Joachim Breitner	ffd0f7de85	feat: add backtrace to check_system interval warnings This adds a stack trace dump when the check_system interval warning fires, making it easier to identify the code path responsible for the gap. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>	2026-03-31 16:17:27 +00:00
Joachim Breitner	4f7de4a1d9	feat: add optional check_system interval monitoring This adds optional monitoring of how frequently `check_system` is called per thread. When `LEAN_CHECK_SYSTEM_INTERVAL_MS` is set, a warning is printed to stderr if the interval between consecutive calls exceeds the threshold. This helps identify code paths where cancellation checks are too infrequent for responsive cancellation. Disabled by default; set e.g. `LEAN_CHECK_SYSTEM_INTERVAL_MS=1000` to enable with a 1-second threshold. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>	2026-03-31 13:51:13 +00:00