Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add graph legend #1363

Open
wants to merge 5 commits into
base: master
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -431,3 +431,4 @@ CONTRIBUTORS.md
MAINTAINERS.md
/website/css/Agda-highlight.css
/website/images/agda_dependency_graph.svg
/website/images/agda_dependency_graph_legend.html
9 changes: 7 additions & 2 deletions ART.md
Original file line number Diff line number Diff line change
Expand Up @@ -2,8 +2,13 @@

<div align="center" style="margin: 2em 0;">
<figure>
<img src="website/images/agda_dependency_graph.svg" alt="A dependency graph of the library, color coded by field. Fredrik Bakke. 2025 - perpetuity" width="95%" style="border-radius: 10px;">
<figcaption>A dependency graph of the library, color coded by field. Fredrik Bakke. 2025 - perpetuity</figcaption>
<img src="website/images/agda_dependency_graph.svg" alt="A dependency graph of the library, color coded by namespace. Fredrik Bakke. 2025 — perpetuity" width="95%" style="border-radius: 10px;">
<br>
<span>
{{#include website/images/agda_dependency_graph_legend.html}}
</span>
<figcaption>A dependency graph of the library, color coded by namespace. Fredrik Bakke. 2025 — perpetuity</figcaption>

</figure>
</div>

Expand Down
4 changes: 2 additions & 2 deletions HOWTO-INSTALL.md
Original file line number Diff line number Diff line change
Expand Up @@ -21,8 +21,8 @@ In order to contribute to the agda-unimath library you will additionally need:
1. `git`
2. `make`
3. `python` version 3.8 or newer
4. The python libraries `pre-commit`, `pybtex`, `requests`, `tomli`, and
`graphviz`. These can be installed by running
4. The python libraries `pre-commit`, `pybtex`, `requests`, `tomli`,
`setuptools`, and `graphviz`. These can be installed by running
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I know this is a draft, but I'm getting worried what you need setuptools for

Copy link
Collaborator Author

@fredrik-bakke fredrik-bakke Mar 12, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't need it, but make serve-website throws errors when it is not installed (although it seems to work *irrespectively)

```shell
python3 -m pip install -r scripts/requirements.txt
```
Expand Down
6 changes: 5 additions & 1 deletion Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -148,9 +148,13 @@ website/css/Agda-highlight.css: ./scripts/generate_agda_css.py ./theme/catppucci
website/images/agda_dependency_graph.svg: ${AGDAFILES}
@python3 ./scripts/generate_dependency_graph_rendering.py website/images/agda_dependency_graph svg || true

website/images/agda_dependency_graph_legend.html: ${AGDAFILES}
@python3 ./scripts/generate_dependency_graph_rendering.py website/images/agda_dependency_graph svg || true

.PHONY: website-prepare
website-prepare: agda-html ./SUMMARY.md ./CONTRIBUTORS.md ./MAINTAINERS.md \
./website/css/Agda-highlight.css ./website/images/agda_dependency_graph.svg
./website/css/Agda-highlight.css ./website/images/agda_dependency_graph.svg \
./website/images/agda_dependency_graph_legend.html
@cp $(METAFILES) ./docs/
@mkdir -p ./docs/website
@cp -r ./website/images ./docs/website/
Expand Down
1 change: 1 addition & 0 deletions flake.nix
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,7 @@
pybtex
requests
tomli
setuptools
graphviz
]);

Expand Down
25 changes: 25 additions & 0 deletions scripts/generate_dependency_graph_rendering.py
Original file line number Diff line number Diff line change
Expand Up @@ -133,6 +133,20 @@ def build_dependency_graph(root_dir, most_imported_drop_count=20):

return graph, file_sizes

def generate_html_legend(label_colors, used_labels, output_file, label_counts):
"""Generate an HTML legend with used namespaces and their colors."""
sorted_labels = sorted(used_labels, key=lambda label: label_counts.get(label, 0), reverse=True)
with open(output_file, 'w') as f:
f.write('<html>\n<head>\n<style>\n')
f.write('.dot { height: 9px; width: 9px; border-radius: 50%; display: inline-block; margin-right: 2.5px; margin-left: 5px }\n')
f.write('.label { white-space: nowrap; font-family: monospaced; font-size: 50%; display: inline-block; }\n')
f.write('</style>\n</head>\n<body>\n')
for label in sorted_labels:
if label in label_colors:
color = label_colors[label]
f.write(f'<span class="code" class="label" id="{label}"><span class="dot" style="background-color: #{color};"></span>{label}</span>\n')
f.write('</body>\n</html>')

def render_graph(graph, file_sizes, output_file, format, repo):
"""Render the dependency graph using Graphviz."""
# Fetch GitHub labels and colors
Expand All @@ -147,14 +161,25 @@ def render_graph(graph, file_sizes, output_file, format, repo):
node_sizes = {node: max(0.05, 0.3 * math.sqrt(file_sizes.get(node, 0) / max_lines)) for node in graph}
node_colors = {node: module_based_color(node[:node.rfind(".")], label_colors) for node in graph}

used_labels = set()
label_counts = defaultdict(int)

for node, dependencies in graph.items():
node_color = node_colors[node]
label = node[:node.rfind(".")]
used_labels.add(label)
label_counts[label] += 1
dot.node(node, shape="circle", style="filled", fillcolor=node_color, color="#FFFFFF00", width=str(node_sizes[node]), height=str(node_sizes[node]), label="")
for dep in dependencies:
if dep in graph: # Ensure we're not linking to removed nodes
edge_color = node_color + "10"
dot.edge(node, dep, color=edge_color, arrowhead="none")

# Generate HTML legend
html_legend_output_file = output_file + "_legend.html"
generate_html_legend(label_colors, used_labels, html_legend_output_file, label_counts)
eprint(f"HTML Legend saved as {html_legend_output_file}")

dot.render(output_file, format=format, cleanup=True)

if __name__ == "__main__":
Expand Down
1 change: 1 addition & 0 deletions scripts/requirements.txt
Original file line number Diff line number Diff line change
Expand Up @@ -3,4 +3,5 @@ pre-commit
pybtex
requests
tomli
setuptools
graphviz
4 changes: 2 additions & 2 deletions src/synthetic-homotopy-theory/homotopy-groups.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -37,8 +37,8 @@ where
- `π₀ A` is the set of
[connected components](foundation.connected-components.md) of `A`, and
- `πᵢ₊₁ A` is the set `πᵢ ΩA` equipped with the
[group structure](group-theory.groups.md) obtained from the [loop
space](synthetic-homotopy theory.loop-spaces.md).
[group structure](group-theory.groups.md) obtained from the
[loop space](synthetic-homotopy-theory.loop-spaces.md).

For `i ≥ 2`, the `i`-th homotopy group `πᵢ A` of `A` is
[abelian](group-theory.abelian-groups.md) by the
Expand Down
3 changes: 2 additions & 1 deletion theme/css/general.css
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,8 @@ body {
}

pre,
code {
code,
.code {
font-family: var(--mono-font) !important;
font-size: var(--code-font-size) !important;
}
Expand Down
Loading