chore: teach lake exe cache about ProofWidgets (#5128)

Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
leanprover-community · Jun 17, 2023 · 64f9723 · 64f9723
1 parent 77738af
commit 64f9723
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/Cache/IO.lean b/Cache/IO.lean
@@ -66,11 +66,13 @@ def isMathlibRoot : IO Bool :=
 def mathlibDepPath : FilePath :=
   LAKEPACKAGESDIR / "mathlib"
 
+-- TODO this should be generated automatically from the information in `lakefile.lean`.
 def getPackageDirs : IO PackageDirs := return .ofList [
   ("Mathlib", if ← isMathlibRoot then "." else mathlibDepPath),
   ("MathlibExtras", if ← isMathlibRoot then "." else mathlibDepPath),
   ("Aesop", LAKEPACKAGESDIR / "aesop"),
   ("Std", LAKEPACKAGESDIR / "std"),
+  ("ProofWidgets", LAKEPACKAGESDIR / "proofwidgets"),
   ("Qq", LAKEPACKAGESDIR / "Qq")
 ]