doc-gen4

lake-manifest.json

@@ -1,7 +1,17 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/PatrickMassot/checkdecls.git",
+ [{"url": "https://github.com/leanprover/doc-gen4",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "5a111ebbb151dc6719734f39b1d3aea8d5affb76",
+   "name": "«doc-gen4»",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.16.0-rc1",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/PatrickMassot/checkdecls.git",
    "type": "git",
    "subDir": null,
    "scope": "",
@@ -21,6 +31,46 @@
    "inputRev": "v4.16.0-rc1",
    "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": "51b0cd28a0ca79ccfa91b8c7d5eb94ba075dfdb4",
+   "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": "46376bc3c8f46ac1a1fd7712856b0f7bd6166098",
+   "name": "BibtexQuery",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/kim-em/md4lean",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "17e3f60bca8b6fdc19a55e2a7c9840a9f7afd1dc",
+   "name": "MD4Lean",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "bump_to_v4.16.0-rc1",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
@@ -90,16 +140,6 @@
    "manifestFile": "lake-manifest.json",
    "inputRev": "v4.16.0-rc1",
    "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"}

lakefile.lean

@@ -15,7 +15,7 @@ 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" @ "main"
+  "https://github.com/leanprover/doc-gen4" @ "v4.16.0-rc1"
 
 @[default_target]
 lean_lib FLT where