diff --git a/Lake/Build/Module.lean b/Lake/Build/Module.lean index 22125c70bc..d917e1c5fb 100644 --- a/Lake/Build/Module.lean +++ b/Lake/Build/Module.lean @@ -67,8 +67,8 @@ abbrev cFile (self : ActiveOleanAndCTargets) := self.cTarget.info end ActiveOleanAndCTargets /-- - An active module `.olean` and `.c` target consists of a single task that - builds both with two dependent targets that compute their individual traces. +An active module `.olean` and `.c` target consists of a single task that +builds both with two dependent targets that compute their individual traces. -/ abbrev ActiveOleanAndCTarget := ActiveBuildTarget ActiveOleanAndCTargets diff --git a/Lake/Build/Package.lean b/Lake/Build/Package.lean index 1d614c9a41..b183dd5cd3 100644 --- a/Lake/Build/Package.lean +++ b/Lake/Build/Package.lean @@ -43,8 +43,8 @@ def packageTargetsToOleanDirs (targets : Array (ActivePackageTarget i)) : List F -- # Build Packages /-- - Builds the package's `extraDepTarget` and combines it with - the given package targets to create a single active opaque target. +Builds the package's `extraDepTarget` and combines it with +the given package targets to create a single active opaque target. -/ def Package.buildDepTargetWith (depTargets : Array (ActiveBuildTarget i)) (self : Package) : BuildM ActiveOpaqueTarget := do @@ -53,11 +53,11 @@ def Package.buildDepTargetWith extraDepTarget.mixOpaqueAsync depTarget /-- - Build an active package target after - resolving the package's dependencies and recursively building them. +Build an active package target after +resolving the package's dependencies and recursively building them. - To build each package, run the given `build` function on it, - which takes the package and its building dependencies as arguments. +To build each package, run the given `build` function on it, +which takes the package and its building dependencies as arguments. -/ def recBuildPackageWithDeps [Monad m] [MonadLiftT BuildM m] [MonadStore Name (Array (ActivePackageTarget i)) m] @@ -77,8 +77,8 @@ def recBuildPackageWithDeps depTargets.push pkgTarget /-- - Build the package along with its dependencies - by using the given `build` function recursively. +Build the package along with its dependencies +by using the given `build` function recursively. -/ def Package.buildRec (self : Package) [Inhabited i] (build : Array (ActivePackageTarget i) → Package → BuildM (ActivePackageTarget i)) @@ -90,8 +90,8 @@ def Package.buildRec (self : Package) [Inhabited i] target.withInfo targets.back.info /-- - Build an `Array` of `Package`s along with their dependencies - by using the given `build` function recursively. +Build an `Array` of `Package`s along with their dependencies +by using the given `build` function recursively. -/ def buildPackageArrayWithDeps (pkgs : Array Package) [Inhabited i] (build : Array (ActivePackageTarget i) → Package → BuildM (ActivePackageTarget i)) @@ -106,8 +106,8 @@ def Package.buildDepTargets [Inhabited i] buildPackageArrayWithDeps (← self.resolveDirectDeps) build /-- - Build an active target for the package by - running the given `RecModuleTargetBuild` on the given root module. +Build an active target for the package by +running the given `RecModuleTargetBuild` on the given root module. -/ def Package.buildModuleDAGTarget [Inhabited i] (mod : Name) (buildMod : RecModuleTargetBuild i) (self : Package) : BuildM (ActivePackageTarget i) := do @@ -117,8 +117,8 @@ def Package.buildModuleDAGTarget [Inhabited i] (mod : Name) return target.withInfo ⟨self, targetMap⟩ /-- - Build an active target for the package by - running the given `RecModuleTargetBuild` on the given root modules. +Build an active target for the package by +running the given `RecModuleTargetBuild` on the given root modules. -/ def Package.buildModulesDAGTarget [Inhabited i] (mods : Array Name) (buildMod : RecModuleTargetBuild i) (self : Package) : BuildM (ActivePackageTarget i) := do @@ -129,9 +129,9 @@ def Package.buildModulesDAGTarget [Inhabited i] (mods : Array Name) return target.withInfo ⟨self, targetMap⟩ /-- - Build an active target for the package by - running the given `RecModuleTargetBuild` on each of its top-level modules - (i.e., those specified in its `libGlobs` configuration). +Build an active target for the package by +running the given `RecModuleTargetBuild` on each of its top-level modules +(i.e., those specified in its `libGlobs` configuration). -/ def Package.buildTarget [Inhabited i] (buildMod : RecModuleTargetBuild i) (self : Package) : BuildM (ActivePackageTarget i) := do @@ -202,10 +202,10 @@ def Package.filterLocalImports return localImports /-- - Build the package's dependencies, returning the list of packages built. +Build the package's dependencies, returning the list of packages built. - Builds only module `.olean` files if the default package facet is - just `oleans`. Otherwise, builds both `.olean` and `.c` files. +Builds only module `.olean` files if the default package facet is +just `oleans`. Otherwise, builds both `.olean` and `.c` files. -/ def Package.buildDefaultDepTargets (self : Package) : BuildM (Array (ActiveBuildTarget Package)) := do @@ -217,11 +217,11 @@ def Package.buildDefaultDepTargets depTargets.map (·.withOnlyPackageInfo) /-- - Build the package's dependencies and a list of imports, - returning the list of packages built. +Build the package's dependencies and a list of imports, +returning the list of packages built. - Builds only module `.olean` files if the default package facet is - just `oleans`. Otherwise, builds both `.olean` and `.c` files. +Builds only module `.olean` files if the default package facet is +just `oleans`. Otherwise, builds both `.olean` and `.c` files. -/ def Package.buildImportsAndDeps (imports : List String := []) (self : Package) : BuildM (List Package) := do diff --git a/Lake/Build/Recursive.lean b/Lake/Build/Recursive.lean index 5d5e02c5e8..1dc51b196f 100644 --- a/Lake/Build/Recursive.lean +++ b/Lake/Build/Recursive.lean @@ -48,11 +48,11 @@ partial def buildTopCore [BEq k] [Inhabited o] [Monad m] [MonadStore k o m] return output /-- - Recursively fills a `MonadStore` of key-object pairs by - building objects topologically (i.e., via a depth-first search with memoization). - If a cycle is detected, the list of keys traversed is thrown. +Recursively fills a `MonadStore` of key-object pairs by +building objects topologically (i.e., via a depth-first search with memoization). +If a cycle is detected, the list of keys traversed is thrown. - Called a suspending scheduler in "Build systems à la carte". +Called a suspending scheduler in "Build systems à la carte". -/ def buildTop [BEq k] [Inhabited o] [Monad m] [MonadStore k o m] (build : RecBuild i o (ExceptT (List k) m)) (keyOf : i → k) (info : i) : ExceptT (List k) m o := diff --git a/Lake/Build/Trace.lean b/Lake/Build/Trace.lean index 0fc992f594..dd4a33f923 100644 --- a/Lake/Build/Trace.lean +++ b/Lake/Build/Trace.lean @@ -45,10 +45,7 @@ export NilTrace (nilTrace) instance [NilTrace t] : Inhabited t := ⟨nilTrace⟩ class MixTrace.{u} (t : Type u) where - /-- - Combine two traces. - The result should be dirty if either of the inputs is dirty. - -/ + /-- Combine two traces. The result should be dirty if either of the inputs is dirty. -/ mixTrace : t → t → t export MixTrace (mixTrace) @@ -83,8 +80,8 @@ end -------------------------------------------------------------------------------- /-- - A content hash. - TODO: Use a secure hash rather than the builtin Lean hash function. +A content hash. +TODO: Use a secure hash rather than the builtin Lean hash function. -/ structure Hash where val : UInt64 @@ -223,16 +220,16 @@ def mix (t1 t2 : BuildTrace) : BuildTrace := instance : MixTrace BuildTrace := ⟨mix⟩ /-- - Check the build trace against the given target info and hash - to see if the target is up-to-date. +Check the build trace against the given target info and hash +to see if the target is up-to-date. -/ def checkAgainstHash [CheckExists i] (info : i) (hash : Hash) (self : BuildTrace) : BaseIO Bool := hash == self.hash <&&> checkExists info /-- - Check the build trace against the given target info and its trace file - to see if the target is up-to-date. +Check the build trace against the given target info and its trace file +to see if the target is up-to-date. -/ def checkAgainstFile [CheckExists i] [GetMTime i] (info : i) (traceFile : FilePath) (self : BuildTrace) : BaseIO Bool := do diff --git a/Lake/CLI/Main.lean b/Lake/CLI/Main.lean index 9d5ead7f5a..7058829fac 100644 --- a/Lake/CLI/Main.lean +++ b/Lake/CLI/Main.lean @@ -130,8 +130,8 @@ def takeFileArg : CliM FilePath := do | some arg => arg /-- - Verify that there are no CLI arguments remaining - before running the given action. +Verify that there are no CLI arguments remaining +before running the given action. -/ def noArgsRem (act : CliM α) : CliM α := do let args ← takeArgs @@ -212,11 +212,11 @@ def verifyInstall : CliM PUnit := do def noConfigFileCode : ExitCode := 2 /-- - Build a list of imports of the package - and print the `.olean` and source directories of every used package. - If no configuration file exists, exit silently with `noConfigFileCode` (i.e, 2). +Build a list of imports of the package +and print the `.olean` and source directories of every used package. +If no configuration file exists, exit silently with `noConfigFileCode` (i.e, 2). - The `print-paths` command is used internally by Lean 4 server. +The `print-paths` command is used internally by Lean 4 server. -/ def printPaths (imports : List String := []) : CliM PUnit := do let (leanInstall, lakeInstall) ← getInstall diff --git a/Lake/Config/Glob.lean b/Lake/Config/Glob.lean index 25557fb248..a32f703846 100644 --- a/Lake/Config/Glob.lean +++ b/Lake/Config/Glob.lean @@ -14,10 +14,7 @@ namespace Lake inductive Glob | /-- Selects just the specified module name. -/ one : Name → Glob -| /-- - Selects all submodules of the specified module, - but not the module itself. - -/ +| /-- Selects all submodules of the specified module, but not the module itself. -/ submodules : Name → Glob | /-- Selects the specified module and all submodules. -/ andSubmodules : Name → Glob diff --git a/Lake/Config/InstallPath.lean b/Lake/Config/InstallPath.lean index 3a19d2209a..3338e22761 100644 --- a/Lake/Config/InstallPath.lean +++ b/Lake/Config/InstallPath.lean @@ -35,9 +35,9 @@ structure LakeInstall where deriving Inhabited, Repr /-- - Try to find the home of the given `lean` command (if it exists) - by calling `lean --print-prefix` and returning the path it prints. - Defaults to trying the `lean` in `PATH`. +Try to find the home of the given `lean` command (if it exists) +by calling `lean --print-prefix` and returning the path it prints. +Defaults to trying the `lean` in `PATH`. -/ def findLeanCmdHome? (lean := "lean") : IO (Option FilePath) := do let out ← IO.Process.output { @@ -50,19 +50,19 @@ def findLeanCmdHome? (lean := "lean") : IO (Option FilePath) := do none /-- - Try to find the installation of the given `lean` command - by calling `findLeanCmdHome?`. +Try to find the installation of the given `lean` command +by calling `findLeanCmdHome?`. - It assumes that the Lean installation is setup the normal way. - That is, with its binaries located in `/bin` and its - libraries and `.olean` files located in `/lib/lean`. +It assumes that the Lean installation is setup the normal way. +That is, with its binaries located in `/bin` and its +libraries and `.olean` files located in `/lib/lean`. -/ def findLeanCmdInstall? (lean := "lean"): IO (Option LeanInstall) := do (← findLeanCmdHome? lean).map fun home => {home} /-- - Check if Lake's executable is co-located with Lean, and, if so, - try to return their joint home by assuming they are both located at `/bin`. +Check if Lake's executable is co-located with Lean, and, if so, +try to return their joint home by assuming they are both located at `/bin`. -/ def findLakeLeanJointHome? : IO (Option FilePath) := do let appPath ← IO.appPath @@ -73,20 +73,20 @@ def findLakeLeanJointHome? : IO (Option FilePath) := do return none /-- - Try to get Lake's home by assuming - the executable is located at `/bin/lake`. +Try to get Lake's home by assuming +the executable is located at `/bin/lake`. -/ def lakeBuildHome? (lake : FilePath) : Option FilePath := do lake.parent.bind FilePath.parent /-- - Try to find Lean's installation by - first checking the `LEAN_SYSROOT` environment variable - and then by trying `findLeanCmdHome?`. +Try to find Lean's installation by +first checking the `LEAN_SYSROOT` environment variable +and then by trying `findLeanCmdHome?`. - It assumes that the Lean installation is setup the normal way. - That is, with its binaries located in `/bin` and its - libraries and `.olean` files located in `/lib/lean`. +It assumes that the Lean installation is setup the normal way. +That is, with its binaries located in `/bin` and its +libraries and `.olean` files located in `/lib/lean`. -/ def findLeanInstall? : IO (Option LeanInstall) := do if let some home ← IO.getEnv "LEAN_SYSROOT" then @@ -96,13 +96,13 @@ def findLeanInstall? : IO (Option LeanInstall) := do return none /-- - Try to find Lake's installation by - first checking the `LAKE_HOME` environment variable - and then by trying the `lakeBuildHome?` of the running executable. +Try to find Lake's installation by +first checking the `LAKE_HOME` environment variable +and then by trying the `lakeBuildHome?` of the running executable. - It assumes that the Lake installation is setup the same way it is built. - That is, with its binary located at `/bin/lake` and its static - library and `.olean` files in `/lib`. +It assumes that the Lake installation is setup the same way it is built. +That is, with its binary located at `/bin/lake` and its static +library and `.olean` files in `/lib`. -/ def findLakeInstall? : IO (Option LakeInstall) := do if let some home ← IO.getEnv "LAKE_HOME" then @@ -113,14 +113,14 @@ def findLakeInstall? : IO (Option LakeInstall) := do return none /-- - Try to get Lake's install path by first trying `findLakeLeanHome?` - then by running `findLeanInstall?` and `findLakeInstall?`. +Try to get Lake's install path by first trying `findLakeLeanHome?` +then by running `findLeanInstall?` and `findLakeInstall?`. - If Lake is co-located with `lean` (i.e., there is `lean` executable - in the same directory as itself), it will assume it was installed with - Lean and their binaries are located in `/bin` with - Lean's libraries and `.olean` files at `/lib/lean` and - Lake's static library and `.olean` files at `/lib/lean`. +If Lake is co-located with `lean` (i.e., there is `lean` executable +in the same directory as itself), it will assume it was installed with +Lean and their binaries are located in `/bin` with +Lean's libraries and `.olean` files at `/lib/lean` and +Lake's static library and `.olean` files at `/lib/lean`. -/ def findInstall? : IO (Option LeanInstall × Option LakeInstall) := do if let some home ← findLakeLeanJointHome? then diff --git a/Lake/Config/Load.lean b/Lake/Config/Load.lean index aefb930f06..9859df51f3 100644 --- a/Lake/Config/Load.lean +++ b/Lake/Config/Load.lean @@ -65,8 +65,8 @@ unsafe def loadUnsafe (dir : FilePath) (args : List String := []) throw <| IO.userError s!"package configuration `{configFile}` has errors" /-- - Load the package located in - the given directory with the given configuration file. +Load the package located in +the given directory with the given configuration file. -/ @[implementedBy loadUnsafe] constant load (dir : FilePath) (args : List String := []) diff --git a/Lake/Config/Package.lean b/Lake/Config/Package.lean index 18c734cf23..b23d48005c 100644 --- a/Lake/Config/Package.lean +++ b/Lake/Config/Package.lean @@ -45,12 +45,12 @@ def defaultBinRoot : Name := `Main -------------------------------------------------------------------------------- /-- - The `src` of a `Dependency`. +The `src` of a `Dependency`. - In Lake, dependency sources currently come into flavors: - * Local `path`s relative to the package's directory. - * Remote `git` repositories that are download from a given `url` - into the packages's `depsDir`. +In Lake, dependency sources currently come into flavors: +* Local `path`s relative to the package's directory. +* Remote `git` repositories that are download from a given `url` + into the packages's `depsDir`. -/ inductive Source where | path (dir : FilePath) : Source @@ -60,22 +60,22 @@ deriving Inhabited, Repr /-- A `Dependency` of a package. -/ structure Dependency where /-- - A `Name` for the dependency. - The names of a package's dependencies cannot clash. + A `Name` for the dependency. + The names of a package's dependencies cannot clash. -/ name : Name /-- - The source of a dependency. - See the documentation of `Source` for more information. + The source of a dependency. + See the documentation of `Source` for more information. -/ src : Source /-- - The subdirectory of the dependency's source where - the dependency's package configuration is located. + The subdirectory of the dependency's source where + the dependency's package configuration is located. -/ dir : FilePath := "." /-- - Arguments to pass to the dependency's package configuration. + Arguments to pass to the dependency's package configuration. -/ args : List String := [] @@ -109,161 +109,158 @@ def toUpperCamelCase (name : Name) : Name := /-- A `Package`'s declarative configuration. -/ structure PackageConfig extends WorkspaceConfig where - /-- - The `Name` of the package. - -/ + /-- The `Name` of the package. -/ name : Name /- - An `Array` of the package's dependencies. - See the documentation of `Dependency` for more information. + An `Array` of the package's dependencies. + See the documentation of `Dependency` for more information. -/ dependencies : Array Dependency := #[] /-- - An extra `OpaqueTarget` that should be built before the package. + An extra `OpaqueTarget` that should be built before the package. - `OpaqueTarget.collectList/collectArray` can be used combine multiple - extra targets into a single `extraDepTarget`. + `OpaqueTarget.collectList/collectArray` can be used combine multiple + extra targets into a single `extraDepTarget`. -/ extraDepTarget : OpaqueTarget := Target.nil /-- - The `PackageFacet` to build on a bare `lake build` of the package. - Can be one of `bin`, `staticLib`, `sharedLib`, or `oleans`. Defaults to `bin`. - See `lake help build` for more info on build facets. + The `PackageFacet` to build on a bare `lake build` of the package. + Can be one of `bin`, `staticLib`, `sharedLib`, or `oleans`. Defaults to `bin`. + See `lake help build` for more info on build facets. -/ defaultFacet : PackageFacet := PackageFacet.bin /-- - Additional arguments to pass to the Lean language server - (i.e., `lean --server`) launched by `lake server`. + Additional arguments to pass to the Lean language server + (i.e., `lean --server`) launched by `lake server`. -/ moreServerArgs : Array String := #[] /-- - The directory containing the package's Lean source files. - Defaults to the package's directory. + The directory containing the package's Lean source files. + Defaults to the package's directory. - (This will be passed to `lean` as the `-R` option.) + (This will be passed to `lean` as the `-R` option.) -/ srcDir : FilePath := "." /-- - The directory to which Lake should output the package's build results. - Defaults to `defaultBuildDir` (i.e., `build`). + The directory to which Lake should output the package's build results. + Defaults to `defaultBuildDir` (i.e., `build`). -/ buildDir : FilePath := defaultBuildDir /-- - The build subdirectory to which Lake should output the package's `.olean` files. - Defaults to `defaultOleanDir` (i.e., `lib`). + The build subdirectory to which Lake should output the package's `.olean` files. + Defaults to `defaultOleanDir` (i.e., `lib`). -/ oleanDir : FilePath := defaultOleanDir - /- - The root module(s) of the package's library. + /-- + The root module(s) of the package's library. - Submodules of these roots (e.g., `Pkg.Foo` of `Pkg`) are considered - part of the package. + Submodules of these roots (e.g., `Pkg.Foo` of `Pkg`) are considered + part of the package. - Defaults to a single root of the package's upper camel case `name`. + Defaults to a single root of the package's upper camel case `name`. -/ libRoots : Array Name := #[toUpperCamelCase name] /-- - An `Array` of module `Glob`s to build for the package's library. - Defaults to a `Glob.one` of each of the module's `libRoots`. + An `Array` of module `Glob`s to build for the package's library. + Defaults to a `Glob.one` of each of the module's `libRoots`. - Submodule globs build every source file within their directory. - Local imports of glob'ed files (i.e., fellow modules of the package) are - also recursively built. + Submodule globs build every source file within their directory. + Local imports of glob'ed files (i.e., fellow modules of the package) are + also recursively built. -/ libGlobs : Array Glob := libRoots.map Glob.one /-- - Additional arguments to pass to `lean` while compiling Lean source files. + Additional arguments to pass to `lean` while compiling Lean source files. -/ moreLeanArgs : Array String := #[] /-- - Additional arguments to pass to `leanc` - while compiling the C source files generated by `lean`. + Additional arguments to pass to `leanc` + while compiling the C source files generated by `lean`. - Lake already passes `-O3` and `-DNDEBUG` automatically, - but you can change this by, for example, adding `-O0` and `-UNDEBUG`. + Lake already passes `-O3` and `-DNDEBUG` automatically, + but you can change this by, for example, adding `-O0` and `-UNDEBUG`. -/ moreLeancArgs : Array String := #[] /-- - The build subdirectory to which Lake should output - the package's intermediary results (e.g., `.c` and `.o` files). - Defaults to `defaultIrDir` (i.e., `ir`). + The build subdirectory to which Lake should output + the package's intermediary results (e.g., `.c` and `.o` files). + Defaults to `defaultIrDir` (i.e., `ir`). -/ irDir : FilePath := defaultIrDir /-- - The name of the package's static library. - Defaults to the package's upper camel case `name`. + The name of the package's static library. + Defaults to the package's upper camel case `name`. -/ libName : String := toUpperCamelCase name |>.toString (escape := false) /-- - The build subdirectory to which Lake should output the package's static library. - Defaults to `defaultLibDir` (i.e., `lib`). + The build subdirectory to which Lake should output the package's static library. + Defaults to `defaultLibDir` (i.e., `lib`). -/ libDir : FilePath := defaultLibDir /-- - The name of the package's binary executable. - Defaults to the package's `name` with any `.` replaced with a `-`. + The name of the package's binary executable. + Defaults to the package's `name` with any `.` replaced with a `-`. -/ binName : String := name.toStringWithSep "-" (escape := false) /-- - The build subdirectory to which Lake should output the package's binary executable. - Defaults to `defaultBinDir` (i.e., `bin`). + The build subdirectory to which Lake should output the package's binary executable. + Defaults to `defaultBinDir` (i.e., `bin`). -/ binDir : FilePath := defaultBinDir /-- - The root module of the package's binary executable. - Defaults to `defaultBinRoot` (i.e., `Main`). + The root module of the package's binary executable. + Defaults to `defaultBinRoot` (i.e., `Main`). - The root is built by recursively building its - local imports (i.e., fellow modules of the package). + The root is built by recursively building its + local imports (i.e., fellow modules of the package). - This setting is most useful for packages that are distributing both a - library and a binary (like Lake itself). In such cases, it is common for - there to be code (e.g., `main`) that is needed for the binary but should - not be included in the library proper. + This setting is most useful for packages that are distributing both a + library and a binary (like Lake itself). In such cases, it is common for + there to be code (e.g., `main`) that is needed for the binary but should + not be included in the library proper. -/ binRoot : Name := defaultBinRoot /-- - Additional library `FileTarget`s - (beyond the package's and its dependencies' libraries) - to build and link to the package's binary executable - (and/or to dependent package's executables). + Additional library `FileTarget`s (beyond the package's and its dependencies' + libraries) to build and link to the package's binary executable (and/or to + dependent package's executables). -/ moreLibTargets : Array FileTarget := #[] /-- - Whether to expose symbols within the executable to the Lean interpreter. - This allows the executable to interpret Lean files (e.g., via - `Lean.Elab.runFrontend`). + Whether to expose symbols within the executable to the Lean interpreter. + This allows the executable to interpret Lean files (e.g., via + `Lean.Elab.runFrontend`). - Implementation-wise, this passes `-rdynamic` to the linker when building - on non-Windows systems. + Implementation-wise, this passes `-rdynamic` to the linker when building + on non-Windows systems. - Defaults to `false`. + Defaults to `false`. -/ supportInterpreter : Bool := false /-- - Additional arguments to pass to `leanc` - while compiling the package's binary executable. - These will come *after* the paths of libraries built with `moreLibTargets`. + Additional arguments to pass to `leanc` while compiling the package's + binary executable. These will come *after* the paths of libraries built + with `moreLibTargets`. -/ moreLinkArgs : Array String := #[] @@ -282,10 +279,10 @@ structure Package where /-- The workspace the package is contained in. -/ workspace : Workspace := {dir, config := config.toWorkspaceConfig} /-- - A `NameMap` of scripts for the package. + A `NameMap` of scripts for the package. - A `Script` is a `(args : List String) → IO UInt32` definition with - a `@[script]` tag that can be run by `lake run