From 620587fc429b8e37ab72426eb1ef85953a74464e Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Sat, 11 Mar 2023 01:28:14 +0000
Subject: [PATCH] feat: make lake clean clean all packages

Fixes leanprover/lake#155
---
 Lake/CLI/Main.lean         | 2 +-
 Lake/Config/Workspace.lean | 6 ++++++
 2 files changed, 7 insertions(+), 1 deletion(-)

diff --git a/Lake/CLI/Main.lean b/Lake/CLI/Main.lean
index f1de4e97cf..1cc079412e 100644
--- a/Lake/CLI/Main.lean
+++ b/Lake/CLI/Main.lean
@@ -296,7 +296,7 @@ protected def printPaths : CliM PUnit := do
 protected def clean : CliM PUnit := do
   processOptions lakeOption
   let config ← mkLoadConfig (← getThe LakeOptions)
-  noArgsRem do (← loadWorkspace config).root.clean
+  noArgsRem do (← loadWorkspace config).clean
 
 protected def script : CliM PUnit := do
   if let some cmd ← takeArg? then
diff --git a/Lake/Config/Workspace.lean b/Lake/Config/Workspace.lean
index 7fddaee5d6..1ea923bb51 100644
--- a/Lake/Config/Workspace.lean
+++ b/Lake/Config/Workspace.lean
@@ -178,3 +178,9 @@ def augmentedEnvVars (self : Workspace) : Array (String × Option String) :=
     ("LEAN_SRC_PATH", some self.augmentedLeanSrcPath.toString),
     (sharedLibPathEnvVar, some self.augmentedSharedLibPath.toString)
   ]
+
+/-- Remove all packages' build outputs (i.e., delete their build directories). -/
+def clean (self : Workspace) : IO Unit := do
+  for (_, pkg) in self.packageMap do
+    pkg.clean
+  self.root.clean
\ No newline at end of file