feat: lake env w/o configuration + more (#2428)

* feat: `lake env` w/o configuration + more

* chore: `lake env printenv DYLD_LIBRARY_PATH` illegal on MacOS

Author: tydeu

src/lake/Lake/CLI/Help.lean

@@ -26,18 +26,18 @@ OPTIONS:
   --update, -U          update manifest before building
 
 COMMANDS:
-  new <name> [<temp>]   create a Lean package in a new directory
-  init <name> [<temp>]  create a Lean package in the current directory
-  build [<targets>...]  build targets
+  new <name> <temp>     create a Lean package in a new directory
+  init <name> <temp>    create a Lean package in the current directory
+  build <targets>...    build targets
   update                update dependencies and save them to the manifest
   upload <tag>          upload build artifacts to a GitHub release
   clean                 remove build outputs
   script                manage and run workspace scripts
   scripts               shorthand for `lake script list`
   run <script>          shorthand for `lake script run`
   serve                 start the Lean language server
-  env <cmd> [<args>...] execute a command in the workspace's environment
-  exe <exe> [<args>...] build an exe and run it in the workspace's environment
+  env <cmd> <args>...   execute a command in Lake's environment
+  exe <exe> <args>...   build an exe and run it in Lake's environment
 
 See `lake help <command>` for more information on a specific command."
 
@@ -97,7 +97,7 @@ TARGET EXAMPLES:        build the ...
   a/+A:c                C file of module `A` of package `a`
   :foo                  facet `foo` of the root package
 
-A bare `build` command will build the default facet of the root package.
+A bare `lake build` command will build the default facet of the root package.
 Package dependencies are not updated during a build."
 
 def helpUpdate :=
@@ -161,12 +161,12 @@ def helpScriptRun :=
 "Run a script
 
 USAGE:
-  lake script run [<package>/]<script> [<args>...]
+  lake script run [[<package>/]<script>] [<args>...]
 
 This command runs the given `script` from `package`, passing `args` to it.
 Defaults to the root package.
 
-A bare `run` command will run the default script(s) of the root package
+A bare `lake run` command will run the default script(s) of the root package
 (with no arguments)."
 
 def helpScriptDoc :=
@@ -188,38 +188,42 @@ with the package configuration's `moreServerArgs` field and `args`.
 "
 
 def helpEnv :=
-"Execute a command in the workspace's environment
+"Execute a command in Lake's environment
 
 USAGE:
-  lake env <cmd> [<args>...]
+  lake env [<cmd>] [<args>...]
 
 Spawns a new process executing `cmd` with the given `args` and with
-the environment set based on the workspace configuration and the detected
-Lean/Lake installations.
+the environment set based on the detected Lean/Lake installations and
+the workspace configuration (if it exists).
 
 Specifically, this command sets the following environment variables:
 
   LAKE                  set to the detected Lake executable
   LAKE_HOME             set to the detected Lake home
-  LEAN_SYSROOT          set to the detected Lean sysroot
+  LEAN_SYSROOT          set to the detected Lean toolchain directory
   LEAN_AR               set to the detected Lean `ar` binary
-  LEAN_CC               set to the detected `cc` (if not using bundled one)
-  LEAN_PATH             adds the workspace's library directories
-  LEAN_SRC_PATH         adds the workspace's source directories
-  PATH                  adds the workspace's library directories (Windows)
-  DYLD_LIBRARY_PATH     adds the workspace's library directories (MacOS)
-  LD_LIBRARY_PATH       adds the workspace's library directories (other Unix)"
+  LEAN_CC               set to the detected `cc` (if not using the bundled one)
+  LEAN_PATH             adds Lake's and the workspace's Lean library dirs
+  LEAN_SRC_PATH         adds Lake's and the workspace's source dirs
+  PATH                  adds Lean's, Lake's, and the workspace's binary dirs
+  PATH                  adds Lean's and the workspace's library dirs (Windows)
+  DYLD_LIBRARY_PATH     adds Lean's and the workspace's library dirs (MacOS)
+  LD_LIBRARY_PATH       adds Lean's and the workspace's library dirs (other)
+
+A bare `lake env` will print out the variables set and their values,
+using the form NAME=VALUE like the POSIX `env` command."
 
 def helpExe :=
-"Build an executable target and run it in the workspace's environment
+"Build an executable target and run it in Lake's environment
 
 USAGE:
   lake exe <exe-target> [<args>...]
 
 Looks for the executable target in the workspace (see `lake help build` to
 learn how to specify targets), builds it if it is out of date, and then runs
-it with the given `args` in the workspace's environment (see `lake help env`
-for how the environment is set)."
+it with the given `args` in Lake's environment (see `lake help env` for how
+the environment is set up)."
 
 def helpScript : (cmd : String) → String
 | "list"      => helpScriptList

src/lake/Lake/CLI/Main.lean

@@ -328,11 +328,19 @@ protected def serve : CliM PUnit := do
   noArgsRem do exit <| ← serve config args
 
 protected def env : CliM PUnit := do
-  let cmd ← takeArg "command"; let args ← takeArgs
   let config ← mkLoadConfig (← getThe LakeOptions)
-  let ws ← loadWorkspace config
-  let ctx := mkLakeContext ws
-  exit <| ← (env cmd args.toArray).run ctx
+  let env ← do
+    if (← config.configFile.pathExists) then
+      pure (← loadWorkspace config).augmentedEnvVars
+    else
+      pure config.env.vars
+  if let some cmd ← takeArg? then
+    let child ← IO.Process.spawn {cmd, args := (← takeArgs).toArray, env}
+    exit <| ← child.wait
+  else
+    env.forM fun (var, val?) =>
+      IO.println s!"{var}={val?.getD ""}"
+    exit 0
 
 protected def exe : CliM PUnit := do
   let exeName ← takeArg "executable name"

src/lake/Lake/Config/Env.lean

@@ -8,29 +8,82 @@ import Lake.Config.InstallPath
 
 open System
 
+/-! # Lake's Environment
+Definitions related to a Lake environment.
+A Lake environment is computed on Lake's startup from
+user-specified CLI options and the process environment.
+-/
+
 namespace Lake
 
-/-- The detected Lake environment. -/
+/-- A Lake environment. -/
 structure Env where
+  /-- The Lake installation of the environment. -/
   lake : LakeInstall
+  /-- The Lean installation of the environment. -/
   lean : LeanInstall
-  leanPath : SearchPath
-  leanSrcPath : SearchPath
-  sharedLibPath : SearchPath
+  /-- The initial Lean library search path of the environment (i.e., `LEAN_PATH`). -/
+  initLeanPath : SearchPath
+  /-- The initial Lean source search path of the environment (i.e., `LEAN_SRC_PATH`). -/
+  initLeanSrcPath : SearchPath
+  /-- The initial shared library search path of the environment. -/
+  initSharedLibPath : SearchPath
+  /-- The initial binary search path of the environment (i.e., `PATH`). -/
+  initPath : SearchPath
   deriving Inhabited, Repr
 
 namespace Env
 
 /-- Compute an `Lake.Env` object from the given installs and set environment variables. -/
 def compute (lake : LakeInstall) (lean : LeanInstall) : BaseIO Env :=
   return {
-    lake, lean
-    leanPath := ← getSearchPath "LEAN_PATH",
-    leanSrcPath := ← getSearchPath "LEAN_SRC_PATH",
-    sharedLibPath := ← getSearchPath sharedLibPathEnvVar
+    lake, lean,
+    initLeanPath := ← getSearchPath "LEAN_PATH",
+    initLeanSrcPath := ← getSearchPath "LEAN_SRC_PATH",
+    initSharedLibPath := ← getSearchPath sharedLibPathEnvVar,
+    initPath := ← getSearchPath "PATH"
   }
 
-/-- Environment variable settings based only on the given Lean and Lake installations. -/
+/--
+The Lean library search path of the environment (i.e., `LEAN_PATH`).
+Combines the initial path of the environment with that of the Lake installation.
+-/
+def path (env : Env) : SearchPath :=
+  if env.lake.binDir = env.lean.binDir then
+    env.lean.binDir :: env.initPath
+  else
+    env.lake.binDir :: env.lean.binDir :: env.initPath
+
+/-
+We include Lake's installation in the cases below to ensure that the
+Lake being used to build is available to the environment (and thus, e.g.,
+the Lean server). Otherwise, it may fall back on whatever the default Lake
+instance is.
+-/
+
+/--
+The Lean library search path of the environment (i.e., `LEAN_PATH`).
+Combines the initial path of the environment with that of the Lake installation.
+-/
+def leanPath (env : Env) : SearchPath :=
+  env.lake.libDir :: env.initLeanPath
+
+/--
+The Lean source search path of the environment (i.e., `LEAN_SRC_PATH`).
+Combines the initial path of the environment with that of the Lake abd Lean
+installations.
+-/
+def leanSrcPath (env : Env) : SearchPath :=
+  env.lake.srcDir :: env.initLeanSrcPath
+
+/--
+The shared library search path of the environment.
+Combines the initial path of the environment with that of the Lean installation.
+-/
+def sharedLibPath (env : Env) : SearchPath :=
+  env.lean.sharedLibPath ++ env.initSharedLibPath
+
+/-- Environment variable settings based only on the Lean and Lake installations. -/
 def installVars (env : Env) : Array (String × Option String)  :=
   #[
     ("LAKE", env.lake.lake.toString),
@@ -42,11 +95,15 @@ def installVars (env : Env) : Array (String × Option String)  :=
 
 /-- Environment variable settings for the `Lake.Env`. -/
 def vars (env : Env) : Array (String × Option String)  :=
-  env.installVars ++ #[
+  let vars := env.installVars ++ #[
     ("LEAN_PATH", some env.leanPath.toString),
     ("LEAN_SRC_PATH", some env.leanSrcPath.toString),
-    (sharedLibPathEnvVar, some env.sharedLibPath.toString)
+    ("PATH", some env.path.toString)
   ]
+  if Platform.isWindows then
+    vars
+  else
+    vars.push (sharedLibPathEnvVar, some <| env.sharedLibPath.toString)
 
 /--
 The default search path the Lake executable

src/lake/Lake/Config/InstallPath.lean

@@ -41,6 +41,7 @@ structure LeanInstall where
   leanLibDir := sysroot / "lib" / "lean"
   includeDir := sysroot / "include"
   systemLibDir := sysroot / "lib"
+  binDir := sysroot / "bin"
   lean := leanExe sysroot
   leanc := leancExe sysroot
   sharedLib := leanSharedLib sysroot
@@ -49,6 +50,16 @@ structure LeanInstall where
   customCc : Bool
   deriving Inhabited, Repr
 
+/--
+A `SearchPath` including the Lean installation's shared library directories
+(i.e., the system library and Lean library directories).
+-/
+def LeanInstall.sharedLibPath (self : LeanInstall) : SearchPath :=
+  if Platform.isWindows then
+    [self.binDir]
+  else
+    [self.leanLibDir, self.systemLibDir]
+
 /-- The `LEAN_CC` of the Lean installation. -/
 def LeanInstall.leanCc? (self : LeanInstall) : Option String :=
   if self.customCc then self.cc.toString else none
@@ -61,6 +72,7 @@ def lakeExe (buildHome : FilePath) :=
 structure LakeInstall where
   home : FilePath
   srcDir := home
+  binDir := home / "build" / "bin"
   libDir := home / "build" / "lib"
   lake := lakeExe <| home / "build"
   deriving Inhabited, Repr
@@ -218,6 +230,7 @@ def findInstall? : BaseIO (Option LeanInstall × Option LakeInstall) := do
       some {
         home,
         srcDir := lean.srcDir / "lake",
+        binDir := lean.binDir,
         libDir := lean.leanLibDir,
         lake := lakeExe home
       }

src/lake/Lake/Config/Workspace.lean

@@ -124,13 +124,21 @@ def addLibraryFacetConfig (cfg : LibraryFacetConfig name) (self : Workspace) : W
 @[inline] def findLibraryFacetConfig? (name : Name) (self : Workspace) : Option (LibraryFacetConfig name) :=
   self.libraryFacetConfigs.find? name
 
-/-- The workspace's binary Lean library paths (which are added to `LEAN_PATH`). -/
+/-- The workspace's binary directories (which are added to `Path`). -/
+def binPath (self : Workspace) : SearchPath :=
+  self.packageList.map (·.binDir)
+
+/-- The workspace's Lean library directories (which are added to `LEAN_PATH`). -/
 def leanPath (self : Workspace) : SearchPath :=
   self.packageList.map (·.leanLibDir)
 
-/-- The workspace's  source directories (which are added to `LEAN_SRC_PATH`). -/
-def leanSrcPath (self : Workspace) : SearchPath :=
-  self.packageList.map (·.srcDir)
+/-- The workspace's source directories (which are added to `LEAN_SRC_PATH`). -/
+def leanSrcPath (self : Workspace) : SearchPath := Id.run do
+  let mut path : SearchPath := {}
+  for pkg in self.packageArray do
+    for (_, config) in pkg.leanLibConfigs do
+      path := pkg.srcDir / config.srcDir :: path
+  return path
 
 /--
 The workspace's shared library path (e.g., for `--load-dynlib`).
@@ -140,44 +148,47 @@ def sharedLibPath (self : Workspace) : SearchPath :=
   self.packageList.map (·.nativeLibDir)
 
 /--
-The detected `LEAN_PATH` of the environment
-augmented with the workspace's `leanPath` and Lake's `libDir`.
+The detected `PATH` of the environment augmented with
+the workspace's `binDir` and Lean and Lake installations' `binDir`.
+-/
+def augmentedPath (self : Workspace) : SearchPath :=
+  self.binPath ++ self.lakeEnv.path
 
-We include Lake's `oleanDir` at the end to ensure that same Lake package being
-used to build is available to the environment (and thus, e.g., the Lean server).
-Otherwise, it may fall back on whatever the default Lake instance is.
+/--
+The detected `LEAN_PATH` of the environment augmented with
+the workspace's `leanPath` and Lake's `libDir`.
 -/
 def augmentedLeanPath (self : Workspace) : SearchPath :=
-  self.lakeEnv.leanPath ++ self.leanPath ++ [self.lakeEnv.lake.libDir]
+  self.leanPath ++ self.lakeEnv.leanPath
 
 /--
-The detected `LEAN_SRC_PATH` of the environment
-augmented with the workspace's `leanSrcPath` and Lake's `srcDir`.
-
-We include Lake's `srcDir` at the end to ensure that same Lake package being
-used to build is available to the environment (and thus, e.g., the Lean server).
-Otherwise, it may fall back on whatever the default Lake instance is.
+The detected `LEAN_SRC_PATH` of the environment augmented with
+the workspace's `leanSrcPath` and Lake's `srcDir`.
 -/
 def augmentedLeanSrcPath (self : Workspace) : SearchPath :=
-  self.lakeEnv.leanSrcPath ++ self.leanSrcPath ++ [self.lakeEnv.lake.srcDir]
+  self.leanSrcPath ++ self.lakeEnv.leanSrcPath
 
 /-
-The detected `sharedLibPathEnv` value of the environment
-augmented with the workspace's `libPath`.
+The detected `sharedLibPathEnv` value of the environment augmented with
+the workspace's `libPath` and Lean installation's shared library directories.
 -/
 def augmentedSharedLibPath (self : Workspace) : SearchPath :=
-  self.lakeEnv.sharedLibPath ++ self.sharedLibPath
+  self.sharedLibPath ++ self.lakeEnv.sharedLibPath
 
 /--
-The detected environment augmented with the Workspace's paths.
+The detected environment augmented with Lake's and the workspace's paths.
 These are the settings use by `lake env` / `Lake.env` to run executables.
 -/
 def augmentedEnvVars (self : Workspace) : Array (String × Option String) :=
-  self.lakeEnv.installVars ++ #[
+  let vars := self.lakeEnv.installVars ++ #[
     ("LEAN_PATH", some self.augmentedLeanPath.toString),
     ("LEAN_SRC_PATH", some self.augmentedLeanSrcPath.toString),
-    (sharedLibPathEnvVar, some self.augmentedSharedLibPath.toString)
+    ("PATH", some self.augmentedPath.toString)
   ]
+  if Platform.isWindows then
+    vars
+  else
+    vars.push (sharedLibPathEnvVar, some self.augmentedSharedLibPath.toString)
 
 /-- Remove all packages' build outputs (i.e., delete their build directories). -/
 def clean (self : Workspace) : IO Unit := do