chore: generate docs

Author: leanprover-community-batteries-bot

docs/doc-data/Batteries--library.docs_built

@@ -0,0 +1 @@
+21c42906adea99f5

docs/doc-data/Batteries--library.docs_built.hash

@@ -0,0 +1,19 @@
+{"synthetic": false,
+ "schemaVersion": "2025-09-10",
+ "outputs": null,
+ "log":
+ [{"message": "Generating documentation for Batteries (1 root modules)",
+   "level": "info"},
+  {"message":
+   ".> ELAN=elan ELAN_HOME=/home/runner/.elan ELAN_TOOLCHAIN=leanprover/lean4:v4.29.0-rc6 LAKE=/home/runner/.elan/toolchains/leanprover--lean4---v4.29.0-rc6/bin/lake LAKE_HOME=/home/runner/.elan/toolchains/leanprover--lean4---v4.29.0-rc6 LAKE_CONFIG=/home/runner/.lake/config.toml LAKE_PKG_URL_MAP={} LAKE_NO_CACHE=false LAKE_CACHE_KEY= LAKE_CACHE_ARTIFACT_ENDPOINT= LAKE_CACHE_REVISION_ENDPOINT= LAKE_CACHE_SERVICE= LEAN=/home/runner/.elan/toolchains/leanprover--lean4---v4.29.0-rc6/bin/lean LEAN_SYSROOT=/home/runner/.elan/toolchains/leanprover--lean4---v4.29.0-rc6 LEAN_AR=/home/runner/.elan/toolchains/leanprover--lean4---v4.29.0-rc6/bin/llvm-ar LEAN_CC= LAKE_CACHE_DIR=/home/runner/.elan/toolchains/leanprover--lean4---v4.29.0-rc6/lake/cache LAKE_ARTIFACT_CACHE= LEAN_PATH=/home/runner/work/batteries/batteries/.lake/packages/plausible/.lake/build/lib/lean:/home/runner/work/batteries/batteries/.lake/packages/MD4Lean/.lake/build/lib/lean:/home/runner/work/batteries/batteries/.lake/packages/BibtexQuery/.lake/build/lib/lean:/home/runner/work/batteries/batteries/.lake/packages/UnicodeBasic/.lake/build/lib/lean:/home/runner/work/batteries/batteries/.lake/packages/Cli/.lake/build/lib/lean:/home/runner/work/batteries/batteries/.lake/packages/leansqlite/.lake/build/lib/lean:/home/runner/work/batteries/batteries/.lake/packages/doc-gen4/.lake/build/lib/lean:/home/runner/work/batteries/batteries/.lake/build/lib/lean:/home/runner/work/batteries/batteries/docs/lib/lean:/home/runner/.elan/toolchains/leanprover--lean4---v4.29.0-rc6/lib/lean LEAN_SRC_PATH=/home/runner/work/batteries/batteries/.lake/packages/plausible:/home/runner/work/batteries/batteries/.lake/packages/plausible:/home/runner/work/batteries/batteries/.lake/packages/MD4Lean:/home/runner/work/batteries/batteries/.lake/packages/MD4Lean:/home/runner/work/batteries/batteries/.lake/packages/BibtexQuery:/home/runner/work/batteries/batteries/.lake/packages/UnicodeBasic:/home/runner/work/batteries/batteries/.lake/packages/UnicodeBasic:/home/runner/work/batteries/batteries/.lake/packages/Cli:/home/runner/work/batteries/batteries/.lake/packages/Cli:/home/runner/work/batteries/batteries/.lake/packages/leansqlite:/home/runner/work/batteries/batteries/.lake/packages/leansqlite:/home/runner/work/batteries/batteries/.lake/packages/doc-gen4:/home/runner/work/batteries/batteries:/home/runner/work/batteries/batteries:/home/runner/.elan/toolchains/leanprover--lean4---v4.29.0-rc6/src/lean/lake LEAN_GITHASH=00659f8e6071d7e46131ed643bf8003b99b044e9 PATH LD_LIBRARY_PATH=/home/runner/.elan/toolchains/leanprover--lean4---v4.29.0-rc6/lib/lean:/home/runner/.elan/toolchains/leanprover--lean4---v4.29.0-rc6/lib:/home/runner/work/batteries/batteries/docs/lib:/home/runner/work/batteries/batteries/.lake/build/lib:/home/runner/work/batteries/batteries/.lake/packages/doc-gen4/.lake/build/lib:/home/runner/work/batteries/batteries/.lake/packages/leansqlite/.lake/build/lib:/home/runner/work/batteries/batteries/.lake/packages/Cli/.lake/build/lib:/home/runner/work/batteries/batteries/.lake/packages/UnicodeBasic/.lake/build/lib:/home/runner/work/batteries/batteries/.lake/packages/BibtexQuery/.lake/build/lib:/home/runner/work/batteries/batteries/.lake/packages/MD4Lean/.lake/build/lib:/home/runner/work/batteries/batteries/.lake/packages/plausible/.lake/build/lib /home/runner/work/batteries/batteries/.lake/packages/doc-gen4/.lake/build/bin/doc-gen4 fromDb --build /home/runner/work/batteries/batteries/docs --manifest /home/runner/work/batteries/batteries/docs/doc-manifest.json /home/runner/work/batteries/batteries/docs/api-docs.db Batteries Init Std Lake Lean",
+   "level": "trace"}],
+ "inputs":
+ [["<nil>", "e0ef540168b1a2cd"],
+  ["<collection>",
+   [["/home/runner/work/batteries/batteries/docs/doc-data/Batteries.doc",
+     "21c42906adea99f5"]]],
+  ["/home/runner/work/batteries/batteries/docs/doc-data/references.json",
+   "16fb262bc340d332"],
+  ["/home/runner/work/batteries/batteries/.lake/packages/doc-gen4/.lake/build/bin/doc-gen4",
+   "830870dc0e47b062"]],
+ "depHash": "9f45899cde755f50"}

docs/doc-data/Batteries--library.docs_built.trace

@@ -0,0 +1 @@
+21c42906adea99f5

docs/doc-data/Batteries.Classes.Cast.doc

@@ -0,0 +1,18 @@
+{"synthetic": false,
+ "schemaVersion": "2025-09-10",
+ "outputs": null,
+ "log":
+ [{"message":
+   ".> ELAN=elan ELAN_HOME=/home/runner/.elan ELAN_TOOLCHAIN=leanprover/lean4:v4.29.0-rc6 LAKE=/home/runner/.elan/toolchains/leanprover--lean4---v4.29.0-rc6/bin/lake LAKE_HOME=/home/runner/.elan/toolchains/leanprover--lean4---v4.29.0-rc6 LAKE_CONFIG=/home/runner/.lake/config.toml LAKE_PKG_URL_MAP={} LAKE_NO_CACHE=false LAKE_CACHE_KEY= LAKE_CACHE_ARTIFACT_ENDPOINT= LAKE_CACHE_REVISION_ENDPOINT= LAKE_CACHE_SERVICE= LEAN=/home/runner/.elan/toolchains/leanprover--lean4---v4.29.0-rc6/bin/lean LEAN_SYSROOT=/home/runner/.elan/toolchains/leanprover--lean4---v4.29.0-rc6 LEAN_AR=/home/runner/.elan/toolchains/leanprover--lean4---v4.29.0-rc6/bin/llvm-ar LEAN_CC= LAKE_CACHE_DIR=/home/runner/.elan/toolchains/leanprover--lean4---v4.29.0-rc6/lake/cache LAKE_ARTIFACT_CACHE= LEAN_PATH=/home/runner/work/batteries/batteries/.lake/packages/plausible/.lake/build/lib/lean:/home/runner/work/batteries/batteries/.lake/packages/MD4Lean/.lake/build/lib/lean:/home/runner/work/batteries/batteries/.lake/packages/BibtexQuery/.lake/build/lib/lean:/home/runner/work/batteries/batteries/.lake/packages/UnicodeBasic/.lake/build/lib/lean:/home/runner/work/batteries/batteries/.lake/packages/Cli/.lake/build/lib/lean:/home/runner/work/batteries/batteries/.lake/packages/leansqlite/.lake/build/lib/lean:/home/runner/work/batteries/batteries/.lake/packages/doc-gen4/.lake/build/lib/lean:/home/runner/work/batteries/batteries/.lake/build/lib/lean:/home/runner/work/batteries/batteries/docs/lib/lean:/home/runner/.elan/toolchains/leanprover--lean4---v4.29.0-rc6/lib/lean LEAN_SRC_PATH=/home/runner/work/batteries/batteries/.lake/packages/plausible:/home/runner/work/batteries/batteries/.lake/packages/plausible:/home/runner/work/batteries/batteries/.lake/packages/MD4Lean:/home/runner/work/batteries/batteries/.lake/packages/MD4Lean:/home/runner/work/batteries/batteries/.lake/packages/BibtexQuery:/home/runner/work/batteries/batteries/.lake/packages/UnicodeBasic:/home/runner/work/batteries/batteries/.lake/packages/UnicodeBasic:/home/runner/work/batteries/batteries/.lake/packages/Cli:/home/runner/work/batteries/batteries/.lake/packages/Cli:/home/runner/work/batteries/batteries/.lake/packages/leansqlite:/home/runner/work/batteries/batteries/.lake/packages/leansqlite:/home/runner/work/batteries/batteries/.lake/packages/doc-gen4:/home/runner/work/batteries/batteries:/home/runner/work/batteries/batteries:/home/runner/.elan/toolchains/leanprover--lean4---v4.29.0-rc6/src/lean/lake LEAN_GITHASH=00659f8e6071d7e46131ed643bf8003b99b044e9 PATH LD_LIBRARY_PATH=/home/runner/.elan/toolchains/leanprover--lean4---v4.29.0-rc6/lib/lean:/home/runner/.elan/toolchains/leanprover--lean4---v4.29.0-rc6/lib:/home/runner/work/batteries/batteries/docs/lib:/home/runner/work/batteries/batteries/.lake/build/lib:/home/runner/work/batteries/batteries/.lake/packages/doc-gen4/.lake/build/lib:/home/runner/work/batteries/batteries/.lake/packages/leansqlite/.lake/build/lib:/home/runner/work/batteries/batteries/.lake/packages/Cli/.lake/build/lib:/home/runner/work/batteries/batteries/.lake/packages/UnicodeBasic/.lake/build/lib:/home/runner/work/batteries/batteries/.lake/packages/BibtexQuery/.lake/build/lib:/home/runner/work/batteries/batteries/.lake/packages/MD4Lean/.lake/build/lib:/home/runner/work/batteries/batteries/.lake/packages/plausible/.lake/build/lib /home/runner/work/batteries/batteries/.lake/packages/doc-gen4/.lake/build/bin/doc-gen4 single --build /home/runner/work/batteries/batteries/docs Batteries.Classes.Cast api-docs.db https://github.com/leanprover-community/batteries/blob/87f6314ff2cc922489cd73cd0fbc2252f39aa153/Batteries/Classes/Cast.lean",
+   "level": "trace"}],
+ "inputs":
+ [["<nil>", "e0ef540168b1a2cd"],
+  ["<collection>",
+   [["/home/runner/work/batteries/batteries/docs/doc-data/Batteries.Util.LibraryNote.doc",
+     "21c42906adea99f5"]]],
+  ["/home/runner/work/batteries/batteries/docs/doc-data/references.json",
+   "16fb262bc340d332"],
+  ["/home/runner/work/batteries/batteries/.lake/packages/doc-gen4/.lake/build/bin/doc-gen4",
+   "830870dc0e47b062"],
+  ["Batteries.Classes.Cast:leanArts", "0c9fb6c4c1eb1e6c"]],
+ "depHash": "a402d4514d0f1d51"}

docs/doc-data/Batteries.Classes.Cast.doc.hash

@@ -0,0 +1 @@
+21c42906adea99f5

docs/doc-data/Batteries.Classes.Cast.doc.trace

@@ -0,0 +1,18 @@
+{"synthetic": false,
+ "schemaVersion": "2025-09-10",
+ "outputs": null,
+ "log":
+ [{"message":
+   ".> ELAN=elan ELAN_HOME=/home/runner/.elan ELAN_TOOLCHAIN=leanprover/lean4:v4.29.0-rc6 LAKE=/home/runner/.elan/toolchains/leanprover--lean4---v4.29.0-rc6/bin/lake LAKE_HOME=/home/runner/.elan/toolchains/leanprover--lean4---v4.29.0-rc6 LAKE_CONFIG=/home/runner/.lake/config.toml LAKE_PKG_URL_MAP={} LAKE_NO_CACHE=false LAKE_CACHE_KEY= LAKE_CACHE_ARTIFACT_ENDPOINT= LAKE_CACHE_REVISION_ENDPOINT= LAKE_CACHE_SERVICE= LEAN=/home/runner/.elan/toolchains/leanprover--lean4---v4.29.0-rc6/bin/lean LEAN_SYSROOT=/home/runner/.elan/toolchains/leanprover--lean4---v4.29.0-rc6 LEAN_AR=/home/runner/.elan/toolchains/leanprover--lean4---v4.29.0-rc6/bin/llvm-ar LEAN_CC= LAKE_CACHE_DIR=/home/runner/.elan/toolchains/leanprover--lean4---v4.29.0-rc6/lake/cache LAKE_ARTIFACT_CACHE= LEAN_PATH=/home/runner/work/batteries/batteries/.lake/packages/plausible/.lake/build/lib/lean:/home/runner/work/batteries/batteries/.lake/packages/MD4Lean/.lake/build/lib/lean:/home/runner/work/batteries/batteries/.lake/packages/BibtexQuery/.lake/build/lib/lean:/home/runner/work/batteries/batteries/.lake/packages/UnicodeBasic/.lake/build/lib/lean:/home/runner/work/batteries/batteries/.lake/packages/Cli/.lake/build/lib/lean:/home/runner/work/batteries/batteries/.lake/packages/leansqlite/.lake/build/lib/lean:/home/runner/work/batteries/batteries/.lake/packages/doc-gen4/.lake/build/lib/lean:/home/runner/work/batteries/batteries/.lake/build/lib/lean:/home/runner/work/batteries/batteries/docs/lib/lean:/home/runner/.elan/toolchains/leanprover--lean4---v4.29.0-rc6/lib/lean LEAN_SRC_PATH=/home/runner/work/batteries/batteries/.lake/packages/plausible:/home/runner/work/batteries/batteries/.lake/packages/plausible:/home/runner/work/batteries/batteries/.lake/packages/MD4Lean:/home/runner/work/batteries/batteries/.lake/packages/MD4Lean:/home/runner/work/batteries/batteries/.lake/packages/BibtexQuery:/home/runner/work/batteries/batteries/.lake/packages/UnicodeBasic:/home/runner/work/batteries/batteries/.lake/packages/UnicodeBasic:/home/runner/work/batteries/batteries/.lake/packages/Cli:/home/runner/work/batteries/batteries/.lake/packages/Cli:/home/runner/work/batteries/batteries/.lake/packages/leansqlite:/home/runner/work/batteries/batteries/.lake/packages/leansqlite:/home/runner/work/batteries/batteries/.lake/packages/doc-gen4:/home/runner/work/batteries/batteries:/home/runner/work/batteries/batteries:/home/runner/.elan/toolchains/leanprover--lean4---v4.29.0-rc6/src/lean/lake LEAN_GITHASH=00659f8e6071d7e46131ed643bf8003b99b044e9 PATH LD_LIBRARY_PATH=/home/runner/.elan/toolchains/leanprover--lean4---v4.29.0-rc6/lib/lean:/home/runner/.elan/toolchains/leanprover--lean4---v4.29.0-rc6/lib:/home/runner/work/batteries/batteries/docs/lib:/home/runner/work/batteries/batteries/.lake/build/lib:/home/runner/work/batteries/batteries/.lake/packages/doc-gen4/.lake/build/lib:/home/runner/work/batteries/batteries/.lake/packages/leansqlite/.lake/build/lib:/home/runner/work/batteries/batteries/.lake/packages/Cli/.lake/build/lib:/home/runner/work/batteries/batteries/.lake/packages/UnicodeBasic/.lake/build/lib:/home/runner/work/batteries/batteries/.lake/packages/BibtexQuery/.lake/build/lib:/home/runner/work/batteries/batteries/.lake/packages/MD4Lean/.lake/build/lib:/home/runner/work/batteries/batteries/.lake/packages/plausible/.lake/build/lib /home/runner/work/batteries/batteries/.lake/packages/doc-gen4/.lake/build/bin/doc-gen4 single --build /home/runner/work/batteries/batteries/docs Batteries.Classes.Deprecated api-docs.db https://github.com/leanprover-community/batteries/blob/87f6314ff2cc922489cd73cd0fbc2252f39aa153/Batteries/Classes/Deprecated.lean",
+   "level": "trace"}],
+ "inputs":
+ [["<nil>", "e0ef540168b1a2cd"],
+  ["<collection>",
+   [["/home/runner/work/batteries/batteries/docs/doc-data/Batteries.Classes.Order.doc",
+     "21c42906adea99f5"]]],
+  ["/home/runner/work/batteries/batteries/docs/doc-data/references.json",
+   "16fb262bc340d332"],
+  ["/home/runner/work/batteries/batteries/.lake/packages/doc-gen4/.lake/build/bin/doc-gen4",
+   "830870dc0e47b062"],
+  ["Batteries.Classes.Deprecated:leanArts", "e4bdf803592b39ef"]],
+ "depHash": "7ab057ee4534b32d"}