From addaa067e15192285e41a3791ad12020f1560183 Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Sat, 7 Dec 2024 12:12:37 +0100 Subject: [PATCH 1/4] bump mathlib --- lake-manifest.json | 36 ++++++++++++++++++------------------ lean-toolchain | 2 +- 2 files changed, 19 insertions(+), 19 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index baad312..a95f1f0 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "485efbc439ee0ebdeae8afb0acd24a5e82e2f771", + "rev": "c016aa9938c4cedc9b7066099f99bcae1b1af625", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -15,17 +15,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "303b23fbcea94ac4f96e590c1cad6618fd4f5f41", + "rev": "ad942fdf0b15c38bface6acbb01d63855a2519ac", "name": "Qq", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "v4.14.0", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "de91b59101763419997026c35a41432ac8691f15", + "rev": "43bcb1964528411e47bfa4edd0c87d1face1fce4", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -35,17 +35,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "1383e72b40dd62a566896a6e348ffe868801b172", + "rev": "2b000e02d50394af68cfb4770a291113d94801b5", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.46", + "inputRev": "v0.0.48", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/lean4-cli", "type": "git", "subDir": null, "scope": "leanprover", - "rev": "726b3c9ad13acca724d4651f14afc4804a7b0e4d", + "rev": "0c8ea32a15a4f74143e4e1e107ba2c412adb90fd", "name": "Cli", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -55,17 +55,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "119b022b3ea88ec810a677888528e50f8144a26e", + "rev": "ed3b856bd8893ade75cafe13e8544d4c2660f377", "name": "importGraph", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "v4.15.0-rc1", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/LeanSearchClient", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "86d0d0584f5cd165353e2f8a30c455cd0e168ac2", + "rev": "d7caecce0d0f003fd5e9cce9a61f1dd6ba83142b", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -75,17 +75,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "42dc02bdbc5d0c2f395718462a76c3d87318f7fa", + "rev": "8e5cb8d424df462f84997dd68af6f40e347c3e35", "name": "plausible", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "v4.15.0-rc1", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, "scope": "", - "rev": "0e836d6e1a3c5ed008688622e261e19fbef05e0e", + "rev": "37305b9e5eff20c7b426a9905ccd04b387203bf1", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null, @@ -95,7 +95,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "11fa569b1b52f987dc5dcea97fd80eaff95c2fce", + "rev": "7edf946a4217aa3aa911290811204096e8464ada", "name": "checkdecls", "manifestFile": "lake-manifest.json", "inputRev": null, @@ -105,7 +105,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "5e95f4776be5e048364f325c7e9d619bb56fb005", + "rev": "fe8e6e649ac8251f43c6f6f934f095ebebce7e7c", "name": "MD4Lean", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -115,7 +115,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "2905ab4ec3961d1fd68ddae0ab4083497e579014", + "rev": "d55279d2ff01759fa75752fcf1a93d1db8db18ff", "name": "UnicodeBasic", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -125,7 +125,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "bdc2fc30b1e834b294759a5d391d83020a90058e", + "rev": "982700bcf78b93166e5b1af0b4b756b8acfdb54b", "name": "BibtexQuery", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -135,7 +135,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "7b6a56e8e4fcf54d3834b225b9814a7c9e4d4bda", + "rev": "4e07f9201e4e4452cd24cf2bd217e93d28f68a69", "name": "«doc-gen4»", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/lean-toolchain b/lean-toolchain index 57a4710..cf25a98 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.14.0-rc2 +leanprover/lean4:v4.15.0-rc1 From 815df64843de99ebd4d171d3c95da0dc43f27bf6 Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Sat, 7 Dec 2024 12:13:52 +0100 Subject: [PATCH 2/4] fix depration --- FormalBook/Chapter_06.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/FormalBook/Chapter_06.lean b/FormalBook/Chapter_06.lean index 20acb7c..f33f254 100644 --- a/FormalBook/Chapter_06.lean +++ b/FormalBook/Chapter_06.lean @@ -189,8 +189,8 @@ theorem wedderburn (h: Fintype R): IsField R := by have finclassa: ∀ (A : ConjClasses Rˣ), Fintype ↑(ConjClasses.carrier A) := fun _ ↦ ConjClasses.instFintypeElemCarrier - have : ∀ (A : ConjClasses Rˣ), Fintype ↑(Set.centralizer {Quotient.out' A}) := - fun _ ↦ setFintype (Set.centralizer {Quotient.out' _}) + have : ∀ (A : ConjClasses Rˣ), Fintype ↑(Set.centralizer {Quotient.out A}) := + fun _ ↦ setFintype (Set.centralizer {Quotient.out _}) letI fintypea : ∀ (A : ConjClasses Rˣ), Fintype ↑{A | have := finclassa A; Fintype.card ↑(ConjClasses.carrier A) > 1} := From 3fa82f4cced1f19495bf02b934ffc4f3f7cd8ca2 Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Sun, 8 Dec 2024 11:28:47 +0100 Subject: [PATCH 3/4] bump again --- lake-manifest.json | 150 ++++++++++++++++++++++----------------------- 1 file changed, 75 insertions(+), 75 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index a95f1f0..46d89ac 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,62 +1,82 @@ {"version": "1.1.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/leanprover-community/batteries", + [{"url": "https://github.com/leanprover/doc-gen4", "type": "git", "subDir": null, - "scope": "leanprover-community", - "rev": "c016aa9938c4cedc9b7066099f99bcae1b1af625", - "name": "batteries", + "scope": "", + "rev": "4e07f9201e4e4452cd24cf2bd217e93d28f68a69", + "name": "«doc-gen4»", "manifestFile": "lake-manifest.json", "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/quote4", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/PatrickMassot/checkdecls.git", "type": "git", "subDir": null, - "scope": "leanprover-community", - "rev": "ad942fdf0b15c38bface6acbb01d63855a2519ac", - "name": "Qq", + "scope": "", + "rev": "7edf946a4217aa3aa911290811204096e8464ada", + "name": "checkdecls", "manifestFile": "lake-manifest.json", - "inputRev": "v4.14.0", - "inherited": true, + "inputRev": null, + "inherited": false, "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/aesop", + {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, - "scope": "leanprover-community", - "rev": "43bcb1964528411e47bfa4edd0c87d1face1fce4", - "name": "aesop", + "scope": "", + "rev": "31530f31d529f37cde81d086fe10b68e9eb1ee2f", + "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": null, + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/mhuisi/lean4-cli", + "type": "git", + "subDir": null, + "scope": "", + "rev": "0c8ea32a15a4f74143e4e1e107ba2c412adb90fd", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/ProofWidgets4", + {"url": "https://github.com/fgdorais/lean4-unicode-basic", "type": "git", "subDir": null, - "scope": "leanprover-community", - "rev": "2b000e02d50394af68cfb4770a291113d94801b5", - "name": "proofwidgets", + "scope": "", + "rev": "d55279d2ff01759fa75752fcf1a93d1db8db18ff", + "name": "UnicodeBasic", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.48", + "inputRev": "main", "inherited": true, "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover/lean4-cli", + {"url": "https://github.com/dupuisf/BibtexQuery", "type": "git", "subDir": null, - "scope": "leanprover", - "rev": "0c8ea32a15a4f74143e4e1e107ba2c412adb90fd", - "name": "Cli", + "scope": "", + "rev": "982700bcf78b93166e5b1af0b4b756b8acfdb54b", + "name": "BibtexQuery", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/acmepjz/md4lean", + "type": "git", + "subDir": null, + "scope": "", + "rev": "fe8e6e649ac8251f43c6f6f934f095ebebce7e7c", + "name": "MD4Lean", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/import-graph", + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "ed3b856bd8893ade75cafe13e8544d4c2660f377", - "name": "importGraph", + "rev": "8e5cb8d424df462f84997dd68af6f40e347c3e35", + "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "v4.15.0-rc1", "inherited": true, @@ -71,75 +91,55 @@ "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/plausible", + {"url": "https://github.com/leanprover-community/import-graph", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "8e5cb8d424df462f84997dd68af6f40e347c3e35", - "name": "plausible", + "rev": "ed3b856bd8893ade75cafe13e8544d4c2660f377", + "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "v4.15.0-rc1", "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/mathlib4.git", - "type": "git", - "subDir": null, - "scope": "", - "rev": "37305b9e5eff20c7b426a9905ccd04b387203bf1", - "name": "mathlib", - "manifestFile": "lake-manifest.json", - "inputRev": null, - "inherited": false, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/PatrickMassot/checkdecls.git", - "type": "git", - "subDir": null, - "scope": "", - "rev": "7edf946a4217aa3aa911290811204096e8464ada", - "name": "checkdecls", - "manifestFile": "lake-manifest.json", - "inputRev": null, - "inherited": false, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/acmepjz/md4lean", + {"url": "https://github.com/leanprover-community/ProofWidgets4", "type": "git", "subDir": null, - "scope": "", - "rev": "fe8e6e649ac8251f43c6f6f934f095ebebce7e7c", - "name": "MD4Lean", + "scope": "leanprover-community", + "rev": "2b000e02d50394af68cfb4770a291113d94801b5", + "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "v0.0.48", "inherited": true, "configFile": "lakefile.lean"}, - {"url": "https://github.com/fgdorais/lean4-unicode-basic", + {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, - "scope": "", - "rev": "d55279d2ff01759fa75752fcf1a93d1db8db18ff", - "name": "UnicodeBasic", + "scope": "leanprover-community", + "rev": "43bcb1964528411e47bfa4edd0c87d1face1fce4", + "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "master", "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/dupuisf/BibtexQuery", + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, - "scope": "", - "rev": "982700bcf78b93166e5b1af0b4b756b8acfdb54b", - "name": "BibtexQuery", + "scope": "leanprover-community", + "rev": "ad942fdf0b15c38bface6acbb01d63855a2519ac", + "name": "Qq", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "v4.14.0", "inherited": true, "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover/doc-gen4", + {"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, - "scope": "", - "rev": "4e07f9201e4e4452cd24cf2bd217e93d28f68a69", - "name": "«doc-gen4»", + "scope": "leanprover-community", + "rev": "c016aa9938c4cedc9b7066099f99bcae1b1af625", + "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", - "inherited": false, - "configFile": "lakefile.lean"}], + "inherited": true, + "configFile": "lakefile.toml"}], "name": "FormalBook", "lakeDir": ".lake"} From 816bf74743941083aa580e75ba6a9ca414ad38b8 Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Mon, 9 Dec 2024 16:38:42 +0100 Subject: [PATCH 4/4] bump again --- lake-manifest.json | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 46d89ac..1b180cf 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "4e07f9201e4e4452cd24cf2bd217e93d28f68a69", + "rev": "82c0223cfb0ba31bcf8bef02519adb92fecf4421", "name": "«doc-gen4»", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "31530f31d529f37cde81d086fe10b68e9eb1ee2f", + "rev": "b202b867947571f7d316d1f591be7e759dc0165c", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null, @@ -135,7 +135,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "c016aa9938c4cedc9b7066099f99bcae1b1af625", + "rev": "74dffd1a83cdd2969a31c9892b0517e7c6f50668", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main",