Adapt to the new doc-gen setup

Instead of making `FLT` depend on `doc-gen4` conditionally, have a new private Lean project `docbuild` that depends on `FLT` and `doc-gen4`. The only change on the user side is that one needs to run `scripts/bump.sh` instead of `scripts/update_mathlib.sh`. I have renamed the script because it does not just update mathlib, and the new name is shorter.
javierlcontreras · Jan 23, 2025 · 1d7e8f2 · 1d7e8f2
1 parent 2d142bb
commit 1d7e8f2
Show file tree

Hide file tree

Showing 8 changed files with 190 additions and 69 deletions.
diff --git a/.github/workflows/blueprint.yml b/.github/workflows/blueprint.yml
@@ -74,14 +74,16 @@ jobs:
       - name: Cache Mathlib docs
         uses: actions/cache@v4
         with:
-          path: |
-            .lake/build/doc
+          path: docbuild/.lake/build/doc
           key: MathlibDoc-${{ hashFiles('lake-manifest.json') }}
           restore-keys: |
             MathlibDoc-
 
       - name: Build project API documentation
-        run: ~/.elan/bin/lake -R -Kenv=dev build FLT:docs
+        working-directory: docbuild
+        run: |
+          ~/.elan/bin/lake exe cache get || true
+          ~/.elan/bin/lake build LeanCamCombi:docs
 
       - name: Check for `docs` folder # this is meant to detect a Jekyll-based website
         id: check_docs
@@ -120,7 +122,7 @@ jobs:
             ~/.elan/bin/lake exe checkdecls blueprint/lean_decls
 
       - name: Copy API documentation to `docs/docs`
-        run: cp -r .lake/build/doc docs/docs
+        run: cp -r docbuild/.lake/build/doc docs/docs
 
       - name: Bundle dependencies
         if: github.event_name == 'push'

diff --git a/docbuild/lake-manifest.json b/docbuild/lake-manifest.json
@@ -0,0 +1,152 @@
+{"version": "1.1.0",
+ "packagesDir": "../.lake/packages",
+ "packages":
+ [{"url": "https://github.com/leanprover/doc-gen4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover",
+   "rev": "e9d995eaa95a4e3c880ffe94c416c34113e0f251",
+   "name": "«doc-gen4»",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"type": "path",
+   "scope": "",
+   "name": "FLT",
+   "manifestFile": "lake-manifest.json",
+   "inherited": false,
+   "dir": "./../",
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/mhuisi/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "0c8ea32a15a4f74143e4e1e107ba2c412adb90fd",
+   "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": "b64b8eab8cfcf24c398e84b11c77b6555b61095a",
+   "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": "9e99cb8cd9ba6906472634e6973c7e27482a70bb",
+   "name": "BibtexQuery",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/acmepjz/md4lean",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "26b1d510d9b5238d36b521d5367c707146fecd9d",
+   "name": "MD4Lean",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/PatrickMassot/checkdecls.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "75d7aea6c81efeb68701164edaaa9116f06b91ba",
+   "name": "checkdecls",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": null,
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/mathlib4.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "2a71f56e8867536abeae5d73fdb6666dc21ff7d4",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/plausible",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "1622a8693b31523c8f82db48e01b14c74bc1f155",
+   "name": "plausible",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.16.0-rc1",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "003ff459cdd85de551f4dcf95cdfeefe10f20531",
+   "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": "f72319c9686788305a8ab059f3c4d8c724785c83",
+   "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": "07f60e90998dfd6592688a14cd67bd4e384b77b2",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v0.0.50",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/aesop",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "79402ad9ab4be9a2286701a9880697e2351e4955",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.16.0-rc1",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "f0c584bcb14c5adfb53079781eeea75b26ebbd32",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.15.0",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/batteries",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "5b23a1297aba9683f231c4b1a7ab4076af4ad53d",
+   "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
@@ -0,0 +1,13 @@
+name = "docbuild"
+reservoir = false
+version = "0.1.0"
+packagesDir = "../.lake/packages"
+
+[[require]]
+name = "FLT"
+path = "../"
+
+[[require]]
+scope = "leanprover"
+name = "doc-gen4"
+rev = "main"
diff --git a/docbuild/lean-toolchain b/docbuild/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.16.0-rc2
diff --git 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": "",
-   "rev": "8c60540fe18528a8a857d4d88094b005af61d97b",
-   "name": "«doc-gen4»",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.16.0-rc2",
-   "inherited": false,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/PatrickMassot/checkdecls.git",
+ [{"url": "https://github.com/PatrickMassot/checkdecls.git",
    "type": "git",
    "subDir": null,
    "scope": "",
@@ -25,52 +15,12 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "720fe962221040f13afa94b1e4a45c60fb9de7be",
+   "rev": "2a71f56e8867536abeae5d73fdb6666dc21ff7d4",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
    "inherited": false,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/mhuisi/lean4-cli",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "0c8ea32a15a4f74143e4e1e107ba2c412adb90fd",
-   "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": "b64b8eab8cfcf24c398e84b11c77b6555b61095a",
-   "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": "9e99cb8cd9ba6906472634e6973c7e27482a70bb",
-   "name": "BibtexQuery",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/acmepjz/md4lean",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "26b1d510d9b5238d36b521d5367c707146fecd9d",
-   "name": "MD4Lean",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
@@ -140,6 +90,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": "0c8ea32a15a4f74143e4e1e107ba2c412adb90fd",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "FLT",
  "lakeDir": ".lake"}
diff --git a/lakefile.lean b/lakefile.lean
@@ -12,11 +12,6 @@ require mathlib from git "https://github.com/leanprover-community/mathlib4.git"
 
 require checkdecls from git "https://github.com/PatrickMassot/checkdecls.git"
 
--- 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
-  "https://github.com/leanprover/doc-gen4" @ "v4.16.0-rc2"
-
 @[default_target]
 lean_lib FLT where
   globs := #[

diff --git a/scripts/bump.sh b/scripts/bump.sh
@@ -0,0 +1,6 @@
+# Update the mathlib version inside the main project
+lake update mathlib
+# Update the doc-gen version inside the docbuild project
+cd docbuild
+lake update doc-gen4
+cd ..
diff --git a/scripts/update_mathlib.sh b/scripts/update_mathlib.sh