fix: do not require Environment to be inhabited

Lake/Build/Monad.lean

@@ -11,8 +11,6 @@ open System
 
 namespace Lake
 
-deriving instance Inhabited for BuildContext
-
 def mkBuildContext (ws : Workspace) (oldMode : Bool) : IO BuildContext := do
   let lean := ws.lakeEnv.lean
   let leanTrace :=

Lake/Config/ExternLib.lean

@@ -15,7 +15,6 @@ structure ExternLib where
   name : Name
   /-- The library's user-defined configuration. -/
   config : ExternLibConfig pkg.name name
-  deriving Inhabited
 
 /-- The external libraries of the package (as an Array). -/
 @[inline] def Package.externLibs (self : Package) : Array ExternLib :=

Lake/Config/LeanExe.lean

@@ -14,7 +14,6 @@ structure LeanExe where
   pkg : Package
    /-- The executable's user-defined configuration. -/
   config : LeanExeConfig
-  deriving Inhabited
 
 /-- The Lean executables of the package (as an Array). -/
 @[inline] def Package.leanExes (self : Package) : Array LeanExe :=

Lake/Config/LeanLib.lean

@@ -14,7 +14,6 @@ structure LeanLib where
   pkg : Package
    /-- The library's user-defined configuration. -/
   config : LeanLibConfig
-  deriving Inhabited
 
 /-- The Lean libraries of the package (as an Array). -/
 @[inline] def Package.leanLibs (self : Package) : Array LeanLib :=

Lake/Config/Module.lean

@@ -19,7 +19,6 @@ structure Module where
   Used to create private modules (e.g., executable roots).
   -/
   keyName : Name := name
-  deriving Inhabited
 
 instance : Hashable Module where hash m := hash m.keyName
 instance : BEq Module where beq m n := m.keyName == n.keyName

Lake/Config/Monad.lean

@@ -20,8 +20,6 @@ abbrev MonadWorkspace (m : Type → Type u) :=
 abbrev MonadLake (m : Type → Type u) :=
   MonadReaderOf Context m
 
-deriving instance Inhabited for Context
-
 /-- Make a `Lake.Context` from a `Workspace`. -/
 def mkLakeContext (ws : Workspace) : Context where
   opaqueWs := ws

Lake/Config/Package.lean

@@ -205,7 +205,10 @@ structure Package where
   defaultTargets : Array Name := #[]
   /-- Scripts for the package. -/
   scripts : NameMap Script := {}
-  deriving Inhabited
+
+instance : Nonempty Package :=
+  have : Inhabited Environment := Classical.inhabited_of_nonempty inferInstance
+  by refine' ⟨{..}⟩ <;> exact default
 
 hydrate_opaque_type OpaquePackage Package
 

Lake/Config/Workspace.lean

@@ -27,7 +27,10 @@ structure Workspace : Type where
   packageFacetConfigs : DNameMap PackageFacetConfig
   /-- Name-configuration map of library facets defined in the workspace. -/
   libraryFacetConfigs : DNameMap LibraryFacetConfig
-  deriving Inhabited
+
+instance : Nonempty Workspace :=
+  have : Inhabited Package := Classical.inhabited_of_nonempty inferInstance
+  by refine' ⟨{..}⟩ <;> exact default
 
 hydrate_opaque_type OpaqueWorkspace Workspace