Support doc-gen4 SQLite database format for extraction

lean/cslib/lake-manifest.json

@@ -1,81 +1,41 @@
-{"version": "1.1.0",
+{"version": "1.2.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover/doc-gen4",
+ [{"url": "https://github.com/leanprover/cslib",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "7be6082d00bb0cfc1e136505dba7718cd5fcaa84",
-   "name": "«doc-gen4»",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.28.0-rc1",
-   "inherited": false,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/cslib",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "00d68a39497c0954bd52ca5237eea2aa152a5387",
+   "rev": "48e29fde33e1d1650a1615ba4d1440a1c36a23c3",
    "name": "Cslib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": false,
    "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover/lean4-cli",
+  {"url": "https://github.com/leanprover/doc-gen4",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "28e0856d4424863a85b18f38868c5420c55f9bae",
-   "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": "8668e1ab7c987fb8ed1349f14c3b7b60bd5f27b6",
-   "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": "1c5c543d2637aebf90c80aead2d401ae88db13cc",
-   "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",
+   "rev": "2c96309e0de1b916d1a0b74c8119fddc7bf7da51",
+   "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
-   "inherited": true,
+   "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "5352afccd6866369be9de43f5b7ec47203555f44",
+   "rev": "ae0c6140a8312511dbb5bc265a0146dd418eca8d",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.28.0-rc1",
+   "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "7311586e1a56af887b1081d05e80c11b6c41d212",
+   "rev": "f449eabb8f7e3feef0366856c20e28a6d2c97ee3",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "5ce7f0a355f522a952a3d678d696bd563bb4fd28",
+   "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -95,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "875ad9d88ed684e39c16bdea260e6ecfa15afd60",
+   "rev": "86503d416c875fdcf3b6b6c54c22581e96c6bda7",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -105,41 +65,92 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "6d65c6e0a25b8a52c13c3adeb63ecde3bfbb6294",
+   "rev": "82d457fb3bdd9efadbae06608ff337d689efdddf",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.86",
+   "inputRev": "v0.0.97",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "f08e838d4f9aea519f3cde06260cfb686fd4bab0",
+   "rev": "f74c7555aaa94eadd7b7bff9170f7983f92aac21",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.30.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "23324752757bf28124a518ec284044c8db79fee5",
+   "rev": "7aa86cb20b8458748dc24d55dab2d7ea01161057",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.30.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "cabbb5a025bfbbc50af9184ed2dfdde6ea4f53a7",
+   "rev": "bf597c77bf9b8e66720d724928207f5911533113",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.30.0-rc1",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover",
+   "rev": "f7d0ca7c926cdde0562af20394dd25d028b839a5",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.30.0-rc1",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover/leansqlite",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "4dfd48ca35193382ddf4c64eef5cdd4f6091bef3",
+   "name": "leansqlite",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/fgdorais/lean4-unicode-basic",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "c8bc12a81fd4ee633719f7fd3f587eca7d0e87ab",
+   "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": "5d31b64fb703c5d77f6ef4d1fb958f9bdf1ea539",
+   "name": "BibtexQuery",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "nightly-testing",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/acmepjz/md4lean",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "6a3fb240133bcb7e1a066fdc784b3fdc304e3fc5",
+   "name": "MD4Lean",
+   "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.toml"}],
+   "configFile": "lakefile.lean"}],
  "name": "«cslib-extractor»",
- "lakeDir": ".lake"}
+ "lakeDir": ".lake",
+ "fixedToolchain": false}

lean/cslib/lakefile.lean

@@ -7,8 +7,8 @@ package «cslib-extractor» where
 lean_lib «CslibExtract» where
   roots := #[`CslibExtract]
 
+require «doc-gen4» from git
+  "https://github.com/leanprover/doc-gen4" @ "main"
+
 require Cslib from git
   "https://github.com/leanprover/cslib" @ "main"
-
-require «doc-gen4» from git
-  "https://github.com/leanprover/doc-gen4" @ "v4.28.0-rc1"

lean/cslib/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.28.0-rc1
+leanprover/lean4:v4.30.0-rc1