From 12c93ebc493ba09fcd24bfa7b6ab325e0405e6c8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Yuyang=20Zhao=20=E8=B5=B5=E9=9B=A8=E6=89=AC?= Date: Fri, 12 Dec 2025 13:19:05 +0800 Subject: [PATCH 1/5] chore: do not require docs --- .github/workflows/docs.yml | 50 +++---------- .github/workflows/pages.yml | 56 ++++++++++++++ docbuild/lake-manifest.json | 142 ++++++++++++++++++++++++++++++++++++ docbuild/lakefile.toml | 13 ++++ docbuild/lean-toolchain | 1 + lake-manifest.json | 62 +++------------- lakefile.lean | 1 - 7 files changed, 234 insertions(+), 91 deletions(-) create mode 100644 .github/workflows/pages.yml create mode 100644 docbuild/lake-manifest.json create mode 100644 docbuild/lakefile.toml create mode 100644 docbuild/lean-toolchain diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml index 97f1d18..b9c26d7 100644 --- a/.github/workflows/docs.yml +++ b/.github/workflows/docs.yml @@ -17,50 +17,22 @@ 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 - run: | - lake build Algorithm:docs - lake build Algorithm:docsHeader - - - name: copy import graph + - id: lean-action + uses: leanprover/lean-action@v1 + with: + use-github-cache: false + - name: Build Doc run: | - cp algorithm.html ./.lake/build/doc - + cd docbuild + MATHLIB_NO_CACHE_ON_UPDATE=1 lake update doc-gen4 algorithm + lake build algorithm:docs + - 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' diff --git a/.github/workflows/pages.yml b/.github/workflows/pages.yml new file mode 100644 index 0000000..c458644 --- /dev/null +++ b/.github/workflows/pages.yml @@ -0,0 +1,56 @@ +name: Pages CI + +on: + push: + branches: ["master"] + pull_request: + workflow_dispatch: + +# Bestows GITHUB_TOKEN permission to deploy to GitHub Pages +permissions: + contents: read + pages: write + id-token: write + +jobs: + build: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - id: lean-action + uses: leanprover/lean-action@v1 + with: + use-github-cache: false + - name: Build Doc + run: | + cd docbuild + MATHLIB_NO_CACHE_ON_UPDATE=1 lake update doc-gen4 CombinatorialGames + lake build CombinatorialGames:docs + - name: Setup Pages + uses: actions/configure-pages@v4 + - name: Upload artifact + uses: actions/upload-pages-artifact@v3 + with: + path: './docbuild/.lake/build/doc' + + deploy: + needs: build + if: github.event_name != 'pull_request' + # Allow only one maximum concurrent deployment to prevent previous updates + concurrency: + group: "pages" + cancel-in-progress: true + + permissions: + pages: write + id-token: write + + environment: + name: github-pages + url: ${{ steps.deployment.outputs.page_url }} + + runs-on: ubuntu-latest + steps: + - name: Deploy to GitHub Pages + id: deployment + uses: actions/deploy-pages@v4 diff --git a/docbuild/lake-manifest.json b/docbuild/lake-manifest.json new file mode 100644 index 0000000..5f70058 --- /dev/null +++ b/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"} diff --git a/docbuild/lakefile.toml b/docbuild/lakefile.toml new file mode 100644 index 0000000..520fd23 --- /dev/null +++ b/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" diff --git a/docbuild/lean-toolchain b/docbuild/lean-toolchain new file mode 100644 index 0000000..7035713 --- /dev/null +++ b/docbuild/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.26.0-rc2 \ No newline at end of file diff --git a/lake-manifest.json b/lake-manifest.json index 496c99e..7c79f12 100644 --- a/lake-manifest.json +++ b/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"} diff --git a/lakefile.lean b/lakefile.lean index 4aee421..3bc251b 100644 --- a/lakefile.lean +++ b/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⟩, From 4e86cb37ee5888395dce7e705b54acec7412f98b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Yuyang=20Zhao=20=E8=B5=B5=E9=9B=A8=E6=89=AC?= Date: Fri, 12 Dec 2025 13:20:55 +0800 Subject: [PATCH 2/5] Delete pages.yml --- .github/workflows/pages.yml | 56 ------------------------------------- 1 file changed, 56 deletions(-) delete mode 100644 .github/workflows/pages.yml diff --git a/.github/workflows/pages.yml b/.github/workflows/pages.yml deleted file mode 100644 index c458644..0000000 --- a/.github/workflows/pages.yml +++ /dev/null @@ -1,56 +0,0 @@ -name: Pages CI - -on: - push: - branches: ["master"] - pull_request: - workflow_dispatch: - -# Bestows GITHUB_TOKEN permission to deploy to GitHub Pages -permissions: - contents: read - pages: write - id-token: write - -jobs: - build: - runs-on: ubuntu-latest - steps: - - uses: actions/checkout@v4 - - id: lean-action - uses: leanprover/lean-action@v1 - with: - use-github-cache: false - - name: Build Doc - run: | - cd docbuild - MATHLIB_NO_CACHE_ON_UPDATE=1 lake update doc-gen4 CombinatorialGames - lake build CombinatorialGames:docs - - name: Setup Pages - uses: actions/configure-pages@v4 - - name: Upload artifact - uses: actions/upload-pages-artifact@v3 - with: - path: './docbuild/.lake/build/doc' - - deploy: - needs: build - if: github.event_name != 'pull_request' - # Allow only one maximum concurrent deployment to prevent previous updates - concurrency: - group: "pages" - cancel-in-progress: true - - permissions: - pages: write - id-token: write - - environment: - name: github-pages - url: ${{ steps.deployment.outputs.page_url }} - - runs-on: ubuntu-latest - steps: - - name: Deploy to GitHub Pages - id: deployment - uses: actions/deploy-pages@v4 From d383c4ea4696a8350a1aba8f60932c9c37725276 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Yuyang=20Zhao=20=E8=B5=B5=E9=9B=A8=E6=89=AC?= Date: Fri, 12 Dec 2025 13:35:41 +0800 Subject: [PATCH 3/5] fix --- .github/workflows/docs.yml | 12 ++++++++++-- docbuild/lean-toolchain | 2 +- 2 files changed, 11 insertions(+), 3 deletions(-) diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml index b9c26d7..82f2d96 100644 --- a/.github/workflows/docs.yml +++ b/.github/workflows/docs.yml @@ -25,8 +25,16 @@ jobs: - name: Build Doc run: | cd docbuild - MATHLIB_NO_CACHE_ON_UPDATE=1 lake update doc-gen4 algorithm - lake build algorithm:docs + - 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 + run: | + lake build Algorithm:docs + lake build Algorithm:docsHeader - name: Setup Pages uses: actions/configure-pages@v4 - name: Upload artifact diff --git a/docbuild/lean-toolchain b/docbuild/lean-toolchain index 7035713..be1fbc3 100644 --- a/docbuild/lean-toolchain +++ b/docbuild/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.26.0-rc2 \ No newline at end of file +leanprover/lean4:v4.26.0-rc2 From 829f609ad1b66659d73309697e6105c439e287c3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Yuyang=20Zhao=20=E8=B5=B5=E9=9B=A8=E6=89=AC?= Date: Fri, 12 Dec 2025 13:53:32 +0800 Subject: [PATCH 4/5] try --- .github/workflows/docs.yml | 7 ------- 1 file changed, 7 deletions(-) diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml index 82f2d96..624701c 100644 --- a/.github/workflows/docs.yml +++ b/.github/workflows/docs.yml @@ -25,14 +25,7 @@ jobs: - name: Build Doc run: | cd docbuild - - 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 - run: | lake build Algorithm:docs lake build Algorithm:docsHeader - name: Setup Pages From 64e39409cf1330c9abd386544e5d203f68bdd319 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Yuyang=20Zhao=20=E8=B5=B5=E9=9B=A8=E6=89=AC?= Date: Fri, 12 Dec 2025 14:11:22 +0800 Subject: [PATCH 5/5] fix --- .github/workflows/docs.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml index 624701c..82c3cce 100644 --- a/.github/workflows/docs.yml +++ b/.github/workflows/docs.yml @@ -24,8 +24,8 @@ jobs: use-github-cache: false - name: Build Doc run: | + lake exe graph ./docbuild/algorithm.html cd docbuild - lake exe graph algorithm.html lake build Algorithm:docs lake build Algorithm:docsHeader - name: Setup Pages