From f9899b7a0ec5a6ca714f9bb7d3b5a09d890ade82 Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Mon, 2 Dec 2024 11:55:25 -0500 Subject: [PATCH] chore: lake: use & check `prelude` --- .github/workflows/check-prelude.yml | 3 ++- src/lake/Lake.lean | 1 + src/lake/Lake/Build.lean | 1 + src/lake/Lake/Build/Actions.lean | 1 + src/lake/Lake/Build/Basic.lean | 1 + src/lake/Lake/Build/Common.lean | 1 + src/lake/Lake/Build/Data.lean | 1 + src/lake/Lake/Build/Executable.lean | 1 + src/lake/Lake/Build/Facets.lean | 1 + src/lake/Lake/Build/Fetch.lean | 1 + src/lake/Lake/Build/Imports.lean | 1 + src/lake/Lake/Build/Index.lean | 1 + src/lake/Lake/Build/Info.lean | 1 + src/lake/Lake/Build/Job.lean | 1 + src/lake/Lake/Build/Key.lean | 1 + src/lake/Lake/Build/Library.lean | 1 + src/lake/Lake/Build/Module.lean | 1 + src/lake/Lake/Build/Package.lean | 1 + src/lake/Lake/Build/Run.lean | 1 + src/lake/Lake/Build/Store.lean | 1 + src/lake/Lake/Build/Targets.lean | 1 + src/lake/Lake/Build/Topological.lean | 1 + src/lake/Lake/Build/Trace.lean | 1 + src/lake/Lake/CLI.lean | 1 + src/lake/Lake/CLI/Actions.lean | 1 + src/lake/Lake/CLI/Build.lean | 1 + src/lake/Lake/CLI/Error.lean | 3 +++ src/lake/Lake/CLI/Help.lean | 1 + src/lake/Lake/CLI/Init.lean | 1 + src/lake/Lake/CLI/Main.lean | 1 + src/lake/Lake/CLI/Serve.lean | 1 + src/lake/Lake/CLI/Translate.lean | 1 + src/lake/Lake/CLI/Translate/Lean.lean | 1 + src/lake/Lake/CLI/Translate/Toml.lean | 1 + src/lake/Lake/Config.lean | 1 + src/lake/Lake/Config/Context.lean | 1 + src/lake/Lake/Config/Defaults.lean | 4 ++++ src/lake/Lake/Config/Dependency.lean | 2 ++ src/lake/Lake/Config/Env.lean | 1 + src/lake/Lake/Config/ExternLib.lean | 1 + src/lake/Lake/Config/ExternLibConfig.lean | 1 + src/lake/Lake/Config/FacetConfig.lean | 1 + src/lake/Lake/Config/Glob.lean | 1 + src/lake/Lake/Config/InstallPath.lean | 2 ++ src/lake/Lake/Config/Lang.lean | 3 +++ src/lake/Lake/Config/LeanConfig.lean | 1 + src/lake/Lake/Config/LeanExe.lean | 1 + src/lake/Lake/Config/LeanExeConfig.lean | 1 + src/lake/Lake/Config/LeanLib.lean | 1 + src/lake/Lake/Config/LeanLibConfig.lean | 1 + src/lake/Lake/Config/Module.lean | 1 + src/lake/Lake/Config/Monad.lean | 1 + src/lake/Lake/Config/Opaque.lean | 1 + src/lake/Lake/Config/Package.lean | 1 + src/lake/Lake/Config/Script.lean | 1 + src/lake/Lake/Config/TargetConfig.lean | 1 + src/lake/Lake/Config/Workspace.lean | 1 + src/lake/Lake/Config/WorkspaceConfig.lean | 1 + src/lake/Lake/DSL.lean | 1 + src/lake/Lake/DSL/Attributes.lean | 1 + src/lake/Lake/DSL/AttributesCore.lean | 1 + src/lake/Lake/DSL/Config.lean | 1 + src/lake/Lake/DSL/DeclUtil.lean | 1 + src/lake/Lake/DSL/Extensions.lean | 1 + src/lake/Lake/DSL/Meta.lean | 1 + src/lake/Lake/DSL/Package.lean | 1 + src/lake/Lake/DSL/Require.lean | 1 + src/lake/Lake/DSL/Script.lean | 1 + src/lake/Lake/DSL/Targets.lean | 1 + src/lake/Lake/Load.lean | 1 + src/lake/Lake/Load/Config.lean | 1 + src/lake/Lake/Load/Lean.lean | 1 + src/lake/Lake/Load/Lean/Elab.lean | 1 + src/lake/Lake/Load/Lean/Eval.lean | 1 + src/lake/Lake/Load/Manifest.lean | 1 + src/lake/Lake/Load/Materialize.lean | 1 + src/lake/Lake/Load/Package.lean | 1 + src/lake/Lake/Load/Resolve.lean | 1 + src/lake/Lake/Load/Toml.lean | 1 + src/lake/Lake/Load/Workspace.lean | 1 + src/lake/Lake/Reservoir.lean | 1 + src/lake/Lake/Toml.lean | 1 + src/lake/Lake/Toml/Data.lean | 1 + src/lake/Lake/Toml/Data/DateTime.lean | 1 + src/lake/Lake/Toml/Data/Dict.lean | 11 ++++----- src/lake/Lake/Toml/Data/Value.lean | 2 ++ src/lake/Lake/Toml/Decode.lean | 2 ++ src/lake/Lake/Toml/Elab.lean | 1 + src/lake/Lake/Toml/Elab/Expression.lean | 1 + src/lake/Lake/Toml/Elab/Value.lean | 1 + src/lake/Lake/Toml/Encode.lean | 1 + src/lake/Lake/Toml/Grammar.lean | 1 + src/lake/Lake/Toml/Load.lean | 1 + src/lake/Lake/Toml/ParserUtil.lean | 1 + src/lake/Lake/Util/Binder.lean | 1 + src/lake/Lake/Util/Casing.lean | 4 ++++ src/lake/Lake/Util/Cli.lean | 25 ++++++++++++++++----- src/lake/Lake/Util/Compare.lean | 2 ++ src/lake/Lake/Util/Cycle.lean | 3 +++ src/lake/Lake/Util/DRBMap.lean | 1 + src/lake/Lake/Util/Date.lean | 2 ++ src/lake/Lake/Util/EStateT.lean | 2 ++ src/lake/Lake/Util/EquipT.lean | 3 +++ src/lake/Lake/Util/Error.lean | 3 +++ src/lake/Lake/Util/Exit.lean | 3 +++ src/lake/Lake/Util/Family.lean | 1 + src/lake/Lake/Util/FilePath.lean | 2 +- src/lake/Lake/Util/Git.lean | 1 + src/lake/Lake/Util/IO.lean | 2 ++ src/lake/Lake/Util/JsonObject.lean | 1 + src/lake/Lake/Util/Lift.lean | 4 ++++ src/lake/Lake/Util/List.lean | 6 ++--- src/lake/Lake/Util/Lock.lean | 2 ++ src/lake/Lake/Util/Log.lean | 1 + src/lake/Lake/Util/MainM.lean | 1 + src/lake/Lake/Util/Message.lean | 1 + src/lake/Lake/Util/Name.lean | 1 + src/lake/Lake/Util/NativeLib.lean | 2 ++ src/lake/Lake/Util/Opaque.lean | 1 + src/lake/Lake/Util/OrdHashSet.lean | 1 + src/lake/Lake/Util/OrderedTagAttribute.lean | 1 + src/lake/Lake/Util/Proc.lean | 1 + src/lake/Lake/Util/RBArray.lean | 1 + src/lake/Lake/Util/Store.lean | 3 +++ src/lake/Lake/Util/StoreInsts.lean | 1 + src/lake/Lake/Util/Sugar.lean | 3 +++ src/lake/Lake/Util/Task.lean | 3 +++ src/lake/Lake/Util/Version.lean | 1 + src/lake/Lake/Version.lean | 2 ++ src/lake/LakeMain.lean | 1 + 130 files changed, 194 insertions(+), 16 deletions(-) diff --git a/.github/workflows/check-prelude.yml b/.github/workflows/check-prelude.yml index 049aad9b2439..cec957f6366f 100644 --- a/.github/workflows/check-prelude.yml +++ b/.github/workflows/check-prelude.yml @@ -14,6 +14,7 @@ jobs: sparse-checkout: | src/Lean src/Std + src/lake/Lake - name: Check Prelude run: | failed_files="" @@ -21,7 +22,7 @@ jobs: if ! grep -q "^prelude$" "$file"; then failed_files="$failed_files$file\n" fi - done < <(find src/Lean src/Std -name '*.lean' -print0) + done < <(find src/Lean src/Std src/lake/Lake -name '*.lean' -print0) if [ -n "$failed_files" ]; then echo -e "The following files should use 'prelude':\n$failed_files" exit 1 diff --git a/src/lake/Lake.lean b/src/lake/Lake.lean index 09633bb52453..57ff3aa4fb0c 100644 --- a/src/lake/Lake.lean +++ b/src/lake/Lake.lean @@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude import Lake.Build import Lake.Config import Lake.DSL diff --git a/src/lake/Lake/Build.lean b/src/lake/Lake/Build.lean index 528d75cdaddd..2bc56f42c067 100644 --- a/src/lake/Lake/Build.lean +++ b/src/lake/Lake/Build.lean @@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude import Lake.Build.Run import Lake.Build.Module import Lake.Build.Package diff --git a/src/lake/Lake/Build/Actions.lean b/src/lake/Lake/Build/Actions.lean index afb7bdb5384c..30388d933a34 100644 --- a/src/lake/Lake/Build/Actions.lean +++ b/src/lake/Lake/Build/Actions.lean @@ -3,6 +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, Siddharth Bhat -/ +prelude import Lake.Util.Proc import Lake.Util.NativeLib import Lake.Util.IO diff --git a/src/lake/Lake/Build/Basic.lean b/src/lake/Lake/Build/Basic.lean index 446264f8aa0e..c18e5c764c0b 100644 --- a/src/lake/Lake/Build/Basic.lean +++ b/src/lake/Lake/Build/Basic.lean @@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude import Lake.Util.Log import Lake.Util.Exit import Lake.Util.Lift diff --git a/src/lake/Lake/Build/Common.lean b/src/lake/Lake/Build/Common.lean index 4917f5ad181a..7658b3483fc6 100644 --- a/src/lake/Lake/Build/Common.lean +++ b/src/lake/Lake/Build/Common.lean @@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude import Lake.Config.Monad import Lake.Build.Actions import Lake.Util.JsonObject diff --git a/src/lake/Lake/Build/Data.lean b/src/lake/Lake/Build/Data.lean index 799f105e23bc..77f4d4276c7a 100644 --- a/src/lake/Lake/Build/Data.lean +++ b/src/lake/Lake/Build/Data.lean @@ -3,6 +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 -/ +prelude import Lake.Build.Key import Lake.Util.Family diff --git a/src/lake/Lake/Build/Executable.lean b/src/lake/Lake/Build/Executable.lean index ff8ec5239136..53999a4b2be7 100644 --- a/src/lake/Lake/Build/Executable.lean +++ b/src/lake/Lake/Build/Executable.lean @@ -3,6 +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 -/ +prelude import Lake.Build.Common namespace Lake diff --git a/src/lake/Lake/Build/Facets.lean b/src/lake/Lake/Build/Facets.lean index bf9bb43eb838..9299dee7255b 100644 --- a/src/lake/Lake/Build/Facets.lean +++ b/src/lake/Lake/Build/Facets.lean @@ -3,6 +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 -/ +prelude import Lake.Build.Job import Lake.Build.Data diff --git a/src/lake/Lake/Build/Fetch.lean b/src/lake/Lake/Build/Fetch.lean index 4359122c41bc..38e9dc7a010f 100644 --- a/src/lake/Lake/Build/Fetch.lean +++ b/src/lake/Lake/Build/Fetch.lean @@ -3,6 +3,7 @@ Copyright (c) 2024 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude import Lake.Util.Error import Lake.Util.Cycle import Lake.Util.EquipT diff --git a/src/lake/Lake/Build/Imports.lean b/src/lake/Lake/Build/Imports.lean index bfe43cfd56ca..efbb03ca3897 100644 --- a/src/lake/Lake/Build/Imports.lean +++ b/src/lake/Lake/Build/Imports.lean @@ -3,6 +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 -/ +prelude import Lake.Build.Module /-! diff --git a/src/lake/Lake/Build/Index.lean b/src/lake/Lake/Build/Index.lean index 73a1db2ca3f1..b696f7db814b 100644 --- a/src/lake/Lake/Build/Index.lean +++ b/src/lake/Lake/Build/Index.lean @@ -3,6 +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 -/ +prelude import Lake.Build.Executable import Lake.Build.Topological diff --git a/src/lake/Lake/Build/Info.lean b/src/lake/Lake/Build/Info.lean index 405f19763268..115cd88bd696 100644 --- a/src/lake/Lake/Build/Info.lean +++ b/src/lake/Lake/Build/Info.lean @@ -3,6 +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 -/ +prelude import Lake.Config.LeanExe import Lake.Config.ExternLib import Lake.Build.Facets diff --git a/src/lake/Lake/Build/Job.lean b/src/lake/Lake/Build/Job.lean index 4bc441c18e05..bcff6b3ea010 100644 --- a/src/lake/Lake/Build/Job.lean +++ b/src/lake/Lake/Build/Job.lean @@ -3,6 +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 -/ +prelude import Lake.Util.Task import Lake.Build.Basic diff --git a/src/lake/Lake/Build/Key.lean b/src/lake/Lake/Build/Key.lean index 6619ecc32d82..97b6329fe88e 100644 --- a/src/lake/Lake/Build/Key.lean +++ b/src/lake/Lake/Build/Key.lean @@ -3,6 +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 -/ +prelude import Lake.Util.Name namespace Lake diff --git a/src/lake/Lake/Build/Library.lean b/src/lake/Lake/Build/Library.lean index 27db61dad0b7..8849b403dc0f 100644 --- a/src/lake/Lake/Build/Library.lean +++ b/src/lake/Lake/Build/Library.lean @@ -3,6 +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 -/ +prelude import Lake.Build.Common import Lake.Build.Targets diff --git a/src/lake/Lake/Build/Module.lean b/src/lake/Lake/Build/Module.lean index 03ca79436beb..253c78dd900a 100644 --- a/src/lake/Lake/Build/Module.lean +++ b/src/lake/Lake/Build/Module.lean @@ -3,6 +3,7 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Sebastian Ullrich, Mac Malone, Siddharth Bhat -/ +prelude import Lake.Util.OrdHashSet import Lake.Util.List import Lean.Elab.ParseImportsFast diff --git a/src/lake/Lake/Build/Package.lean b/src/lake/Lake/Build/Package.lean index ec8185b0ffc3..35ee042fdc89 100644 --- a/src/lake/Lake/Build/Package.lean +++ b/src/lake/Lake/Build/Package.lean @@ -3,6 +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 -/ +prelude import Lake.Util.Git import Lake.Util.Sugar import Lake.Build.Common diff --git a/src/lake/Lake/Build/Run.lean b/src/lake/Lake/Build/Run.lean index 6ca3671a9b48..43bf3f92b9dc 100644 --- a/src/lake/Lake/Build/Run.lean +++ b/src/lake/Lake/Build/Run.lean @@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone, Gabriel Ebner, Sebastian Ullrich -/ +prelude import Lake.Util.Lock import Lake.Build.Index diff --git a/src/lake/Lake/Build/Store.lean b/src/lake/Lake/Build/Store.lean index 40b534c64d94..ba1a3fa0faeb 100644 --- a/src/lake/Lake/Build/Store.lean +++ b/src/lake/Lake/Build/Store.lean @@ -3,6 +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 -/ +prelude import Lake.Build.Data import Lake.Util.StoreInsts diff --git a/src/lake/Lake/Build/Targets.lean b/src/lake/Lake/Build/Targets.lean index 4901eca6edb9..9a51def55f5b 100644 --- a/src/lake/Lake/Build/Targets.lean +++ b/src/lake/Lake/Build/Targets.lean @@ -3,6 +3,7 @@ Copyright (c) 2023 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude import Lake.Config.Monad /-! # Build Target Fetching diff --git a/src/lake/Lake/Build/Topological.lean b/src/lake/Lake/Build/Topological.lean index b5bb54ee00c4..b6e5962ca664 100644 --- a/src/lake/Lake/Build/Topological.lean +++ b/src/lake/Lake/Build/Topological.lean @@ -3,6 +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 -/ +prelude import Lake.Util.Cycle import Lake.Util.Store import Lake.Util.EquipT diff --git a/src/lake/Lake/Build/Trace.lean b/src/lake/Lake/Build/Trace.lean index 2552f6e3e254..3980b6e1741a 100644 --- a/src/lake/Lake/Build/Trace.lean +++ b/src/lake/Lake/Build/Trace.lean @@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude import Lake.Util.IO import Lean.Data.Json diff --git a/src/lake/Lake/CLI.lean b/src/lake/Lake/CLI.lean index 2695b6a4cf4d..da2a7ade7272 100644 --- a/src/lake/Lake/CLI.lean +++ b/src/lake/Lake/CLI.lean @@ -3,4 +3,5 @@ Copyright (c) 2021 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude import Lake.CLI.Main diff --git a/src/lake/Lake/CLI/Actions.lean b/src/lake/Lake/CLI/Actions.lean index a627be0d6612..732a0a5f42fe 100644 --- a/src/lake/Lake/CLI/Actions.lean +++ b/src/lake/Lake/CLI/Actions.lean @@ -3,6 +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 -/ +prelude import Lake.Build.Run import Lake.Build.Targets import Lake.CLI.Build diff --git a/src/lake/Lake/CLI/Build.lean b/src/lake/Lake/CLI/Build.lean index 9f47c117f284..05aaa760a6c1 100644 --- a/src/lake/Lake/CLI/Build.lean +++ b/src/lake/Lake/CLI/Build.lean @@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude import Lake.Build.Index import Lake.CLI.Error diff --git a/src/lake/Lake/CLI/Error.lean b/src/lake/Lake/CLI/Error.lean index 221b91193e02..37d97c541dd1 100644 --- a/src/lake/Lake/CLI/Error.lean +++ b/src/lake/Lake/CLI/Error.lean @@ -3,6 +3,9 @@ Copyright (c) 2022 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude +import Init.Data.ToString +import Init.System.FilePath namespace Lake open Lean (Name) diff --git a/src/lake/Lake/CLI/Help.lean b/src/lake/Lake/CLI/Help.lean index 1ef1390e24f5..26a4f44005fb 100644 --- a/src/lake/Lake/CLI/Help.lean +++ b/src/lake/Lake/CLI/Help.lean @@ -3,6 +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 -/ +prelude import Lake.Version namespace Lake diff --git a/src/lake/Lake/CLI/Init.lean b/src/lake/Lake/CLI/Init.lean index a36ca4792020..9b2bbacda722 100644 --- a/src/lake/Lake/CLI/Init.lean +++ b/src/lake/Lake/CLI/Init.lean @@ -3,6 +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 -/ +prelude import Lake.Util.Git import Lake.Util.Sugar import Lake.Util.Version diff --git a/src/lake/Lake/CLI/Main.lean b/src/lake/Lake/CLI/Main.lean index ec27ba1b129f..b333732aed21 100644 --- a/src/lake/Lake/CLI/Main.lean +++ b/src/lake/Lake/CLI/Main.lean @@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude import Lake.Load import Lake.Build.Imports import Lake.Util.Error diff --git a/src/lake/Lake/CLI/Serve.lean b/src/lake/Lake/CLI/Serve.lean index eab1b99439b0..4598b7206e94 100644 --- a/src/lake/Lake/CLI/Serve.lean +++ b/src/lake/Lake/CLI/Serve.lean @@ -3,6 +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 -/ +prelude import Lake.Load import Lake.Build import Lake.Util.MainM diff --git a/src/lake/Lake/CLI/Translate.lean b/src/lake/Lake/CLI/Translate.lean index 9a75e638cfd9..943b4d195bbd 100644 --- a/src/lake/Lake/CLI/Translate.lean +++ b/src/lake/Lake/CLI/Translate.lean @@ -3,6 +3,7 @@ Copyright (c) 2024 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude import Lake.Config.Lang import Lake.Config.Package import Lake.CLI.Translate.Toml diff --git a/src/lake/Lake/CLI/Translate/Lean.lean b/src/lake/Lake/CLI/Translate/Lean.lean index 0319dd77d01b..ad00fe069120 100644 --- a/src/lake/Lake/CLI/Translate/Lean.lean +++ b/src/lake/Lake/CLI/Translate/Lean.lean @@ -3,6 +3,7 @@ Copyright (c) 2024 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude import Lake.DSL import Lake.Config.Package import Lean.Parser.Module diff --git a/src/lake/Lake/CLI/Translate/Toml.lean b/src/lake/Lake/CLI/Translate/Toml.lean index 50a7c58a830c..5f75fa843091 100644 --- a/src/lake/Lake/CLI/Translate/Toml.lean +++ b/src/lake/Lake/CLI/Translate/Toml.lean @@ -3,6 +3,7 @@ Copyright (c) 2024 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude import Lake.Toml.Encode import Lake.Config.Package diff --git a/src/lake/Lake/Config.lean b/src/lake/Lake/Config.lean index cc67357d0adb..0677dbc6c978 100644 --- a/src/lake/Lake/Config.lean +++ b/src/lake/Lake/Config.lean @@ -3,4 +3,5 @@ Copyright (c) 2021 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude import Lake.Config.Monad diff --git a/src/lake/Lake/Config/Context.lean b/src/lake/Lake/Config/Context.lean index b3bdb799c227..01fc2c4dd2c5 100644 --- a/src/lake/Lake/Config/Context.lean +++ b/src/lake/Lake/Config/Context.lean @@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude import Lake.Config.Opaque import Lake.Config.InstallPath diff --git a/src/lake/Lake/Config/Defaults.lean b/src/lake/Lake/Config/Defaults.lean index 60ff94095f2f..36ea4f8a02c2 100644 --- a/src/lake/Lake/Config/Defaults.lean +++ b/src/lake/Lake/Config/Defaults.lean @@ -3,7 +3,11 @@ Copyright (c) 2022 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude +import Init.System.FilePath + namespace Lake + open System (FilePath) /-- diff --git a/src/lake/Lake/Config/Dependency.lean b/src/lake/Lake/Config/Dependency.lean index 6ee9ee701e1c..246c4b68d565 100644 --- a/src/lake/Lake/Config/Dependency.lean +++ b/src/lake/Lake/Config/Dependency.lean @@ -3,6 +3,8 @@ 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 -/ +prelude +import Init.System.FilePath import Lean.Data.NameMap /- # Package Dependency Configuration diff --git a/src/lake/Lake/Config/Env.lean b/src/lake/Lake/Config/Env.lean index e50343c480e1..1f99bb5c4797 100644 --- a/src/lake/Lake/Config/Env.lean +++ b/src/lake/Lake/Config/Env.lean @@ -3,6 +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 -/ +prelude import Lake.Util.Name import Lake.Util.NativeLib import Lake.Config.InstallPath diff --git a/src/lake/Lake/Config/ExternLib.lean b/src/lake/Lake/Config/ExternLib.lean index cbda507695e6..92020e374ade 100644 --- a/src/lake/Lake/Config/ExternLib.lean +++ b/src/lake/Lake/Config/ExternLib.lean @@ -3,6 +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 -/ +prelude import Lake.Config.Package namespace Lake diff --git a/src/lake/Lake/Config/ExternLibConfig.lean b/src/lake/Lake/Config/ExternLibConfig.lean index fbc52a051a0e..16644168f1f6 100644 --- a/src/lake/Lake/Config/ExternLibConfig.lean +++ b/src/lake/Lake/Config/ExternLibConfig.lean @@ -3,6 +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 -/ +prelude import Lake.Build.Job import Lake.Build.Data diff --git a/src/lake/Lake/Config/FacetConfig.lean b/src/lake/Lake/Config/FacetConfig.lean index 63d1090b05f9..ffb3609e39ae 100644 --- a/src/lake/Lake/Config/FacetConfig.lean +++ b/src/lake/Lake/Config/FacetConfig.lean @@ -3,6 +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, Mario Carneiro -/ +prelude import Lake.Build.Fetch namespace Lake diff --git a/src/lake/Lake/Config/Glob.lean b/src/lake/Lake/Config/Glob.lean index 26637af7e7de..15d893b6663a 100644 --- a/src/lake/Lake/Config/Glob.lean +++ b/src/lake/Lake/Config/Glob.lean @@ -3,6 +3,7 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mario Carneiro, Mac Malone -/ +prelude import Lean.Util.Path import Lake.Util.Name diff --git a/src/lake/Lake/Config/InstallPath.lean b/src/lake/Lake/Config/InstallPath.lean index a0877ef9316f..b9ffc6e0c2ca 100644 --- a/src/lake/Lake/Config/InstallPath.lean +++ b/src/lake/Lake/Config/InstallPath.lean @@ -3,6 +3,8 @@ Copyright (c) 2021 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude +import Init.Control.Option import Lake.Util.NativeLib import Lake.Config.Defaults diff --git a/src/lake/Lake/Config/Lang.lean b/src/lake/Lake/Config/Lang.lean index d12e9b0fdc99..b686dada0749 100644 --- a/src/lake/Lake/Config/Lang.lean +++ b/src/lake/Lake/Config/Lang.lean @@ -3,6 +3,9 @@ Copyright (c) 2024 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude +import Init.Data.ToString.Basic + namespace Lake /-- Lake configuration language identifier. -/ diff --git a/src/lake/Lake/Config/LeanConfig.lean b/src/lake/Lake/Config/LeanConfig.lean index 464b9907f61d..6c2337c83111 100644 --- a/src/lake/Lake/Config/LeanConfig.lean +++ b/src/lake/Lake/Config/LeanConfig.lean @@ -3,6 +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 -/ +prelude import Lean.Util.LeanOptions namespace Lake diff --git a/src/lake/Lake/Config/LeanExe.lean b/src/lake/Lake/Config/LeanExe.lean index dc880b08e5c6..fcef19affe04 100644 --- a/src/lake/Lake/Config/LeanExe.lean +++ b/src/lake/Lake/Config/LeanExe.lean @@ -3,6 +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 -/ +prelude import Lean.Compiler.FFI import Lake.Config.Module diff --git a/src/lake/Lake/Config/LeanExeConfig.lean b/src/lake/Lake/Config/LeanExeConfig.lean index 347383c6ad79..51598dc1ec9b 100644 --- a/src/lake/Lake/Config/LeanExeConfig.lean +++ b/src/lake/Lake/Config/LeanExeConfig.lean @@ -3,6 +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 -/ +prelude import Lake.Build.Facets import Lake.Config.LeanConfig diff --git a/src/lake/Lake/Config/LeanLib.lean b/src/lake/Lake/Config/LeanLib.lean index 7a6af946ec8d..50f76f061b57 100644 --- a/src/lake/Lake/Config/LeanLib.lean +++ b/src/lake/Lake/Config/LeanLib.lean @@ -3,6 +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 -/ +prelude import Lake.Config.Package namespace Lake diff --git a/src/lake/Lake/Config/LeanLibConfig.lean b/src/lake/Lake/Config/LeanLibConfig.lean index 0bae37ff3f12..7b28084bd949 100644 --- a/src/lake/Lake/Config/LeanLibConfig.lean +++ b/src/lake/Lake/Config/LeanLibConfig.lean @@ -3,6 +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 -/ +prelude import Lake.Util.Casing import Lake.Build.Facets import Lake.Config.InstallPath diff --git a/src/lake/Lake/Config/Module.lean b/src/lake/Lake/Config/Module.lean index 51e9e6a1c5b4..a0a3124e20d5 100644 --- a/src/lake/Lake/Config/Module.lean +++ b/src/lake/Lake/Config/Module.lean @@ -3,6 +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 -/ +prelude import Lake.Build.Trace import Lake.Config.LeanLib import Lake.Util.OrdHashSet diff --git a/src/lake/Lake/Config/Monad.lean b/src/lake/Lake/Config/Monad.lean index a548520a303b..8f426c846e88 100644 --- a/src/lake/Lake/Config/Monad.lean +++ b/src/lake/Lake/Config/Monad.lean @@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude import Lake.Config.Context import Lake.Config.Workspace diff --git a/src/lake/Lake/Config/Opaque.lean b/src/lake/Lake/Config/Opaque.lean index 9f3e2eba19de..bcf5c32c3a1f 100644 --- a/src/lake/Lake/Config/Opaque.lean +++ b/src/lake/Lake/Config/Opaque.lean @@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude import Lake.Util.Name import Lake.Util.Opaque diff --git a/src/lake/Lake/Config/Package.lean b/src/lake/Lake/Config/Package.lean index 16498576bf9a..4bbdec2886c0 100644 --- a/src/lake/Lake/Config/Package.lean +++ b/src/lake/Lake/Config/Package.lean @@ -3,6 +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 -/ +prelude import Lake.Config.Opaque import Lake.Config.Defaults import Lake.Config.LeanLibConfig diff --git a/src/lake/Lake/Config/Script.lean b/src/lake/Lake/Config/Script.lean index b80f37a6696a..becd5ecf3728 100644 --- a/src/lake/Lake/Config/Script.lean +++ b/src/lake/Lake/Config/Script.lean @@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude import Lake.Util.Exit import Lake.Config.Context diff --git a/src/lake/Lake/Config/TargetConfig.lean b/src/lake/Lake/Config/TargetConfig.lean index db754244e260..4169990b40c9 100644 --- a/src/lake/Lake/Config/TargetConfig.lean +++ b/src/lake/Lake/Config/TargetConfig.lean @@ -3,6 +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 -/ +prelude import Lake.Build.Fetch namespace Lake diff --git a/src/lake/Lake/Config/Workspace.lean b/src/lake/Lake/Config/Workspace.lean index 29638b2c9df5..eddf6dba5964 100644 --- a/src/lake/Lake/Config/Workspace.lean +++ b/src/lake/Lake/Config/Workspace.lean @@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude import Lean.Util.Paths import Lake.Config.FacetConfig import Lake.Config.TargetConfig diff --git a/src/lake/Lake/Config/WorkspaceConfig.lean b/src/lake/Lake/Config/WorkspaceConfig.lean index b5250d953672..cd4d16b54b0e 100644 --- a/src/lake/Lake/Config/WorkspaceConfig.lean +++ b/src/lake/Lake/Config/WorkspaceConfig.lean @@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude import Lake.Config.Defaults open System diff --git a/src/lake/Lake/DSL.lean b/src/lake/Lake/DSL.lean index ec4003ad61bc..4240392b199e 100644 --- a/src/lake/Lake/DSL.lean +++ b/src/lake/Lake/DSL.lean @@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude import Lake.DSL.DeclUtil import Lake.DSL.Attributes import Lake.DSL.Extensions diff --git a/src/lake/Lake/DSL/Attributes.lean b/src/lake/Lake/DSL/Attributes.lean index 7c89acd56cb8..ad9ef0e3e5fb 100644 --- a/src/lake/Lake/DSL/Attributes.lean +++ b/src/lake/Lake/DSL/Attributes.lean @@ -3,6 +3,7 @@ Copyright (c) 2024 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude import Lake.DSL.AttributesCore open Lean diff --git a/src/lake/Lake/DSL/AttributesCore.lean b/src/lake/Lake/DSL/AttributesCore.lean index ad5a00878c30..89784b9eeb7b 100644 --- a/src/lake/Lake/DSL/AttributesCore.lean +++ b/src/lake/Lake/DSL/AttributesCore.lean @@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude import Lake.Util.OrderedTagAttribute open Lean diff --git a/src/lake/Lake/DSL/Config.lean b/src/lake/Lake/DSL/Config.lean index 1ea682f2b70d..20c9bd8ccb83 100644 --- a/src/lake/Lake/DSL/Config.lean +++ b/src/lake/Lake/DSL/Config.lean @@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude import Lean.Elab.ElabRules import Lake.DSL.Extensions diff --git a/src/lake/Lake/DSL/DeclUtil.lean b/src/lake/Lake/DSL/DeclUtil.lean index ce098a62d9b4..6bff854c2f6f 100644 --- a/src/lake/Lake/DSL/DeclUtil.lean +++ b/src/lake/Lake/DSL/DeclUtil.lean @@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude import Lake.DSL.Config import Lake.Util.Binder import Lake.Util.Name diff --git a/src/lake/Lake/DSL/Extensions.lean b/src/lake/Lake/DSL/Extensions.lean index 453f840009c3..150805a4f9e4 100644 --- a/src/lake/Lake/DSL/Extensions.lean +++ b/src/lake/Lake/DSL/Extensions.lean @@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude import Lean.Environment open Lean diff --git a/src/lake/Lake/DSL/Meta.lean b/src/lake/Lake/DSL/Meta.lean index 91cb3540bddf..8251cf7bde73 100644 --- a/src/lake/Lake/DSL/Meta.lean +++ b/src/lake/Lake/DSL/Meta.lean @@ -3,6 +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 -/ +prelude import Lean.Elab.Eval import Lean.Elab.ElabRules import Lake.Util.FilePath diff --git a/src/lake/Lake/DSL/Package.lean b/src/lake/Lake/DSL/Package.lean index 25c42390d463..ac51c26fdf16 100644 --- a/src/lake/Lake/DSL/Package.lean +++ b/src/lake/Lake/DSL/Package.lean @@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude import Lake.Config.Package import Lake.DSL.Attributes import Lake.DSL.DeclUtil diff --git a/src/lake/Lake/DSL/Require.lean b/src/lake/Lake/DSL/Require.lean index 76a0dd4ca04c..7fec264f741d 100644 --- a/src/lake/Lake/DSL/Require.lean +++ b/src/lake/Lake/DSL/Require.lean @@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude import Lean.Parser.Command import Lake.Config.Dependency import Lake.DSL.Extensions diff --git a/src/lake/Lake/DSL/Script.lean b/src/lake/Lake/DSL/Script.lean index 9eb3f9417e80..9565f0cf88cf 100644 --- a/src/lake/Lake/DSL/Script.lean +++ b/src/lake/Lake/DSL/Script.lean @@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude import Lake.Config.Package import Lake.DSL.Attributes import Lake.DSL.DeclUtil diff --git a/src/lake/Lake/DSL/Targets.lean b/src/lake/Lake/DSL/Targets.lean index 650ae2207062..c8c4bc36920c 100644 --- a/src/lake/Lake/DSL/Targets.lean +++ b/src/lake/Lake/DSL/Targets.lean @@ -3,6 +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 -/ +prelude import Lake.DSL.DeclUtil import Lake.Build.Index diff --git a/src/lake/Lake/Load.lean b/src/lake/Lake/Load.lean index 9b71d35bb7c7..bfc557c1af95 100644 --- a/src/lake/Lake/Load.lean +++ b/src/lake/Lake/Load.lean @@ -3,4 +3,5 @@ Copyright (c) 2022 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude import Lake.Load.Workspace diff --git a/src/lake/Lake/Load/Config.lean b/src/lake/Lake/Load/Config.lean index d5929bf8cd4b..f9027af7fe68 100644 --- a/src/lake/Lake/Load/Config.lean +++ b/src/lake/Lake/Load/Config.lean @@ -3,6 +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 -/ +prelude import Lean.Data.Name import Lean.Data.Options import Lake.Config.Defaults diff --git a/src/lake/Lake/Load/Lean.lean b/src/lake/Lake/Load/Lean.lean index 08aab790c347..c95e6a24e3b8 100644 --- a/src/lake/Lake/Load/Lean.lean +++ b/src/lake/Lake/Load/Lean.lean @@ -3,6 +3,7 @@ Copyright (c) 2024 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude import Lake.Load.Lean.Elab import Lake.Load.Lean.Eval diff --git a/src/lake/Lake/Load/Lean/Elab.lean b/src/lake/Lake/Load/Lean/Elab.lean index 20d5334464cb..c83fe093df16 100644 --- a/src/lake/Lake/Load/Lean/Elab.lean +++ b/src/lake/Lake/Load/Lean/Elab.lean @@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude import Lean.Elab.Frontend import Lake.DSL.Extensions import Lake.DSL.Attributes diff --git a/src/lake/Lake/Load/Lean/Eval.lean b/src/lake/Lake/Load/Lean/Eval.lean index 67ed546e412b..244ae86c8213 100644 --- a/src/lake/Lake/Load/Lean/Eval.lean +++ b/src/lake/Lake/Load/Lean/Eval.lean @@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude import Lake.DSL.Attributes import Lake.Config.Workspace import Lean.DocString diff --git a/src/lake/Lake/Load/Manifest.lean b/src/lake/Lake/Load/Manifest.lean index 3aa23a7c0044..f15b70f781d5 100644 --- a/src/lake/Lake/Load/Manifest.lean +++ b/src/lake/Lake/Load/Manifest.lean @@ -3,6 +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, Gabriel Ebner -/ +prelude import Lake.Util.Log import Lake.Util.Name import Lake.Util.FilePath diff --git a/src/lake/Lake/Load/Materialize.lean b/src/lake/Lake/Load/Materialize.lean index b8a7268082a4..c3c514dcbff3 100644 --- a/src/lake/Lake/Load/Materialize.lean +++ b/src/lake/Lake/Load/Materialize.lean @@ -3,6 +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 -/ +prelude import Lake.Util.Git import Lake.Load.Manifest import Lake.Config.Dependency diff --git a/src/lake/Lake/Load/Package.lean b/src/lake/Lake/Load/Package.lean index fc6b970ee1a6..173bc972ba10 100644 --- a/src/lake/Lake/Load/Package.lean +++ b/src/lake/Lake/Load/Package.lean @@ -3,6 +3,7 @@ Copyright (c) 2024 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude import Lake.Load.Lean import Lake.Load.Toml diff --git a/src/lake/Lake/Load/Resolve.lean b/src/lake/Lake/Load/Resolve.lean index 9d4888aae026..f52d06b01330 100644 --- a/src/lake/Lake/Load/Resolve.lean +++ b/src/lake/Lake/Load/Resolve.lean @@ -3,6 +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, Gabriel Ebner -/ +prelude import Lake.Config.Monad import Lake.Util.StoreInsts import Lake.Build.Topological diff --git a/src/lake/Lake/Load/Toml.lean b/src/lake/Lake/Load/Toml.lean index 59955be78855..ce0271df81a1 100644 --- a/src/lake/Lake/Load/Toml.lean +++ b/src/lake/Lake/Load/Toml.lean @@ -3,6 +3,7 @@ Copyright (c) 2024 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude import Lake.Toml.Load import Lake.Toml.Decode import Lake.Config.Package diff --git a/src/lake/Lake/Load/Workspace.lean b/src/lake/Lake/Load/Workspace.lean index c17adecbc17a..32d2a84cae30 100644 --- a/src/lake/Lake/Load/Workspace.lean +++ b/src/lake/Lake/Load/Workspace.lean @@ -3,6 +3,7 @@ Copyright (c) 2024 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude import Lake.Load.Resolve import Lake.Build.Module import Lake.Build.Package diff --git a/src/lake/Lake/Reservoir.lean b/src/lake/Lake/Reservoir.lean index 2ed295344164..8ebfc93213cb 100644 --- a/src/lake/Lake/Reservoir.lean +++ b/src/lake/Lake/Reservoir.lean @@ -3,6 +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 -/ +prelude import Lake.Util.Log import Lake.Util.Proc import Lake.Util.JsonObject diff --git a/src/lake/Lake/Toml.lean b/src/lake/Lake/Toml.lean index df3e653e59d7..1fb1f0a4e690 100644 --- a/src/lake/Lake/Toml.lean +++ b/src/lake/Lake/Toml.lean @@ -3,4 +3,5 @@ Copyright (c) 2024 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude import Lake.Toml.Load diff --git a/src/lake/Lake/Toml/Data.lean b/src/lake/Lake/Toml/Data.lean index 04ef0bc18185..f97a045e9dea 100644 --- a/src/lake/Lake/Toml/Data.lean +++ b/src/lake/Lake/Toml/Data.lean @@ -3,6 +3,7 @@ Copyright (c) 2024 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude import Lake.Toml.Data.Value /-! diff --git a/src/lake/Lake/Toml/Data/DateTime.lean b/src/lake/Lake/Toml/Data/DateTime.lean index 4b4c9a7b3856..da77dae5c984 100644 --- a/src/lake/Lake/Toml/Data/DateTime.lean +++ b/src/lake/Lake/Toml/Data/DateTime.lean @@ -3,6 +3,7 @@ Copyright (c) 2024 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude import Lake.Util.Date /-! diff --git a/src/lake/Lake/Toml/Data/Dict.lean b/src/lake/Lake/Toml/Data/Dict.lean index de40e3163bed..ae5476f55cd8 100644 --- a/src/lake/Lake/Toml/Data/Dict.lean +++ b/src/lake/Lake/Toml/Data/Dict.lean @@ -3,7 +3,9 @@ Copyright (c) 2024 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude import Lean.Data.NameMap +import Init.Data.Nat.Fold /-! # Red-Black Dictionary @@ -33,11 +35,10 @@ instance : EmptyCollection (RBDict α β cmp) := ⟨RBDict.empty⟩ def mkEmpty (capacity : Nat) : RBDict α β cmp := {items := .mkEmpty capacity, indices := {}} -def ofArray (items : Array (α × β)) : RBDict α β cmp := Id.run do - let mut indices := mkRBMap α Nat cmp - for h : i in [0:items.size] do - indices := indices.insert items[i].1 i - return {items, indices} +def ofArray (items : Array (α × β)) : RBDict α β cmp := + let indices := items.size.fold (init := mkRBMap α Nat cmp) fun i _ indices => + indices.insert items[i].1 i + {items, indices} protected def beq [BEq (α × β)] (self other : RBDict α β cmp) : Bool := self.items == other.items diff --git a/src/lake/Lake/Toml/Data/Value.lean b/src/lake/Lake/Toml/Data/Value.lean index be64ef8d875d..b76ed30cf8c1 100644 --- a/src/lake/Lake/Toml/Data/Value.lean +++ b/src/lake/Lake/Toml/Data/Value.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude +import Init.Data.Float import Lake.Toml.Data.Dict import Lake.Toml.Data.DateTime diff --git a/src/lake/Lake/Toml/Decode.lean b/src/lake/Lake/Toml/Decode.lean index 309db6f697a4..1d2e1b46cd64 100644 --- a/src/lake/Lake/Toml/Decode.lean +++ b/src/lake/Lake/Toml/Decode.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude +import Init.System.FilePath import Lake.Toml.Data /-! diff --git a/src/lake/Lake/Toml/Elab.lean b/src/lake/Lake/Toml/Elab.lean index 7403d606e1b4..e953ee92ebb1 100644 --- a/src/lake/Lake/Toml/Elab.lean +++ b/src/lake/Lake/Toml/Elab.lean @@ -3,6 +3,7 @@ Copyright (c) 2024 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude import Lake.Toml.Elab.Expression /-! diff --git a/src/lake/Lake/Toml/Elab/Expression.lean b/src/lake/Lake/Toml/Elab/Expression.lean index 081a0b668423..9f13942f8975 100644 --- a/src/lake/Lake/Toml/Elab/Expression.lean +++ b/src/lake/Lake/Toml/Elab/Expression.lean @@ -3,6 +3,7 @@ Copyright (c) 2024 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude import Lake.Toml.Elab.Value /-! diff --git a/src/lake/Lake/Toml/Elab/Value.lean b/src/lake/Lake/Toml/Elab/Value.lean index 7ba4a9085f15..7970ff7fa6f0 100644 --- a/src/lake/Lake/Toml/Elab/Value.lean +++ b/src/lake/Lake/Toml/Elab/Value.lean @@ -3,6 +3,7 @@ Copyright (c) 2024 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude import Lean.CoreM import Lake.Toml.Data.Value import Lake.Toml.Grammar diff --git a/src/lake/Lake/Toml/Encode.lean b/src/lake/Lake/Toml/Encode.lean index a3fde0ed4ead..e3e425df43c0 100644 --- a/src/lake/Lake/Toml/Encode.lean +++ b/src/lake/Lake/Toml/Encode.lean @@ -3,6 +3,7 @@ Copyright (c) 2024 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude import Lake.Toml.Data import Lake.Util.FilePath diff --git a/src/lake/Lake/Toml/Grammar.lean b/src/lake/Lake/Toml/Grammar.lean index 349d985bb206..805976e38a62 100644 --- a/src/lake/Lake/Toml/Grammar.lean +++ b/src/lake/Lake/Toml/Grammar.lean @@ -3,6 +3,7 @@ Copyright (c) 2024 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude import Lake.Toml.ParserUtil /-! diff --git a/src/lake/Lake/Toml/Load.lean b/src/lake/Lake/Toml/Load.lean index 919ff4e6941b..c5c518fae112 100644 --- a/src/lake/Lake/Toml/Load.lean +++ b/src/lake/Lake/Toml/Load.lean @@ -3,6 +3,7 @@ Copyright (c) 2024 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude import Lake.Toml.Elab import Lake.Util.Message diff --git a/src/lake/Lake/Toml/ParserUtil.lean b/src/lake/Lake/Toml/ParserUtil.lean index de874dc03549..b92cc1e42f18 100644 --- a/src/lake/Lake/Toml/ParserUtil.lean +++ b/src/lake/Lake/Toml/ParserUtil.lean @@ -3,6 +3,7 @@ Copyright (c) 2024 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude import Lean.Parser import Lean.PrettyPrinter.Formatter diff --git a/src/lake/Lake/Util/Binder.lean b/src/lake/Lake/Util/Binder.lean index 21adec6e6a0f..5ccc90bb6815 100644 --- a/src/lake/Lake/Util/Binder.lean +++ b/src/lake/Lake/Util/Binder.lean @@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude import Lean.Parser.Term import Lean.Elab.Term import Lean.Expr diff --git a/src/lake/Lake/Util/Casing.lean b/src/lake/Lake/Util/Casing.lean index 662c339f6113..56be3909213d 100644 --- a/src/lake/Lake/Util/Casing.lean +++ b/src/lake/Lake/Util/Casing.lean @@ -3,7 +3,11 @@ Copyright (c) 2022 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude +import Init.Data.String.Basic + namespace Lake + open Lean (Name) /-- Converts a snake case, kebab case, or lower camel case `String` to upper camel case. -/ diff --git a/src/lake/Lake/Util/Cli.lean b/src/lake/Lake/Util/Cli.lean index 4b8e5782b713..bb63bf9b00f0 100644 --- a/src/lake/Lake/Util/Cli.lean +++ b/src/lake/Lake/Util/Cli.lean @@ -3,6 +3,8 @@ Copyright (c) 2021 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude +import Init.Data.Array.Basic namespace Lake @@ -75,8 +77,18 @@ variable [Monad m] [MonadStateOf ArgList m] /-- Process a multiple short options grouped together (ex. `-xyz` as `x`, `y`, `z`). -/ @[inline] def multiShortOption (handle : Char → m PUnit) (opt : String) : m PUnit := do - -- TODO: this code is assuming all characters are ASCII. - for i in [1:opt.length] do handle (opt.get ⟨i⟩) + let rec loop (p : String.Pos) := do + if h : opt.atEnd p then + return + else + handle (opt.get' p h) + loop (opt.next' p h) + termination_by opt.utf8ByteSize - p.byteIdx + decreasing_by + simp [String.atEnd] at h + apply Nat.sub_lt_sub_left h + simp [String.lt_next opt p] + loop ⟨1⟩ /-- Splits a long option of the form `"--long foo bar"` into `--long` and `"foo bar"`. -/ @[inline] def longOptionOrSpace (handle : String → m α) (opt : String) : m α := @@ -102,8 +114,9 @@ variable [Monad m] [MonadStateOf ArgList m] /-- Process a short option of the form `-x`, `-x=arg`, `-x arg`, or `-long`. -/ @[inline] def shortOption -(shortHandle : Char → m α) (longHandle : String → m α) -(opt : String) : m α := + (shortHandle : Char → m α) (longHandle : String → m α) + (opt : String) +: m α := if opt.length == 2 then -- `-x` shortHandle (opt.get ⟨1⟩) else -- `-c(.+)` @@ -151,7 +164,9 @@ partial def processLeadingOptions (handle : String → m PUnit) : m PUnit := do processLeadingOptions handle /-- Process every option and collect the remaining arguments into an `Array`. -/ -partial def collectArgs (option : String → m PUnit) (args : Array String := #[]) : m (Array String) := do +partial def collectArgs + (option : String → m PUnit) (args : Array String := #[]) +: m (Array String) := do if let some arg ← takeArg? then let len := arg.length if len > 1 && arg.get 0 == '-' then -- `-(.+)` diff --git a/src/lake/Lake/Util/Compare.lean b/src/lake/Lake/Util/Compare.lean index 8dec7bb51195..c26a11846a85 100644 --- a/src/lake/Lake/Util/Compare.lean +++ b/src/lake/Lake/Util/Compare.lean @@ -3,6 +3,8 @@ Copyright (c) 2022 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude +import Init.Data.Ord namespace Lake diff --git a/src/lake/Lake/Util/Cycle.lean b/src/lake/Lake/Util/Cycle.lean index 7187f2a111ab..9f308244186a 100644 --- a/src/lake/Lake/Util/Cycle.lean +++ b/src/lake/Lake/Util/Cycle.lean @@ -3,6 +3,9 @@ Copyright (c) 2022 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude +import Init.Control.Except +import Init.Data.List.Basic namespace Lake diff --git a/src/lake/Lake/Util/DRBMap.lean b/src/lake/Lake/Util/DRBMap.lean index 722f44e513fd..3451ff161471 100644 --- a/src/lake/Lake/Util/DRBMap.lean +++ b/src/lake/Lake/Util/DRBMap.lean @@ -3,6 +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 -/ +prelude import Lean.Data.RBMap import Lake.Util.Compare diff --git a/src/lake/Lake/Util/Date.lean b/src/lake/Lake/Util/Date.lean index e49a21def12c..2775bcf5d26a 100644 --- a/src/lake/Lake/Util/Date.lean +++ b/src/lake/Lake/Util/Date.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude +import Init.Data.Ord /-! # Date diff --git a/src/lake/Lake/Util/EStateT.lean b/src/lake/Lake/Util/EStateT.lean index 36bc5eab9498..5fcf982b4c65 100644 --- a/src/lake/Lake/Util/EStateT.lean +++ b/src/lake/Lake/Util/EStateT.lean @@ -3,6 +3,8 @@ Copyright (c) 2024 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone, Leonardo de Moura, Mario Carneiro -/ +prelude +import Init.Control.State namespace Lake diff --git a/src/lake/Lake/Util/EquipT.lean b/src/lake/Lake/Util/EquipT.lean index 59e27b1a2e4c..972c2c670ae2 100644 --- a/src/lake/Lake/Util/EquipT.lean +++ b/src/lake/Lake/Util/EquipT.lean @@ -3,6 +3,9 @@ Copyright (c) 2022 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude +import Init.Control.Except + namespace Lake /-- diff --git a/src/lake/Lake/Util/Error.lean b/src/lake/Lake/Util/Error.lean index 127242eceab9..0fac5a62639e 100644 --- a/src/lake/Lake/Util/Error.lean +++ b/src/lake/Lake/Util/Error.lean @@ -3,6 +3,9 @@ Copyright (c) 2021 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude +import Init.System.IO + namespace Lake class MonadError (m : Type u → Type v) where diff --git a/src/lake/Lake/Util/Exit.lean b/src/lake/Lake/Util/Exit.lean index 2ce22f9a23bf..9f3cad4769a6 100644 --- a/src/lake/Lake/Util/Exit.lean +++ b/src/lake/Lake/Util/Exit.lean @@ -3,6 +3,9 @@ Copyright (c) 2021 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude +import Init.Data.UInt.Basic + namespace Lake /-- A process exit / return code. -/ diff --git a/src/lake/Lake/Util/Family.lean b/src/lake/Lake/Util/Family.lean index 9418b4a196ac..e62d72c8c670 100644 --- a/src/lake/Lake/Util/Family.lean +++ b/src/lake/Lake/Util/Family.lean @@ -3,6 +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 -/ +prelude import Lean.Parser.Command /-! diff --git a/src/lake/Lake/Util/FilePath.lean b/src/lake/Lake/Util/FilePath.lean index f4fa96a9d01f..6a4a5d103230 100644 --- a/src/lake/Lake/Util/FilePath.lean +++ b/src/lake/Lake/Util/FilePath.lean @@ -3,7 +3,7 @@ Copyright (c) 2024 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ -import Lean.ToExpr +prelude import Lean.Data.Json open System Lean diff --git a/src/lake/Lake/Util/Git.lean b/src/lake/Lake/Util/Git.lean index cc365d053f05..53971647b813 100644 --- a/src/lake/Lake/Util/Git.lean +++ b/src/lake/Lake/Util/Git.lean @@ -3,6 +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 -/ +prelude import Lake.Util.Proc import Lake.Util.Lift diff --git a/src/lake/Lake/Util/IO.lean b/src/lake/Lake/Util/IO.lean index 7fae188e340b..d38c06c7e915 100644 --- a/src/lake/Lake/Util/IO.lean +++ b/src/lake/Lake/Util/IO.lean @@ -3,6 +3,8 @@ Copyright (c) 2021 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude +import Init.System.IO namespace Lake diff --git a/src/lake/Lake/Util/JsonObject.lean b/src/lake/Lake/Util/JsonObject.lean index 48fb2a5d6134..38af63fdb8a5 100644 --- a/src/lake/Lake/Util/JsonObject.lean +++ b/src/lake/Lake/Util/JsonObject.lean @@ -3,6 +3,7 @@ Copyright (c) 2024 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude import Lean.Data.Json open Lean diff --git a/src/lake/Lake/Util/Lift.lean b/src/lake/Lake/Util/Lift.lean index 7dd0a21f83f3..0e9c79de33ba 100644 --- a/src/lake/Lake/Util/Lift.lean +++ b/src/lake/Lake/Util/Lift.lean @@ -3,6 +3,10 @@ Copyright (c) 2022 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude +import Init.System.IO +import Init.Control.Option + namespace Lake instance (priority := low) [Monad m] [MonadExceptOf PUnit m] : Alternative m where diff --git a/src/lake/Lake/Util/List.lean b/src/lake/Lake/Util/List.lean index 807082562819..ec0aae369a63 100644 --- a/src/lake/Lake/Util/List.lean +++ b/src/lake/Lake/Util/List.lean @@ -3,8 +3,8 @@ Copyright (c) 2023 Siddharth Bhat. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Siddharth Bhat -/ - -open Lean +prelude +import Init.Data.List.Notation namespace Lake @@ -15,5 +15,3 @@ def List.squeeze [BEq α] : List α → List α match List.squeeze xs with | [] => [x] | x' :: xs' => if x == x' then x' :: xs' else x :: x' :: xs' - -end Lake diff --git a/src/lake/Lake/Util/Lock.lean b/src/lake/Lake/Util/Lock.lean index 576e2e1c8d8f..3af80b2eaf78 100644 --- a/src/lake/Lake/Util/Lock.lean +++ b/src/lake/Lake/Util/Lock.lean @@ -3,6 +3,8 @@ Copyright (c) 2021 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone, Gabriel Ebner, Sebastian Ullrich -/ +prelude +import Init.System.IO /-! # Lock File Utilities diff --git a/src/lake/Lake/Util/Log.lean b/src/lake/Lake/Util/Log.lean index 8ed7f1123ce2..cb08f050d9bc 100644 --- a/src/lake/Lake/Util/Log.lean +++ b/src/lake/Lake/Util/Log.lean @@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude import Lake.Util.Error import Lake.Util.EStateT import Lake.Util.Lift diff --git a/src/lake/Lake/Util/MainM.lean b/src/lake/Lake/Util/MainM.lean index 24dcea7a0717..82582af71435 100644 --- a/src/lake/Lake/Util/MainM.lean +++ b/src/lake/Lake/Util/MainM.lean @@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude import Lake.Util.Log import Lake.Util.Exit import Lake.Util.Error diff --git a/src/lake/Lake/Util/Message.lean b/src/lake/Lake/Util/Message.lean index 0d7847fa6c98..a5954dfdaf69 100644 --- a/src/lake/Lake/Util/Message.lean +++ b/src/lake/Lake/Util/Message.lean @@ -3,6 +3,7 @@ Copyright (c) 2024 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude import Lean.Message import Lean.Exception import Lean.Parser.Basic diff --git a/src/lake/Lake/Util/Name.lean b/src/lake/Lake/Util/Name.lean index cfbd05f98d75..4c4c5e198ee0 100644 --- a/src/lake/Lake/Util/Name.lean +++ b/src/lake/Lake/Util/Name.lean @@ -3,6 +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 -/ +prelude import Lean.Data.Json import Lean.Data.NameMap import Lake.Util.DRBMap diff --git a/src/lake/Lake/Util/NativeLib.lean b/src/lake/Lake/Util/NativeLib.lean index 672c3337485a..abdf6bd4412e 100644 --- a/src/lake/Lake/Util/NativeLib.lean +++ b/src/lake/Lake/Util/NativeLib.lean @@ -3,6 +3,8 @@ Copyright (c) 2022 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude +import Init.System.IO open System namespace Lake diff --git a/src/lake/Lake/Util/Opaque.lean b/src/lake/Lake/Util/Opaque.lean index 9905ab59548b..f4f857cff85c 100644 --- a/src/lake/Lake/Util/Opaque.lean +++ b/src/lake/Lake/Util/Opaque.lean @@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude import Lake.Util.Binder import Lean.Parser.Command diff --git a/src/lake/Lake/Util/OrdHashSet.lean b/src/lake/Lake/Util/OrdHashSet.lean index 003af356e14b..713813b7187c 100644 --- a/src/lake/Lake/Util/OrdHashSet.lean +++ b/src/lake/Lake/Util/OrdHashSet.lean @@ -3,6 +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 -/ +prelude import Lean.Data.HashSet import Std.Data.HashSet.Basic diff --git a/src/lake/Lake/Util/OrderedTagAttribute.lean b/src/lake/Lake/Util/OrderedTagAttribute.lean index a486a380a28f..1e2ca66973aa 100644 --- a/src/lake/Lake/Util/OrderedTagAttribute.lean +++ b/src/lake/Lake/Util/OrderedTagAttribute.lean @@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Gabriel Ebner -/ +prelude import Lean.Attributes open Lean diff --git a/src/lake/Lake/Util/Proc.lean b/src/lake/Lake/Util/Proc.lean index 89cc5989eb64..eb0a86a3e5e0 100644 --- a/src/lake/Lake/Util/Proc.lean +++ b/src/lake/Lake/Util/Proc.lean @@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone -/ +prelude import Lake.Util.Log namespace Lake diff --git a/src/lake/Lake/Util/RBArray.lean b/src/lake/Lake/Util/RBArray.lean index 3794801f6c91..287e0fd4a46d 100644 --- a/src/lake/Lake/Util/RBArray.lean +++ b/src/lake/Lake/Util/RBArray.lean @@ -3,6 +3,7 @@ Copyright (c) 2023 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude import Lean.Data.RBMap namespace Lake diff --git a/src/lake/Lake/Util/Store.lean b/src/lake/Lake/Util/Store.lean index 123ea39296c4..446c34cb69f0 100644 --- a/src/lake/Lake/Util/Store.lean +++ b/src/lake/Lake/Util/Store.lean @@ -3,6 +3,9 @@ Copyright (c) 2022 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude +import Init.Notation + namespace Lake /-- A monad equipped with a dependently typed key-value store for a particular key. -/ diff --git a/src/lake/Lake/Util/StoreInsts.lean b/src/lake/Lake/Util/StoreInsts.lean index 05fb57090126..5ee67d98570d 100644 --- a/src/lake/Lake/Util/StoreInsts.lean +++ b/src/lake/Lake/Util/StoreInsts.lean @@ -3,6 +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 -/ +prelude import Lake.Util.DRBMap import Lake.Util.RBArray import Lake.Util.Family diff --git a/src/lake/Lake/Util/Sugar.lean b/src/lake/Lake/Util/Sugar.lean index 842c3977f22b..52db1339bf47 100644 --- a/src/lake/Lake/Util/Sugar.lean +++ b/src/lake/Lake/Util/Sugar.lean @@ -3,6 +3,9 @@ Copyright (c) 2022 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude +import Init.Notation + namespace Lake macro "try " x:term " else " y:term : term => diff --git a/src/lake/Lake/Util/Task.lean b/src/lake/Lake/Util/Task.lean index c986852fd11f..afe7a137e71c 100644 --- a/src/lake/Lake/Util/Task.lean +++ b/src/lake/Lake/Util/Task.lean @@ -3,6 +3,9 @@ Copyright (c) 2021 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude +import Init.Control.Option + namespace Lake instance : Monad Task where diff --git a/src/lake/Lake/Util/Version.lean b/src/lake/Lake/Util/Version.lean index 8c16fec1e853..c3ca84018433 100644 --- a/src/lake/Lake/Util/Version.lean +++ b/src/lake/Lake/Util/Version.lean @@ -3,6 +3,7 @@ Copyright (c) 2024 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude import Lean.Elab.Eval import Lake.Util.Date diff --git a/src/lake/Lake/Version.lean b/src/lake/Lake/Version.lean index 05b856e438f5..dba5c6c4dade 100644 --- a/src/lake/Lake/Version.lean +++ b/src/lake/Lake/Version.lean @@ -3,6 +3,8 @@ Copyright (c) 2021 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +prelude +import Init.Data.ToString namespace Lake diff --git a/src/lake/LakeMain.lean b/src/lake/LakeMain.lean index 620b9bd485f3..8fa420c697c6 100644 --- a/src/lake/LakeMain.lean +++ b/src/lake/LakeMain.lean @@ -3,6 +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 -/ +prelude import Lake import Lake.CLI