Try add Verso doc to pages; add mechanism to trigger all CI [annotate]

utensil · Oct 28, 2024 · 302149c · 302149c
1 parent e9a5370
commit 302149c
Show file tree

Hide file tree

Showing 6 changed files with 16 additions and 3 deletions.
diff --git a/.allci b/.allci
@@ -0,0 +1,2 @@
+# change the number below to trigger all CI
+1
diff --git a/.github/workflows/aya.yml b/.github/workflows/aya.yml
@@ -6,6 +6,7 @@ on:
     paths:
       - '.github/workflows/aya.yml'
       - 'aya/**'
+      - '.allci'
   # Allows you to run this workflow manually from the Actions tab
   workflow_dispatch:
 

diff --git a/.github/workflows/lean4.yml b/.github/workflows/lean4.yml
@@ -9,7 +9,7 @@ on:
     paths:
       - '.github/workflows/lean4.yml'
       - 'lean4*/**'
-
+      - '.allci'
   # Allows you to run this workflow manually from the Actions tab
   workflow_dispatch:
 
@@ -133,8 +133,13 @@ jobs:
           just annotate DuperXp
           popd
 
+          pushd lean4-verso-xp
+          just doc
+          popd
+
           just pages lean4
           just pages lean4-duper-xp
+          just pages lean4-verso-xp
       # - name: Try mk_all
       #   shell: bash
       #   run: |

diff --git a/.github/workflows/tla.yml b/.github/workflows/tla.yml
@@ -6,6 +6,7 @@ on:
     paths:
       - '.github/workflows/tla.yml'
       - 'tla/**'
+      - '.allci'
   # Allows you to run this workflow manually from the Actions tab
   workflow_dispatch:
 

diff --git a/justfile b/justfile
@@ -53,6 +53,9 @@ up *NAME:
     lake -R build
 
 [no-cd]
-vdoc:
+doc:
     lake -R exe mkVersoDoc
-    open _out/html-multi/index.html
+
+[no-cd]
+vdoc: doc
+    open dist/html-multi/index.html
diff --git a/lean4-verso-xp/Main.lean b/lean4-verso-xp/Main.lean
@@ -7,6 +7,7 @@ def main :=
   manualMain (%doc VersoXp) (config := config)
 where
   config := {
+    destination := "dist",
     extraFiles := [("static", "static")],
     -- extraCss := ["/static/colors.css", "/static/theme.css", "/static/print.css", "/static/fonts/source-serif/source-serif-text.css", "/static/fonts/source-code-pro/source-code-pro.css", "/static/katex/katex.min.css"],
     -- extraJs := ["/static/katex/katex.min.js", "/static/math.js", "/static/print.js"],