fix: remove empty .out.expected (lint.py flags empty files)

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

.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

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

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/Elab/BuiltinTerm.lean

@@ -387,7 +387,7 @@ private def mkSilentAnnotationIfHole (e : Expr) : TermElabM Expr := do
   | _ => throwUnsupportedSyntax
 
 private unsafe def evalFilePathUnsafe (stx : Syntax) : TermElabM System.FilePath :=
-  evalTerm System.FilePath (Lean.mkConst ``System.FilePath) stx
+  evalTerm System.FilePath (Lean.mkConst ``System.FilePath) stx (checkMeta := false)
 
 @[implemented_by evalFilePathUnsafe]
 private opaque evalFilePath (stx : Syntax) : TermElabM System.FilePath

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/Elab/Eval.lean

@@ -14,11 +14,12 @@ public section
 namespace Lean.Elab.Term
 open Meta
 
-unsafe def evalTerm (α) (type : Expr) (value : Syntax) (safety := DefinitionSafety.safe) : TermElabM α := withoutModifyingEnv do
+unsafe def evalTerm (α) (type : Expr) (value : Syntax) (safety := DefinitionSafety.safe)
+    (checkMeta : Bool := true) : TermElabM α := withoutModifyingEnv do
   let v ← elabTermEnsuringType value type
   synthesizeSyntheticMVarsNoPostponing
   let v ← instantiateMVars v
   if (← logUnassignedUsingErrorInfos (← getMVars v)) then throwAbortTerm
-  evalExpr α type v safety
+  evalExpr α type v safety (checkMeta := checkMeta)
 
 end Lean.Elab.Term

src/Lean/Meta/Eval.lean

@@ -36,14 +36,16 @@ unsafe def evalExprCore (α) (value : Expr) (checkType : Expr → MetaM Unit)
        value, hints := ReducibilityHints.opaque,
        safety
     }
-    modifyEnv (markMeta · name)
+    if checkMeta then
+      modifyEnv (markMeta · name)
     -- compilation will invariably wait on `checked`
     let _ ← traceBlock "compiler env" (← getEnv).checked
     -- now that we've already waited, async would just introduce (minor) overhead and trigger
     -- `Task.get` blocking debug code
     withOptions (Elab.async.set · false) do
     withOptions (Compiler.compiler.postponeCompile.set · false) do
-    withOptions (Compiler.compiler.relaxedMetaCheck.set · true) do
+    withOptions (fun opts => if checkMeta then Compiler.compiler.relaxedMetaCheck.set opts true
+                             else Compiler.compiler.checkMeta.set opts false) do
       addAndCompile decl
       evalConst (checkMeta := checkMeta) α name
 

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

tests/elab/13310.lean

@@ -0,0 +1,16 @@
+-- Regression test for https://github.com/leanprover/lean4/issues/13310
+-- `include_str` should not require `public meta import Init.System.FilePath`
+
+module
+
+-- Before the fix, this would produce:
+--   Invalid `meta` definition `_tmp✝`, `System.FilePath.mk` is not accessible here;
+--   consider adding `public meta import Init.System.FilePath`
+-- After the fix, `include_str` evaluates the file path without meta checks, so the
+-- only error is about computing the parent directory (expected in the elab test runner
+-- which passes a bare filename without a directory prefix).
+/--
+error: cannot compute parent directory of `13310.lean`
+-/
+#guard_msgs in
+def hello := include_str "13310.txt"

tests/elab/derivingDelta.lean

@@ -380,22 +380,3 @@ deriving instance NCP for NCPAlias
 
 /-- info: instNCPNCPAlias -/
 #guard_msgs in #synth NCP NCPAlias
-
-/-!
-Prop-valued instances should be `theorem`s, not `def`s (issue #13295).
--/
-def Foo (α : Type u) := List α
-deriving instance Nonempty for Foo
-
-/--
-info: theorem instNonemptyFoo.{u_1} : ∀ (α : Type u_1), Nonempty (Foo α) :=
-fun α => instNonemptyFoo._proof_1 α
--/
-#guard_msgs in #print instNonemptyFoo
-
--- NCP is Prop-valued, so its derived instance should also be a theorem.
-/--
-info: theorem instNCPNCPAlias : NCP NCPAlias :=
-instNCPNCPAlias._proof_1
--/
-#guard_msgs in #print instNCPNCPAlias

tests/elab/deriving_diamond_defeq.lean

@@ -81,7 +81,7 @@ set_option pp.all true in
 #check @instMyHigherMyAlias
 
 /--
-info: theorem instMyHigherMyAlias : @MyHigher MyAlias instBaseMyAlias :=
+info: @[implicit_reducible] def instMyHigherMyAlias : @MyHigher MyAlias instBaseMyAlias :=
 instMyHigherMyAlias._proof_1
 -/
 #guard_msgs in