File dependencies

Author: YaelDillies

.github/workflows/push_master.yml

@@ -36,6 +36,11 @@ jobs:
       - name: Copy README.md to website/index.md
         run: cp README.md website/index.md
 
+      - name: Upstreaming dashboard
+        run: |
+          mkdir -p website/_includes
+          python3 scripts/upstreaming_dashboard.py
+
       - name: Install elan
         run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:4.0.0
 
@@ -45,11 +50,11 @@ jobs:
       - name: Build project
         run: ~/.elan/bin/lake build LeanCamCombi
 
-      - name: Print files to upstream
+      - name: File dependencies
         run: |
-          mkdir -p website/_includes
-          python3 scripts/upstreaming_dashboard.py
-          python3 scripts/import_graph.py
+          sudo apt-get update
+          sudo apt install graphviz -y
+          lake exe graph website/file_deps.pdf
 
       - name: Cache dependencies docs
         uses: actions/cache@v3

scripts/import_graph.py

@@ -35,7 +35,7 @@ <h2 class="project-tagline">{{ page.description | default: site.description | de
     <!-- <a href="blueprint" class="btn">Blueprint</a> -->
     <a href="docs" class="btn">Documentation</a>
     <a href="upstreaming" class="btn">Upstreaming dashboard</a>
-    <a href="import-graph" class="btn">Import Graph</a>
+    <a href="file_deps.pdf" class="btn">File dependencies</a>
     {% if site.github.is_project_page %}
     <a href="{{ site.github.repository_url }}" class="btn">View on GitHub</a>
     {% endif %}