Fix shared annotation issues [annotate]

utensil · Oct 23, 2024 · fa7c66b · fa7c66b
1 parent bd3510c
commit fa7c66b
Show file tree

Hide file tree

Showing 12 changed files with 1,663 additions and 16 deletions.
diff --git a/.github/workflows/lean4.yml b/.github/workflows/lean4.yml
@@ -82,11 +82,13 @@ jobs:
           steps.annotate.outputs.annotate == 'true'
         run: |
           cd lean4
-          ./install_deps.sh
-          ./annotate_all.sh
+          just annotate Playground
+          cd lean4-duper-xp
+          just annotate DuperXp
           # lake env leanInk analyze examples/Help.lean
           cd ..
           just pages lean4
+          just pages lean4-duper-xp
       # - name: Try mk_all
       #   shell: bash
       #   run: |

diff --git a/.gitignore b/.gitignore
@@ -6,7 +6,7 @@ lean4/.ipynb_checkpoints
 tla/bin/
 tla/*.old
 tla/*.cfg
-aya/dist/
+**/dist/
 tla/*.aux
 tla/*.dvi
 tla/*.log

diff --git a/justfile b/justfile
@@ -18,12 +18,19 @@ default:
 @check-pages:
     #!/usr/bin/env bash
     missing_dirs=()
-    for dir in aya lean4; do
+    for dir in aya lean4 tla; do
         if [ ! -d "github-pages/$dir" ]; then
             missing_dirs+=("$dir")
         fi
     done
     if [ ${#missing_dirs[@]} -ne 0 ]; then
         echo "Missing directories: ${missing_dirs[*]}"
         exit 1
-    fi
+    fi
+
+[no-cd]
+@annotate LIB_DIR:
+    #!/usr/bin/env bash
+    ../lean4-xp-kit/install_deps.sh
+    ../lean4-xp-kit/annotate_all.sh {{LIB_DIR}}
+