diff --git a/.gitignore b/.gitignore
index 8560c43..3ec510d 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,3 +1,3 @@
/build
-/lean_packages
+/lean_packages/*
!/lean_packages/manifest.json
diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean
index 0b93e63..2a596ed 100644
--- a/DocGen4/Output.lean
+++ b/DocGen4/Output.lean
@@ -126,12 +126,13 @@ def htmlOutputIndex (baseConfig : SiteBaseContext) : IO Unit := do
let mut allDecls : List (String × Json) := []
let mut allInstances : HashMap String (Array String) := .empty
let mut importedBy : HashMap String (Array String) := .empty
+ let mut allModules : List (String × Json) := []
for entry in ←System.FilePath.readDir declarationsBasePath do
if entry.fileName.startsWith "declaration-data-" && entry.fileName.endsWith ".bmp" then
- IO.println s!"Processing: {entry.fileName}"
let fileContent ← FS.readFile entry.path
let .ok jsonContent := Json.parse fileContent | unreachable!
let .ok (module : JsonModule) := fromJson? jsonContent | unreachable!
+ allModules := (module.name, Json.str <| moduleNameToLink module.name |>.run baseConfig) :: allModules
allDecls := (module.declarations.map (λ d => (d.name, toJson d))) ++ allDecls
for inst in module.instances do
let mut insts := allInstances.findD inst.className #[]
@@ -147,7 +148,8 @@ def htmlOutputIndex (baseConfig : SiteBaseContext) : IO Unit := do
let finalJson := Json.mkObj [
("declarations", Json.mkObj allDecls),
("instances", Json.mkObj postProcessInstances),
- ("importedBy", Json.mkObj postProcessImportedBy)
+ ("importedBy", Json.mkObj postProcessImportedBy),
+ ("modules", Json.mkObj allModules)
]
-- The root JSON for find
FS.writeFile (declarationsBasePath / "declaration-data.bmp") finalJson.compress
diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean
index 9f274e6..4aa50ee 100644
--- a/DocGen4/Output/Module.lean
+++ b/DocGen4/Output/Module.lean
@@ -195,7 +195,7 @@ def internalNav (members : Array Name) (moduleName : Name) : HtmlM Html := do
Imported by
-
+
[members.map declarationToNavLink]
diff --git a/DocGen4/Output/Template.lean b/DocGen4/Output/Template.lean
index e569983..ae7878b 100644
--- a/DocGen4/Output/Template.lean
+++ b/DocGen4/Output/Template.lean
@@ -15,6 +15,11 @@ open scoped DocGen4.Jsx
The HTML template used for all pages.
-/
def baseHtmlGenerator (title : String) (site : Array Html) : BaseHtmlM Html := do
+ let moduleConstant :=
+ if let some module := (←getCurrentName) then
+ #[]
+ else
+ #[]
pure
@@ -26,6 +31,7 @@ def baseHtmlGenerator (title : String) (site : Array Html) : BaseHtmlM Html := d
+ [moduleConstant]
diff --git a/lean_packages/manifest.json b/lean_packages/manifest.json
new file mode 100644
index 0000000..a039515
--- /dev/null
+++ b/lean_packages/manifest.json
@@ -0,0 +1,20 @@
+{"version": 1,
+ "packages":
+ [{"url": "https://github.com/mhuisi/lean4-cli",
+ "rev": "112b35fc348a4a18d2111ac2c6586163330b4941",
+ "name": "Cli"},
+ {"url": "https://github.com/hargonix/LeanInk",
+ "rev": "cb529041f71a4ea8348628a8c723326e3e4bdecc",
+ "name": "leanInk"},
+ {"url": "https://github.com/xubaiw/Unicode.lean",
+ "rev": "1fb004da96aa1d1e98535951e100439a60f5b7f0",
+ "name": "Unicode"},
+ {"url": "https://github.com/leanprover-community/mathlib4.git",
+ "rev": "ecd37441047e490ff2ad339e16f45bb8b58591bd",
+ "name": "mathlib"},
+ {"url": "https://github.com/leanprover/lake",
+ "rev": "a7bc6addee9fc07c0ee43d0dcb537faa41844217",
+ "name": "lake"},
+ {"url": "https://github.com/xubaiw/CMark.lean",
+ "rev": "8f17d13d3046c517f7f02062918d81bc69e45cce",
+ "name": "CMark"}]}
\ No newline at end of file
diff --git a/static/declaration-data.js b/static/declaration-data.js
index 1b3167e..a12d4f1 100644
--- a/static/declaration-data.js
+++ b/static/declaration-data.js
@@ -99,6 +99,22 @@ export class DeclarationDataCenter {
declNameToLink(declName) {
return this.declarationData.declarations[declName].docLink;
}
+
+ /**
+ * Find all modules that imported the given one.
+ * @returns {Array}
+ */
+ moduleImportedBy(moduleName) {
+ return this.declarationData.importedBy[moduleName];
+ }
+
+ /**
+ * Analogous to Lean moduleNameToLink
+ * @returns {String}
+ */
+ moduleNameToLink(moduleName) {
+ return this.declarationData.modules[moduleName];
+ }
}
function isSeparater(char) {
diff --git a/static/importedBy.js b/static/importedBy.js
new file mode 100644
index 0000000..dab932d
--- /dev/null
+++ b/static/importedBy.js
@@ -0,0 +1,19 @@
+import { DeclarationDataCenter } from "./declaration-data.js";
+
+fillImportedBy();
+
+async function fillImportedBy() {
+ if (!MODULE_NAME) {
+ return;
+ }
+ const dataCenter = await DeclarationDataCenter.init();
+ const moduleName = MODULE_NAME;
+ const importedByList = document.querySelector(".imported-by-list");
+ const importedBy = dataCenter.moduleImportedBy(moduleName);
+ var innerHTML = "";
+ for(var module of importedBy) {
+ const moduleLink = dataCenter.moduleNameToLink(module);
+ innerHTML += `${module}`
+ }
+ importedByList.innerHTML = innerHTML;
+}
diff --git a/static/instances.js b/static/instances.js
index 983311c..cc7d113 100644
--- a/static/instances.js
+++ b/static/instances.js
@@ -11,7 +11,6 @@ async function annotateInstances() {
const instances = dataCenter.instancesForClass(className);
var innerHTML = "";
for(var instance of instances) {
- // TODO: probably fix site root
const instanceLink = dataCenter.declNameToLink(instance);
innerHTML += `${instance}`
}