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
|
2022-10-05 10:05:58 +00:00
|
|
|
|
import Lean.Data.HashMap
|
2021-11-27 15:19:56 +00:00
|
|
|
|
|
|
|
|
|
namespace DocGen4
|
|
|
|
|
|
2022-10-05 10:05:58 +00:00
|
|
|
|
open Lean System 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-08-11 19:37:10 +00:00
|
|
|
|
def lakeSetup : IO (Except UInt32 Lake.Workspace) := do
|
2022-03-06 17:51:06 +00:00
|
|
|
|
let (leanInstall?, lakeInstall?) ← Lake.findInstall?
|
2022-07-23 11:01:25 +00:00
|
|
|
|
match ←(EIO.toIO' <| Lake.mkLoadConfig {leanInstall?, lakeInstall?}) with
|
2022-07-20 14:18:57 +00:00
|
|
|
|
| .ok config =>
|
2022-08-11 16:30:28 +00:00
|
|
|
|
let ws : Lake.Workspace ← Lake.loadWorkspace config
|
|
|
|
|
|>.run Lake.MonadLog.eio
|
|
|
|
|
|>.toIO (λ _ => IO.userError "Failed to load Lake workspace")
|
2022-07-23 11:01:25 +00:00
|
|
|
|
pure <| Except.ok ws
|
2022-07-20 14:18:57 +00:00
|
|
|
|
| .error err =>
|
2022-07-23 11:01:25 +00:00
|
|
|
|
throw <| IO.userError err.toString
|
2021-11-27 15:19:56 +00:00
|
|
|
|
|
2022-07-21 16:26:01 +00:00
|
|
|
|
def envOfImports (imports : List Name) : IO Environment := do
|
|
|
|
|
importModules (imports.map (Import.mk · false)) Options.empty
|
|
|
|
|
|
|
|
|
|
def loadInit (imports : List Name) : IO Hierarchy := do
|
|
|
|
|
let env ← envOfImports imports
|
2022-07-23 11:01:25 +00:00
|
|
|
|
pure <| Hierarchy.fromArray env.header.moduleNames
|
2022-07-21 16:26:01 +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.
|
|
|
|
|
-/
|
2022-07-21 16:26:01 +00:00
|
|
|
|
def load (task : Process.AnalyzeTask) : IO (Process.AnalyzerResult × Hierarchy) := do
|
|
|
|
|
let env ← envOfImports task.getLoad
|
2021-12-15 11:02:05 +00:00
|
|
|
|
IO.println "Processing modules"
|
2022-06-19 14:41:59 +00:00
|
|
|
|
let config := {
|
|
|
|
|
-- TODO: parameterize maxHeartbeats
|
|
|
|
|
maxHeartbeats := 100000000,
|
|
|
|
|
options := ⟨[(`pp.tagAppFns, true)]⟩,
|
|
|
|
|
-- TODO: Figure out whether this could cause some bugs
|
|
|
|
|
fileName := default,
|
|
|
|
|
fileMap := default,
|
|
|
|
|
}
|
2022-07-21 16:26:01 +00:00
|
|
|
|
|
|
|
|
|
Prod.fst <$> Meta.MetaM.toIO (Process.process task) config { env := env } {} {}
|
2021-11-27 15:19:56 +00:00
|
|
|
|
|
2022-08-11 19:37:10 +00:00
|
|
|
|
def loadCore : IO (Process.AnalyzerResult × Hierarchy) := do
|
2022-10-05 10:05:58 +00:00
|
|
|
|
load <| .loadAll [`Init, `Lean]
|
2022-08-11 19:37:10 +00:00
|
|
|
|
|
2021-11-27 15:19:56 +00:00
|
|
|
|
end DocGen4
|