From 68ee200b1dfc2090b894e303d2f4a67f4e123fd0 Mon Sep 17 00:00:00 2001
From: "Junyoung/\"Clare\" Jang" <jjc9310@gmail.com>
Date: Tue, 1 Oct 2024 14:37:54 -0400
Subject: [PATCH] Update CI to use correct base

---
 .github/workflows/ci_build.yaml    | 5 +----
 scripts/generate_dep.py            | 5 +++--
 theories/CoqMakefile.mk.local-late | 3 ++-
 3 files changed, 6 insertions(+), 7 deletions(-)

diff --git a/.github/workflows/ci_build.yaml b/.github/workflows/ci_build.yaml
index 2e7b93d..03941e4 100644
--- a/.github/workflows/ci_build.yaml
+++ b/.github/workflows/ci_build.yaml
@@ -64,14 +64,11 @@ jobs:
           script: |
             startGroup "Build binary"
               make pretty-timed
-              if [[ "${{ env.DOC_DEPLOY }}" == 'true' ]]; then
-                make coqdoc
-              fi
             endGroup
             startGroup "Build HTMLs for GitHub pages"
               if [[ "${{ env.DOC_DEPLOY }}" == 'true' ]]; then
                 make coqdoc
-                make depgraphdoc
+                DOC_BASE="${{ env.DOC_DEPLOY_DEST }}" make depgraphdoc
                 mv theories/html html
                 mv theories/dep.html html/dep.html
                 cp assets/styling.css html/styling.css
diff --git a/scripts/generate_dep.py b/scripts/generate_dep.py
index 163bf14..56fc515 100644
--- a/scripts/generate_dep.py
+++ b/scripts/generate_dep.py
@@ -1,4 +1,4 @@
-import itertools, re, sys, textwrap
+import itertools, os, re, sys, textwrap
 from pathlib import Path
 from typing import Iterable
 
@@ -20,6 +20,7 @@
 
 GRAPH_SET: set[str] = set()
 RANKED_GRAPH_SET: set[str] = set()
+DOC_BASE = os.environ["DOC_BASE"] if "DOC_BASE" in os.environ else ""
 
 def under_subgraph(name: str, body: str) -> str:
     return f"""subgraph "{name}" {{ {body} }}"""
@@ -93,7 +94,7 @@ def gen_graph() -> str:
     return textwrap.dedent(f"""
       digraph Mcltt {{
         graph [center=true,class="depgraph",cluster=true,fontname="Open Sans",fontsize=28,label="Mcltt",labeljust=l,labelloc=t,penwidth=2,size=15,splines=true,tooltip=""];
-        node [fontsize=18,shape=note,style=filled,URL="https://beluga-lang.github.io/McLTT/\\N.html"];
+        node [fontsize=18,shape=note,style=filled,URL="https://beluga-lang.github.io/McLTT/{DOC_BASE}/\\N.html"];
         {default_subgraph_decl("Algorithmic")}
         {default_subgraph_decl("Core")}
         {core_subgraph_decl("Completeness")}
diff --git a/theories/CoqMakefile.mk.local-late b/theories/CoqMakefile.mk.local-late
index fccd5e8..2d8af51 100644
--- a/theories/CoqMakefile.mk.local-late
+++ b/theories/CoqMakefile.mk.local-late
@@ -21,6 +21,7 @@ COQDOCFLAGS := \
   --index indexpage --no-lib-name --parse-comments \
   --with-header $(EXTRA_DIR)/header.html --with-footer $(EXTRA_DIR)/footer.html
 export COQDOCFLAGS
+DOC_BASE ?= ""
 
 post-all:: $(COQPARSERFILE) $(PARSERMESSAGEEXTRACTIONFILE) check_parserMessages
 	@echo "Separate Extraction main." | $(COQTOP) $(COQFLAGS) $(COQLIBS) -topfile Entrypoint.v -l Entrypoint.v
@@ -56,7 +57,7 @@ $(DEPGRAPHDOT): $(VFILES) $(DEPGRAPHSCRIPT)
 	@coqdep $(VFILES) -f _CoqProject | python3 "$(DEPGRAPHSCRIPT)" | tred > "$@"
 
 $(DEPGRAPHDOC): $(DEPGRAPHDOT) $(DEPPOSTPROCESSSCRIPT)
-	@dot -T svg "$(DEPGRAPHDOT)" | python3 "$(DEPPOSTPROCESSSCRIPT)" > "$(DEPGRAPHDOC)"
+	@DOC_BASE=$(DOC_BASE) dot -T svg "$(DEPGRAPHDOT)" | python3 "$(DEPPOSTPROCESSSCRIPT)" > "$(DEPGRAPHDOC)"
 
 .PHONY: depgraphdoc
 depgraphdoc: $(DEPGRAPHDOC)