ci: fix doc

XintaoYu · Nov 30, 2023 · d0d056f · d0d056f
1 parent 4b8c22d
commit d0d056f
Show file tree

Hide file tree

Showing 4 changed files with 46 additions and 12 deletions.
diff --git a/.github/workflows/build.yaml b/.github/workflows/build.yaml
@@ -1,8 +1,6 @@
 name: Build
-
 permissions:
   contents: write
-
 on:
   push:
     branches:

diff --git a/.github/workflows/docs.yaml b/.github/workflows/docs.yaml
@@ -1,16 +1,17 @@
 name: Build docs
-
-permissions:
-  contents: write
-  pages: write
-  id-token: write
-
 on:
   push:
     branches:
       - "master"
 jobs:
   build:
+    permissions:
+      contents: read
+      pages: write
+      id-token: write
+    environment:
+      name: github-pages
+      url: ${{ steps.deployment.outputs.page_url }}
     runs-on: ubuntu-latest
     steps:
       - name: Checkout Project
@@ -23,14 +24,12 @@ jobs:
           curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s - -y --default-toolchain `cat ./lean-toolchain`
           echo "$HOME/.elan/bin" >> $GITHUB_PATH
       - run: |
-          export CI_BUILD=1
-          lake -Kenv=CI_BUILD update && lake -Kenv=CI_BUILD exe cache get && lake -Kenv=CI_BUILD build && lake -Kenv=CI_BUILD build EuclideanGeometry:docs
+          lake -Kenv=CI_BUILD exe cache get && lake -Kenv=CI_BUILD build && lake -Kenv=CI_BUILD build EuclideanGeometry:docs
       - name: Fix permissions
         run: |
           chmod -c -R +rX "./.lake/build/doc/" | while read line; do
             echo "::warning title=Invalid file permissions automatically fixed::$line"
           done
-
       - name: Upload artifact
         uses: actions/upload-pages-artifact@v1
         with:

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -54,6 +54,42 @@
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
    "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/xubaiw/CMark.lean",
+   "type": "git",
+   "subDir": null,
+   "rev": "0077cbbaa92abf855fc1c0413e158ffd8195ec77",
+   "name": "CMark",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/fgdorais/lean4-unicode-basic",
+   "type": "git",
+   "subDir": null,
+   "rev": "280d75fdfe7be8eb337be7f1bf8479b4aac09f71",
+   "name": "UnicodeBasic",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/hargonix/LeanInk",
+   "type": "git",
+   "subDir": null,
+   "rev": "2447df5cc6e48eb965c3c3fba87e46d353b5e9f1",
+   "name": "leanInk",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "doc-gen",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/doc-gen4.git",
+   "type": "git",
+   "subDir": null,
+   "rev": "3cc5df1be7f6db5ac13f26edda3fc258e199ab5f",
+   "name": "«doc-gen4»",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "3cc5df1be7f6db5ac13f26edda3fc258e199ab5f",
+   "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "EG",
  "lakeDir": ".lake"}
diff --git a/lakefile.lean b/lakefile.lean
@@ -14,4 +14,5 @@ require mathlib from git
   "https://github.com/leanprover-community/mathlib4.git"
 
 meta if get_config? env = some "CI_BUILD" then
-require «doc-gen4» from git "https://github.com/leanprover/doc-gen4.git"
+require «doc-gen4» from git
+  "https://github.com/leanprover/doc-gen4.git" @ "3cc5df1be7f6db5ac13f26edda3fc258e199ab5f"