From cee959078db44e7dbff46e1e98a3678888cf0ad4 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Sat, 17 Dec 2022 19:58:27 -0800
Subject: [PATCH] fix: do not require Environment to be inhabited

---
 Lake/Build/Monad.lean      | 2 --
 Lake/Config/ExternLib.lean | 1 -
 Lake/Config/LeanExe.lean   | 1 -
 Lake/Config/LeanLib.lean   | 1 -
 Lake/Config/Module.lean    | 1 -
 Lake/Config/Monad.lean     | 2 --
 Lake/Config/Package.lean   | 5 ++++-
 Lake/Config/Workspace.lean | 5 ++++-
 8 files changed, 8 insertions(+), 10 deletions(-)

diff --git a/Lake/Build/Monad.lean b/Lake/Build/Monad.lean
index ba6cbf9018..62bed905ed 100644
--- a/Lake/Build/Monad.lean
+++ b/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 :=
diff --git a/Lake/Config/ExternLib.lean b/Lake/Config/ExternLib.lean
index 77b2043727..a15472381b 100644
--- a/Lake/Config/ExternLib.lean
+++ b/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 :=
diff --git a/Lake/Config/LeanExe.lean b/Lake/Config/LeanExe.lean
index 7920b73253..0cc55ea114 100644
--- a/Lake/Config/LeanExe.lean
+++ b/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 :=
diff --git a/Lake/Config/LeanLib.lean b/Lake/Config/LeanLib.lean
index a29a0fa775..592e722749 100644
--- a/Lake/Config/LeanLib.lean
+++ b/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 :=
diff --git a/Lake/Config/Module.lean b/Lake/Config/Module.lean
index c6c41e3f6b..481e07a92c 100644
--- a/Lake/Config/Module.lean
+++ b/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
diff --git a/Lake/Config/Monad.lean b/Lake/Config/Monad.lean
index 56abd391a9..0908101c93 100644
--- a/Lake/Config/Monad.lean
+++ b/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
diff --git a/Lake/Config/Package.lean b/Lake/Config/Package.lean
index 432e05a4f9..2f4a6310b1 100644
--- a/Lake/Config/Package.lean
+++ b/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
 
diff --git a/Lake/Config/Workspace.lean b/Lake/Config/Workspace.lean
index 4fefa00ea9..6c1eab0a88 100644
--- a/Lake/Config/Workspace.lean
+++ b/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