From 812440c812a77e62405366ae172695dc3d688644 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Thu, 20 Mar 2025 12:56:28 -0400 Subject: [PATCH] chore: Bump to v4.18.0-rc1 --- PhysLean/Mathematics/List.lean | 16 +++++----- PhysLean/Mathematics/List/InsertionSort.lean | 5 +-- PhysLean/Meta/TransverseTactics.lean | 2 +- .../FieldSpecification/TimeOrder.lean | 2 +- README.md | 6 ++-- lake-manifest.json | 32 +++++++++---------- lakefile.toml | 4 +-- lean-toolchain | 2 +- 8 files changed, 35 insertions(+), 34 deletions(-) diff --git a/PhysLean/Mathematics/List.lean b/PhysLean/Mathematics/List.lean index beb95b3..46d29af 100644 --- a/PhysLean/Mathematics/List.lean +++ b/PhysLean/Mathematics/List.lean @@ -63,10 +63,10 @@ lemma dropWile_eraseIdx {I : Type} (P : I → Prop) [DecidablePred P] : | [], _, h => by simp | a :: [], 0, h => by - simp only [List.dropWhile, nonpos_iff_eq_zero, List.length_eq_zero, List.takeWhile_eq_nil_iff, - List.length_singleton, zero_lt_one, Fin.zero_eta, Fin.isValue, List.get_eq_getElem, - Fin.val_eq_zero, List.getElem_cons_zero, decide_eq_true_eq, forall_const, zero_le, - Nat.sub_eq_zero_of_le, List.eraseIdx_zero, ite_not, List.nil_eq] + simp only [List.eraseIdx_zero, nonpos_iff_eq_zero, List.length_eq_zero_iff, + List.takeWhile_eq_nil_iff, List.length_singleton, zero_lt_one, Fin.zero_eta, Fin.isValue, + List.get_eq_getElem, Fin.val_eq_zero, List.getElem_cons_zero, decide_eq_true_eq, forall_const, + List.dropWhile, zero_le, Nat.sub_eq_zero_of_le, ite_not] simp_all only [List.length_cons, List.length_nil, List.get_eq_getElem, Fin.val_eq_zero, List.getElem_cons_zero, implies_true, List.tail_cons, List.dropWhile_nil, decide_true, decide_false, ite_self] @@ -86,17 +86,17 @@ lemma dropWile_eraseIdx {I : Type} (P : I → Prop) [DecidablePred P] : zero_le, ↓reduceIte, tsub_zero, List.eraseIdx_cons_succ, List.eraseIdx_nil] exact Nat.le_add_left [a].length n | a :: b :: l, 0, h => by - simp only [List.dropWhile, List.takeWhile, nonpos_iff_eq_zero, List.length_eq_zero, zero_le, + simp only [List.dropWhile, List.takeWhile, nonpos_iff_eq_zero, List.length_eq_zero_iff, zero_le, Nat.sub_eq_zero_of_le, List.eraseIdx_zero] by_cases hPb : P b · have hPa : P a := by simpa using h ⟨0, by simp⟩ ⟨1, by simp⟩ (by simp [Fin.lt_def]) (by simpa using hPb) simp [hPb, hPa] - · simp only [hPb, decide_false, nonpos_iff_eq_zero, List.length_eq_zero] + · simp only [hPb, decide_false, nonpos_iff_eq_zero, List.length_eq_zero_iff] simp_all only [List.length_cons, List.get_eq_getElem] simp_rw [decide_false] simp_all only [List.tail_cons, decide_false, Bool.false_eq_true, not_false_eq_true, - List.dropWhile_cons_of_neg, nonpos_iff_eq_zero, List.length_eq_zero] + List.dropWhile_cons_of_neg, nonpos_iff_eq_zero, List.length_eq_zero_iff] split next x heq => simp_all only [decide_eq_true_eq, List.length_singleton, nonpos_iff_eq_zero, one_ne_zero, @@ -579,7 +579,7 @@ lemma orderedInsert_eq_insertIdx_orderedInsertPos {I : Type} (le1 : I → I → erw [List.getElem_insertIdx_of_lt] exact hn' · simp only [hn', ↓reduceIte] - rw [List.getElem_insertIdx_of_ge] + rw [List.getElem_insertIdx_of_gt] · rfl · omega diff --git a/PhysLean/Mathematics/List/InsertionSort.lean b/PhysLean/Mathematics/List/InsertionSort.lean index f11bab9..12c5b32 100644 --- a/PhysLean/Mathematics/List/InsertionSort.lean +++ b/PhysLean/Mathematics/List/InsertionSort.lean @@ -196,7 +196,7 @@ lemma takeWhile_orderedInsert' {α : Type} (r : α → α → Prop) [DecidableRe (List.takeWhile (fun c => !decide (r b c)) (List.orderedInsert r a l)).length = (List.takeWhile (fun c => !decide (r b c)) l).length | [] => by - simp only [List.orderedInsert, List.takeWhile_nil, List.length_nil, List.length_eq_zero, + simp only [List.orderedInsert, List.takeWhile_nil, List.length_nil, List.length_eq_zero_iff, List.takeWhile_eq_nil_iff, List.length_singleton, zero_lt_one, Fin.zero_eta, Fin.isValue, List.get_eq_getElem, Fin.val_eq_zero, List.getElem_cons_zero, Bool.not_eq_eq_eq_not, Bool.not_true, decide_eq_false_iff_not, Decidable.not_not, forall_const] @@ -209,7 +209,8 @@ lemma takeWhile_orderedInsert' {α : Type} (r : α → α → Prop) [DecidableRe simp only [List.orderedInsert] by_cases h : r b c · simp only [h, decide_true, Bool.not_true, Bool.false_eq_true, not_false_eq_true, - List.takeWhile_cons_of_neg, List.length_nil, List.length_eq_zero, List.takeWhile_eq_nil_iff, + List.takeWhile_cons_of_neg, List.length_nil, List.length_eq_zero_iff, + List.takeWhile_eq_nil_iff, List.get_eq_getElem, Bool.not_eq_eq_eq_not, decide_eq_false_iff_not, Decidable.not_not] by_cases hac : r a c · simp [hac, hrba] diff --git a/PhysLean/Meta/TransverseTactics.lean b/PhysLean/Meta/TransverseTactics.lean index e90ca14..9ee2289 100644 --- a/PhysLean/Meta/TransverseTactics.lean +++ b/PhysLean/Meta/TransverseTactics.lean @@ -81,7 +81,7 @@ open transverseTactics in /-- Applies `visitTacticInfo` to each tactic in a file. -/ unsafe def transverseTactics (file : FilePath) (visitTacticInfo : FilePath → ContextInfo → TacticInfo → MetaM Unit) : IO Unit := do - searchPathRef.set compile_time_search_path% + initSearchPath (← findSysroot) /- This is equivalent to `(IO.FS.readFile file).bind (fun fileContent => do ...)`. -/ let fileContent ← IO.FS.readFile file enableInitializersExecution diff --git a/PhysLean/QFT/PerturbationTheory/FieldSpecification/TimeOrder.lean b/PhysLean/QFT/PerturbationTheory/FieldSpecification/TimeOrder.lean index c032411..174f8b0 100644 --- a/PhysLean/QFT/PerturbationTheory/FieldSpecification/TimeOrder.lean +++ b/PhysLean/QFT/PerturbationTheory/FieldSpecification/TimeOrder.lean @@ -293,7 +293,7 @@ lemma orderedInsert_swap_eq_time {φ ψ : 𝓕.CrAnFieldOp} List.takeWhile_cons_of_neg, List.append_nil, List.append_cancel_left_eq, List.cons.injEq, true_and] rw [List.dropWhile_append] - simp only [List.isEmpty_eq_true, List.dropWhile_eq_nil_iff, Bool.not_eq_eq_eq_not, Bool.not_true, + simp only [List.isEmpty_iff, List.dropWhile_eq_nil_iff, Bool.not_eq_eq_eq_not, Bool.not_true, decide_eq_false_iff_not, crAnTimeOrderRel_refl, decide_true, Bool.false_eq_true, not_false_eq_true, List.dropWhile_cons_of_neg, ite_eq_left_iff, not_forall, Classical.not_imp, Decidable.not_not, List.append_left_eq_self, forall_exists_index, and_imp] diff --git a/README.md b/README.md index a311832..7f6bad1 100644 --- a/README.md +++ b/README.md @@ -7,7 +7,7 @@ [![](https://img.shields.io/badge/Informal_dependencies-Graph-green)](https://heplean.com/InformalGraph) [![](https://img.shields.io/badge/View_The-Stats-blue)](https://heplean.com/Stats) -[![](https://img.shields.io/badge/Lean-v4.17.0-blue)](https://github.com/leanprover/lean4/releases/tag/v4.17.0) +[![](https://img.shields.io/badge/Lean-v4.18.0--rc1-blue)](https://github.com/leanprover/lean4/releases/tag/v4.18.0) [![Gitpod Ready-to-Code](https://img.shields.io/badge/Gitpod-ready--to--code-blue?logo=gitpod)](https://gitpod.io/#https://github.com/HEPLean/HepLean) A project to digitalize physics. @@ -60,8 +60,8 @@ How HepLean was used: *Theorems from the space-time files of HepLean were includ ## Contributing -We would love to have you involved! See the [Get Involved](https://heplean.com/GetInvolved.html) page to see how you can get involved. -Any contributions are welcome! If you have any questions or want permission permission to create a pull-request for this +We would love to have you involved! See the [Get Involved](https://heplean.com/GetInvolved.html) page to see how you can get involved. +Any contributions are welcome! If you have any questions or want permission permission to create a pull-request for this repository contact Joseph Tooby-Smith on the [Lean Zulip](https://leanprover.zulipchat.com), or email. ## Installation diff --git a/lake-manifest.json b/lake-manifest.json index 8b0c0fe..708cb02 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,47 +5,47 @@ "type": "git", "subDir": null, "scope": "", - "rev": "b031cb6aa39c6db80532975c43594f247b8d4b51", + "rev": "1b489cdbe4bc57a6acdddb9a5dc5699acacdecdd", "name": "«doc-gen4»", "manifestFile": "lake-manifest.json", - "inputRev": "v4.17.0", + "inputRev": "v4.18.0-rc1", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, "scope": "", - "rev": "5269898d6a51d047931107c8d72d934d8d5d3753", + "rev": "6cecf71a82a22ea7c01598800e12f3e8eb66894b", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.17.0", + "inputRev": "v4.18.0-rc1", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/mhuisi/lean4-cli", "type": "git", "subDir": null, "scope": "", - "rev": "c53b3371dd0fe5f3dd75a2df543c3550e246465a", + "rev": "dd423cf2b153b5b14cb017ee4beae788565a3925", "name": "Cli", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/fgdorais/lean4-unicode-basic", + {"url": "https://github.com/jcommelin/lean4-unicode-basic", "type": "git", "subDir": null, "scope": "", - "rev": "d890360c960358a42965bdc15defa3fd09feba38", + "rev": "458e2d3feda3999490987eabee57b8bb88b1949c", "name": "UnicodeBasic", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "bump_to_v4.18.0-rc1", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/dupuisf/BibtexQuery", "type": "git", "subDir": null, "scope": "", - "rev": "63a4bd4ffa4b67dbd8cf5489a0f01bfdc084602c", + "rev": "c07de335d35ed6b118e084ec48cffc39b40d29d2", "name": "BibtexQuery", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "c708be04267e3e995a14ac0d08b1530579c1525a", + "rev": "ebfb31672ab0a5b6d00a018ff67d2ec51ed66f3a", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -85,7 +85,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "0447b0a7b7f41f0a1749010db3f222e4a96f9d30", + "rev": "08372f1ec11df288ff76621ead7b0b575cb29355", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -95,17 +95,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "799f6986de9f61b784ff7be8f6a8b101045b8ffd", + "rev": "a602d13aca2913724c7d47b2d7df0353620c4ee8", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.52", + "inputRev": "v0.0.53", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "56a2c80b209c253e0281ac4562a92122b457dcc0", + "rev": "ec060e0e10c685be8af65f288e23d026c9fde245", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -115,7 +115,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "95561f7a5811fae6a309e4a1bbe22a0a4a98bf03", + "rev": "d892d7a88ad0ccf748fb8e651308ccd13426ba73", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -125,7 +125,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "efcc7d9bd9936ecdc625baf0d033b60866565cd5", + "rev": "092b30de8e7ee78e96b24c235d99e26f2942d77e", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/lakefile.toml b/lakefile.toml index 323c19a..0f3ec35 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -6,12 +6,12 @@ defaultTargets = ["PhysLean"] [[require]] name = "mathlib" git = "https://github.com/leanprover-community/mathlib4.git" -rev = "v4.17.0" +rev = "v4.18.0-rc1" [[require]] name = "«doc-gen4»" git = "https://github.com/leanprover/doc-gen4" -rev = "v4.17.0" +rev = "v4.18.0-rc1" [[lean_lib]] name = "PhysLean" diff --git a/lean-toolchain b/lean-toolchain index 9d729a3..ee45541 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.17.0 \ No newline at end of file +leanprover/lean4:v4.18.0-rc1 \ No newline at end of file