Merge main into nightly-testing

.github/workflows/docs-deploy.yml

@@ -0,0 +1,38 @@
+name: Deploy Docs
+
+on:
+  workflow_dispatch:
+  schedule:
+    - cron: '0 10 * * *' # daily (UTC 10:00)
+
+permissions:
+  contents: write
+
+jobs:
+  deploy-docs:
+    runs-on: ubuntu-latest
+    if: github.repository_owner == 'leanprover-community'
+    steps:
+
+      - name: Checkout
+        uses: actions/checkout@v4
+
+      - name: Install Lean
+        uses: leanprover/lean-action@v1
+        with:
+          test: false
+          lint: false
+          use-github-cache: true
+
+      - name: Build Docs
+        working-directory: docs
+        run: lake build -q Batteries:docs
+
+      - name: Deploy Docs
+        run: |
+          git config user.name "leanprover-community-batteries-bot"
+          git config user.email "[email protected]"
+          git checkout -b docs
+          git add docs/doc docs/doc-data
+          git commit -m "chore: generate docs"
+          git push origin docs --force

.github/workflows/docs-release.yml

@@ -0,0 +1,46 @@
+name: Release Docs
+
+on:
+  push:
+    tags:
+      - "v[0-9]+.[0-9]+.[0-9]+"
+      - "v[0-9]+.[0-9]+.[0-9]+-rc[0-9]+"
+
+permissions:
+  contents: write
+
+jobs:
+  build-docs:
+    runs-on: ubuntu-latest
+    if: github.repository_owner == 'leanprover-community'
+    steps:
+
+      - name: Checkout
+        uses: actions/checkout@v4
+
+      - name: Install Lean
+        uses: leanprover/lean-action@v1
+        with:
+          test: false
+          lint: false
+          use-github-cache: true
+
+      - name: Build Docs
+        working-directory: docs
+        run: lake build -q Batteries:docs
+
+      - name: Compress Docs
+        working-directory: docs
+        env:
+          TAG_NAME: ${{ github.ref_name }}
+        run: |
+          tar -czf docs-${TAG_NAME}.tar.gz doc doc-data
+          zip -rq docs-${TAG_NAME}.zip doc doc-data
+
+      - name: Release Docs
+        uses: softprops/action-gh-release@v2
+        with:
+          files: |
+            docs/docs-${{ github.ref_name }}.tar.gz
+            docs/docs-${{ github.ref_name }}.zip
+          fail_on_unmatched_files: true

README.md

@@ -36,31 +36,17 @@ Additionally, please make sure that you're using the version of Lean that the cu
 
 # Documentation
 
-You can generate `batteries`' documentation with
-
-```text
-# if you're generating documentation for the first time
-> lake -R -Kdoc=on update
-...
-# actually generate the documentation
-> lake -R -Kdoc=on build Batteries:docs
-...
-> ls build/doc/index.html
-build/doc/index.html
-```
-
-After generating the docs, run `lake build -R` to reset the configuration.
+You can generate `batteries` documentation with
 
-The top-level HTML file will be located at `build/doc/Batteries.html`, though to actually expose the
-documentation as a server you need to
-
-```text
-> cd build/doc
-> python3 -m http.server
-Serving HTTP on :: port 8000 (http://[::]:8000/) ...
+```sh
+cd docs
+lake build Batteries:docs
 ```
 
-Note that documentation for the latest nightly of `batteries` is available as part of [the Mathlib 4
+The top-level HTML file will be located at `docs/doc/index.html`, though to actually expose the
+documentation you need to run a HTTP server (e.g. `python3 -m http.server`) in the `docs/doc` directory.
+
+Note that documentation for the latest nightly of `batteries` is also available as part of [the Mathlib 4
 documentation][mathlib4 docs].
 
 [mathlib4 docs]: https://leanprover-community.github.io/mathlib4_docs/Batteries.html

docs/README.md

@@ -0,0 +1 @@
+../README.md

docs/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": "8add673e2ea4da0929103ad19dc824e1c0b7437d",
+   "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": "docs",
+ "lakeDir": ".lake"}

docs/lakefile.toml

@@ -0,0 +1,13 @@
+name = "docs"
+reservoir = false
+packagesDir = "../.lake/packages"
+buildDir = "."
+
+[[require]]
+scope = "leanprover"
+name = "doc-gen4"
+rev = "main"
+
+[[require]]
+name = "batteries"
+path = ".."