From 850ee173464cf704c34dbd66501dd245db2e7372 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Mon, 29 Aug 2022 09:59:59 -0400 Subject: [PATCH] chore: move Bootstrap.System.Uri to Init --- src/Bootstrap.lean | 1 - src/Bootstrap/System.lean | 1 - src/Init/System.lean | 1 + src/{Bootstrap => Init}/System/Uri.lean | 3 +++ src/Lean/Server/FileWorker.lean | 1 - src/Lean/Server/GoTo.lean | 1 - src/Lean/Server/References.lean | 1 - src/Lean/Server/Utils.lean | 1 - src/Lean/Server/Watchdog.lean | 1 - tests/lean/Uri.lean | 2 -- 10 files changed, 4 insertions(+), 9 deletions(-) delete mode 100644 src/Bootstrap/System.lean rename src/{Bootstrap => Init}/System/Uri.lean (98%) diff --git a/src/Bootstrap.lean b/src/Bootstrap.lean index 200bbe45c2..e8b07f4b84 100644 --- a/src/Bootstrap.lean +++ b/src/Bootstrap.lean @@ -6,4 +6,3 @@ Authors: Leonardo de Moura import Bootstrap.Data import Bootstrap.ShareCommon import Bootstrap.Dynamic -import Bootstrap.System diff --git a/src/Bootstrap/System.lean b/src/Bootstrap/System.lean deleted file mode 100644 index b345620a9e..0000000000 --- a/src/Bootstrap/System.lean +++ /dev/null @@ -1 +0,0 @@ -import Bootstrap.System.Uri diff --git a/src/Init/System.lean b/src/Init/System.lean index 0585f2c7ff..b3f1dae2d0 100644 --- a/src/Init/System.lean +++ b/src/Init/System.lean @@ -6,3 +6,4 @@ Authors: Leonardo de Moura prelude import Init.System.IO import Init.System.Platform +import Init.System.Uri diff --git a/src/Bootstrap/System/Uri.lean b/src/Init/System/Uri.lean similarity index 98% rename from src/Bootstrap/System/Uri.lean rename to src/Init/System/Uri.lean index c39eb30725..a84943f6c1 100644 --- a/src/Bootstrap/System/Uri.lean +++ b/src/Init/System/Uri.lean @@ -3,6 +3,9 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Chris Lovett -/ +prelude +import Init.Data.String.Extra +import Init.System.FilePath namespace System namespace Uri diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean index d253945d7c..cacac221a0 100644 --- a/src/Lean/Server/FileWorker.lean +++ b/src/Lean/Server/FileWorker.lean @@ -6,7 +6,6 @@ Authors: Marc Huisinga, Wojciech Nawrocki -/ import Init.System.IO import Bootstrap.Data.RBMap -import Bootstrap.System.Uri import Lean.Environment diff --git a/src/Lean/Server/GoTo.lean b/src/Lean/Server/GoTo.lean index d81e5857cd..313d0db918 100644 --- a/src/Lean/Server/GoTo.lean +++ b/src/Lean/Server/GoTo.lean @@ -7,7 +7,6 @@ Authors: Sebastian Ullrich, Lars König, Wojciech Nawrocki import Lean.Data.Json.FromToJson import Lean.Util.Path import Lean.Server.Utils -import Bootstrap.System.Uri namespace Lean.Server diff --git a/src/Lean/Server/References.lean b/src/Lean/Server/References.lean index 721341c1d4..84bab6e618 100644 --- a/src/Lean/Server/References.lean +++ b/src/Lean/Server/References.lean @@ -5,7 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Joscha Mennicken -/ import Lean.Server.Utils -import Bootstrap.System.Uri /-! # Representing collected and deduplicated definitions and usages -/ diff --git a/src/Lean/Server/Utils.lean b/src/Lean/Server/Utils.lean index ef1d153c2e..8fa6e70884 100644 --- a/src/Lean/Server/Utils.lean +++ b/src/Lean/Server/Utils.lean @@ -9,7 +9,6 @@ import Lean.Data.Lsp import Lean.Server.InfoUtils import Init.System.FilePath import Lean.Parser.Basic -import Bootstrap.System.Uri namespace IO diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean index be08e62f46..b5ac2fa470 100644 --- a/src/Lean/Server/Watchdog.lean +++ b/src/Lean/Server/Watchdog.lean @@ -7,7 +7,6 @@ Authors: Marc Huisinga, Wojciech Nawrocki import Init.System.IO import Init.Data.ByteArray import Bootstrap.Data.RBMap -import Bootstrap.System.Uri import Lean.Elab.Import import Lean.Util.Paths diff --git a/tests/lean/Uri.lean b/tests/lean/Uri.lean index 094d113f24..c1ffed8905 100644 --- a/tests/lean/Uri.lean +++ b/tests/lean/Uri.lean @@ -1,5 +1,3 @@ -import Bootstrap.System.Uri - open Lean open System.Uri