diff --git a/Algorithm/Graph/Dijkstra.lean b/Algorithm/Graph/Dijkstra.lean index f992d5e..55ad6d8 100644 --- a/Algorithm/Graph/Dijkstra.lean +++ b/Algorithm/Graph/Dijkstra.lean @@ -11,7 +11,7 @@ public import Mathlib.Algebra.Order.Monoid.Canonical.Defs public import Mathlib.Algebra.Order.Monoid.Unbundled.WithTop import Mathlib.Algebra.Order.Monoid.WithTop -import Mathlib.Data.Set.Lattice +import Mathlib.Data.Set.Lattice.Indexed import Mathlib.Tactic.Order /-! diff --git a/lake-manifest.json b/lake-manifest.json index 81e974b..c3176ab 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,17 +5,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "85e3a25e006c35636f0e53b0e9296caca2685bc0", + "rev": "5ed2965256430c3649e86755f9576b54eca72435", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.34.0-rc2", + "inputRev": "v4.34.0", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "d9598f07b1bc701f1e3aae163d2681c1fd978793", + "rev": "118aa17ee84656b8bd727fef7c458ee8c833385c", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "ba67e212be1197b84c1f1f6299488a10a3002713", + "rev": "ddf04cf3949fa556442341e87d47f9f6e6074707", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "d8823026ac7ef130c253089d95685f9877b95323", + "rev": "e928b72544873815af278d38681b31c0293588e3", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "a8acbfd87375ff4abe14ce09db5b7664d383bc7f", + "rev": "106ff4fafc74ef4ac99d81dbf3ab399118f497a5", "name": "proofwidgets", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -55,7 +55,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "18889deb9e83ea7420ef51c160d6f88552e744e3", + "rev": "355695d523e41d0554926416cba2a2b3544fbbc9", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "507746ab8f4b643ccdacb2ec4cdb5853fa9f8ab3", + "rev": "6a489d9af5d0c47e5b259e2e8bcdfc1811b5a259", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "d54dddc581e08be364c278052863524bff7a99a9", + "rev": "f2effa3d803fda822b1f97b806c47cf2adfbcbc2", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -85,10 +85,10 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "ab3a82db9fea14cf0fd7f5a2de650f4b534640af", + "rev": "e92c9f15fdfacc8536f31cfb3b7ad26c3c8cd204", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.34.0-rc2", + "inputRev": "v4.34.0", "inherited": true, "configFile": "lakefile.toml"}], "name": "algorithm", diff --git a/lakefile.lean b/lakefile.lean index 3ed812f..a244add 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -2,7 +2,7 @@ import Lake open Lake DSL -require "leanprover-community" / "mathlib" @ git "v4.34.0-rc2" +require "leanprover-community" / "mathlib" @ git "v4.34.0" abbrev algorithmOnlyLinters : Array LeanOption := #[ ⟨`linter.mathlibStandardSet, true⟩, @@ -23,6 +23,7 @@ package algorithm where testDriver := "AlgorithmTest" lintDriver := "batteries/runLinter" lintDriverArgs := #["Algorithm"] + builtinLint := true @[default_target] lean_lib Algorithm where diff --git a/lean-toolchain b/lean-toolchain index b814d98..12359f9 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.34.0-rc2 +leanprover/lean4:v4.34.0