diff --git a/DocGen4.lean b/DocGen4.lean
index 2b8c14f..bc6d9b6 100644
--- a/DocGen4.lean
+++ b/DocGen4.lean
@@ -3,7 +3,9 @@ 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 DocGen4.Hierarchy
import DocGen4.Process
import DocGen4.Load
import DocGen4.ToHtmlFormat
+import DocGen4.IncludeStr
+import DocGen4.Output
diff --git a/DocGen4/Load.lean b/DocGen4/Load.lean
index 7d04c64..0767545 100644
--- a/DocGen4/Load.lean
+++ b/DocGen4/Load.lean
@@ -42,15 +42,10 @@ def lakeSetupSearchPath (lakePath : System.FilePath) (imports : Array String) :
| 2 => pure [] -- no lakefile.lean
| _ => throw $ userError s!"`{cmdStr}` failed:\n{stdout}\nstderr:\n{stderr}"
-def load (imports : List Name) : IO (HashMap Name Module) := do
+def load (imports : List Name) : IO AnalyzerResult := do
let env ← importModules (List.map (Import.mk · false) imports) Options.empty
-- TODO parameterize maxHeartbeats
- let doc ← Prod.fst <$> (Meta.MetaM.toIO process { maxHeartbeats := 100000000} { env := env} {} {})
- for (_, module) in doc.toList do
- let s ← Core.CoreM.toIO module.prettyPrint {} { env := env }
- IO.println s.fst
- IO.println s!"Processed {List.foldl (λ a (_, b) => a + b.members.size) 0 doc.toList} declarations"
- IO.println s!"Processed {doc.size} modules"
- return doc
+ let res ← Prod.fst <$> (Meta.MetaM.toIO process { maxHeartbeats := 100000000} { env := env} {} {})
+ return res
end DocGen4
diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean
new file mode 100644
index 0000000..9c1f124
--- /dev/null
+++ b/DocGen4/Output.lean
@@ -0,0 +1,130 @@
+/-
+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
+import Std.Data.HashMap
+import DocGen4.Process
+import DocGen4.ToHtmlFormat
+import DocGen4.IncludeStr
+
+namespace DocGen4
+
+open Lean Std
+open scoped DocGen4.Jsx
+
+structure SiteContext where
+ root : String
+ result : AnalyzerResult
+
+abbrev HtmlM := Reader SiteContext
+
+def getRoot : HtmlM String := do (←read).root
+def getResult : HtmlM AnalyzerResult := do (←read).result
+
+def templateExtends {α β : Type} (base : α → HtmlM β) (new : HtmlM α) : HtmlM β :=
+ new >>= base
+
+def nameToPath (n : Name) : String := do
+ let parts := n.components.map Name.toString
+ return (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html"
+
+partial def moduleListAux (h : Hierarchy) : HtmlM Html := do
+ if h.getChildren.toList.length == 0 then
+
+ else
+ let children := Array.mk (h.getChildren.toList.map Prod.snd)
+ -- TODO: Is having no children really the correct criterium for a clickable module?
+ let (dirs, files) := children.partition (λ c => c.getChildren.toList.length != 0)
+ let nodes := (←(dirs.mapM moduleListAux)) ++ (←(files.mapM moduleListAux))
+ return
+ {h.getName.toString}
+ [nodes]
+
+
+def moduleList : HtmlM (Array Html) := do
+ let hierarchy := (←getResult).hierarchy
+ let mut list := Array.empty
+ for (n, cs) in hierarchy.getChildren do
+ list := list.push {n.toString}
+ list := list.push $ ←moduleListAux cs
+ list
+
+def navbar : HtmlM Html := do
+
+ General documentation
+
+ /-
+ TODO: Add these in later
+
+
+
+
+
+
+ -/
+ Library
+ [←moduleList]
+
+
+def baseHtml (title : String) (site : Html) : HtmlM Html := do
+
+
+ {title}
+
+ {title}
+ -- TODO: Replace this form with our own search
+
+
+
+
+ Welcome to the documentation page
+ What is up?
+
+
+open IO System
+
+def styleCss : String := include_str "./static/style.css"
+
+def htmlOutput (result : AnalyzerResult) : IO Unit := do
+ -- TODO: parameterize this
+ let config := { root := "/", result := result }
+ let basePath := FilePath.mk "./build/doc/"
+ let indexHtml := ReaderT.run index config
+ FS.createDirAll basePath
+ FS.writeFile (basePath / "index.html") indexHtml.toString
+ FS.writeFile (basePath / "style.css") styleCss
+
+end DocGen4
+
diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean
index 89b7313..950beac 100644
--- a/DocGen4/Process.lean
+++ b/DocGen4/Process.lean
@@ -9,6 +9,8 @@ import Lean.PrettyPrinter
import Std.Data.HashMap
import Lean.Meta.SynthInstance
+import DocGen4.Hierarchy
+
namespace DocGen4
open Lean Meta PrettyPrinter Std
@@ -221,7 +223,6 @@ def ofConstant : (Name × ConstantInfo) → MetaM (Option DocInfo) := λ (name,
some $ instanceInfo info
else
some $ definitionInfo info
- -- TODO: Differentiate between all the different types of inductives (structures, classes etc.)
| ConstantInfo.inductInfo i =>
let env ← getEnv
if isStructure env i.name then
@@ -265,7 +266,12 @@ def prettyPrint (m : Module) : CoreM String := do
end Module
-def process : MetaM (HashMap Name Module) := do
+structure AnalyzerResult where
+ modules : HashMap Name Module
+ hierarchy : Hierarchy
+ deriving Inhabited
+
+def process : MetaM AnalyzerResult := do
let env ← getEnv
let mut res := mkHashMap env.header.moduleNames.size
for module in env.header.moduleNames do
@@ -289,6 +295,6 @@ def process : MetaM (HashMap Name Module) := do
res := res.insert moduleName {module with members := module.members.push dinfo}
| none => panic! "impossible"
| none => ()
- return res
+ return { modules := res, hierarchy := Hierarchy.fromArray env.header.moduleNames }
end DocGen4
diff --git a/Main.lean b/Main.lean
index a4bab64..cdae0ee 100644
--- a/Main.lean
+++ b/Main.lean
@@ -8,4 +8,4 @@ def main (args : List String) : IO Unit := do
let path ← lakeSetupSearchPath (←getLakePath) modules.toArray
IO.println s!"Loading modules from: {path}"
let doc ← load $ modules.map Name.mkSimple
- return ()
+ htmlOutput doc
diff --git a/static/style.css b/static/style.css
new file mode 100644
index 0000000..5743e2f
--- /dev/null
+++ b/static/style.css
@@ -0,0 +1,562 @@
+@import url('https://fonts.googleapis.com/css2?family=Merriweather&family=Open+Sans&family=Source+Code+Pro&family=Source+Code+Pro:wght@600&display=swap');
+
+* {
+ box-sizing: border-box;
+}
+
+body {
+ font-family: 'Open Sans', sans-serif;
+}
+h1, h2, h3, h4, h5, h6 {
+ font-family: 'Merriweather', serif;
+}
+
+body { line-height: 1.5; }
+nav { line-height: normal; }
+
+:root {
+ --header-height: 3em;
+ --header-bg: #f8f8f8;
+ --fragment-offset: calc(var(--header-height) + 1em);
+ --content-width: 55vw;
+}
+@supports (width: min(10px, 5vw)) {
+ :root {
+ --content-width: clamp(20em, 55vw, 60em);
+ }
+}
+
+#nav_toggle {
+ display: none;
+}
+label[for="nav_toggle"] {
+ display: none;
+}
+
+header {
+ height: var(--header-height);
+ float: left;
+ position: fixed;
+ width: 100vw;
+ max-width: 100%;
+ left: 0;
+ right: 0;
+ top: 0;
+ --header-side-padding: 2em;
+ padding: 0 var(--header-side-padding);
+ background: var(--header-bg);
+ z-index: 1;
+ display: flex;
+ align-items: center;
+ justify-content: space-between;
+}
+@supports (width: min(10px, 5vw)) {
+ header {
+ --header-side-padding: calc(max(2em, (100vw - var(--content-width) - 30em) / 2));
+ }
+}
+@media screen and (max-width: 1000px) {
+ :root {
+ --content-width: 100vw;
+ }
+
+ .internal_nav {
+ display: none;
+ }
+
+ body .nav {
+ width: 100vw;
+ max-width: 100vw;
+ margin-left: 1em;
+ z-index: 1;
+ }
+
+ body main {
+ width: unset;
+ max-width: unset;
+ margin-left: unset;
+ margin-right: unset;
+ }
+ body .decl > div {
+ overflow-x: unset;
+ }
+
+ #nav_toggle:not(:checked) ~ .nav {
+ display: none;
+ }
+ #nav_toggle:checked ~ main {
+ visibility: hidden;
+ }
+
+ label[for="nav_toggle"]::before {
+ content: '≡';
+ }
+ label[for="nav_toggle"] {
+ display: inline-block;
+ margin-right: 1em;
+ border: 1px solid #ccc;
+ padding: 0.5ex 1ex;
+ cursor: pointer;
+ background: #eee;
+ }
+ #nav_toggle:checked ~ * label[for="nav_toggle"] {
+ background: white;
+ }
+
+ body header h1 {
+ font-size: 100%;
+ }
+
+ header {
+ --header-side-padding: 1ex;
+ }
+}
+@media screen and (max-width: 700px) {
+ header h1 span { display: none; }
+ :root { --header-side-padding: 1ex; }
+ #search_form button { display: none; }
+ #search_form input { width: 100%; }
+ header #search_results {
+ left: 1ex;
+ right: 1ex;
+ width: inherit;
+ }
+ body header > * { margin: 0; }
+}
+
+header > * {
+ display: inline-block;
+ padding: 0;
+ margin: 0 1em;
+ vertical-align: middle;
+}
+
+header h1 {
+ font-weight: normal;
+ font-size: 160%;
+}
+
+header header_filename {
+ font-size: 150%;
+}
+@media (max-width: 80em) {
+ .header .header_filename {
+ display: none;
+ }
+}
+
+/* inserted by nav.js */
+#search_results {
+ position: absolute;
+ top: var(--header-height);
+ right: calc(var(--header-side-padding));
+ width: calc(20em + 4em);
+ z-index: 1;
+ background: var(--header-bg);
+ border: 1px solid #aaa;
+ border-top: none;
+ overflow-x: hidden;
+ overflow-y: auto;
+ max-height: calc(100vh - var(--header-height));
+}
+
+#search_results:empty {
+ display: none;
+}
+
+#search_results[state="loading"]:empty {
+ display: block;
+ cursor: progress;
+}
+#search_results[state="loading"]:empty::before {
+ display: block;
+ content: ' 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 ';
+ padding: 1ex;
+ animation: marquee 10s linear infinite;
+}
+@keyframes marquee {
+ 0% { transform: translate(100%, 0); }
+ 100% { transform: translate(-100%, 0); }
+}
+
+#search_results[state="done"]:empty {
+ display: block;
+ text-align: center;
+ padding: 1ex;
+}
+#search_results[state="done"]:empty::before {
+ content: '(no results)';
+ font-style: italic;
+}
+
+#search_results a {
+ display: block;
+ color: inherit;
+ padding: 1ex;
+ border-left: 0.5ex solid transparent;
+ padding-left: 0.5ex;
+ cursor: pointer;
+}
+#search_results .selected {
+ background: white;
+ border-color: #f0a202;
+}
+
+main, nav {
+ margin-top: calc(var(--header-height) + 1em);
+}
+
+/* extra space for scrolling things to the top */
+main {
+ margin-bottom: 90vh;
+}
+
+main {
+ max-width: var(--content-width);
+ /* center it: */
+ margin-left: auto;
+ margin-right: auto;
+}
+
+nav {
+ float: left;
+ height: calc(100vh - var(--header-height) - 1em);
+ position: fixed;
+ top: 0;
+ overflow: auto;
+ scrollbar-width: thin;
+ scrollbar-color: transparent transparent;
+}
+
+nav:hover {
+ scrollbar-color: gray transparent;
+}
+
+nav {
+ --column-available-space: calc((100vw - var(--content-width) - 5em)/2);
+ --column-width: calc(var(--column-available-space) - 1ex);
+ --dist-to-edge: 1ex;
+ width: var(--content-width);
+ max-width: var(--column-width);
+}
+@supports (width: min(10px, 5vw)) {
+ .nav { --desired-column-width: 20em; }
+ .internal_nav { --desired-column-width: 30em; }
+ nav {
+ --column-available-space: calc(max(0px, (100vw - var(--content-width) - 5em)/2));
+ --column-width: calc(clamp(0px, var(--column-available-space) - 1ex, var(--desired-column-width)));
+ --dist-to-edge: calc(max(1ex, var(--column-available-space) - var(--column-width)));
+ }
+}
+
+.nav { left: var(--dist-to-edge); }
+.internal_nav { right: var(--dist-to-edge); }
+
+.internal_nav .nav_link, .taclink {
+ /* indent everything but first line by 2ex */
+ text-indent: -2ex; padding-left: 2ex;
+}
+
+.internal_nav .imports {
+ margin-bottom: 1rem;
+}
+
+.tagfilter-div {
+ margin-bottom: 1em;
+}
+.tagfilter-div > summary {
+ margin-bottom: 1ex;
+}
+
+.nav details > * {
+ padding-left: 2ex;
+}
+.nav summary {
+ cursor: pointer;
+ padding-left: 0;
+}
+.nav summary::marker {
+ font-size: 85%;
+}
+
+.nav .nav_file {
+ display: inline-block;
+}
+
+.nav h3 {
+ margin-block-end: 4px;
+}
+
+.nav h4 {
+ margin-bottom: 1ex;
+}
+
+/* People use way too long declaration names. */
+.internal_nav, .decl_name {
+ overflow-wrap: break-word;
+}
+
+.decl > div, .mod_doc {
+ padding-left: 8px;
+ padding-right: 8px;
+}
+
+.decl {
+ margin-top: 20px;
+ margin-bottom: 20px;
+}
+
+.decl > div {
+ /* sometimes declarations arguments are way too long
+ and would continue into the right column,
+ so put a scroll bar there: */
+ overflow-x: auto;
+}
+
+/* Make `#id` links appear below header. */
+.decl, h1[id], h2[id], h3[id], h4[id], h5[id], h6[id] {
+ scroll-margin-top: var(--fragment-offset);
+}
+/* don't need as much vertical space for these
+inline elements */
+a[id], li[id] {
+ scroll-margin-top: var(--header-height);
+}
+
+/* HACK: Safari doesn't support scroll-margin-top for
+fragment links (yet?)
+https://caniuse.com/mdn-css_properties_scroll-margin-top
+https://bugs.webkit.org/show_bug.cgi?id=189265
+*/
+@supports not (scroll-margin-top: var(--fragment-offset)) {
+ .decl::before, h1[id]::before, h2[id]::before, h3[id]::before,
+ h4[id]::before, h5[id]::before, h6[id]::before,
+ a[id]::before, li[id]::before {
+ content: "";
+ display: block;
+ height: var(--fragment-offset);
+ margin-top: calc(-1 * var(--fragment-offset));
+ box-sizing: inherit;
+ visibility: hidden;
+ width: 1px;
+ }
+}
+
+
+/* hide # after markdown headings except on hover */
+.markdown-heading:not(:hover) > .hover-link {
+ visibility: hidden;
+}
+
+main h2, main h3, main h4, main h5, main h6 {
+ margin-top: 2rem;
+}
+.decl + .mod_doc > h2,
+ .decl + .mod_doc > h3,
+ .decl + .mod_doc > h4,
+ .decl + .mod_doc > h5,
+ .decl + .mod_doc > h6 {
+ margin-top: 4rem;
+}
+
+.def {
+ border-left: 10px solid #92dce5;
+ border-top: 2px solid #92dce5;
+}
+
+.theorem {
+ border-left: 10px solid #8fe388;
+ border-top: 2px solid #8fe388;
+}
+
+.axiom, .constant {
+ border-left: 10px solid #f44708;
+ border-top: 2px solid #f44708;
+}
+
+.structure, .inductive {
+ border-left: 10px solid #f0a202;
+ border-top: 2px solid #f0a202;
+}
+
+.fn {
+ display: inline-block;
+ /* border: 1px dashed red; */
+ text-indent: -1ex;
+ padding-left: 1ex;
+ white-space: pre-wrap;
+ vertical-align: top;
+}
+
+.fn { --fn: 1; }
+.fn .fn { --fn: 2; }
+.fn .fn .fn { --fn: 3; }
+.fn .fn .fn .fn { --fn: 4; }
+.fn .fn .fn .fn .fn { --fn: 5; }
+.fn .fn .fn .fn .fn .fn { --fn: 6; }
+.fn .fn .fn .fn .fn .fn .fn { --fn: 7; }
+.fn .fn .fn .fn .fn .fn .fn .fn { --fn: 8; }
+.fn {
+ transition: background-color 100ms ease-in-out;
+}
+
+.def .fn:hover {
+ background-color: hsla(187, 61%, calc(100% - 5%*var(--fn)));
+ box-shadow: 0 0 0 1px hsla(187, 61%, calc(100% - 5%*(var(--fn) + 1)));
+ border-radius: 5px;
+}
+.theorem .fn:hover {
+ background-color: hsla(115, 62%, calc(100% - 5%*var(--fn)));
+ box-shadow: 0 0 0 1px hsla(115, 62%, calc(100% - 5%*(var(--fn) + 1)));
+ border-radius: 5px;
+}
+.axiom .fn:hover, .constant .fn:hover {
+ background-color: hsla(16, 94%, calc(100% - 5%*var(--fn)));
+ box-shadow: 0 0 0 1px hsla(16, 94%, calc(100% - 5%*(var(--fn) + 1)));
+ border-radius: 5px;
+}
+.structure .fn:hover, .inductive .fn:hover {
+ background-color: hsla(40, 98%, calc(100% - 5%*var(--fn)));
+ box-shadow: 0 0 0 1px hsla(40, 98%, calc(100% - 5%*(var(--fn) + 1)));
+ border-radius: 5px;
+}
+
+.decl_args, .decl_type {
+ font-weight: normal;
+}
+
+.implicits, .impl_arg {
+ color: black;
+ white-space: nowrap;
+}
+
+.decl_kind, .decl_name {
+ font-weight: bold;
+}
+
+/* break long declaration names at periods where possible */
+.break_within {
+ word-break: break-all;
+}
+
+.break_within .name {
+ word-break: normal;
+}
+
+.decl_header {
+ /* indent everything but first line twice as much as decl_type */
+ text-indent: -8ex; padding-left: 8ex;
+}
+
+.decl_type {
+ margin-top: 2px;
+ margin-left: 4ex; /* extra indentation */
+}
+
+.imports li, code, .decl_header, .attributes, .structure_field,
+ .constructor, .instances li, .equation, #search_results div {
+ font-family: 'Source Code Pro', monospace;
+}
+
+pre {
+ white-space: break-spaces;
+}
+
+code, pre { background: #f3f3f3; }
+code, pre { border-radius: 5px; }
+code { padding: 1px 3px; }
+pre { padding: 1ex; }
+pre code { padding: 0 0; }
+
+#howabout code { background: inherit; }
+#howabout li { margin-bottom: 0.5ex; }
+
+.structure_fields, .constructors {
+ display: block;
+ padding-inline-start: 0;
+ margin-top: 1ex;
+ text-indent: -2ex; padding-left: 2ex;
+}
+
+.structure_field {
+ display: block;
+}
+.structure_field:before {
+ content: '(';
+ color: gray;
+}
+.structure_field:after {
+ content: ')';
+ color: gray;
+}
+
+.constructor {
+ display: block;
+}
+.constructor:before {
+ content: '| ';
+ color: gray;
+}
+
+/** Don't show underline on types, to prevent the ≤ vs < confusion. **/
+a:link, a:visited, a:active {
+ color:hsl(210, 100%, 30%);
+ text-decoration: none;
+}
+
+/** Show it on hover though. **/
+a:hover {
+ text-decoration: underline;
+}
+
+.impl_arg {
+ font-style: italic;
+ transition: opacity 300ms ease-in;
+}
+
+.decl_header:not(:hover) .impl_arg {
+ opacity: 30%;
+ transition: opacity 1000ms ease-out;
+}
+
+.gh_link {
+ float: right;
+ margin-left: 20px;
+}
+
+.docfile h2, .note h2 {
+ margin-block-start: 3px;
+ margin-block-end: 0px;
+}
+
+.docfile h2 a {
+ color: black;
+}
+
+.tags {
+ margin-bottom: 1ex;
+}
+
+.tags ul {
+ display: inline;
+ padding: 0;
+}
+
+.tags li {
+ border: 1px solid #555;
+ border-radius: 4px;
+ list-style-type: none;
+ padding: 1px 3px;
+ margin-left: 1ex;
+ display: inline-block;
+}
+
+/* used by nav.js */
+.hide { display: none; }
+
+.tactic, .note {
+ border-top: 3px solid #0479c7;
+ padding-top: 2em;
+ margin-top: 2em;
+ margin-bottom: 2em;
+}