From f4bae4cd2a8ee0fa595ab417932a790e15d8cb5a Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Mon, 29 Aug 2022 01:03:08 -0400 Subject: [PATCH 1/4] chore: move Std -> Bootstrap --- Lake/Util/DRBMap.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Lake/Util/DRBMap.lean b/Lake/Util/DRBMap.lean index 182f970417..21cf85e9e2 100644 --- a/Lake/Util/DRBMap.lean +++ b/Lake/Util/DRBMap.lean @@ -3,7 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura, Mac Malone -/ -import Std.Data.RBMap +import Bootstrap.Data.RBMap import Lake.Util.Compare namespace Lake From 21262e5dca563ab2cbcfb911beb7a4dc8b646607 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Mon, 29 Aug 2022 11:14:25 -0400 Subject: [PATCH 2/4] chore: move Bootstrap.Data -> Lean.Data --- Lake/Util/DRBMap.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Lake/Util/DRBMap.lean b/Lake/Util/DRBMap.lean index 21cf85e9e2..ef64f4f1d4 100644 --- a/Lake/Util/DRBMap.lean +++ b/Lake/Util/DRBMap.lean @@ -3,7 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura, Mac Malone -/ -import Bootstrap.Data.RBMap +import Lean.Data.RBMap import Lake.Util.Compare namespace Lake From 024a298eb7b11fffa6ac3c742124671a1a2e5140 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Tue, 13 Sep 2022 19:11:13 +0200 Subject: [PATCH 3/4] chore: use new constructor docstring syntax --- Lake/Config/Glob.lean | 12 ++++++------ Lake/Config/LeanConfig.lean | 16 ++++++++-------- 2 files changed, 14 insertions(+), 14 deletions(-) diff --git a/Lake/Config/Glob.lean b/Lake/Config/Glob.lean index ceb503d17d..fb920434a2 100644 --- a/Lake/Config/Glob.lean +++ b/Lake/Config/Glob.lean @@ -13,12 +13,12 @@ namespace Lake /-- A specification of a set of module names. -/ inductive Glob -| /-- Selects just the specified module name. -/ - one : Name → Glob -| /-- Selects all submodules of the specified module, but not the module itself. -/ - submodules : Name → Glob -| /-- Selects the specified module and all submodules. -/ - andSubmodules : Name → Glob + /-- Selects just the specified module name. -/ + | one : Name → Glob + /-- Selects all submodules of the specified module, but not the module itself. -/ + | submodules : Name → Glob + /-- Selects the specified module and all submodules. -/ + | andSubmodules : Name → Glob deriving Inhabited, Repr instance : Coe Name Glob := ⟨Glob.one⟩ diff --git a/Lake/Config/LeanConfig.lean b/Lake/Config/LeanConfig.lean index 0c1b40c53a..6110a01560 100644 --- a/Lake/Config/LeanConfig.lean +++ b/Lake/Config/LeanConfig.lean @@ -10,28 +10,28 @@ Lake equivalent of CMake's [`CMAKE_BUILD_TYPE`](https://stackoverflow.com/a/59314670). -/ inductive BuildType -| /-- + /-- Debug optimization, asserts enabled, custom debug code enabled, and debug info included in executable (so you can step through the code with a debugger and have address to source-file:line-number translation). For example, passes `-Og -g` when compiling C code. -/ - debug -| /-- + | debug + /-- Optimized, *with* debug info, but no debug code or asserts (e.g., passes `-O3 -g -DNDEBUG` when compiling C code). -/ - relWithDebInfo -| /-- + | relWithDebInfo + /-- Same as `release` but optimizing for size rather than speed (e.g., passes `-Os -DNDEBUG` when compiling C code). -/ - minSizeRel -| /-- + | minSizeRel + /-- High optimization level and no debug info, code, or asserts (e.g., passes `-O3 -DNDEBUG` when compiling C code). -/ - release + | release deriving Inhabited, Repr, DecidableEq, Ord instance : LT BuildType := ltOfOrd From 032dc4bc8f0ca5756f5903342172eb322fb722cb Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Wed, 14 Sep 2022 05:13:34 -0400 Subject: [PATCH 4/4] chore: move NameMap into a separate file --- Lake/Config/Dependency.lean | 2 +- Lake/Util/Name.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Lake/Config/Dependency.lean b/Lake/Config/Dependency.lean index 4553132442..b92d07b7e2 100644 --- a/Lake/Config/Dependency.lean +++ b/Lake/Config/Dependency.lean @@ -3,7 +3,7 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone -/ -import Lean.Data.Name +import Lean.Data.NameMap namespace Lake open Lean System diff --git a/Lake/Util/Name.lean b/Lake/Util/Name.lean index f2c294c659..2641a0363b 100644 --- a/Lake/Util/Name.lean +++ b/Lake/Util/Name.lean @@ -3,7 +3,7 @@ Copyright (c) 2022 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ -import Lean.Data.Name +import Lean.Data.NameMap import Lake.Util.Compare open Lean