fix: have Lake not create core aliases into Lake namespace

src/lake/Lake/Build/Executable.lean

@@ -6,6 +6,7 @@ Authors: Mac Malone
 import Lake.Build.Common
 
 namespace Lake
+open System (FilePath)
 
 /-! # Lean Executable Build
 The build function definition for a Lean executable.

src/lake/Lake/Build/Facets.lean

@@ -16,7 +16,8 @@ definitions.
 -/
 
 namespace Lake
-export System (SearchPath FilePath)
+open Lean (Name)
+open System (SearchPath FilePath)
 
 /-- A dynamic/shared library for linking. -/
 structure Dynlib where

src/lake/Lake/Build/Index.lean

@@ -17,6 +17,7 @@ This module leverages the index to perform topologically-based recursive builds.
 
 open Lean
 namespace Lake
+open System (FilePath)
 
 /--
 Converts a conveniently-typed target facet build function into its

src/lake/Lake/Build/Info.lean

@@ -16,6 +16,7 @@ the build.
 -/
 
 namespace Lake
+open Lean (Name)
 
 /-- The type of Lake's build info. -/
 inductive BuildInfo

src/lake/Lake/Build/Key.lean

@@ -6,6 +6,7 @@ Authors: Mac Malone
 import Lake.Util.Name
 
 namespace Lake
+open Lean (Name)
 
 /-- The type of keys in the Lake build store. -/
 inductive BuildKey

src/lake/Lake/Build/Library.lean

@@ -11,6 +11,7 @@ Build function definitions for a library's builtin facets.
 -/
 
 namespace Lake
+open System (FilePath)
 
 /-! ## Build Lean & Static Lib -/
 

src/lake/Lake/Build/Package.lean

@@ -15,6 +15,7 @@ Build function definitions for a package's builtin facets.
 
 open System
 namespace Lake
+open Lean (Name)
 
 /-- Compute a topological ordering of the package's transitive dependencies. -/
 def Package.recComputeDeps (self : Package) : FetchM (Array Package) := do

src/lake/Lake/Build/Store.lean

@@ -15,6 +15,7 @@ topological-based build of an initial key's dependencies).
 -/
 
 namespace Lake
+open Lean (Name NameMap)
 
 /-- A monad equipped with a Lake build store. -/
 abbrev MonadBuildStore (m) := MonadDStore BuildKey BuildData m

src/lake/Lake/Build/Targets.lean

@@ -10,6 +10,8 @@ Utilities for fetching package, library, module, and executable targets and face
 -/
 
 namespace Lake
+open Lean (Name)
+open System (FilePath)
 
 /-! ## Package Facets & Targets -/
 

src/lake/Lake/CLI/Actions.lean

@@ -8,6 +8,8 @@ import Lake.Build.Targets
 import Lake.CLI.Build
 
 namespace Lake
+open Lean (Name)
+open System (FilePath)
 
 def env (cmd : String) (args : Array String := #[]) : LakeT IO UInt32 := do
   IO.Process.spawn {cmd, args, env := ← getAugmentedEnv} >>= (·.wait)

src/lake/Lake/CLI/Build.lean

@@ -7,6 +7,7 @@ import Lake.Build.Index
 import Lake.CLI.Error
 
 namespace Lake
+open Lean (Name)
 
 /-! ## Build Target Specifiers -/
 

src/lake/Lake/CLI/Init.lean

@@ -13,6 +13,7 @@ import Lake.Build.Actions
 
 namespace Lake
 open Git System
+open Lean (Name)
 
 /-- The default module of an executable in `std` package. -/
 def defaultExeRoot : Name := `Main

src/lake/Lake/CLI/Main.lean

@@ -19,7 +19,7 @@ import Lake.CLI.Serve
 -- # CLI
 
 open System
-open Lean (Json toJson fromJson? LeanPaths)
+open Lean (Json toJson fromJson? LeanPaths NameMap)
 
 namespace Lake
 

src/lake/Lake/CLI/Serve.lean

@@ -10,6 +10,7 @@ import Lean.Util.FileSetupInfo
 
 namespace Lake
 open Lean
+open System (FilePath)
 
 /-- Exit code to return if `setup-file` cannot find the config file. -/
 def noConfigFileCode : ExitCode := 2

src/lake/Lake/Config/ExternLib.lean

@@ -6,6 +6,7 @@ Authors: Mac Malone
 import Lake.Config.Package
 
 namespace Lake
+open Lean (Name)
 
 /-- An external library -- its package plus its configuration. -/
 structure ExternLib where

src/lake/Lake/Config/FacetConfig.lean

@@ -6,6 +6,7 @@ Authors: Mac Malone, Mario Carneiro
 import Lake.Build.Fetch
 
 namespace Lake
+open Lean (Name)
 
 /-- A facet's declarative configuration. -/
 structure FacetConfig (DataFam : Name → Type) (ι : Type) (name : Name) : Type where

src/lake/Lake/Config/Monad.lean

@@ -7,7 +7,7 @@ import Lake.Config.Context
 import Lake.Config.Workspace
 
 open System
-open Lean (Name)
+open Lean (Name NameMap)
 
 /-! # Lake Configuration Monads
 Definitions and helpers for interacting with the Lake configuration monads.

src/lake/Lake/Config/TargetConfig.lean

@@ -6,6 +6,7 @@ Authors: Mac Malone
 import Lake.Build.Fetch
 
 namespace Lake
+open Lean (Name)
 
 /-- A custom target's declarative configuration. -/
 structure TargetConfig (pkgName name : Name) : Type where

src/lake/Lake/Config/Workspace.lean

@@ -12,6 +12,7 @@ import Lake.Util.Log
 open System
 
 namespace Lake
+open Lean (Name)
 
 /-- A Lake workspace -- the top-level package directory. -/
 structure Workspace : Type where

src/lake/Lake/DSL/Targets.lean

@@ -12,6 +12,7 @@ Macros for declaring Lake targets and facets.
 
 namespace Lake.DSL
 open Lean Parser Command
+open System (FilePath)
 
 syntax buildDeclSig :=
   identOrStr (ppSpace simpleBinder)? Term.typeSpec declValSimple

src/lake/Lake/Load/Package.lean

@@ -15,6 +15,7 @@ from Lake configuration file (either Lean or TOML).
 open Lean
 
 namespace Lake
+open System (FilePath)
 
 /--
 Return whether a configuration file with the given name

src/lake/Lake/Load/Toml.lean

@@ -17,6 +17,7 @@ Lake configuration file written in TOML.
 -/
 
 namespace Lake
+open System (FilePath)
 
 open Toml
 

src/lake/Lake/Util/Name.lean

@@ -11,8 +11,7 @@ import Lake.Util.RBArray
 open Lean
 
 namespace Lake
-
-export Lean (Name NameMap)
+open Lean (Name NameMap)
 
 /--
 First tries to convert a string into a legal name.

src/lake/examples/targets/lakefile.lean

@@ -40,7 +40,7 @@ package_facet print_name pkg : Unit := Job.async do
   IO.println pkg.name
   return ((), .nil)
 
-module_facet get_src mod : FilePath := do
+module_facet get_src mod : System.FilePath := do
   inputTextFile mod.leanFile
 
 module_facet print_src mod : Unit := do