r
/
bookshelf-doc
mirror of https://github.com/jrpotter/bookshelf-doc
1
Fork 0
Code Issues Packages Projects Releases Wiki Activity

doc: Load

main
Henrik Böving 2022-05-19 20:45:12 +02:00
parent 5fd076530e
commit c05a9cf5e5
1 changed files with 9 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
DocGen4/Load.lean
View File

@ -13,6 +13,11 @@ namespace DocGen4
open Lean System Std IO open Lean System Std IO
/--
Sets up a lake workspace for the current project. Furthermore initialize
the Lean search path with the path to the proper compiler from lean-toolchain
as well as all the dependencies.
-/
def lakeSetup (imports : List String) : IO (Except UInt32 (Lake.Workspace × String)) := do def lakeSetup (imports : List String) : IO (Except UInt32 (Lake.Workspace × String)) := do
let (leanInstall?, lakeInstall?) ← Lake.findInstall? let (leanInstall?, lakeInstall?) ← Lake.findInstall?
let res ← StateT.run Lake.Cli.loadWorkspace {leanInstall?, lakeInstall?} |>.toIO' let res ← StateT.run Lake.Cli.loadWorkspace {leanInstall?, lakeInstall?} |>.toIO'
@ -28,6 +33,10 @@ def lakeSetup (imports : List String) : IO (Except UInt32 (Lake.Workspace × Str
pure $ Except.ok (ws, lean.githash) pure $ Except.ok (ws, lean.githash)
| Except.error rc => pure $ Except.error rc | Except.error rc => pure $ Except.error rc
/--
Load a list of modules from the current Lean search path into an `Environment`
to process for documentation.
-/
def load (imports : List Name) : IO AnalyzerResult := do def load (imports : List Name) : IO AnalyzerResult := do
let env ← importModules (List.map (Import.mk · false) imports) Options.empty let env ← importModules (List.map (Import.mk · false) imports) Options.empty
-- TODO parameterize maxHeartbeats -- TODO parameterize maxHeartbeats