chore: lake: use & check prelude

leanprover · Dec 2, 2024 · 91722ce · 91722ce
1 parent 27df5e9
commit 91722ce
Show file tree

Hide file tree

Showing 130 changed files with 193 additions and 16 deletions.
diff --git a/.github/workflows/check-prelude.yml b/.github/workflows/check-prelude.yml
@@ -21,7 +21,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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
-Original file line number
+Diff line change
@@ Expand Up / @@ -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
     /-!
@@ Expand Down @@