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
|
2021-12-15 08:24:49 +00:00
|
|
|
|
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
|
|
|
|
|
|
2021-12-15 08:24:49 +00:00
|
|
|
|
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}
|
2022-02-19 17:15:43 +00:00
|
|
|
|
let basePath := FilePath.mk "." / "build" / "doc"
|
2022-02-15 11:12:17 +00:00
|
|
|
|
let indexHtml := ReaderT.run index config
|
2022-02-20 17:12:49 +00:00
|
|
|
|
let findHtml := ReaderT.run find config
|
2022-02-15 11:12:17 +00:00
|
|
|
|
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-02-15 11:12:17 +00:00
|
|
|
|
let config := { config with depthToRoot := 2 }
|
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
|
|
|
|
|
|
2022-04-06 23:31:27 +00:00
|
|
|
|
let root := Id.run <| ReaderT.run (getRoot) config
|
|
|
|
|
FS.writeFile (basePath / "site-root.js") (siteRootJs.replace "{siteRoot}" root)
|
2022-02-22 04:40:14 +00:00
|
|
|
|
FS.writeFile (basePath / "declaration-data.js") declarationDataCenterJs
|
2021-12-13 20:36:21 +00:00
|
|
|
|
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
|
2022-02-15 11:12:17 +00:00
|
|
|
|
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
|
2022-02-15 11:12:17 +00:00
|
|
|
|
FS.createDirAll $ fileDir
|
|
|
|
|
FS.writeFile filePath moduleHtml.toString
|
2021-12-12 12:21:53 +00:00
|
|
|
|
|
|
|
|
|
end DocGen4
|
|
|
|
|
|