chore: do not require docs

.github/workflows/docs.yml

@@ -17,50 +17,23 @@ jobs:
     name: build docs
     runs-on: ubuntu-latest
     steps:
-      - name: clean up
-        run: |
-          rm -rf $HOME/.elan
-          rm -rf $HOME/.cache/mathlib
-
       - uses: actions/checkout@v4
-
-      - name: install elan
-        run: |
-          set -o pipefail
-          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
-          echo "$HOME/.elan/bin" >> $GITHUB_PATH
-
-      - name: set default toolchain
-        run: |
-          elan default $(cat lean-toolchain)
-
-      - name: get cache
-        run: lake exe cache get
-
-      - name: build algorithm
-        run: env LEAN_ABORT_ON_PANIC=1 lake build
-
-      - name: build doc-gen4
-        run: |
-          env DISABLE_EQUATIONS=1 lake build doc-gen4
-
-      - name: build import graph
-        run: |
-          lake exe graph algorithm.html
-
-      - name: generate docs
+      - id: lean-action
+        uses: leanprover/lean-action@v1
+        with:
+          use-github-cache: false
+      - name: Build Doc
         run: |
+          lake exe graph ./docbuild/algorithm.html
+          cd docbuild
           lake build Algorithm:docs
           lake build Algorithm:docsHeader
-
-      - name: copy import graph
-        run: |
-          cp algorithm.html ./.lake/build/doc
-
+      - name: Setup Pages
+        uses: actions/configure-pages@v4
       - name: Upload artifact
         uses: actions/upload-pages-artifact@v3
         with:
-          path: './.lake/build/doc'
+          path: './docbuild/.lake/build/doc'
 
   deploy:
     if: github.ref == 'refs/heads/master'

docbuild/lake-manifest.json

@@ -0,0 +1,142 @@
+{"version": "1.1.0",
+ "packagesDir": "../.lake/packages",
+ "packages":
+ [{"url": "https://github.com/leanprover/doc-gen4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover",
+   "rev": "2679356b3372d52f76d6d984eef16cade7956e0c",
+   "name": "«doc-gen4»",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.26.0-rc2",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"type": "path",
+   "scope": "",
+   "name": "algorithm",
+   "manifestFile": "lake-manifest.json",
+   "inherited": false,
+   "dir": "../",
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "7e1ced9e049a4fab2508980ec4877ca9c46dffc9",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/fgdorais/lean4-unicode-basic",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "106abeac8ee53a047b238976281b0e5017bded8a",
+   "name": "UnicodeBasic",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/dupuisf/BibtexQuery",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "3ab4379b2b92448717de66b7d3e254ac1487aede",
+   "name": "BibtexQuery",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/acmepjz/md4lean",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "38ac5945d744903ffcc473ce1030223991b11cf6",
+   "name": "MD4Lean",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/mathlib4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "d5c9558e75342a10d6321e6a8c798a14f68ae23c",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.26.0-rc2",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/plausible",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "74835c84b38e4070b8240a063c6417c767e551ae",
+   "name": "plausible",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "2ed4ba69b6127de8f5c2af83cccacd3c988b06bf",
+   "name": "LeanSearchClient",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/import-graph",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "6e3bb4bf31f731ab28891fe229eb347ec7d5dad3",
+   "name": "importGraph",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "2aaad968dd10a168b644b6a5afd4b92496af4710",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v0.0.82",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/aesop",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "9c70abdd9215b76019340fad65138e2e8d21843e",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "a31845b5557fd5e47d52b9e2977a1b0eff3c38c3",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/batteries",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "afe9302d9243cee630b0be95322b38b90342ddbf",
+   "name": "batteries",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"}],
+ "name": "docbuild",
+ "lakeDir": ".lake"}

docbuild/lakefile.toml

@@ -0,0 +1,13 @@
+name = "docbuild"
+reservoir = false
+version = "0.1.0"
+packagesDir = "../.lake/packages"
+
+[[require]]
+name = "algorithm"
+path = "../"
+
+[[require]]
+scope = "leanprover"
+name = "doc-gen4"
+rev = "v4.26.0-rc2"

docbuild/lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:v4.26.0-rc2

lake-manifest.json

@@ -1,17 +1,7 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover/doc-gen4",
-   "type": "git",
-   "subDir": null,
-   "scope": "leanprover",
-   "rev": "2679356b3372d52f76d6d984eef16cade7956e0c",
-   "name": "«doc-gen4»",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.26.0-rc2",
-   "inherited": false,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/mathlib4",
+ [{"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
@@ -21,46 +11,6 @@
    "inputRev": "v4.26.0-rc2",
    "inherited": false,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/lean4-cli",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "7e1ced9e049a4fab2508980ec4877ca9c46dffc9",
-   "name": "Cli",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/fgdorais/lean4-unicode-basic",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "106abeac8ee53a047b238976281b0e5017bded8a",
-   "name": "UnicodeBasic",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/dupuisf/BibtexQuery",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "3ab4379b2b92448717de66b7d3e254ac1487aede",
-   "name": "BibtexQuery",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
-   "inherited": true,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/acmepjz/md4lean",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "38ac5945d744903ffcc473ce1030223991b11cf6",
-   "name": "MD4Lean",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
@@ -130,6 +80,16 @@
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover",
+   "rev": "7e1ced9e049a4fab2508980ec4877ca9c46dffc9",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.26.0-rc2",
+   "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "algorithm",
  "lakeDir": ".lake"}

lakefile.lean

@@ -3,7 +3,6 @@ import Lake
 open Lake DSL
 
 require "leanprover-community" / "mathlib" @ git "v4.26.0-rc2"
-require "leanprover" / "doc-gen4" @ git "v4.26.0-rc2"
 
 abbrev algorithmOnlyLinters : Array LeanOption := #[
   ⟨`linter.mathlibStandardSet, true⟩,