Merge branch 'nightly-with-mathlib' of https://github.com/leanprover/lean4 into joachim/issue11342

Author: nomeata

.claude/commands/release.md

@@ -39,6 +39,7 @@ These comments explain the scripts' behavior, which repositories get special han
 
 ## Important Notes
 
+- **NEVER merge PRs autonomously** - always wait for the user to merge PRs themselves
 - The `release_steps.py` script is idempotent - it's safe to rerun
 - The `release_checklist.py` script is idempotent - it's safe to rerun
 - Some repositories depend on others (e.g., mathlib4 depends on batteries, aesop, etc.)

.github/workflows/ci.yml

@@ -52,7 +52,7 @@ jobs:
       - name: Checkout
         uses: actions/checkout@v5
         # don't schedule nightlies on forks
-        if: github.event_name == 'schedule' && github.repository == 'leanprover/lean4' || inputs.action == 'release nightly'
+        if: github.event_name == 'schedule' && github.repository == 'leanprover/lean4' || inputs.action == 'release nightly' || (startsWith(github.ref, 'refs/tags/') && github.repository == 'leanprover/lean4')
       - name: Set Nightly
         if: github.event_name == 'schedule' && github.repository == 'leanprover/lean4' || inputs.action == 'release nightly'
         id: set-nightly
@@ -115,7 +115,7 @@ jobs:
           CMAKE_MAJOR=$(grep -E "^set\(LEAN_VERSION_MAJOR " src/CMakeLists.txt | grep -oE '[0-9]+')
           CMAKE_MINOR=$(grep -E "^set\(LEAN_VERSION_MINOR " src/CMakeLists.txt | grep -oE '[0-9]+')
           CMAKE_PATCH=$(grep -E "^set\(LEAN_VERSION_PATCH " src/CMakeLists.txt | grep -oE '[0-9]+')
-          CMAKE_IS_RELEASE=$(grep -E "^set\(LEAN_VERSION_IS_RELEASE " src/CMakeLists.txt | grep -oE '[0-9]+')
+          CMAKE_IS_RELEASE=$(grep -m 1 -E "^set\(LEAN_VERSION_IS_RELEASE " src/CMakeLists.txt | grep -oE '[0-9]+')
 
           # Expected values from tag parsing
           TAG_MAJOR="${{ steps.set-release.outputs.LEAN_VERSION_MAJOR }}"

doc/dev/release_checklist.md

@@ -69,6 +69,10 @@ We'll use `v4.6.0` as the intended release version as a running example.
     - `repl`:
       There are two copies of `lean-toolchain`/`lakefile.lean`:
       in the root, and in `test/Mathlib/`. Edit both, and run `lake update` in both directories.
+    - `lean-fro.org`:
+      After updating the toolchains and running `lake update`, you must run `scripts/update.sh` to regenerate
+      the site content. This script updates generated files that depend on the Lean version.
+      The `release_steps.py` script handles this automatically.
 - An awkward situation that sometimes occurs (e.g. with Verso) is that the `master`/`main` branch has already been moved
   to a nightly toolchain that comes *after* the stable toolchain we are
   targeting. In this case it is necessary to create a branch `releases/v4.6.0` from the last commit which was on

script/release_steps.py

@@ -23,6 +23,7 @@
    - Special merging strategies for repositories with nightly-testing branches
    - Safety checks for repositories using bump branches
    - Custom build and test procedures
+   - lean-fro.org: runs scripts/update.sh to regenerate site content
 
 6. Commits the changes with message "chore: bump toolchain to {version}"
 
@@ -412,20 +413,14 @@ def execute_release_steps(repo, version, config):
         run_command("lake update", cwd=repo_path, stream_output=True)
         print(blue("Running `lake update` in examples/hero..."))
         run_command("lake update", cwd=repo_path / "examples" / "hero", stream_output=True)
+
+        # Run scripts/update.sh to regenerate content
+        print(blue("Running `scripts/update.sh` to regenerate content..."))
+        run_command("scripts/update.sh", cwd=repo_path, stream_output=True)
+        print(green("Content regenerated successfully"))
     elif repo_name == "cslib":
         print(blue("Updating lakefile.toml..."))
         run_command(f'perl -pi -e \'s/"v4\\.[0-9]+(\\.[0-9]+)?(-rc[0-9]+)?"/"' + version + '"/g\' lakefile.*', cwd=repo_path)
-        
-        print(blue("Updating docs/lakefile.toml..."))
-        run_command(f'perl -pi -e \'s/"v4\\.[0-9]+(\\.[0-9]+)?(-rc[0-9]+)?"/"' + version + '"/g\' lakefile.*', cwd=repo_path / "docs")
-
-        # Update lean-toolchain in docs
-        print(blue("Updating docs/lean-toolchain..."))
-        docs_toolchain = repo_path / "docs" / "lean-toolchain"
-        with open(docs_toolchain, "w") as f:
-            f.write(f"leanprover/lean4:{version}\n")
-        print(green(f"Updated docs/lean-toolchain to leanprover/lean4:{version}"))
-
         run_command("lake update", cwd=repo_path, stream_output=True)
     elif dependencies:
         run_command(f'perl -pi -e \'s/"v4\\.[0-9]+(\\.[0-9]+)?(-rc[0-9]+)?"/"' + version + '"/g\' lakefile.*', cwd=repo_path)

src/Init/Data/Nat/Bitwise/Basic.lean

@@ -144,7 +144,10 @@ Asserts that the `(n+1)`th least significant bit of `m` is not set.
 
 (This definition is used by Lean internally for compact bitmaps.)
 -/
-@[expose, reducible] protected def hasNotBit (m n : Nat) : Prop :=
-  1 &&& (m >>> n) ≠ 1
+@[expose] protected def hasNotBit (m n : Nat) : Prop :=
+  Nat.land 1 (Nat.shiftRight m n) ≠ 1
+
+@[grind =]
+theorem hasNotBit_eq (m n : Nat) : Nat.hasNotBit m n = (1 &&& (m >>> n) ≠ 1) := rfl
 
 end Nat

src/Init/Data/Nat/Log2.lean

@@ -35,7 +35,7 @@ Examples:
  * `Nat.log2 7 = 2`
  * `Nat.log2 8 = 3`
 -/
-@[extern "lean_nat_log2"]
+@[expose, extern "lean_nat_log2"]
 def log2 (n : @& Nat) : Nat :=
   -- Lean "assembly"
   n.rec (fun _ => nat_lit 0) (fun _ ih n =>

src/Init/Grind/Lemmas.lean

@@ -4,13 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Init.ByCases
 public import Init.Grind.Util
-
+public import Init.Grind.Ring.Basic
 public section
-
 namespace Lean.Grind
 
 theorem rfl_true : true = true :=
@@ -193,6 +191,15 @@ theorem Nat.or_congr {a b : Nat} {k₁ k₂ k : Nat} (h₁ : a = k₁) (h₂ : b
 theorem Nat.shiftLeft_congr {a b : Nat} {k₁ k₂ k : Nat} (h₁ : a = k₁) (h₂ : b = k₂) : k == k₁ <<< k₂ → a <<< b = k := by simp_all
 theorem Nat.shiftRight_congr {a b : Nat} {k₁ k₂ k : Nat} (h₁ : a = k₁) (h₂ : b = k₂) : k == k₁ >>> k₂ → a >>> b = k := by simp_all
 
-theorem Nat.hasNotBit_congr {a b : Nat} {k₁ k₂ : Nat} {k : Bool} (h₁ : a = k₁) (h₂ : b = k₂) : k == Nat.hasNotBit k₁ k₂ → Nat.hasNotBit a b = k := by simp_all
+/-! Semiring propagators -/
+
+theorem Semiring.one_mul_congr {α} [Semiring α] {a b : α} (h : a = 1) : a*b = b := by
+  simp [h, Semiring.one_mul]
+theorem Semiring.zero_mul_congr {α} [Semiring α] {a b : α} (h : a = 0) : a*b = 0 := by
+  simp [h, Semiring.zero_mul]
+theorem Semiring.mul_one_congr {α} [Semiring α] {a b : α} (h : b = 1) : a*b = a := by
+  simp [h, Semiring.mul_one]
+theorem Semiring.mul_zero_congr {α} [Semiring α] {a b : α} (h : b = 0) : a*b = 0 := by
+  simp [h, Semiring.mul_zero]
 
 end Lean.Grind

src/Init/Grind/Norm.lean

@@ -152,6 +152,12 @@ theorem smul_int_eq_mul {α} [Ring α] (i : Int) (a : α) : i • a = Int.cast i
 theorem Int.subNatNat_eq (a b : Nat) : Int.subNatNat a b = NatCast.natCast a - NatCast.natCast b := by
   apply Int.subNatNat_eq_coe
 
+theorem Int.sign_eq (x : Int) : x.sign = if x > 0 then 1 else if x < 0 then -1 else 0 := by
+  split; simp [*]
+  split; simp [*]
+  have : x = 0 := by omega
+  simp [*]
+
 -- Remark: for additional `grind` simprocs, check `Lean/Meta/Tactic/Grind`
 init_grind_norm
   /- Pre theorems -/
@@ -197,6 +203,11 @@ init_grind_norm
   Int.Linear.sub_fold Int.Linear.neg_fold
   -- Int divides
   Int.one_dvd Int.zero_dvd
+  -- Int alternative div and mod. We just expand them
+  Int.fdiv_eq_ediv Int.tdiv_eq_ediv
+  Int.fmod_eq_emod Int.tmod_eq_emod Int.bmod_eq_emod
+  -- Int sign. We just expand it
+  Int.sign_eq
   -- Function composition
   Function.const_apply Function.comp_apply Function.const_comp
   Function.comp_const Function.true_comp Function.false_comp

src/Init/Grind/Tactics.lean

@@ -156,10 +156,10 @@ theorems and helps prevent an excessive number of instantiations.
 - `grind only [<name>, ...]` is like `grind [<name>, ...]` but does not use theorems tagged with `@[grind]`.
 - `grind (gen := <num>)` sets the maximum generation.
 
-### Linear integer arithmetic (`cutsat`)
+### Linear integer arithmetic (`lia`)
 
 `grind` can solve goals that reduce to **linear integer arithmetic (LIA)** using an
-integrated decision procedure called **`cutsat`**.  It understands
+integrated decision procedure called **`lia`**.  It understands
 
 * equalities   `p = 0`
 * inequalities  `p ≤ 0`
@@ -172,7 +172,7 @@ This *model-based* search is **complete for LIA**.
 
 #### Key options:
 
-* `grind -cutsat` disable the solver (useful for debugging)
+* `grind -lia` disable the solver (useful for debugging)
 * `grind +qlia` accept rational models (shrinks the search space but is incomplete for ℤ)
 
 #### Examples:
@@ -297,7 +297,7 @@ syntax (name := grindTrace)
 /--
 `cutsat` solves linear integer arithmetic goals.
 
-It is a implemented as a thin wrapper around the `grind` tactic, enabling only the `cutsat` solver.
+It is a implemented as a thin wrapper around the `grind` tactic, enabling only the `lia` solver.
 Please use `grind` instead if you need additional capabilities.
 
 **Deprecated**: Use `lia` instead.
@@ -307,7 +307,7 @@ syntax (name := cutsat) "cutsat" optConfig : tactic
 /--
 `lia` solves linear integer arithmetic goals.
 
-It is a implemented as a thin wrapper around the `grind` tactic, enabling only the `cutsat` solver.
+It is a implemented as a thin wrapper around the `grind` tactic, enabling only the `lia` solver.
 Please use `grind` instead if you need additional capabilities.
 -/
 syntax (name := lia) "lia" optConfig : tactic

src/Lean/Meta.lean

@@ -58,3 +58,4 @@ public import Lean.Meta.BinderNameHint
 public import Lean.Meta.TryThis
 public import Lean.Meta.Hint
 public import Lean.Meta.MethodSpecs
+public import Lean.Meta.CtorIdxHInj