chore: update release workflow

.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

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.
 
 -----
 

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"}

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"]