bookshelf-doc/DocGen4/Load.lean

48 lines
1.7 KiB
Plaintext
Raw Normal View History

2021-12-10 12:29:04 +00:00
/-
Copyright (c) 2021 Henrik Böving. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving
-/
2021-11-27 15:19:56 +00:00
import Lean
2022-03-06 17:51:06 +00:00
import Lake
2022-05-21 10:50:55 +00:00
import Lake.CLI.Main
2021-11-27 15:19:56 +00:00
import DocGen4.Process
import Std.Data.HashMap
2021-11-27 15:19:56 +00:00
namespace DocGen4
open Lean System Std IO
2021-11-27 15:19:56 +00:00
2022-05-19 18:45:12 +00:00
/--
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.
-/
2022-03-06 17:51:06 +00:00
def lakeSetup (imports : List String) : IO (Except UInt32 (Lake.Workspace × String)) := do
let (leanInstall?, lakeInstall?) ← Lake.findInstall?
let res ← StateT.run Lake.Cli.loadWorkspace {leanInstall?, lakeInstall?} |>.toIO'
match res with
| Except.ok (ws, options) =>
let lean := leanInstall?.get!
if lean.githash ≠ Lean.githash then
IO.println s!"WARNING: This doc-gen was built with Lean: {Lean.githash} but the project is running on: {lean.githash}"
let lake := lakeInstall?.get!
let ctx ← Lake.mkBuildContext ws lean lake
ws.root.buildImportsAndDeps imports |>.run Lake.LogMethods.eio ctx
initSearchPath (←findSysroot) ws.leanPaths.oleanPath
pure $ Except.ok (ws, lean.githash)
| Except.error rc => pure $ Except.error rc
2021-11-27 15:19:56 +00:00
2022-05-19 18:45:12 +00:00
/--
Load a list of modules from the current Lean search path into an `Environment`
to process for documentation.
-/
def load (imports : List Name) : IO Process.AnalyzerResult := do
2021-11-27 15:19:56 +00:00
let env ← importModules (List.map (Import.mk · false) imports) Options.empty
-- TODO parameterize maxHeartbeats
2021-12-15 11:02:05 +00:00
IO.println "Processing modules"
Prod.fst <$> Meta.MetaM.toIO Process.process { maxHeartbeats := 100000000, options := ⟨[(`pp.tagAppFns, true)]⟩ } { env := env} {} {}
2021-11-27 15:19:56 +00:00
end DocGen4