Merge pull request #12 from mjdemedeiros/doc-gen

Update dependencies to support doc-gen4

lake-manifest.json

@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "f3e6d5d994e7d6a6c5bb5820068d9c7d2d004e30",
+   "rev": "7b3c48b58fa0ae1c8f27889bdb086ea5e4b27b06",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -22,7 +22,7 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "de11e0ecf372976e6d627c210573146153090d2d",
+   "rev": "e8c8a42642ceb5af33708b79ae8a3148b681c236",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -58,11 +58,47 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "3570694dc49dfeb1c8d364aad7e3b6fcb6c6f0eb",
+   "rev": "dfedb0f929c2a8336ca48766c2902651313864ba",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
    "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/xubaiw/CMark.lean",
+   "type": "git",
+   "subDir": null,
+   "rev": "ba7b47bd773954b912ecbf5b1c9993c71a166f05",
+   "name": "CMark",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/fgdorais/lean4-unicode-basic",
+   "type": "git",
+   "subDir": null,
+   "rev": "effd8b8771cfd7ece69db99448168078e113c61f",
+   "name": "UnicodeBasic",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/hargonix/LeanInk",
+   "type": "git",
+   "subDir": null,
+   "rev": "f1f904e00d79a91ca6a76dec6e318531a7fd2a0f",
+   "name": "leanInk",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "doc-gen",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/doc-gen4",
+   "type": "git",
+   "subDir": null,
+   "rev": "b334278bbe691cb41af3e472ea0a85b6be81e98e",
+   "name": "«doc-gen4»",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "sampcert",
  "lakeDir": ".lake"}

lakefile.lean

@@ -13,3 +13,7 @@ lean_lib «SampCert» where
 lean_lib «FastExtract» where
 
 lean_lib «VMC» where
+
+-- From doc-gen4 
+meta if get_config? env = some "doc" then 
+require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.8.0-rc1
+leanprover/lean4:v4.8.0-rc2