Add interactive library explorer (#1138)

@JobPetrovcic created an interactive graph for exploring definitions in
the library. This PR embeds the explorer on our website.

Some more work is still required outside of this repository, which is
why this PR is a draft.

Co-authored-by: Job Petrovčič <[email protected]>

CONTRIBUTORS.toml

@@ -242,3 +242,8 @@ github = "UlrikBuchholtz"
 displayName = "Garrett Figueroa"
 usernames = [ "Garrett Figueroa", "djspacewhale" ]
 github = "djspacewhale"
+
+[[contributors]]
+displayName = "Job Petrovčič"
+usernames = [ "Job Petrovčič", "JobPetrovcic" ]
+github = "JobPetrovcic"

Makefile

@@ -50,7 +50,8 @@ METAFILES := \
 	STATEMENT-OF-INCLUSION.md \
 	SUMMARY.md \
 	TEMPLATE.lagda.md \
-	USERS.md
+	USERS.md \
+	VISUALIZATION.md
 
 .PHONY: agdaFiles
 agdaFiles:

VISUALIZATION.md

@@ -0,0 +1,52 @@
+# Interactive explorer of the library
+
+Below is an interactive explorer of modules and definitions in agda-unimath. It
+displays various properties of the nodes in the dependency graph, and also
+allows you to determine dependencies between individual definitions. Hover over
+ⓘ for detailed usage instructions.
+
+<p id="small-display-notice" style="display:none">
+  ⚠ The explorer is not optimized for small screens. It may be
+  difficult to control on mobile devices.
+</p>
+
+<style>
+  .sidetoc { display: none; }
+  @media(max-width:1100px) {
+    #small-display-notice { display: block !important; }
+  }
+</style>
+
+<div align="center">
+  <iframe
+    src="https://jobpetrovcic.github.io/Unimath-Visualization-Deployment/visualize"
+    style="background: white"
+    scrolling="no"
+    width="1000"
+    height="600"
+    referrerpolicy="no-referrer">
+  </iframe>
+</div>
+
+The interactive explorer was developed by Job Petrovčič. In addition, Vojtěch
+Štěpančík, Matej Petković, and Andrej Bauer contributed invaluable suggestions
+and offered helpful support.
+
+### Notes
+
+The explorer is built and deployed outside of the agda-unimath repository, using
+a fork of Agda. For that reason the definitions in the graph may lag behind the
+definitions on the website by a few hours.
+
+The explorer has a few known limitations. Most noticeably it doesn't recognize
+the `open import ... renaming (X to Y) public` pattern of exporting definitions,
+so in particular the
+[`foundation.universe-levels`](foundation.universe-levels.md) module is not
+shown, and references to `UU` in the source code show up as references to
+`Agda.Primitive.Set`. Note that one of the consequences is that two `Prop`s
+appear in the search results --- the first one being `Agda.Primitive.Prop`,
+which is Agda's
+[proof-irrelevant sort](https://agda.readthedocs.io/en/latest/language/prop.html)
+and isn't used anywhere in the library, and the second being agda-unimath's
+[`foundation-core.propositions.Prop`](foundation-core.propositions.md), which is
+the type of homotopy propositions.

book.toml

@@ -42,7 +42,8 @@ suppress_processing = [
   "USERS.md",
   "GRANT-ACKNOWLEDGEMENTS.md",
   "SUMMARY.md",
-  "ART.md"
+  "ART.md",
+  "VISUALIZATION.md"
 ]
 
 [preprocessor.concepts]

scripts/generate_main_index_file.py

@@ -117,8 +117,9 @@ def generate_index(root_path):
   - [Guidelines for mixfix operators](MIXFIX-OPERATORS.md)
   - [Citing sources](CITING-SOURCES.md)
   - [Citing the library](CITE-THIS-LIBRARY.md)
-- [Library contents](SUMMARY.md)
+- [Library explorer](VISUALIZATION.md)
 - [Art](ART.md)
+- [Full list of library contents](SUMMARY.md)
 {literature_index}
 
 # The agda-unimath library

website/js/custom.js

@@ -21,6 +21,7 @@ if (link) {
     'STATEMENT-OF-INCLUSION.md',
     'SUMMARY.md',
     'USERS.md',
+    'VISUALIZATION.md',
     'index.md',
   ];
   if (!fileList.includes(filename)) {