feat: generate docs from subdirectory

BatteriesDocs.lean

@@ -0,0 +1,19 @@
+/-
+Copyright (c) 2024 François G. Dorais. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: François G. Dorais
+-/
+
+import Batteries
+
+/-! # Batteries Documentation
+
+To generate documentation for Batteries:
+
+1. Change to the `BatteriesDocs` subdirectory
+2. Run `lake build BatteriesDocs:docs`
+
+The [`doc-gen4`](https://github.com/leanprover/doc-gen4) documentation will be found in the
+`.lake/buid/doc` and `.lake/build/doc-data` subdirectories.
+
+-/

BatteriesDocs/lake-manifest.json

@@ -0,0 +1,62 @@
+{"version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "https://github.com/acmepjz/md4lean",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "5e95f4776be5e048364f325c7e9d619bb56fb005",
+   "name": "MD4Lean",
+   "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": "b41bc9cec7f433d6e1d74ff3b59edaaf58ad2915",
+   "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": "bdc2fc30b1e834b294759a5d391d83020a90058e",
+   "name": "BibtexQuery",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/mhuisi/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "726b3c9ad13acca724d4651f14afc4804a7b0e4d",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover/doc-gen4",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "b6ae1cf11e83d972ffa363f9cdc8a2f89aaa24dc",
+   "name": "«doc-gen4»",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"type": "path",
+   "scope": "",
+   "name": "batteries",
+   "manifestFile": "lake-manifest.json",
+   "inherited": false,
+   "dir": "./..",
+   "configFile": "lakefile.toml"}],
+ "name": "«batteries-docs»",
+ "lakeDir": ".lake"}

BatteriesDocs/lakefile.toml

@@ -0,0 +1,16 @@
+name = "batteries-docs"
+reservoir = false
+defaultTargets = ["BatteriesDocs"]
+
+[[require]]
+name = "doc-gen4"
+git = "https://github.com/leanprover/doc-gen4"
+rev = "main"
+
+[[require]]
+name = "batteries"
+path = ".."
+
+[[lean_lib]]
+name = "BatteriesDocs"
+srcDir = ".."

BatteriesDocs/lean-toolchain

@@ -0,0 +1 @@
+../lean-toolchain