bookshelf-doc/DocGen4/Output.lean

140 lines
5.6 KiB
Plaintext
Raw Normal View History

2021-12-12 12:21:53 +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
-/
import Lean
2022-03-06 17:51:06 +00:00
import Lake
2021-12-12 12:21:53 +00:00
import DocGen4.Process
import DocGen4.Output.Base
import DocGen4.Output.Index
import DocGen4.Output.Module
import DocGen4.Output.NotFound
2022-02-13 14:42:15 +00:00
import DocGen4.Output.Find
2022-02-22 20:26:20 +00:00
import DocGen4.Output.Semantic
2021-12-12 12:21:53 +00:00
namespace DocGen4
open Lean Std IO System Output
2021-12-13 12:00:53 +00:00
2022-01-09 15:57:19 +00:00
/-
Three link types from git supported:
- https://github.com/org/repo
- https://github.com/org/repo.git
- git@github.com:org/repo.git
TODO: This function is quite brittle and very github specific, we can
probably do better.
-/
2022-03-06 17:51:06 +00:00
def getGithubBaseUrl (gitUrl : String) : String := Id.run do
let mut url := gitUrl
2022-01-09 15:57:19 +00:00
if url.startsWith "git@" then
url := url.drop 15
url := url.dropRight 4
2022-02-12 14:09:13 +00:00
pure s!"https://github.com/{url}"
2022-01-09 15:57:19 +00:00
else if url.endsWith ".git" then
2022-02-12 14:09:13 +00:00
pure $ url.dropRight 4
2022-01-09 15:57:19 +00:00
else
2022-02-12 14:09:13 +00:00
pure url
2022-01-09 15:57:19 +00:00
2022-03-06 17:51:06 +00:00
def getProjectGithubUrl : IO String := do
let out ← IO.Process.output {cmd := "git", args := #["remote", "get-url", "origin"]}
if out.exitCode != 0 then
throw <| IO.userError <| "git exited with code " ++ toString out.exitCode
pure out.stdout.trimRight
def getProjectCommit : IO String := do
2022-01-09 15:57:19 +00:00
let out ← IO.Process.output {cmd := "git", args := #["rev-parse", "HEAD"]}
if out.exitCode != 0 then
throw <| IO.userError <| "git exited with code " ++ toString out.exitCode
2022-02-12 14:09:13 +00:00
pure out.stdout.trimRight
2022-01-09 15:57:19 +00:00
2022-03-06 17:51:06 +00:00
def sourceLinker (ws : Lake.Workspace) (leanHash : String): IO (Name → Option DeclarationRange → String) := do
-- Compute a map from package names to source URL
let mut gitMap := Std.mkHashMap
let projectBaseUrl := getGithubBaseUrl (←getProjectGithubUrl)
let projectCommit ← getProjectCommit
gitMap := gitMap.insert ws.root.name (projectBaseUrl, projectCommit)
for pkg in ws.packageArray do
for dep in pkg.dependencies do
let value := match dep.src with
| Lake.Source.git url commit => (getGithubBaseUrl url, commit)
-- TODO: What do we do here if linking a source is not possible?
| _ => ("https://example.com", "master")
gitMap := gitMap.insert dep.name value
pure $ λ module range =>
let parts := module.components.map Name.toString
2022-01-09 15:57:19 +00:00
let path := (parts.intersperse "/").foldl (· ++ ·) ""
2022-03-06 17:51:06 +00:00
let root := module.getRoot
let basic := if root == `Lean root == `Init root == `Std then
s!"https://github.com/leanprover/lean4/blob/{leanHash}/src/{path}.lean"
2022-01-09 15:57:19 +00:00
else
2022-03-06 17:51:06 +00:00
match ws.packageForModule? module with
| some pkg =>
let (baseUrl, commit) := gitMap.find! pkg.name
s!"{baseUrl}/blob/{commit}/{path}.lean"
| none => "https://example.com"
2022-01-09 15:57:19 +00:00
match range with
| some range => s!"{basic}#L{range.pos.line}-L{range.endPos.line}"
| none => basic
2022-04-06 23:31:27 +00:00
def htmlOutput (result : AnalyzerResult) (ws : Lake.Workspace) (leanHash: String) : IO Unit := do
let config : SiteContext := { depthToRoot := 0, result := result, currentName := none, sourceLinker := ←sourceLinker ws leanHash}
let basePath := FilePath.mk "." / "build" / "doc"
let indexHtml := ReaderT.run index config
2022-04-07 11:14:01 +00:00
let findHtml := ReaderT.run find { config with depthToRoot := 1 }
let notFoundHtml := ReaderT.run notFound config
2022-02-13 14:42:15 +00:00
FS.createDirAll basePath
FS.createDirAll (basePath / "find")
2022-02-22 20:26:20 +00:00
FS.createDirAll (basePath / "semantic")
2022-02-13 14:42:15 +00:00
2022-02-13 14:03:49 +00:00
let mut declList := #[]
2022-04-06 23:53:06 +00:00
for (_, mod) in result.moduleInfo.toArray do
2022-02-18 04:52:01 +00:00
for decl in filterMapDocInfo mod.members do
2022-02-20 17:12:49 +00:00
let name := decl.getName.toString
2022-04-07 10:44:33 +00:00
let config := { config with depthToRoot := 0 }
2022-02-22 07:01:14 +00:00
let doc := decl.getDocString.getD ""
2022-04-06 23:31:27 +00:00
let root := Id.run <| ReaderT.run (getRoot) config
let link := root ++ s!"../semantic/{decl.getName.hash}.xml#"
2022-02-22 20:26:20 +00:00
let docLink := Id.run <| ReaderT.run (declNameToLink decl.getName) config
let sourceLink := Id.run <| ReaderT.run (getSourceUrl mod.name decl.getDeclarationRange) config
2022-02-22 21:32:37 +00:00
let obj := Json.mkObj [("name", name), ("doc", doc), ("link", link), ("docLink", docLink), ("sourceLink", sourceLink)]
2022-02-13 14:03:49 +00:00
declList := declList.push obj
2022-02-22 20:26:20 +00:00
let xml := toString <| Id.run <| ReaderT.run (semanticXml decl) config
FS.writeFile (basePath / "semantic" / s!"{decl.getName.hash}.xml") xml
2022-02-13 14:03:49 +00:00
let json := Json.arr declList
2022-02-13 14:42:15 +00:00
2022-02-22 20:26:20 +00:00
FS.writeFile (basePath / "semantic" / "docgen4.xml") <| toString <| Id.run <| ReaderT.run schemaXml config
2021-12-12 12:21:53 +00:00
FS.writeFile (basePath / "index.html") indexHtml.toString
2021-12-13 12:00:53 +00:00
FS.writeFile (basePath / "404.html") notFoundHtml.toString
2022-02-22 04:40:14 +00:00
FS.writeFile (basePath / "find" / "index.html") findHtml.toString
FS.writeFile (basePath / "style.css") styleCss
let declarationDataPath := basePath / "declaration-data.bmp"
FS.writeFile declarationDataPath json.compress
FS.writeFile (basePath / "declaration-data.timestamp") <| toString (←declarationDataPath.metadata).modified.sec
FS.writeFile (basePath / "declaration-data.js") declarationDataCenterJs
FS.writeFile (basePath / "nav.js") navJs
2022-02-22 04:40:14 +00:00
FS.writeFile (basePath / "find" / "find.js") findJs
FS.writeFile (basePath / "how-about.js") howAboutJs
2022-02-13 13:25:37 +00:00
FS.writeFile (basePath / "search.js") searchJs
2022-02-17 19:27:00 +00:00
FS.writeFile (basePath / "mathjax-config.js") mathjaxConfigJs
2022-02-20 17:12:49 +00:00
2021-12-17 16:20:44 +00:00
for (module, content) in result.moduleInfo.toArray do
let fileDir := moduleNameToDirectory basePath module
let filePath := moduleNameToFile basePath module
-- path: 'basePath/module/components/till/last.html'
-- The last component is the file name, so we drop it from the depth to root.
let config := { config with depthToRoot := module.components.dropLast.length }
2021-12-13 12:00:53 +00:00
let moduleHtml := ReaderT.run (moduleToHtml content) config
FS.createDirAll $ fileDir
FS.writeFile filePath moduleHtml.toString
2021-12-12 12:21:53 +00:00
end DocGen4