From 783a61ab7642ff98ea4cd9a1ace4ca6339325f0d Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Fri, 21 Oct 2022 11:23:29 -0700 Subject: [PATCH 1/2] chore: Min/Max typeclasses --- Lake/Build/Trace.lean | 2 ++ Lake/Config/LeanConfig.lean | 2 ++ 2 files changed, 4 insertions(+) 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 From 56d0fbd5370a7e737d402a82dc4368840908e05c Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Tue, 25 Oct 2022 15:20:38 -0700 Subject: [PATCH 2/2] chore: bump Lean version --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index f06bd53924..01e11a9e1d 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2022-08-05 +leanprover/lean4:nightly-2022-10-25