chore: lake: use & check prelude (#6289)

This PR adapts Lake modules to use `prelude` and includes them in the `check-prelude` CI.
2024-12-02 14:55:05 -05:00 · 2024-12-02 14:55:05 -05:00 · d9d54c1f99
commit d9d54c1f99
parent b2336fd980
130 changed files with 195 additions and 16 deletions
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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

--- 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
--- 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

--- 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
--- 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

 /-!
--- 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

--- 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
--- 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

--- 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
--- 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

--- 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
--- 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
--- 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

--- 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

--- 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
--- 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
--- 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

--- 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
--- 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
--- 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

--- 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)
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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

--- 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
--- 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

--- 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)

 /--
--- 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
--- 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
--- 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
--- 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

--- 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
--- 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

--- a/src/lake/Lake/Config/InstallPath.lean
+++ b/src/lake/Lake/Config/InstallPath.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
 import Lean.Compiler.FFI
 import Lake.Util.NativeLib
 import Lake.Config.Defaults
--- 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. -/
--- 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
--- 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 Lake.Config.Module

 namespace Lake
--- 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

--- 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
--- 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
--- 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
--- 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

--- 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

--- 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
--- 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

--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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

--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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

--- 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
--- 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
--- 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

--- 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
--- 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
--- 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
--- 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
--- 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

--- 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
--- 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
--- 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
--- 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
--- 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
--- 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

 /-!
--- 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

 /-!
--- 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
--- 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

--- 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

 /-!
--- 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

 /-!
--- 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

 /-!
--- 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
--- 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

--- 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

 /-!
--- 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

--- 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

--- 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
--- 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. -/
--- 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 -- `-(.+)`
--- 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

--- 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

--- 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

--- a/Show more
+++ b/Show more