From 48fa9815ef67510c0cdd5e448047ce4f41f89158 Mon Sep 17 00:00:00 2001 From: Joscha Date: Mon, 3 Aug 2026 17:29:50 +0200 Subject: [PATCH 1/2] chore: bump toolchain to v4.33.0-rc2 --- lake-manifest.json | 22 +++++++++++----------- lakefile.toml | 2 +- lean-toolchain | 2 +- 3 files changed, 13 insertions(+), 13 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 7f68c0042..6555f9bca 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,17 +5,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "169c26b52a38b704fad2c009372d76844a059bdf", + "rev": "51e6992efd06126df61a496bebf8f49482a4e129", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "169c26b52a38b704fad2c009372d76844a059bdf", + "inputRev": "v4.33.0-rc2", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "b1c4a69a7e247ab7df20460212001673d74f08c0", + "rev": "123d15766ba49356c02ebad2a4462dfe12d79899", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "0498c7c070c143a3bf7379f4d99a2c63bb9d9715", + "rev": "f5c090429dff3cf66cb65562526c9ea6e8edfbcb", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "18a90119a5d316358fde6c86e0ca24e59212e32c", + "rev": "bb3469a87774349fe01898d8bf2fc6a1ce6411ca", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "b1436dc749e722c9920036b52cdc43b3451d0b69", + "rev": "222c58dad7706a6e7cae46c0edd65ea881d3ee27", "name": "proofwidgets", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -55,7 +55,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "57d3325be72a842920813bcb40f96a6f7393c185", + "rev": "7db8190085343afde2f5d2cdcc9bac719b6ec02c", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "ee41917ae11d38479fb8fb24745f7ca4bf0a784d", + "rev": "ef42f8944eaf5b6cbfbe75d1917d824c7dd6cf33", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "2c810760f0a0c4536b397dbe30ca9b2f2f467366", + "rev": "76e1c118b0700b4ceafe99532e887d6431625e1a", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -85,10 +85,10 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "da07ca808b6718cb2aed14dba154e5a08b8f8ecf", + "rev": "1319485273bf87833fa472afbcefdedecb16b45f", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.33.0-rc1", + "inputRev": "v4.33.0-rc2", "inherited": true, "configFile": "lakefile.toml"}], "name": "cslib", diff --git a/lakefile.toml b/lakefile.toml index a1fe432a2..fe1d2e777 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -18,7 +18,7 @@ weak.linter.unicodeLinter = false [[require]] name = "mathlib" scope = "leanprover-community" -rev = "169c26b52a38b704fad2c009372d76844a059bdf" +rev = "v4.33.0-rc2" [[lean_lib]] name = "Cslib" diff --git a/lean-toolchain b/lean-toolchain index fd85b262b..c084c7fbe 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.33.0-rc1 +leanprover/lean4:v4.33.0-rc2 From b363c67c2a9ca443fd90fd1d6363d530ff06d7f6 Mon Sep 17 00:00:00 2001 From: Joscha Date: Mon, 3 Aug 2026 20:07:41 +0200 Subject: [PATCH 2/2] fix lints? --- Cslib/Foundations/Semantics/LTS/Termination.lean | 4 ++-- Cslib/MachineLearning/PACLearning/VersionSpace.lean | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/Cslib/Foundations/Semantics/LTS/Termination.lean b/Cslib/Foundations/Semantics/LTS/Termination.lean index 9f3e4184c..6d72fe5ce 100644 --- a/Cslib/Foundations/Semantics/LTS/Termination.lean +++ b/Cslib/Foundations/Semantics/LTS/Termination.lean @@ -63,13 +63,13 @@ states. -/ theorem Acyclic.toBoundedUpTo [Finite State] (h : lts.Acyclic) : lts.BoundedUpTo (Nat.card State) := by classical - letI := Fintype.ofFinite State + let := Fintype.ofFinite State rw [Nat.card_eq_fintype_card] intro s1 μs s2 hmtr obtain ⟨states, hexec⟩ := Execution.of_mTr hmtr have hchain : states.IsChain (Relation.TransGen lts.UnlabelledTr) := hexec.isChain.imp_of_mem_imp fun _ _ _ _ htr => .single htr - letI : Std.Irrefl (Relation.TransGen lts.UnlabelledTr) := h.acyclic + let : Std.Irrefl (Relation.TransGen lts.UnlabelledTr) := h.acyclic have hcard := hchain.pairwise.nodup.length_le_card grind [Execution] diff --git a/Cslib/MachineLearning/PACLearning/VersionSpace.lean b/Cslib/MachineLearning/PACLearning/VersionSpace.lean index ee8a7c9c2..f3989e345 100644 --- a/Cslib/MachineLearning/PACLearning/VersionSpace.lean +++ b/Cslib/MachineLearning/PACLearning/VersionSpace.lean @@ -252,7 +252,7 @@ private lemma pi_map_graph_eq_one (Measure.pi (fun _ : Fin m => P.map (fun x => (x, c x)))) (Set.univ.pi (fun _ : Fin m => {p : α × β | p.2 = c p.1})) = 1 := by have hφ : Measurable (fun x : α => (x, c x)) := by fun_prop - haveI : IsProbabilityMeasure (P.map (fun x : α => (x, c x))) := + have : IsProbabilityMeasure (P.map (fun x : α => (x, c x))) := Measure.isProbabilityMeasure_map hφ.aemeasurable rw [Measure.pi_pi] simp [map_graph_eq_one hcm P hG] @@ -269,7 +269,7 @@ theorem ae_mem_versionSpace_of_realizable ∂(Measure.pi (fun _ : Fin m => P.map (fun x => (x, c x)))), c ∈ VersionSpace C S := by have hφ : Measurable (fun x : α => (x, c x)) := by fun_prop - haveI : IsProbabilityMeasure (P.map (fun x : α => (x, c x))) := + have : IsProbabilityMeasure (P.map (fun x : α => (x, c x))) := Measure.isProbabilityMeasure_map hφ.aemeasurable rw [ae_iff] have hsub : {S : Fin m → α × β | ¬ c ∈ VersionSpace C S} ⊆