From fc7227ba6c638ce14b0f7b1f12264007adf57cf7 Mon Sep 17 00:00:00 2001
From: palalansouki <palalansouki@gmail.com>
Date: Fri, 9 Aug 2024 09:08:26 +0900
Subject: [PATCH] fix ci

---
 .github/workflows/ci.yml   | 94 +++++++++++++++++++++++++++++++-------
 .github/workflows/docs.yml | 39 ----------------
 lakefile.lean              | 10 ++--
 3 files changed, 84 insertions(+), 59 deletions(-)
 delete mode 100644 .github/workflows/docs.yml

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 7d0fd97..09e9870 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -1,35 +1,97 @@
 name: CI
 
+# https://github.com/FormalizedFormalLogic/Foundation/blob/master/.github/workflows/ci.yml
+
 on:
   push:
     branches:
-      - master
+      - "master"
   pull_request:
+  workflow_dispatch:
+
+permissions:
+  contents: read
+  pages: write
+  id-token: write
 
-# concurrency:
-#   group: ${{ github.workflow }}-${{ github.ref }}
-#   cancel-in-progress: true
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
 
 jobs:
   build:
+    name: Build project
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
       - name: Install elan
         run: |
           curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
           echo "$HOME/.elan/bin" >> $GITHUB_PATH
-      - name: Cache outputs
-        uses: actions/cache@v3
+      - name: Check toolchain version
+        run: |
+          elan --version
+          lake --version
+          lean --version
+      - uses: actions/cache@v4
         with:
-          path: ./.lake
-          key: deps-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
-          restore-keys: |
-            deps-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}
-            deps-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}
-      - name: Build
+          path: .lake
+          key: lake-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}
+          restore-keys: lake-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}
+
+      - name: Fetching cache
+        run: lake -R -Kenv=ci exe cache get
+
+      - name: Build project
+        run: lake -R -Kenv=ci build
+
+      - uses: ts-graphviz/setup-graphviz@v2
+      - name: Generate import graph
         run: |
-          lake exe cache get
-          lake build
+          lake -R -Kenv=ci exe graph
+          dot -Tpng ./import_graph.dot -o import_graph.png
+          dot -Tpdf ./import_graph.dot -o import_graph.pdf
+      - name: Upload import graph
+        uses: actions/upload-artifact@v4
+        if: github.ref == 'refs/heads/master'
+        with:
+          name: import_graph
+          path: |
+            ./import_graph.dot
+            ./import_graph.png
+            ./import_graph.pdf
 
-# reference: https://github.com/iehality/lean4-logic/blob/master/.github/workflows/ci.yml
\ No newline at end of file
+      # Generate document only master branch
+      - name: Generate document
+        if: github.ref == 'refs/heads/master'
+        run: lake -R -Kenv=ci build Logic:docs Arithmetization:docs
+      - name: Upload document
+        uses: actions/upload-artifact@v4
+        if: github.ref == 'refs/heads/master'
+        with:
+          name: docs
+          path: ./.lake/build/doc
+
+  deploy:
+    name: Deploy to GitHub Pages
+    runs-on: ubuntu-latest
+    if: github.ref == 'refs/heads/master'
+    environment:
+      name: github-pages
+      url: ${{ steps.deployment.outputs.page_url }}
+    needs:
+      - build
+    steps:
+      - uses: actions/download-artifact@v4
+        with:
+          name: docs
+          path: ./_site/docs/
+      - uses: actions/download-artifact@v4
+        with:
+          name: import_graph
+          path: ./_site/assets/import_graph/
+      - uses: actions/upload-pages-artifact@v3
+        with:
+          path: ./_site
+      - uses: actions/deploy-pages@v4
+        id: deployment
\ No newline at end of file
diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml
deleted file mode 100644
index 7eeffb7..0000000
--- a/.github/workflows/docs.yml
+++ /dev/null
@@ -1,39 +0,0 @@
-name: docs
-
-on:
-  push:
-    branches:
-      - "master"
-
-jobs:
-  build:
-    runs-on: ubuntu-latest
-    environment:
-      name: github-pages
-      url: ${{ steps.deployment.outputs.page_url }}
-    permissions:
-      pages: write
-      id-token: write
-    steps:
-      - uses: actions/checkout@v3
-      - name: Install elan
-        run: |
-          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
-          echo "$HOME/.elan/bin" >> $GITHUB_PATH
-      - name: Cache outputs
-        uses: actions/cache@v3
-        with:
-          path: ./.lake
-          key: deps-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
-          restore-keys: |
-            deps-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}
-            deps-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}
-      - run: |
-          lake -R -Kenv=dev exe cache get && lake -R -Kenv=dev build && lake -R -Kenv=dev build Logic:docs Arithmetization:docs
-      - name: Upload artifact
-        uses: actions/upload-pages-artifact@v1
-        with:
-          path: ./.lake/build/doc/
-      - name: Deploy to GitHub Pages
-        uses: actions/deploy-pages@v1
-        id: deployment
\ No newline at end of file
diff --git a/lakefile.lean b/lakefile.lean
index 6782d69..e397b3e 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -10,10 +10,12 @@ lean_lib «Arithmetization» {
   -- add any library configuration options here
 }
 
-require logic from git "https://github.com/iehality/lean4-logic" @ "master"
+require logic from git "https://github.com/FormalizedFormalLogic/Foundation" @ "master"
 
 require proofwidgets from git "https://github.com/leanprover-community/ProofWidgets4"@"v0.0.39"
 
-meta if get_config? env = some "dev" then
-require «doc-gen4» from git
-  "https://github.com/leanprover/doc-gen4" @ "main"
+meta if get_config? env = some "ci" then
+require importGraph from git "https://github.com/leanprover-community/import-graph" @ "main"
+
+meta if get_config? env = some "ci" then
+require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"