diff --git a/Lake/Build/Trace.lean b/Lake/Build/Trace.lean
index 7dd8045d8e..4b7141e573 100644
--- a/Lake/Build/Trace.lean
+++ b/Lake/Build/Trace.lean
@@ -153,6 +153,8 @@ instance : Repr MTime := inferInstanceAs (Repr SystemTime)
 instance : Ord MTime := inferInstanceAs (Ord SystemTime)
 instance : LT MTime := ltOfOrd
 instance : LE MTime := leOfOrd
+instance : Min MTime := minOfLe
+instance : Max MTime := maxOfLe
 
 instance : NilTrace MTime := ⟨0⟩
 instance : MixTrace MTime := ⟨max⟩
diff --git a/Lake/Config/LeanConfig.lean b/Lake/Config/LeanConfig.lean
index 6110a01560..7a84bcc1f4 100644
--- a/Lake/Config/LeanConfig.lean
+++ b/Lake/Config/LeanConfig.lean
@@ -36,6 +36,8 @@ deriving Inhabited, Repr, DecidableEq, Ord
 
 instance : LT BuildType := ltOfOrd
 instance : LE BuildType := leOfOrd
+instance : Min BuildType := minOfLe
+instance : Max BuildType := maxOfLe
 
 /-- The arguments to pass to `leanc` based on the build type. -/
 def BuildType.leancArgs : BuildType → Array String
diff --git a/lean-toolchain b/lean-toolchain
index 253e2446c5..01e11a9e1d 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2022-10-20
+leanprover/lean4:nightly-2022-10-25