Skip to content

Commit

Permalink
chore: update docs for v1.1.0
Browse files Browse the repository at this point in the history
  • Loading branch information
fgdorais committed Nov 3, 2024
1 parent aa5daef commit a58140b
Showing 1 changed file with 15 additions and 14 deletions.
29 changes: 15 additions & 14 deletions README.md
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
# Lean 4 / Unicode Basic

Unicode support for Lean 4.
Basic Unicode support for Lean 4.

Unicode properties that are currently supported by `UnicodeBasic` include:

Expand All @@ -26,37 +26,38 @@ Unicode properties that are currently supported by `UnicodeBasic` include:
* `Uppercase`
* `White_Space`

To keep the `UnicodeLibrary` library lightweight, only commonly used properties can be supported. If you need a property not yet in the list above, please submit a feature request!
To keep the `UnicodeBasic` library lightweight, only commonly used properties can be supported. If you need a property not yet in the list above, please submit a feature request!

## Installation

Add the following dependency to your project's `lakefile.toml`:

```toml
[[require]]
name = "UnicodeBasic"
name = "lean4-unicode-basic"
git = "https://github.com/fgdorais/lean4-unicode-basic.git"
rev = "main"
rev = "main" # or any specific revision
```

Or your project's `lakefile.lean`:
Then add `import UnicodeBasic` at the top of any Lean file where you plan to use this library.

```lean
require UnicodeBasic from git
"https://github.com/fgdorais/lean4-unicode-basic" @ "main"
```
## Usage

Then add `import UnicodeBasic` at the top of any Lean file where you plan to use this library.
The main entry point is the root file `UnicodeBasic`. This file contains a description of the main API as well as all primary library functions. The file `UnicodeBasic.Types` contains all the primary data types used in the library.

Use the branch `"docs"` instead of `"main"` if you need to have local library documentation. ([doc-gen4](https://github.com/leanprover/doc-gen4) cannot be used directly because of a circular dependency.)
The remaining files are implementation details. Some of these may be of interest for developers. For example `UnicodeBasic.CharacterDatabase` defines a stream type for parsing files from the [Unicode Character Database](https://www.unicode.org/Public/UCD/latest/ucd/).

## Documentation

Documentation for the library is located at [dorais.org/lean4-unicode-basic/docs/](https://www.dorais.org/lean4-unicode-basic/docs/).
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:

The main entry point is the root file [`UnicodeBasic`](https://www.dorais.org/lean4-unicode-basic/docs/UnicodeBasic.html). This file contains a description of the main API as well as all primary library functions. The file [`UnicodeBasic.Types`](https://www.dorais.org/lean4-unicode-basic/docs/UnicodeBasic/Types.html) contains all the primary data types used in the library.
1. Change to the `docs` directory
2. Run `lake update`
3. Run `lake build UnicodeDocs:docs`

The remaining files are implementation details. Some of these may be of interest for developers. For example [`UnicodeBasic.CharacterDatabase`](https://www.dorais.org/lean4-unicode-basic/docs/UnicodeBasic/CharacterDatabase.html) defines a stream type for parsing files from the [Unicode Character Database](https://www.unicode.org/Public/UCD/latest/ucd/).
The doc-gen4 documentation will then be found in the `docs/.lake/build/doc` and `docs/.lake/build/doc-data` directories.

-----

Expand Down

0 comments on commit a58140b

Please sign in to comment.