chore: Update Lean to v4.31.0

Benchmarks/Compile/lake-manifest.json

@@ -5,20 +5,20 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "8a178386ffc0f5fef0b77738bb5449d50efeea95",
+   "rev": "fabf563a7c95a166b8d7b6efca11c8b4dc9d911f",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.29.0",
+   "inputRev": "v4.31.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/ImperialCollegeLondon/FLT",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "2d9083d31e10033122dedbcd9406389c2df5be86",
+   "rev": "d4f80bf20098083e8750b0e6b1b2109cd7c52cda",
    "name": "flt",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.29.0",
+   "inputRev": "v4.31.0",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"type": "path",
@@ -32,7 +32,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "83e90935a17ca19ebe4b7893c7f7066e266f50d3",
+   "rev": "63045536fe95024e6c18fc7b48e03f506701c5bc",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -52,7 +52,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "48d5698bc464786347c1b0d859b18f938420f060",
+   "rev": "5c7542ed018c78194f1e2b903eaf6a792b74c03d",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -62,17 +62,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "3c52dee17f0cd89c1ec14de78920d1bdaa3d26b3",
+   "rev": "24b0d9dc081c5423f8eec7e866c441e5184f29d9",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.95",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "7152850e7b216a0d409701617721b6e469d34bf6",
+   "rev": "e3cb2f741431ce31bf73549fb52316a57368b06f",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -82,7 +82,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "707efb56d0696634e9e965523a1bbe9ac6ce141d",
+   "rev": "f46324995fca5f0483b742e4eb4daec7f4ee50d2",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -92,7 +92,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "756e3321fd3b02a85ffda19fef789916223e578c",
+   "rev": "fa08db58b30eb033edcdab331bba000827f9f785",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -102,10 +102,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "7802da01beb530bf051ab657443f9cd9bc3e1a29",
+   "rev": "92564e5770e4d09f2d86dfbf8ada1e9c715b384c",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.29.0",
+   "inputRev": "v4.31.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/PatrickMassot/checkdecls.git",
@@ -122,20 +122,20 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "d15f36cf76eb5834b0e623e02b97fd4d95e56cc7",
+   "rev": "2342f0d7f5af12e232b12b8815cd2ada5d0c2bb6",
    "name": "Blake3",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "d15f36cf76eb5834b0e623e02b97fd4d95e56cc7",
+   "inputRev": "2342f0d7f5af12e232b12b8815cd2ada5d0c2bb6",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/argumentcomputer/LSpec",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "d3c15b93a1dd4e7c8d5c0c3825c9555737e55c3e",
+   "rev": "3e23a4ad2e91eaf07845cecad157b7ffbb437aed",
    "name": "LSpec",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "d3c15b93a1dd4e7c8d5c0c3825c9555737e55c3e",
+   "inputRev": "3e23a4ad2e91eaf07845cecad157b7ffbb437aed",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "Compile",

Benchmarks/Compile/lakefile.toml

@@ -27,9 +27,9 @@ path = "../.."
 [[require]]
 name = "flt"
 git = "https://github.com/ImperialCollegeLondon/FLT"
-rev = "v4.29.0"
+rev = "v4.31.0"
 
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4"
-rev = "v4.29.0"
+rev = "v4.31.0"

Benchmarks/Compile/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.29.0
+leanprover/lean4:v4.31.0

Ix/Address.lean

@@ -1,6 +1,5 @@
 module
 public import Lean.ToExpr
-public import Ix.ByteArray
 public import Ix.Common
 public import Blake3.Rust
 

Ix/Aiur/Compiler.lean

@@ -37,7 +37,7 @@ structure CompiledToplevel where
   bytecode : Bytecode.Toplevel
   nameMap : Std.HashMap Global Bytecode.FunIdx
 
-@[inline, expose]
+@[inline]
 def CompiledToplevel.getFuncIdx (ct : CompiledToplevel) (name : Lean.Name) :
     Option Bytecode.FunIdx :=
   ct.nameMap[Global.mk name]?

Ix/Aiur/Goldilocks.lean

@@ -18,7 +18,7 @@ instance : OfNat G n := ⟨G.ofNat n⟩
   let u64 := u8.toUInt64
   have h : u64 < gSize := by
     have lt256 : u64 < 256 := by
-      simpa [UInt64.lt_iff_toNat_lt] using UInt8.toNat_lt _
+      simpa [u64, UInt64.lt_iff_toNat_lt, UInt8.toNat_toUInt64] using UInt8.toNat_lt _
     exact UInt64.lt_trans lt256 (by decide)
   ⟨u64, h⟩
 

Ix/Benchmark/Bench.lean

@@ -9,8 +9,6 @@ public import Ix.Benchmark.Report
 
 public section
 
-open Batteries (RBMap)
-
 /-!
 # Benchmarking library modeled after Criterion in Rust and Haskell
 

Ix/Common.lean

@@ -297,6 +297,7 @@ def runFrontend (input : String) (filePath : FilePath) : IO Environment := do
   checkToolchain
   let inputCtx := Parser.mkInputContext input filePath.toString
   let (header, parserState, messages) ← Parser.parseHeader inputCtx
+  unsafe enableInitializersExecution  -- required for `processHeader`'s `loadExts := true` import
   let (env, messages) ← processHeader header default messages inputCtx 0
   let env := env.setMainModule default
   let commandState := Command.mkState env messages default

Ix/CompileM.lean

@@ -484,7 +484,7 @@ partial def compileExpr (e : Expr) : CompileM (Ixon.Expr × UInt64) := do
     let univIndices ← lvls.mapM compileAndInternUniv
     compileName name
     let nameAddr := name.getHash
-    match mutCtx.find? name with
+    match mutCtx.get? name with
     | some recIdx =>
       let root ← allocArenaNode (.ref nameAddr)
       pure (.recur recIdx.toUInt64 univIndices, root)
@@ -615,7 +615,7 @@ partial def compareExpr (ctx : Ix.MutCtx) (xlvls ylvls : List Name)
     let univs ← SOrder.zipM (compareLevel xlvls ylvls) xls.toList yls.toList
     if univs.ord != .eq then pure univs
     else if x == y then pure ⟨true, .eq⟩
-    else match ctx.find? x, ctx.find? y with
+    else match ctx.get? x, ctx.get? y with
     | some nx, some ny => pure ⟨false, compare nx ny⟩
     | some _, none => pure ⟨true, .lt⟩
     | none, some _ => pure ⟨true, .gt⟩
@@ -649,7 +649,7 @@ partial def compareExpr (ctx : Ix.MutCtx) (xlvls ylvls : List Name)
   | .lit .., _ => pure ⟨true, .lt⟩
   | _, .lit .. => pure ⟨true, .gt⟩
   | .proj tnx ix tx _, .proj tny iy ty _ => do
-    let tn ← match ctx.find? tnx, ctx.find? tny with
+    let tn ← match ctx.get? tnx, ctx.get? tny with
       | some nx, some ny => pure ⟨false, compare nx ny⟩
       | none, some _ => pure ⟨true, .gt⟩
       | some _, none => pure ⟨true, .lt⟩
@@ -1351,7 +1351,7 @@ def compileMutualBlock (classes : List (List MutConst))
 
 /-- Build mutCtx for an inductive: includes the inductive and all its constructors. -/
 def buildInductiveMutCtx (i : InductiveVal) (ctorVals : Array ConstructorVal) : Ix.MutCtx := Id.run do
-  let mut ctx : Ix.MutCtx := Batteries.RBMap.empty
+  let mut ctx : Ix.MutCtx := Std.TreeMap.empty
   -- Inductive at index 0
   ctx := ctx.insert i.cnst.name 0
   -- Constructors at indices 1, 2, ...
@@ -1370,7 +1370,7 @@ def BlockResult.mk' (block : Ixon.Constant) (blockMeta : Ixon.ConstantMeta := .e
     Returns BlockResult with the constant and any projections needed. -/
 def compileConstantInfo (const : ConstantInfo) : CompileM BlockResult := do
   let name := const.getCnst.name
-  let mutCtx : Ix.MutCtx := Batteries.RBMap.empty.insert name 0
+  let mutCtx : Ix.MutCtx := Std.TreeMap.empty.insert name 0
   withMutCtx mutCtx do
     match const with
     | .defnInfo d =>

Ix/Environment.lean

@@ -8,7 +8,7 @@ module
 
 public import Blake3.Rust
 public import Std.Data.HashMap
-public import Batteries.Data.RBMap
+public import Std.Data.TreeMap
 public import Ix.Address
 
 public section
@@ -616,14 +616,11 @@ def Environment.toRaw (env : Environment) : RawEnvironment :=
 /-! ## Context Types for Compilation -/
 
 /-- Mutual context mapping Name to index within block. -/
-abbrev MutCtx := Batteries.RBMap Name Nat nameCompare
+abbrev MutCtx := Std.TreeMap Name Nat nameCompare
 
 instance : Ord MutCtx where
   compare a b := compare a.toList b.toList
 
-/-- Set of Names (for tracking constants in a block). -/
-abbrev NameSet := Batteries.RBSet Name nameCompare
-
 end Ix
 
 end

Ix/Merkle.lean

@@ -34,7 +34,6 @@
 
 module
 public import Ix.Address
-public import Ix.ByteArray
 
 public section
 

Ix/Meta.lean

@@ -35,6 +35,7 @@ def getFileEnv (path : FilePath) : IO Environment := do
   let source ← IO.FS.readFile path
   let inputCtx := Parser.mkInputContext source path.toString
   let (header, parserState, messages) ← Parser.parseHeader inputCtx
+  unsafe enableInitializersExecution  -- required for `processHeaderCore`'s `loadExts := true` import
   let (env, messages) ← processHeaderCore
     (HeaderSyntax.startPos header) (HeaderSyntax.imports header)
     (isModule := false) default messages inputCtx 0
@@ -79,7 +80,7 @@ def fetchMathlibCache (cwd : Option FilePath) : IO Unit := do
   let root := cwd.getD "."
   let manifest := root / "lake-manifest.json"
   let contents ← IO.FS.readFile manifest
-  if contents.containsSubstr "leanprover-community/mathlib4" then
+  if contents.contains "leanprover-community/mathlib4" then
     let mathlibBuild := root / ".lake" / "packages" / "mathlib" / ".lake" / "build"
     if ← mathlibBuild.pathExists then
       println! "Mathlib cache already present, skipping fetch."

Tests/Ix/Kernel/TutorialMeta.lean

@@ -194,7 +194,7 @@ def elabAndAddTestCaseDecl (name : TSyntax ``declId) (type value : Term) (outcom
     (declKind : ConstantKind) (skipTC := false) : CommandElabM Unit := liftTermElabM do
   let (declName, lparams) ← match name with
     | `(declId| $n:ident) => pure (n.getId, [])
-    | `(declId| $n:ident .{ $[$ls:ident],* }) => pure (n.getId, ls.toList.map (·.getId))
+    | `(declId| $n:ident.{ $[$ls:ident],* }) => pure (n.getId, ls.toList.map (·.getId))
     | _ => throwUnsupportedSyntax
   withLevelNames lparams do
     let typeExpr ← elabTermAndSynthesize type none

Tests/Keccak.lean

@@ -2,7 +2,6 @@ module
 
 public import Ix.Keccak
 public import LSpec
-public import Ix.ByteArray
 
 open LSpec
 

Tests/Main.lean

@@ -1,5 +1,4 @@
 import Tests.Aiur
-import Tests.ByteArray
 import Tests.Ix.Ixon
 import Tests.Ix.IxVM
 import Tests.Ix.Claim
@@ -38,7 +37,6 @@ opaque tmpDecodeConstMap : @& List (Lean.Name × Lean.ConstantInfo) → USize
 /-- Primary test suites - run by default -/
 def primarySuites : Std.HashMap String (List LSpec.TestSeq) := .ofList [
   ("ffi", Tests.FFI.suite),
-  ("byte-array", Tests.ByteArray.suite),
   ("ixon", Tests.Ixon.suite),
   ("claim", Tests.Claim.suite),
   ("merkle", Tests.Merkle.suite),

crates/ffi/src/lib.rs

@@ -8,7 +8,6 @@
 ))]
 pub mod _iroh;
 pub mod aiur;
-pub mod byte_array;
 #[cfg(all(
   feature = "net",
   not(all(target_os = "macos", target_arch = "aarch64"))