From d688d050891741869d3359c45e1c80fcfb7d0836 Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Sun, 30 Jul 2023 14:40:24 -0400
Subject: [PATCH] chore: update to new Lean/Lake version

---
 lakefile.lean  | 15 ++-------------
 lean-toolchain |  2 +-
 2 files changed, 3 insertions(+), 14 deletions(-)

diff --git a/lakefile.lean b/lakefile.lean
index bc1253e..0362a70 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -60,21 +60,10 @@ target coreDocs : FilePath := do
     return (dataFile, trace)
 
 library_facet docs (lib) : FilePath := do
-  let some docGen4Pkg ← findPackage? `«doc-gen4»
-    | error "no doc-gen4 package found in workspace"
-  let some docGen4 := docGen4Pkg.findLeanExe? `«doc-gen4»
-    | error "no doc-gen4 executable configuration found in workspace"
-  let exeJob ← docGen4.exe.fetch
-
-  -- XXX: Workaround remove later
-  let coreJob ← if docGen4Pkg.name = _package.name then
-    let job := fetch <| docGen4Pkg.target `coreDocs
-    job
-  else
-    error "wrong package"
-
   let mods ← lib.modules.fetch
   let moduleJobs ← BuildJob.mixArray <| ← mods.mapM (fetch <| ·.facet `docs)
+  let coreJob : BuildJob FilePath ← coreDocs.fetch
+  let exeJob ← «doc-gen4».fetch
   -- Shared with DocGen4.Output
   let basePath := (←getWorkspace).root.buildDir / "doc"
   let dataFile := basePath / "declarations" / "declaration-data.bmp"
diff --git a/lean-toolchain b/lean-toolchain
index efc56ff..e183d2c 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2023-07-29
+leanprover/lean4:nightly-2023-07-30