From e6047ba5227277c06879db3dd6533d8fc722fcb3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20G=2E=20Dorais?= Date: Tue, 12 Nov 2024 18:13:55 -0500 Subject: [PATCH] feat: generate docs from subdirectory (#1028) Co-authored-by: Kim Morrison --- .github/workflows/docs-deploy.yml | 38 ++++++++++++++++++ .github/workflows/docs-release.yml | 46 ++++++++++++++++++++++ README.md | 30 ++++----------- docs/README.md | 1 + docs/lake-manifest.json | 62 ++++++++++++++++++++++++++++++ docs/lakefile.toml | 13 +++++++ 6 files changed, 168 insertions(+), 22 deletions(-) create mode 100644 .github/workflows/docs-deploy.yml create mode 100644 .github/workflows/docs-release.yml create mode 120000 docs/README.md create mode 100644 docs/lake-manifest.json create mode 100644 docs/lakefile.toml diff --git a/.github/workflows/docs-deploy.yml b/.github/workflows/docs-deploy.yml new file mode 100644 index 0000000000..39746f19d3 --- /dev/null +++ b/.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 "leanprover-community-batteries-bot@users.noreply.github.com" + git checkout -b docs + git add docs/doc docs/doc-data + git commit -m "chore: generate docs" + git push origin docs --force diff --git a/.github/workflows/docs-release.yml b/.github/workflows/docs-release.yml new file mode 100644 index 0000000000..2926a31340 --- /dev/null +++ b/.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 diff --git a/README.md b/README.md index f8cc2415ac..2873f65536 100644 --- a/README.md +++ b/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 diff --git a/docs/README.md b/docs/README.md new file mode 120000 index 0000000000..32d46ee883 --- /dev/null +++ b/docs/README.md @@ -0,0 +1 @@ +../README.md \ No newline at end of file diff --git a/docs/lake-manifest.json b/docs/lake-manifest.json new file mode 100644 index 0000000000..9c082aa9e8 --- /dev/null +++ b/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"} diff --git a/docs/lakefile.toml b/docs/lakefile.toml new file mode 100644 index 0000000000..0726079709 --- /dev/null +++ b/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 = ".."