From 5eef5f3f2d96b874ce0aa6d9637b351a55e0316d Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Fri, 17 Jul 2026 17:50:09 -0400 Subject: [PATCH] chore: Update Lean to v4.31.0 --- Benchmarks/Compile/lake-manifest.json | 34 +++++++++++++-------------- Benchmarks/Compile/lakefile.toml | 4 ++-- Benchmarks/Compile/lean-toolchain | 2 +- Ix/Address.lean | 1 - Ix/Aiur/Compiler.lean | 2 +- Ix/Aiur/Goldilocks.lean | 2 +- Ix/Benchmark/Bench.lean | 2 -- Ix/ByteArray.lean | 18 -------------- Ix/Common.lean | 1 + Ix/CompileM.lean | 10 ++++---- Ix/Environment.lean | 7 ++---- Ix/Merkle.lean | 1 - Ix/Meta.lean | 3 ++- Tests/ByteArray.lean | 24 ------------------- Tests/Ix/Kernel/TutorialMeta.lean | 2 +- Tests/Keccak.lean | 1 - Tests/Main.lean | 2 -- crates/ffi/src/byte_array.rs | 11 --------- crates/ffi/src/lib.rs | 1 - flake.lock | 12 +++++----- lake-manifest.json | 16 ++++++------- lakefile.lean | 8 +++---- lean-toolchain | 2 +- 23 files changed, 52 insertions(+), 114 deletions(-) delete mode 100644 Ix/ByteArray.lean delete mode 100644 Tests/ByteArray.lean delete mode 100644 crates/ffi/src/byte_array.rs diff --git a/Benchmarks/Compile/lake-manifest.json b/Benchmarks/Compile/lake-manifest.json index 7915fb728..cecf2892b 100644 --- a/Benchmarks/Compile/lake-manifest.json +++ b/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", diff --git a/Benchmarks/Compile/lakefile.toml b/Benchmarks/Compile/lakefile.toml index fa9bb4d8f..661b49c3e 100644 --- a/Benchmarks/Compile/lakefile.toml +++ b/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" diff --git a/Benchmarks/Compile/lean-toolchain b/Benchmarks/Compile/lean-toolchain index 14791d727..18640c8b0 100644 --- a/Benchmarks/Compile/lean-toolchain +++ b/Benchmarks/Compile/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.29.0 +leanprover/lean4:v4.31.0 diff --git a/Ix/Address.lean b/Ix/Address.lean index c0d69b4f3..e1441d08e 100644 --- a/Ix/Address.lean +++ b/Ix/Address.lean @@ -1,6 +1,5 @@ module public import Lean.ToExpr -public import Ix.ByteArray public import Ix.Common public import Blake3.Rust diff --git a/Ix/Aiur/Compiler.lean b/Ix/Aiur/Compiler.lean index ae2503994..36e543b9c 100644 --- a/Ix/Aiur/Compiler.lean +++ b/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]? diff --git a/Ix/Aiur/Goldilocks.lean b/Ix/Aiur/Goldilocks.lean index 8b431ad8c..b22f5cd48 100644 --- a/Ix/Aiur/Goldilocks.lean +++ b/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⟩ diff --git a/Ix/Benchmark/Bench.lean b/Ix/Benchmark/Bench.lean index 4a77d1ccf..50a90cd53 100644 --- a/Ix/Benchmark/Bench.lean +++ b/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 diff --git a/Ix/ByteArray.lean b/Ix/ByteArray.lean deleted file mode 100644 index 06f56e2b5..000000000 --- a/Ix/ByteArray.lean +++ /dev/null @@ -1,18 +0,0 @@ -module - -public section - -namespace ByteArray - -def beqNoFFI (a b : ByteArray) : Bool := - a.data == b.data - -@[extern "rs_byte_array_beq"] -def beq : @& ByteArray → @& ByteArray → Bool := - beqNoFFI - -instance : BEq ByteArray := ⟨ByteArray.beq⟩ - -end ByteArray - -end diff --git a/Ix/Common.lean b/Ix/Common.lean index c2756fe77..e1c81974b 100644 --- a/Ix/Common.lean +++ b/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 diff --git a/Ix/CompileM.lean b/Ix/CompileM.lean index cd0fce281..d1a7c677a 100644 --- a/Ix/CompileM.lean +++ b/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 => diff --git a/Ix/Environment.lean b/Ix/Environment.lean index 4580764b5..c157eb743 100644 --- a/Ix/Environment.lean +++ b/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 diff --git a/Ix/Merkle.lean b/Ix/Merkle.lean index 411ba1400..383989c82 100644 --- a/Ix/Merkle.lean +++ b/Ix/Merkle.lean @@ -34,7 +34,6 @@ module public import Ix.Address -public import Ix.ByteArray public section diff --git a/Ix/Meta.lean b/Ix/Meta.lean index 1e7e38351..7caf96ce2 100644 --- a/Ix/Meta.lean +++ b/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." diff --git a/Tests/ByteArray.lean b/Tests/ByteArray.lean deleted file mode 100644 index 92be1a47b..000000000 --- a/Tests/ByteArray.lean +++ /dev/null @@ -1,24 +0,0 @@ -module - -public import LSpec -public import Ix.ByteArray - -def arrays : List ByteArray := [ - ⟨#[]⟩, ⟨#[1]⟩, ⟨#[0, 3]⟩, ⟨#[1, 1, 1]⟩, ⟨#[3, 3, 3, 3]⟩, ⟨#[13]⟩ -] - -def arrays' : List ByteArray := [ - ⟨#[1]⟩, ⟨#[2]⟩, ⟨#[0, 3, 0]⟩, ⟨#[1, 2, 1]⟩, ⟨#[3, 3, 4, 3]⟩, ⟨#[13, 0]⟩ -] - -open LSpec - -def beq : TestSeq := - arrays.zip arrays |>.foldl (init := .done) fun tSeq (x, y) => - tSeq ++ (test s!"{x} == {y}" $ x.beq y && x.beqNoFFI y && y.beq x && y.beqNoFFI x) - -def neq : TestSeq := - arrays.zip arrays' |>.foldl (init := .done) fun tSeq (x, y) => - tSeq ++ (test s!"{x} != {y}" $ !x.beq y && !x.beqNoFFI y && !y.beq x && !y.beqNoFFI x) - -public def Tests.ByteArray.suite := [beq, neq] diff --git a/Tests/Ix/Kernel/TutorialMeta.lean b/Tests/Ix/Kernel/TutorialMeta.lean index 7bd6a027b..ac875fb13 100644 --- a/Tests/Ix/Kernel/TutorialMeta.lean +++ b/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 diff --git a/Tests/Keccak.lean b/Tests/Keccak.lean index 98d614ef8..1110d329b 100644 --- a/Tests/Keccak.lean +++ b/Tests/Keccak.lean @@ -2,7 +2,6 @@ module public import Ix.Keccak public import LSpec -public import Ix.ByteArray open LSpec diff --git a/Tests/Main.lean b/Tests/Main.lean index 8a1eebd06..1e6a65b0c 100644 --- a/Tests/Main.lean +++ b/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), diff --git a/crates/ffi/src/byte_array.rs b/crates/ffi/src/byte_array.rs deleted file mode 100644 index ab53b2d8b..000000000 --- a/crates/ffi/src/byte_array.rs +++ /dev/null @@ -1,11 +0,0 @@ -use lean_ffi::object::{LeanBorrowed, LeanByteArray}; - -/// `@& ByteArray → @& ByteArray → Bool` -/// Efficient implementation for `BEq ByteArray` -#[unsafe(no_mangle)] -extern "C" fn rs_byte_array_beq( - a: LeanByteArray>, - b: LeanByteArray>, -) -> bool { - a.as_bytes() == b.as_bytes() -} diff --git a/crates/ffi/src/lib.rs b/crates/ffi/src/lib.rs index 38df7e1dd..5b404001c 100644 --- a/crates/ffi/src/lib.rs +++ b/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")) diff --git a/flake.lock b/flake.lock index 7468797d5..f991113e3 100644 --- a/flake.lock +++ b/flake.lock @@ -33,11 +33,11 @@ ] }, "locked": { - "lastModified": 1776364162, - "narHash": "sha256-l3FectIPaz5Fq1q0YSG7wR7VyybZqt56Sj4kebEoZ+Q=", + "lastModified": 1784318821, + "narHash": "sha256-mgyIRIZAs5pKAD8HT1sATU9QibhEXXaCovjUFT0j3gg=", "owner": "argumentcomputer", "repo": "Blake3.lean", - "rev": "aaf530784082a2c00b0a93648741429d274102ca", + "rev": "2342f0d7f5af12e232b12b8815cd2ada5d0c2bb6", "type": "github" }, "original": { @@ -254,11 +254,11 @@ "nixpkgs": "nixpkgs" }, "locked": { - "lastModified": 1775267043, - "narHash": "sha256-yUCn4Wc5kLboN9JHom/SJAknn7aoSEDyerqFq3k7g0I=", + "lastModified": 1784223297, + "narHash": "sha256-rmEX8SXvtT7Fi8hOZuCXCbpyzno3iTQYnV3WKzsAVHw=", "owner": "lenianiva", "repo": "lean4-nix", - "rev": "56e917e2766385d0b096ea8be9c40ae54bfe138a", + "rev": "82993165f5f30879fc9d40734615ec54cb541e61", "type": "github" }, "original": { diff --git a/lake-manifest.json b/lake-manifest.json index 2c6d163ca..55d5c5df4 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,40 +5,40 @@ "type": "git", "subDir": null, "scope": "", - "rev": "756e3321fd3b02a85ffda19fef789916223e578c", + "rev": "fa08db58b30eb033edcdab331bba000827f9f785", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "v4.29.0", + "inputRev": "v4.31.0", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/lean4-cli", "type": "git", "subDir": null, "scope": "", - "rev": "7802da01beb530bf051ab657443f9cd9bc3e1a29", + "rev": "92564e5770e4d09f2d86dfbf8ada1e9c715b384c", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.29.0", + "inputRev": "v4.31.0", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/argumentcomputer/Blake3.lean", "type": "git", "subDir": null, "scope": "", - "rev": "d15f36cf76eb5834b0e623e02b97fd4d95e56cc7", + "rev": "2342f0d7f5af12e232b12b8815cd2ada5d0c2bb6", "name": "Blake3", "manifestFile": "lake-manifest.json", - "inputRev": "d15f36cf76eb5834b0e623e02b97fd4d95e56cc7", + "inputRev": "2342f0d7f5af12e232b12b8815cd2ada5d0c2bb6", "inherited": false, "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": false, "configFile": "lakefile.toml"}], "name": "ix", diff --git a/lakefile.lean b/lakefile.lean index 8b9ee021e..2f16693b0 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -5,16 +5,16 @@ package ix where version := v!"0.1.0" require LSpec from git - "https://github.com/argumentcomputer/LSpec" @ "d3c15b93a1dd4e7c8d5c0c3825c9555737e55c3e" + "https://github.com/argumentcomputer/LSpec" @ "3e23a4ad2e91eaf07845cecad157b7ffbb437aed" require Blake3 from git - "https://github.com/argumentcomputer/Blake3.lean" @ "d15f36cf76eb5834b0e623e02b97fd4d95e56cc7" + "https://github.com/argumentcomputer/Blake3.lean" @ "2342f0d7f5af12e232b12b8815cd2ada5d0c2bb6" require Cli from git - "https://github.com/leanprover/lean4-cli" @ "v4.29.0" + "https://github.com/leanprover/lean4-cli" @ "v4.31.0" require batteries from git - "https://github.com/leanprover-community/batteries" @ "v4.29.0" + "https://github.com/leanprover-community/batteries" @ "v4.31.0" /-! ## FFI diff --git a/lean-toolchain b/lean-toolchain index 14791d727..18640c8b0 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.29.0 +leanprover/lean4:v4.31.0