style: fix doubled word in Lake docstring

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

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 [<file.tgz>]
 
 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."

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

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)

src/lake/Lake/DSL/Syntax.lean

@@ -119,7 +119,7 @@ into the workspace's `packagesDir`.
 from <path>
 ```
 
-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**

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,