bump Lean version

[Ptival]

This nightly version includes performance improvements that help with some code generated by SAIL.

Namely:

• perf: avoid quadratic calculation of notAlts in match splitter leanprover/lean4#11196
• perf: use Nat-based bitmask in sparse cases construction leanprover/lean4#11200

I'm not sure what the process is for bumping Lean versions, so please let me know if I should be doing something else!

[ineol]

Thank you for the patch!

I'm curious, have you measured how much faster compilation is?

To fix the deprecation warnings you can use this diff:

diff --git a/patch b/patch
new file mode 100644
index 0000000000..e69de29bb2
diff --git a/src/sail_lean_backend/Sail/IntRange.lean b/src/sail_lean_backend/Sail/IntRange.lean
index 9e79c37d0a..ac46302746 100644
--- a/src/sail_lean_backend/Sail/IntRange.lean
+++ b/src/sail_lean_backend/Sail/IntRange.lean
@@ -16,7 +16,7 @@
   infer_instance
 
 theorem toNat_le {n : Nat} : Int.toNat m ≤ n ↔ m ≤ n := by
-  rw [Int.ofNat_le.symm, Int.toNat_eq_max, Int.max_le]; exact and_iff_left (Int.ofNat_zero_le _)
+  rw [Int.ofNat_le.symm, Int.toNat_eq_max, Int.max_le]; exact and_iff_left (Int.natCast_nonneg _)
 
 theorem lt_toNat {m : Nat} : m < Int.toNat n ↔ (m : Int) < n := by rw [← Int.not_le, ← Nat.not_le, toNat_le]
 
diff --git a/src/sail_lean_backend/Sail/Sail.lean b/src/sail_lean_backend/Sail/Sail.lean
index a9298a3042..6fbd19de55 100644
--- a/src/sail_lean_backend/Sail/Sail.lean
+++ b/src/sail_lean_backend/Sail/Sail.lean
@@ -97,7 +97,7 @@
 def updateBE (x : BitVec m) (n : Nat) (b : BitVec 1) := updateSubrange' x (m - n - 1) _ b
 
 def toBin {w : Nat} (x : BitVec w) : String :=
-  List.asString (List.map (fun c => if c then '1' else '0') (List.ofFn (BitVec.getMsb x)))
+  String.ofList (List.map (fun c => if c then '1' else '0') (List.ofFn (BitVec.getMsb x)))
 
 def toFormatted {w : Nat} (x : BitVec w) : String :=
   if (length x % 4) == 0 then
@@ -127,7 +127,7 @@
   let len := str.length
   if h : n < 4 || len = 0 then BitVec.zero n else
     let bv := parse_hex_bits_digits (n-4) (str.take (len-1))
-    let c := str.get! ⟨len-1⟩ |> charToHex
+    let c := String.Pos.Raw.get! str ⟨len-1⟩ |> charToHex
     BitVec.append bv c |>.cast (by simp_all)
 decreasing_by simp_all <;> omega
 
@@ -137,7 +137,7 @@
   -- TODO: when there are lemmas about `String.take`, replace with WF induction
   go (fuel : Nat) (str : String) :=
     if fuel = 0 then 0 else
-      let lsd := str.get! ⟨str.length - 1⟩
+      let lsd := String.Pos.Raw.get! str ⟨str.length - 1⟩
       let rest := str.take (str.length - 1)
       (charToHex lsd).setWidth n + 10#n * go (fuel-1) rest

[github-actions]

Test Results

   16 files     36 suites   0s ⏱️
1 006 tests 1 003 ✅  3 💤 0 ❌
4 857 runs  4 815 ✅ 42 💤 0 ❌

Results for commit 7d1623f.