diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index 1cfa7700..a40c32f5 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -27,15 +27,15 @@ jobs: working-directory: docs run: | lake update - lake build UnicodeDocs:docs + lake build - name: Compress Docs - working-directory: docs/.lake/build + 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 + tar -czf docs-${TAG_NAME}.tar.gz doc doc-data + zip -rq docs-${TAG_NAME}.zip doc doc-data - name: Release uses: softprops/action-gh-release@v2 diff --git a/README.md b/README.md index 4a8db231..16fabfa4 100644 --- a/README.md +++ b/README.md @@ -49,15 +49,16 @@ The remaining files are implementation details. Some of these may be of interest ## Documentation +Documentation can be found at [www.dorais.org/lean4-unicode-basic/doc/](https://www.dorais.org/lean4-unicode-basic/doc/). + Since [doc-gen4](https://github.com/leanprover/doc-gen4) depends on this library, it cannot be used to generate documentation for this library in the usual manner. For this reason, documentation are provided for each release since version 1.1.0. Users can still generate local documentation using these instructions: 1. Change to the `docs` directory -2. Run `lake update` -3. Run `lake build UnicodeDocs:docs` +2. Run `lake build` -The doc-gen4 documentation will then be found in the `docs/.lake/build/doc` and `docs/.lake/build/doc-data` directories. +The doc-gen4 documentation will then be found in the `docs/doc` and `docs/doc-data` directories. ----- diff --git a/docs/lake-manifest.json b/docs/lake-manifest.json new file mode 100644 index 00000000..cf8e73fb --- /dev/null +++ b/docs/lake-manifest.json @@ -0,0 +1,52 @@ +{"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"}, + {"type": "path", + "scope": "", + "name": "UnicodeBasic", + "manifestFile": "lake-manifest.json", + "inherited": false, + "dir": "./..", + "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": "e18c6c23dd7cb1f12d79d6304262351df943aa37", + "name": "«doc-gen4»", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": false, + "configFile": "lakefile.lean"}], + "name": "UnicodeDocs", + "lakeDir": ".lake"} diff --git a/docs/lakefile.toml b/docs/lakefile.toml index abb65867..ce2cd596 100644 --- a/docs/lakefile.toml +++ b/docs/lakefile.toml @@ -1,5 +1,6 @@ name = "UnicodeDocs" reservoir = false +buildDir = "." defaultTargets = ["UnicodeDocs"] [[require]] @@ -14,3 +15,4 @@ path = ".." [[lean_lib]] name = "UnicodeDocs" srcDir = ".." +defaultFacets = ["docs"]