diff --git a/Lake/Build/Actions.lean b/Lake/Build/Actions.lean
index d169172828..b9f6833ed5 100644
--- a/Lake/Build/Actions.lean
+++ b/Lake/Build/Actions.lean
@@ -32,15 +32,10 @@ def proc (args : IO.Process.SpawnArgs) : BuildM PUnit := do
     logError s!"external command {args.cmd} exited with status {out.exitCode}"
     failure
 
-def getSearchPath (envVar : String) : IO SearchPath := do
-  match (← IO.getEnv envVar) with
-  | some path => pure <| SearchPath.parse path
-  | none => pure []
-
 def compileLeanModule (leanFile : FilePath)
 (oleanFile? ileanFile? cFile? : Option FilePath)
-(oleanPath : SearchPath := []) (rootDir : FilePath := ".")
-(dynlibs : Array FilePath := #[]) (dynlibPath : SearchPath := {})
+(leanPath : SearchPath := []) (rootDir : FilePath := ".")
+(dynlibs : Array String := #[]) (dynlibPath : SearchPath := {})
 (leanArgs : Array String := #[]) (lean : FilePath := "lean")
 : BuildM PUnit := do
   let mut args := leanArgs ++
@@ -56,19 +51,12 @@ def compileLeanModule (leanFile : FilePath)
     args := args ++ #["-c", cFile.toString]
   for dynlib in dynlibs do
     args := args.push s!"--load-dynlib={dynlib}"
-  let dynlibVar :=
-    if Platform.isWindows then
-      "PATH"
-    else if Platform.isOSX then
-      "DYLD_LIBRARY_PATH"
-    else
-      "LD_LIBRARY_PATH"
   proc {
     args
     cmd := lean.toString
     env := #[
-      ("LEAN_PATH", oleanPath.toString),
-      (dynlibVar, (← getSearchPath dynlibVar) ++ dynlibPath |>.toString)
+      ("LEAN_PATH", leanPath.toString),
+      (sharedLibPathEnvVar, (← getSearchPath sharedLibPathEnvVar) ++ dynlibPath |>.toString)
     ]
   }
 
diff --git a/Lake/Build/Imports.lean b/Lake/Build/Imports.lean
index e7be6d9dac..cb7d00a225 100644
--- a/Lake/Build/Imports.lean
+++ b/Lake/Build/Imports.lean
@@ -53,4 +53,4 @@ def Package.buildImportsAndDeps (imports : List String) (self : Package) : Build
     let dynlibs ← dynlibTargets.mapM (·.build)
     let externLibs ← externLibTargets.mapM (·.build)
     -- Note: Lean wants the external library symbols before module symbols
-    return  externLibs ++ dynlibs
+    return externLibs ++ dynlibs
diff --git a/Lake/Build/Module.lean b/Lake/Build/Module.lean
index eac738094d..0d256bf64f 100644
--- a/Lake/Build/Module.lean
+++ b/Lake/Build/Module.lean
@@ -14,7 +14,7 @@ namespace Lake
 
 -- # Solo Module Targets
 
-def Module.soloTarget (mod : Module) (dynlibs : Array FilePath)
+def Module.soloTarget (mod : Module) (dynlibs : Array String)
 (dynlibPath : SearchPath) (depTarget : BuildTarget x) (leanOnly : Bool) : OpaqueTarget :=
   Target.opaque <| depTarget.bindOpaqueSync fun depTrace => do
     let argTrace : BuildTrace := pureHash mod.leanArgs
@@ -24,12 +24,12 @@ def Module.soloTarget (mod : Module) (dynlibs : Array FilePath)
     if leanOnly then
       unless modUpToDate do
         compileLeanModule mod.leanFile mod.oleanFile mod.ileanFile none
-          (← getOleanPath) mod.rootDir dynlibs dynlibPath mod.leanArgs (← getLean)
+          (← getLeanPath) mod.rootDir dynlibs dynlibPath mod.leanArgs (← getLean)
     else
       let cUpToDate ← modTrace.checkAgainstFile mod.cFile mod.cTraceFile
       unless modUpToDate && cUpToDate do
         compileLeanModule mod.leanFile mod.oleanFile mod.ileanFile mod.cFile
-          (← getOleanPath) mod.rootDir dynlibs dynlibPath mod.leanArgs (← getLean)
+          (← getLeanPath) mod.rootDir dynlibs dynlibPath mod.leanArgs (← getLean)
       modTrace.writeToFile mod.cTraceFile
     modTrace.writeToFile mod.traceFile
     return mixTrace (← computeTrace mod) depTrace
@@ -79,7 +79,9 @@ def recBuildExternalDynlibs (pkgs : Array Package)
       if let some parent := target.info.parent then
         libDirs := libDirs.push parent
       if let some stem := target.info.fileStem then
-        if stem.startsWith "lib" then
+        if Platform.isWindows then
+          targets := targets.push <| target.withInfo stem
+        else if stem.startsWith "lib" then
           targets := targets.push <| target.withInfo <| stem.drop 3
         else
           logWarning s!"external library `{target.info}` was skipped because it does not start with `lib`"
@@ -147,7 +149,7 @@ artifact.
     <| ← imports.mapM (·.leanBin.recBuild)
   let depTarget := Target.active <| ← extraDepTarget.mixOpaqueAsync
     <| ← dynlibsTarget.mixOpaqueAsync importTarget
-  let dynlibs := dynlibsTarget.info.map (FilePath.mk s!"lib{·}.{sharedLibExt}")
+  let dynlibs := dynlibsTarget.info.map toString
 
   -- Build Module
   let modTarget ← mod.soloTarget dynlibs libDirs.toList depTarget leanOnly |>.activate
diff --git a/Lake/CLI/Main.lean b/Lake/CLI/Main.lean
index 62bebbf0c0..136815c31f 100644
--- a/Lake/CLI/Main.lean
+++ b/Lake/CLI/Main.lean
@@ -219,14 +219,14 @@ def printPaths (config : LakeConfig) (imports : List String := []) : MainM PUnit
     exit noConfigFileCode
 
 def env (cmd : String) (args : Array String := #[]) : LakeT IO UInt32 := do
-  IO.Process.spawn {cmd, args, env := ← getLeanEnv} >>= (·.wait)
+  IO.Process.spawn {cmd, args, env := ← getAugmentedEnv} >>= (·.wait)
 
 def serve (config : LakeConfig) (args : Array String) : LogIO UInt32 := do
   let (extraEnv, moreServerArgs) ←
     try
       let ws ← loadWorkspace config
       let ctx := mkLakeContext ws config
-      pure (← LakeT.run ctx getLeanEnv, ws.root.moreServerArgs)
+      pure (← LakeT.run ctx getAugmentedEnv, ws.root.moreServerArgs)
     catch _ =>
       logWarning "package configuration has errors, falling back to plain `lean --server`"
       pure (#[(invalidConfigEnvVar, "1")], #[])
diff --git a/Lake/Config/InstallPath.lean b/Lake/Config/InstallPath.lean
index 449c976432..db8985499d 100644
--- a/Lake/Config/InstallPath.lean
+++ b/Lake/Config/InstallPath.lean
@@ -3,15 +3,11 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+import Lake.Util.NativeLib
+
 open System
 namespace Lake
 
-/-- The shared library file extension for the `Platform`. -/
-def sharedLibExt : String :=
-  if Platform.isWindows then "dll"
-  else if Platform.isOSX  then "dylib"
-  else "so"
-
 /-- Standard path of `lean` in Lean installation. -/
 def leanExe (sysroot : FilePath) :=
   sysroot / "bin" / "lean" |>.withExtension FilePath.exeExtension
diff --git a/Lake/Config/LeanLib.lean b/Lake/Config/LeanLib.lean
index 6a3175aa17..c63521f174 100644
--- a/Lake/Config/LeanLib.lean
+++ b/Lake/Config/LeanLib.lean
@@ -50,17 +50,17 @@ namespace LeanLib
 @[inline] def isBuildableModule (mod : Name) (self : LeanLib) : Bool :=
   self.config.isBuildableModule mod
 
-/-- The file name of the library's static binary (i.e., `lib{libName}.a`) -/
+/-- The file name of the library's static binary (i.e., its `.a`) -/
 @[inline] def staticLibFileName (self : LeanLib) : FilePath :=
-  s!"lib{self.config.libName}.a"
+  nameToStaticLib self.config.libName
 
 /-- The path to the static library in the package's `libDir`. -/
 @[inline] def staticLibFile (self : LeanLib) : FilePath :=
   self.pkg.libDir / self.staticLibFileName
 
-/-- The file name of the library's shared binary (i.e., its `dll`/`dylib`/`so`) . -/
+/-- The file name of the library's shared binary (i.e., its `dll`, `dylib`, or `so`) . -/
 @[inline] def sharedLibFileName (self : LeanLib) : FilePath :=
-  s!"{self.config.libName}.{sharedLibExt}"
+  nameToSharedLib self.config.libName
 
 /-- The path to the shared library in the package's `libDir`. -/
 @[inline] def sharedLibFile (self : LeanLib) : FilePath :=
diff --git a/Lake/Config/Module.lean b/Lake/Config/Module.lean
index 2f12ce4223..34cb9b8d64 100644
--- a/Lake/Config/Module.lean
+++ b/Lake/Config/Module.lean
@@ -67,12 +67,12 @@ abbrev pkg (self : Module) : Package :=
 @[inline] def oFile (self : Module) : FilePath :=
   Lean.modToFilePath self.pkg.irDir self.name "o"
 
-@[inline] def dynlibName (self : Module) : FilePath :=
+@[inline] def dynlibName (self : Module) : String :=
   -- NOTE: file name MUST be unique on Windows
   self.name.toStringWithSep "-"
 
 @[inline] def dynlibFile (self : Module) : FilePath :=
-  self.pkg.libDir / s!"lib{self.dynlibName}.{sharedLibExt}"
+  self.pkg.libDir / nameToSharedLib self.dynlibName
 
 @[inline] def buildType (self : Module) : BuildType :=
   self.lib.buildType
diff --git a/Lake/Config/Monad.lean b/Lake/Config/Monad.lean
index 0d3eb13484..e203d1644d 100644
--- a/Lake/Config/Monad.lean
+++ b/Lake/Config/Monad.lean
@@ -34,20 +34,16 @@ instance [Monad m] : MonadLake (LakeT m) where
   getLakeInstall := (·.lake) <$> read
   getWorkspace := (·.workspace) <$> read
 
-variable [MonadLake m]
+instance [MonadLake m] [Monad m] [MonadLiftT n m] : MonadLiftT (LakeT n) m where
+  monadLift x := do
+    liftM <| x {
+      lean := ← getLeanInstall
+      lake := ← getLakeInstall
+      opaqueWs := ← getWorkspace
+    }
 
-def getLeanEnv [Monad m] : m (Array (String × Option String)) := do
-  let ws ← getWorkspace
-  let lean ← getLeanInstall
-  return #[
-    ("LEAN_SYSROOT", lean.sysroot.toString),
-    ("LEAN_AR", lean.ar.toString),
-    ("LEAN_CC", lean.cc.toString),
-    ("LEAN_PATH", ws.oleanPath.toString),
-    ("LEAN_SRC_PATH", ws.leanSrcPath.toString)
-  ]
-
-variable [Functor m]
+section
+variable [MonadLake m] [Functor m]
 
 @[inline] def findPackage? (name : Name) : m (Option Package) :=
   (·.findPackage? name) <$> getWorkspace
@@ -64,9 +60,15 @@ variable [Functor m]
 @[inline] def findExternLib? (mod : Name) : m (Option ExternLib) :=
   (·.findExternLib? mod) <$> getWorkspace
 
-@[inline] def getOleanPath : m SearchPath :=
+@[inline] def getLeanPath : m SearchPath :=
   (·.oleanPath) <$> getWorkspace
 
+@[inline] def getLeanSrcPath : m SearchPath :=
+  (·.leanSrcPath) <$> getWorkspace
+
+@[inline] def getLibPath : m SearchPath :=
+  (·.libPath) <$> getWorkspace
+
 @[inline] def getLeanSysroot : m FilePath :=
   (·.sysroot) <$> getLeanInstall
 
@@ -91,5 +93,34 @@ variable [Functor m]
 @[inline] def getLeanCc : m FilePath :=
   (·.cc) <$> getLeanInstall
 
+@[inline] def getLake : m FilePath :=
+  (·.lake) <$> getLakeInstall
+
+@[inline] def getLakeHome : m FilePath :=
+  (·.home) <$> getLakeInstall
+
 @[inline] def getLakeOleanDir : m FilePath :=
   (·.oleanDir) <$> getLakeInstall
+
+end
+
+@[inline] def getAugmentedLeanPath : LakeT IO SearchPath := do
+  return (← getSearchPath "LEAN_PATH") ++ (← getLeanPath)
+
+@[inline] def getAugmentedLeanSrcPath : LakeT IO SearchPath := do
+  return (← getSearchPath "LEAN_SRC_PATH") ++ (← getLeanSrcPath)
+
+@[inline] def getAugmentedLibPath : LakeT IO SearchPath := do
+  return (← getSearchPath sharedLibPathEnvVar) ++ (← getLibPath)
+
+def getAugmentedEnv : LakeT IO (Array (String × Option String)) :=
+  return #[
+    ("LAKE", (← getLake).toString),
+    ("LAKE_HOME", (← getLakeHome).toString),
+    ("LEAN_SYSROOT", (← getLeanSysroot).toString),
+    ("LEAN_AR", (← getLeanAr).toString),
+    ("LEAN_CC", (← getLeanCc).toString),
+    ("LEAN_PATH", (← getAugmentedLeanPath).toString),
+    ("LEAN_SRC_PATH", (← getAugmentedLeanSrcPath).toString),
+    (sharedLibPathEnvVar, (← getAugmentedLibPath).toString)
+  ]
diff --git a/Lake/Config/Workspace.lean b/Lake/Config/Workspace.lean
index 4a94a1a8ec..84d7dbc357 100644
--- a/Lake/Config/Workspace.lean
+++ b/Lake/Config/Workspace.lean
@@ -108,6 +108,13 @@ def oleanPath (self : Workspace) : SearchPath :=
 def leanSrcPath (self : Workspace) : SearchPath :=
   self.packageList.map (·.srcDir)
 
+/--
+The shared library path of the workspace (e.g., for `--load-dynlib`).
+This is added to the `sharedLibPathEnvVar` by `lake env`.
+-/
+def libPath (self : Workspace) : SearchPath :=
+  self.packageList.map (·.libDir)
+
 /-- The `LeanPaths` of the workspace. -/
 def leanPaths (self : Workspace) : LeanPaths where
   oleanPath := self.packageList.map (·.oleanDir)
diff --git a/Lake/Util/Async.lean b/Lake/Util/Async.lean
index a0dce44fde..5b44bb0c43 100644
--- a/Lake/Util/Async.lean
+++ b/Lake/Util/Async.lean
@@ -5,7 +5,7 @@ Authors: Mac Malone
 -/
 import Lake.Util.Task
 import Lake.Util.OptionIO
-import Lake.Util.Misc
+import Lake.Util.Lift
 
 /-!
 This module Defines the asynchronous monadic interface for Lake.
@@ -84,10 +84,10 @@ instance : Async OptionIO BaseIO OptionIOTask where
 instance : Await Task Id := ⟨Task.get⟩
 
 instance : Await (EIOTask ε) (EIO ε) where
-  await x := IO.wait x >>= liftExcept
+  await x := IO.wait x >>= liftM
 
 instance : Await OptionIOTask OptionIO where
-  await x := IO.wait x >>= liftOption
+  await x := IO.wait x >>= liftM
 
 instance [Await k m] : Await (ExceptT ε k) (ExceptT ε m) where
   await x := ExceptT.mk <| await x.run
@@ -203,18 +203,12 @@ instance : ApplicativeAsync BaseIO BaseIOTask where
 
 instance [ApplicativeAsync n k] : ApplicativeAsync n (ExceptT ε k) where
   seqWithAsync f ka kb :=
-    let h xa xb : Except ε _ := Id.run <| ExceptT.run do
-      let a ← liftExcept xa
-      let b ← liftExcept xb
-      pure <| f a b
+    let h xa xb : Except ε _ := return f (← xa) (← xb)
     cast (by delta ExceptT; rfl) <| seqWithAsync (n := n) h ka kb
 
 instance [ApplicativeAsync n k] : ApplicativeAsync n (OptionT k) where
   seqWithAsync f ka kb :=
-    let h xa xb := Id.run <| OptionT.run do
-      let a ← liftOption xa
-      let b ← liftOption xb
-      pure <| f a b
+    let h xa xb : Option _ := return f (← xa) (← xb)
     cast (by delta OptionT; rfl) <| seqWithAsync (n := n) h ka kb
 
 --------------------------------------------------------------------------------
diff --git a/Lake/Util/Git.lean b/Lake/Util/Git.lean
index 96c235e4a2..19114a816b 100644
--- a/Lake/Util/Git.lean
+++ b/Lake/Util/Git.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
 -/
 import Lake.Util.Log
-import Lake.Util.Misc
+import Lake.Util.Lift
 
 open System
 namespace Lake
diff --git a/Lake/Util/Lift.lean b/Lake/Util/Lift.lean
new file mode 100644
index 0000000000..c9b45a79c2
--- /dev/null
+++ b/Lake/Util/Lift.lean
@@ -0,0 +1,32 @@
+/-
+Copyright (c) 2022 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+
+namespace Lake
+
+instance [Pure m] : MonadLiftT Id m where
+  monadLift act := pure act.run
+
+instance [Alternative m] : MonadLiftT Option m where
+  monadLift
+    | some a => pure a
+    | none => failure
+
+instance [Pure m] [MonadExceptOf ε m] : MonadLiftT (Except ε) m where
+  monadLift
+    | .ok a => pure a
+    | .error e => throw e
+
+instance [Bind m] [MonadReaderOf ρ m] [MonadLiftT n m] : MonadLiftT (ReaderT ρ n) m where
+  monadLift act := do act (← read)
+
+instance [Monad m] [MonadStateOf σ m] [MonadLiftT n m] : MonadLiftT (StateT σ n) m where
+  monadLift act := do let (a, s) ← act (← get); set s; pure a
+
+instance [Monad m] [Alternative m] [MonadLiftT n m] : MonadLiftT (OptionT n) m where
+  monadLift act := act.run >>= liftM
+
+instance [Monad m] [MonadExceptOf ε m] [MonadLiftT n m] : MonadLiftT (ExceptT ε n) m where
+  monadLift act := act.run >>= liftM
diff --git a/Lake/Util/Misc.lean b/Lake/Util/Misc.lean
deleted file mode 100644
index ee9ca4d754..0000000000
--- a/Lake/Util/Misc.lean
+++ /dev/null
@@ -1,14 +0,0 @@
-/-
-Copyright (c) 2021 Mac Malone. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mac Malone
--/
-
-namespace Lake
-
-def liftOption [Alternative m] : Option α → m α
-| some a => pure a
-| none => failure
-
-instance [MonadLiftT m n] : MonadLiftT (ReaderT ρ m) (ReaderT ρ n) where
-  monadLift x := fun r => liftM <| x r
diff --git a/Lake/Util/NativeLib.lean b/Lake/Util/NativeLib.lean
new file mode 100644
index 0000000000..0a6fff1df0
--- /dev/null
+++ b/Lake/Util/NativeLib.lean
@@ -0,0 +1,42 @@
+/-
+Copyright (c) 2021 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+
+open System
+namespace Lake
+
+/-- The shared library file extension for the `Platform`. -/
+def sharedLibExt : String :=
+  if Platform.isWindows then "dll"
+  else if Platform.isOSX  then "dylib"
+  else "so"
+
+/-- Convert a library name into its static library file name for the `Platform`. -/
+def nameToStaticLib (name : String) : String :=
+  if Platform.isWindows then s!"{name}.a" else s!"lib{name}.a"
+
+/-- Convert a library name into its shared library file name for the `Platform`. -/
+def nameToSharedLib (name : String) : String :=
+  if Platform.isWindows then s!"{name}.dll"
+  else if Platform.isOSX  then s!"lib{name}.dylib"
+  else s!"lib{name}.so"
+
+/--
+The environment variable that stores the search path
+used to find shared libraries on the `Platform`.
+-/
+def sharedLibPathEnvVar :=
+  if Platform.isWindows then
+    "PATH"
+  else if Platform.isOSX then
+    "DYLD_LIBRARY_PATH"
+  else
+    "LD_LIBRARY_PATH"
+
+/-- Gets a `SearchPath` from an environment variable. -/
+def getSearchPath (envVar : String) : IO SearchPath := do
+  match (← IO.getEnv envVar) with
+  | some path => pure <| SearchPath.parse path
+  | none => pure []
diff --git a/Lake/Util/Store.lean b/Lake/Util/Store.lean
index 686bb919fd..2f55b7064f 100644
--- a/Lake/Util/Store.lean
+++ b/Lake/Util/Store.lean
@@ -24,6 +24,6 @@ instance [MonadDStore κ β m] : MonadStore1 k (β k) m where
 /-- A monad equipped with a key-object store. -/
 abbrev MonadStore κ α m := MonadDStore κ (fun _ => α) m
 
-instance [MonadLiftT m n] [MonadDStore κ β m] : MonadDStore κ β n where
+instance [MonadLift m n] [MonadDStore κ β m] : MonadDStore κ β n where
   fetch? k := liftM (m := m) <| fetch? k
   store k a := liftM (m := m) <| store k a
diff --git a/README.md b/README.md
index 8916cb8aff..e00f7e102b 100644
--- a/README.md
+++ b/README.md
@@ -172,6 +172,8 @@ lean_exe «target-name» {
 
 A external library target is a non-Lean **static** library that will be linked to the binaries of the package and its dependents (e.g., their shared libraries and executables).
 
+**Important:** For the external library to link properly when `precompileModules` is on, the static library produced by an `extern_lib` target must following the platform's naming conventions for libraries (i.e., be named `foo.a` on Windows and `libfoo.a` on Unix). To make this easy, there is the `Lake.nameToStaticLib` utility function to convert a library name into its proper file name for the platform.
+
 **Syntax**
 
 ```lean
diff --git a/examples/ffi/lib/lakefile.lean b/examples/ffi/lib/lakefile.lean
index 8907aa98d1..c99b5e3dac 100644
--- a/examples/ffi/lib/lakefile.lean
+++ b/examples/ffi/lib/lakefile.lean
@@ -23,5 +23,5 @@ def ffiOTarget : FileTarget :=
     compileO oFile srcFile #["-I", (← getLeanIncludeDir).toString, "-fPIC"] "c++"
 
 extern_lib cLib :=
-  let libFile := cBuildDir / s!"libleanffi.a"
+  let libFile := cBuildDir / nameToStaticLib "leanffi"
   staticLibTarget libFile #[ffiOTarget]
diff --git a/examples/targets/test.sh b/examples/targets/test.sh
index c8ec05cf3c..2a64e762c2 100755
--- a/examples/targets/test.sh
+++ b/examples/targets/test.sh
@@ -4,10 +4,13 @@ set -exo pipefail
 LAKE=${LAKE:-../../build/bin/lake}
 
 if [ "$OS" = Windows_NT ]; then
+LIB_PREFIX=
 SHARED_LIB_EXT=dll
 elif [ "`uname`" = Darwin ]; then
+LIB_PREFIX=lib
 SHARED_LIB_EXT=dylib
 else
+LIB_PREFIX=lib
 SHARED_LIB_EXT=so
 fi
 
@@ -38,8 +41,8 @@ $LAKE build a b
 $LAKE build foo:static
 $LAKE build bar:shared
 
-test -f ./build/lib/libFoo.a
-test -f ./build/lib/Bar.$SHARED_LIB_EXT
+test -f ./build/lib/${LIB_PREFIX}Foo.a
+test -f ./build/lib/${LIB_PREFIX}Bar.$SHARED_LIB_EXT
 
 $LAKE build bark | grep -m1 Bark!