chore: use weakLeanArgs for Lake plugin

.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 }}

.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: |

.gitignore

@@ -34,4 +34,3 @@ wdErr.txt
 wdIn.txt
 wdOut.txt
 downstream_releases/
-.claude/worktrees/

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"]:

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}")

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`.
 

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

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

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

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 -/
 
 /--

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

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

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

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

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

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

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'

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.
 

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

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]

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

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}"

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

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

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

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.

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
@@ -76,7 +77,7 @@ globs = ["Lake.*"]
 defaultFacets = ["static", "static.export"]
 # Load the previous stage's lake native code into lake's build process in order to prevent ABI
 # breakages from affecting bootstrapping.
-moreLeanArgs = ["--plugin", "${PREV_STAGE}/${CMAKE_RELATIVE_LIBRARY_OUTPUT_DIRECTORY}/libLake_shared${CMAKE_SHARED_LIBRARY_SUFFIX}"]
+weakLeanArgs = ["--plugin", "${PREV_STAGE}/${CMAKE_RELATIVE_LIBRARY_OUTPUT_DIRECTORY}/libLake_shared${CMAKE_SHARED_LIBRARY_SUFFIX}"]
 
 [[lean_lib]]
 name = "LakeMain"

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; }
 }

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.")
     );