Skip to content

Commit

Permalink
chore(scripts/mk_all): gracefully run loadWorkspace (#17953)
Browse files Browse the repository at this point in the history
Changes `scripts/mk_all` to run `loadWorkspace` using Lake's `toBaseIO` utility. In addition to being a bit cleaner, this adaption will also be necessary once leanprover/lean4#5684 lands.
  • Loading branch information
tydeu committed Oct 30, 2024
1 parent 926fb9e commit 801cc3e
Showing 1 changed file with 2 additions and 1 deletion.
3 changes: 2 additions & 1 deletion scripts/mk_all.lean
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,8 @@ it includes `Mathlib/Tactic`. -/
def getLeanLibs : IO (Array String) := do
let (elanInstall?, leanInstall?, lakeInstall?) ← findInstall?
let config ← MonadError.runEIO <| mkLoadConfig { elanInstall?, leanInstall?, lakeInstall? }
let ws ← MonadError.runEIO (MainM.runLogIO (loadWorkspace config)).toEIO
let some ws ← loadWorkspace config |>.toBaseIO
| throw <| IO.userError "failed to load Lake workspace"
let package := ws.root
let libs := (package.leanLibs.map (·.name)).map (·.toString)
return if package.name == `mathlib then
Expand Down

0 comments on commit 801cc3e

Please sign in to comment.