Speed up CI (#41)

fpvandoorn · Aug 14, 2024 · 0b365f9 · 0b365f9
1 parent 8c1eed7
commit 0b365f9
Show file tree

Hide file tree

Showing 4 changed files with 46 additions and 7 deletions.
diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml
@@ -51,6 +51,8 @@ jobs:
             .lake/build/doc/Std
             .lake/build/doc/Mathlib
             .lake/build/doc/declarations
+            .lake/build/doc/find
+            .lake/build/doc/*.*
             !.lake/build/doc/declarations/declaration-data-BonnAnalysis*
           key: MathlibDoc-${{ hashFiles('lake-manifest.json') }}
           restore-keys: MathlibDoc-
@@ -78,16 +80,19 @@ jobs:
             leanblueprint web
             cp -r blueprint/web docs/blueprint
 
-      - name: Remove lake files from documentation
-        run: |
-          find .lake/build/doc -name "*.trace" -delete
-          find .lake/build/doc -name "*.hash" -delete
+      # - name: Check declarations
+      #   run: ~/.elan/bin/lake exe checkdecls blueprint/lean_decls
 
       - name: Copy documentation to `docs/docs`
         run: |
           sudo chown -R runner docs
           cp -r .lake/build/doc docs/docs
 
+      - name: Remove lake files from documentation in `docs/docs`
+        run: |
+          find docs/docs -name "*.trace" -delete
+          find docs/docs -name "*.hash" -delete
+
       - name: Bundle dependencies
         uses: ruby/setup-ruby@v1
         with:
@@ -113,5 +118,5 @@ jobs:
         id: deployment
         uses: actions/deploy-pages@v4
 
-      - name: Make sure the cache works
-        run: mv docs/docs .lake/build/doc
+      # - name: Make sure the cache works
+      #   run: mv docs/docs .lake/build/doc
diff --git a/.github/workflows/push_pr.yml b/.github/workflows/push_pr.yml
@@ -12,10 +12,31 @@ jobs:
           fetch-depth: 0
 
       - 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
+        run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
 
       - name: Get cache
         run: ~/.elan/bin/lake exe cache get
 
       - name: Build project
         run: ~/.elan/bin/lake build BonnAnalysis
+
+      - name: Build blueprint and copy to `docs/blueprint`
+        uses: xu-cheng/texlive-action@v2
+        with:
+          docker_image: ghcr.io/xu-cheng/texlive-full:20231201
+          run: |
+            export PIP_BREAK_SYSTEM_PACKAGES=1
+            apk update
+            apk add --update make py3-pip git pkgconfig graphviz graphviz-dev gcc musl-dev
+            git config --global --add safe.directory $GITHUB_WORKSPACE
+            git config --global --add safe.directory `pwd`
+            python3 -m venv env
+            source env/bin/activate
+            pip install --upgrade pip requests wheel
+            pip install pygraphviz --global-option=build_ext --global-option="-L/usr/lib/graphviz/" --global-option="-R/usr/lib/graphviz/"
+            pip install leanblueprint
+            leanblueprint pdf
+            leanblueprint web
+
+      # - name: Check declarations
+      #   run: ~/.elan/bin/lake exe checkdecls blueprint/lean_decls
diff --git a/lake-manifest.json b/lake-manifest.json
@@ -71,6 +71,16 @@
    "inputRev": null,
    "inherited": false,
    "configFile": "lakefile.lean"},
+  {"url": "https://github.com/PatrickMassot/checkdecls.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "21a36f3c07a9229e1287483c16a0dd04e479ecc5",
+   "name": "checkdecls",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
   {"url": "https://github.com/acmepjz/md4lean",
    "type": "git",
    "subDir": null,

diff --git a/lakefile.lean b/lakefile.lean
@@ -29,6 +29,9 @@ package «bonnAnalysis» where
 require mathlib from git
   "https://github.com/leanprover-community/mathlib4.git"
 
+require checkdecls from git
+  "https://github.com/PatrickMassot/checkdecls.git" @ "master"
+
 -- This is run only if we're in `dev` mode. This is so not everyone has to build doc-gen
 meta if get_config? env = some "dev" then
 require «doc-gen4» from git