diff --git a/src/lake/Lake/Build/Infos.lean b/src/lake/Lake/Build/Infos.lean index 35f8a03fdeb2..3654708cdb79 100644 --- a/src/lake/Lake/Build/Infos.lean +++ b/src/lake/Lake/Build/Infos.lean @@ -214,7 +214,7 @@ public abbrev Package.target (target : Name) (self : Package) : BuildInfo := /- Build info for applying the specified facet to the package. -It is the user's obiligation to ensure the facet in question is a package facet. +It is the user's obligation to ensure the facet in question is a package facet. -/ public abbrev Package.facetCore (facet : Name) (self : Package) : BuildInfo := .facet self.key facetKind (toFamily self) facet @@ -267,7 +267,7 @@ end Package /- Build info for applying the specified facet to the library. -It is the user's obiligation to ensure the facet in question is a library facet. +It is the user's obligation to ensure the facet in question is a library facet. -/ public abbrev LeanLib.facetCore (facet : Name) (self : LeanLib) : BuildInfo := .facet self.key facetKind (toFamily self) facet @@ -308,7 +308,7 @@ end LeanLib /- Build info for applying the specified facet to the executable. -It is the user's obiligation to ensure the facet in question is the executable facet. +It is the user's obligation to ensure the facet in question is the executable facet. -/ public abbrev LeanExe.facetCore (facet : Name) (self : LeanExe) : BuildInfo := .facet self.key facetKind (toFamily self) facet @@ -321,7 +321,7 @@ public abbrev LeanExe.exe (self : LeanExe) : BuildInfo := /- Build info for applying the specified facet to the external library. -It is the user's obiligation to ensure the facet in question is an external library facet. +It is the user's obligation to ensure the facet in question is an external library facet. -/ public abbrev ExternLib.facetCore (facet : Name) (self : ExternLib) : BuildInfo := .facet self.key facetKind (toFamily self) facet @@ -342,7 +342,7 @@ public abbrev ExternLib.dynlib (self : ExternLib) : BuildInfo := /- Build info for applying the specified facet to the input file. -It is the user's obiligation to ensure the facet in question is an external library facet. +It is the user's obligation to ensure the facet in question is an external library facet. -/ public abbrev InputFile.facetCore (facet : Name) (self : InputFile) : BuildInfo := .facet self.key facetKind (toFamily self) facet @@ -353,7 +353,7 @@ public abbrev InputFile.default (self : InputFile) : BuildInfo := /- Build info for applying the specified facet to the input directory. -It is the user's obiligation to ensure the facet in question is an external library facet. +It is the user's obligation to ensure the facet in question is an external library facet. -/ public abbrev InputDir.facetCore (facet : Name) (self : InputDir) : BuildInfo := .facet self.key facetKind (toFamily self) facet diff --git a/src/lake/Lake/CLI/Help.lean b/src/lake/Lake/CLI/Help.lean index bba4a18e8453..d61e73e6deab 100644 --- a/src/lake/Lake/CLI/Help.lean +++ b/src/lake/Lake/CLI/Help.lean @@ -271,13 +271,13 @@ package or its dependencies. It merely verifies that one is specified. " def helpPack := -"Pack build artifacts into a archive for distribution +"Pack build artifacts into an archive for distribution USAGE: lake pack [] Packs the root package's `buildDir` into a gzip tar archive using `tar`. -If a path for the archive is not specified, creates a archive in the package's +If a path for the archive is not specified, creates an archive in the package's Lake directory (`.lake`) named according to its `buildArchive` setting. Does NOT build any artifacts. It just packs the existing ones." diff --git a/src/lake/Lake/CLI/Serve.lean b/src/lake/Lake/CLI/Serve.lean index 335345d1bfce..27d3e8953010 100644 --- a/src/lake/Lake/CLI/Serve.lean +++ b/src/lake/Lake/CLI/Serve.lean @@ -32,7 +32,7 @@ public def invalidConfigEnvVar := "LAKE_INVALID_CONFIG" /-- Build the dependencies of a Lean file and print the computed module's setup as JSON. -If `header?` is not not `none`, it will be used to determine imports instead of the +If `header?` is not `none`, it will be used to determine imports instead of the file's own header. Requires a configuration file to succeed. If no configuration file exists, it diff --git a/src/lake/Lake/Config/Dependency.lean b/src/lake/Lake/Config/Dependency.lean index 49a983b49be6..457352257b5d 100644 --- a/src/lake/Lake/Config/Dependency.lean +++ b/src/lake/Lake/Config/Dependency.lean @@ -26,7 +26,7 @@ The source of a `Dependency`. That is, where Lake should look to materialize the dependency. -/ public inductive DependencySrc where -/- A package located a fixed path relative to the dependent package's directory. -/ +/- A package located at a fixed path relative to the dependent package's directory. -/ | path (dir : FilePath) /- A package cloned from a Git repository available at a fixed Git `url`. -/ | git (url : String) (rev : Option String) (subDir : Option FilePath) diff --git a/src/lake/Lake/DSL/Syntax.lean b/src/lake/Lake/DSL/Syntax.lean index c5411749f14d..3946b55c0a0b 100644 --- a/src/lake/Lake/DSL/Syntax.lean +++ b/src/lake/Lake/DSL/Syntax.lean @@ -119,7 +119,7 @@ into the workspace's `packagesDir`. from ``` -Lake loads the package located a fixed `path` relative to the +Lake loads the package located at a fixed `path` relative to the requiring package's directory. **Git Dependencies** diff --git a/src/lake/Lake/Load/Lean/Elab.lean b/src/lake/Lake/Load/Lean/Elab.lean index d116fb65453d..7e8c7ffd1c38 100644 --- a/src/lake/Lake/Load/Lean/Elab.lean +++ b/src/lake/Lake/Load/Lean/Elab.lean @@ -198,7 +198,7 @@ public def importConfigFile (cfg : LoadConfig) : LogIO Environment := do imported and the (shared) lock is then released. If the trace is out-of-date, Lake upgrades the trace to read-write handle - with an exclusive lock. Lake does this by first acquiring a exclusive lock to + with an exclusive lock. Lake does this by first acquiring an exclusive lock to configuration's lock file (i.e. `olean.lock`). While holding this lock, Lake releases the shared lock on the trace, re-opens the trace with a read-write handle, and acquires an exclusive lock on the trace. It then releases its @@ -212,7 +212,7 @@ public def importConfigFile (cfg : LoadConfig) : LogIO Environment := do This is because we are already holding a shared lock on the trace. If multiple process race for this lock, one will get it and then - wait for an exclusive lock one the trace file, but be blocked by the + wait for an exclusive lock on the trace file, but be blocked by the other process with a shared lock waiting on this file. While there is likely a way to sequence this to avoid erroring,