From 07bc639eea32deaeb82fd9f387d4244ca4bcb47d Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 23 May 2024 08:13:33 +1000 Subject: [PATCH 1/2] update Mathlib and Lean; broken --- lake-manifest.json | 22 +++++++++++----------- lean-toolchain | 2 +- 2 files changed, 12 insertions(+), 12 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index b75d25e8..7458b1b1 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,11 +1,11 @@ {"version": 7, "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/leanprover/std4", + [{"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, - "rev": "3025cb124492b423070f20cf0a70636f757d117f", - "name": "std", + "rev": "7b3c48b58fa0ae1c8f27889bdb086ea5e4b27b06", + "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, @@ -13,7 +13,7 @@ {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, - "rev": "64365c656d5e1bffa127d2a1795f471529ee0178", + "rev": "53156671405fbbd5402ed17a79bd129b961bd8d6", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -22,19 +22,19 @@ {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, - "rev": "0a21a48c286c4a4703c0be6ad2045f601f31b1d0", + "rev": "e8c8a42642ceb5af33708b79ae8a3148b681c236", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", "inherited": true, - "configFile": "lakefile.lean"}, + "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/ProofWidgets4", "type": "git", "subDir": null, - "rev": "fe1eff53bd0838c657aa6126fe4dd75ad9939d9a", + "rev": "e6b6247c61280c77ade6bbf0bc3c66a44fe2e0c5", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.35", + "inputRev": "v0.0.36", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/lean4-cli", @@ -49,16 +49,16 @@ {"url": "https://github.com/leanprover-community/import-graph.git", "type": "git", "subDir": null, - "rev": "188eb34fcf1125e89d651ad462d02598219718ca", + "rev": "35e38eb320982cfd2fcc864e0e0467ca223c8cdb", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, - "configFile": "lakefile.lean"}, + "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/mathlib4", "type": "git", "subDir": null, - "rev": "db651742f2c631e5b8525e9aabcf3d61ed094a4a", + "rev": "dfedb0f929c2a8336ca48766c2902651313864ba", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": "master", diff --git a/lean-toolchain b/lean-toolchain index d8a6d7ef..78f39e21 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.8.0-rc1 +leanprover/lean4:v4.8.0-rc2 From e3386db8a89694b21a89f5369a67adb40d2e5e87 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 23 May 2024 08:19:41 +1000 Subject: [PATCH 2/2] fix imports --- MIL/C01_Introduction/S02_Overview.lean | 2 +- MIL/C04_Sets_and_Functions/S01_Sets.lean | 1 - 2 files changed, 1 insertion(+), 2 deletions(-) diff --git a/MIL/C01_Introduction/S02_Overview.lean b/MIL/C01_Introduction/S02_Overview.lean index b5358f45..f29eb599 100644 --- a/MIL/C01_Introduction/S02_Overview.lean +++ b/MIL/C01_Introduction/S02_Overview.lean @@ -1,4 +1,4 @@ -import Mathlib.Data.Nat.Parity +import Mathlib.Algebra.Group.Nat import MIL.Common open Nat diff --git a/MIL/C04_Sets_and_Functions/S01_Sets.lean b/MIL/C04_Sets_and_Functions/S01_Sets.lean index f4a4674b..15f90d2d 100644 --- a/MIL/C04_Sets_and_Functions/S01_Sets.lean +++ b/MIL/C04_Sets_and_Functions/S01_Sets.lean @@ -1,7 +1,6 @@ -- BOTH: import Mathlib.Data.Set.Lattice import Mathlib.Data.Nat.Prime -import Mathlib.Data.Nat.Parity import MIL.Common /- TEXT: