feat: implement full UCD 17.0

.github/workflows/build.yml

@@ -15,14 +15,51 @@ jobs:
   build:
     runs-on: ubuntu-latest
     steps:
-
-      - name: checkout
+      - name: Checkout
         uses: actions/checkout@v7
 
-      - name: build
+      - name: Build Common
+        uses: leanprover/lean-action@v1
+        with:
+          build: true
+          build-args: "--wfail"
+          lake-package-directory: common
+          test: false
+          use-mathlib-cache: false
+
+      - name: Build Table Generators
         uses: leanprover/lean-action@v1
         with:
           build: true
-          build-args: "--wfail UnicodeBasic UnicodeData lookup makeCLib makeTables"
-          test: true
+          build-args: "--wfail"
+          lake-package-directory: table-generators
+          test: false
           use-mathlib-cache: false
+
+      - name: Build Library
+        uses: leanprover/lean-action@v1
+        with:
+          build: true
+          build-args: "--wfail"
+          lake-package-directory: lib
+          test: false
+
+      - name: Build Lean Scripts
+        uses: leanprover/lean-action@v1
+        with:
+          build: true
+          build-args: "--wfail"
+          lake-package-directory: lean-scripts
+          test: false
+
+      - name: Build Tests
+        uses: leanprover/lean-action@v1
+        with:
+          build: true
+          build-args: "--wfail"
+          lake-package-directory: tests
+          test: false
+
+      - name: Run Tests
+        working-directory: tests
+        run: lake exe testAll -- --timeout 120

.github/workflows/publish.yml

@@ -10,16 +10,24 @@ jobs:
   deploy-docs:
     runs-on: ubuntu-latest
     steps:
-
       - name: Checkout
         uses: actions/checkout@v7
 
-      - name: Install Lean
+      - name: Build UnicodeBasic Docs
+        uses: leanprover/lean-action@v1
+        with:
+          build: true
+          build-args: "--keep-toolchain UnicodeBasic:docs"
+          lake-package-directory: lib
+          test: false
+
+      - name: Build UnicodeData Docs
         uses: leanprover/lean-action@v1
         with:
+          build: true
+          build-args: "--keep-toolchain UnicodeData:docs"
+          lake-package-directory: table-generators
           test: false
-          lint: false
-          use-github-cache: true
 
       - name: Build Docs
         working-directory: docs

.github/workflows/push-to-nightly.yml

@@ -23,6 +23,6 @@ jobs:
           git config user.name "${{ github.actor }}"
           git config user.email "${{ github.actor_id }}+${{ github.actor }}@users.noreply.github.com"
           git merge origin/main --no-commit --strategy-option ours --allow-unrelated-histories
-          git restore --staged lean-toolchain lake-manifest.json
+          git restore --staged */lean-toolchain */lake-manifest.json
           git commit --allow-empty -m "chore: merge main into nightly-testing"
           git push origin nightly-testing

.github/workflows/release.yml

@@ -12,17 +12,24 @@ jobs:
   build:
     runs-on: ubuntu-latest
     steps:
-
       - name: Checkout
         uses: actions/checkout@v7
 
-      - name: Install Lean
+      - name: Build UnicodeBasic Docs
+        uses: leanprover/lean-action@v1
+        with:
+          build: true
+          build-args: "--keep-toolchain UnicodeBasic:docs"
+          lake-package-directory: lib
+          test: false
+
+      - name: Build UnicodeData Docs
         uses: leanprover/lean-action@v1
         with:
-          build: false
+          build: true
+          build-args: "--wfail"
+          lake-package-directory: lib
           test: false
-          lint: false
-          use-github-cache: true
 
       - name: Build Docs
         working-directory: docs
@@ -36,7 +43,7 @@ jobs:
           tar -czf docs-${TAG_NAME}.tar.gz doc doc-data
           zip -rq docs-${TAG_NAME}.zip doc doc-data
 
-      - name: Release
+      - name: Upload Release Assets
         uses: softprops/action-gh-release@v3
         with:
           files: |

.github/workflows/update-nightly-toolchain.yml

@@ -9,33 +9,35 @@ jobs:
   update:
     runs-on: ubuntu-latest
     steps:
-
-      - name: checkout
+      - name: Checkout
         uses: actions/checkout@v7
         with:
           ref: nightly-testing
           token: ${{ secrets.UNICODE_BASIC_TOKEN }}
 
-      - name: install jq
+      - name: Install jq
         uses: dcarbone/install-jq-action@v4
 
-      - name: set user
+      - name: Set User
         run: |
           git config user.name "${{ github.actor }}"
           git config user.email "${{ github.actor_id }}+${{ github.actor }}@users.noreply.github.com"
 
-      - name: get toochain tags
+      - name: Get Toolchain Tags
         id: toolchain-tag
         run: |
           LEAN_TAG=$(curl -s "https://api.github.com/repos/leanprover/lean4-nightly/releases" | jq -r '.[0].tag_name')
-          REPO_TAG=$(cut -d ':' -f2 lean-toolchain | tr -d '\n')
+          REPO_TAG=$(cut -d ':' -f2 common/lean-toolchain | tr -d '\n')
           echo "lean_tag=$LEAN_TAG" >> $GITHUB_OUTPUT
           echo "repo_tag=$REPO_TAG" >> $GITHUB_OUTPUT
 
-      - name: commit and push
+      - name: Update Toolchain Files
+        if: ${{ steps.toolchain-tag.outputs.lean_tag != steps.toolchain-tag.outputs.repo_tag }}
+        run: just set-toolchain "${{ steps.toolchain-tag.outputs.lean_tag }}"
+
+      - name: Commit and Push
         if: ${{ steps.toolchain-tag.outputs.lean_tag != steps.toolchain-tag.outputs.repo_tag }}
         run: |
-          echo "leanprover/lean4:${{ steps.toolchain-tag.outputs.lean_tag }}" > lean-toolchain
-          git add lean-toolchain
+          git add common/lean-toolchain lean-scripts/lean-toolchain lib/lean-toolchain table-generators/lean-toolchain tests/lean-toolchain
           git commit -m "chore: update toolchain ${{ steps.toolchain-tag.outputs.lean_tag }}"
           git push origin nightly-testing

.github/workflows/update-toolchain.yml

@@ -10,33 +10,31 @@ jobs:
     name: update toolchain
     runs-on: ubuntu-latest
     steps:
-
-      - name: checkout
+      - name: Checkout
         uses: actions/checkout@v7
         with:
           ref: nightly-testing
           fetch-depth: 0
 
-      - name: install jq
+      # - name: Fetch Main
+      #   run: git fetch origin main:refs/remotes/origin/main --depth=1
+
+      - name: Install jq
         uses: dcarbone/install-jq-action@v4
 
-      - name: get toolchain tags
+      - name: Get Toolchain Tags
         id: toolchain-tag
         run: |
-          REPO_TAG=$(git show main:lean-toolchain | cut -d':' -f2 | tr -d '\n')
+          REPO_TAG=$(git show origin/main:common/lean-toolchain | cut -d':' -f2 | tr -d '\n')
           LEAN_TAG=$(curl -s "https://api.github.com/repos/leanprover/lean4/releases" | jq -r '.[0].tag_name' | tr -d '\n')
           echo "repo_tag=$REPO_TAG" >> $GITHUB_OUTPUT
           echo "lean_tag=$LEAN_TAG" >> $GITHUB_OUTPUT
 
-      - name: update toolchain
-        id: update
+      - name: Update Toolchain Files
         if: ${{ steps.toolchain-tag.outputs.lean_tag != steps.toolchain-tag.outputs.repo_tag }}
-        run: |
-          git config user.name "${{ github.actor }}"
-          git config user.email "${{ github.actor_id }}+${{ github.actor }}@users.noreply.github.com"
-          echo "leanprover/lean4:${{ steps.toolchain-tag.outputs.lean_tag }}" > lean-toolchain
+        run: just set-toolchain "${{ steps.toolchain-tag.outputs.lean_tag }}"
 
-      - name: create pull request
+      - name: Create Pull Request
         if: ${{ steps.toolchain-tag.outputs.lean_tag != steps.toolchain-tag.outputs.repo_tag }}
         uses: peter-evans/create-pull-request@v8
         with:

.gitignore

@@ -1,2 +1,4 @@
-/.lake
+*/.lake/
+tests/.spec-failures
+.data-ucd-download-meta.json
 *~

README.md

@@ -7,26 +7,62 @@ Unicode properties that are currently supported by `UnicodeBasic` include:
 * `Alphabetic`
 * `Bidi_Class`
 * `Bidi_Control`
+* `Bidi_Paired_Bracket`
+* `Bidi_Paired_Bracket_Type`
 * `Bidi_Mirrored`
+* `Bidi_Mirroring_Glyph`
 * `Canonical_Combining_Class`
+* `Case_Folding`
 * `Case_Ignorable`
 * `Cased`
+* `Dash`
 * `Decomposition_Mapping`
 * `Decomposition_Type`
 * `Default_Ignorable_Code_Point`
+* `Diacritic`
+* `East_Asian_Width`
+* `Emoji_Component`
+* `Emoji_Modifier_Base`
+* `Emoji_Modifier`
+* `Emoji_Presentation`
+* `Emoji`
+* `Extended_Pictographic`
+* `Extender`
+* `Block`
 * `General_Category`
+* `Grapheme_Base`
+* `Grapheme_Cluster_Break`
+* `Grapheme_Extend`
 * `Hex_Digit`
+* `Hyphen`
+* `ID_Continue`
+* `ID_Start`
+* `Line_Break`
+* `Lowercase`
 * `Math`
 * `Name`
+* `Noncharacter_Code_Point`
 * `Numeric_Type`
 * `Numeric_Value`
-* `Noncharacter_Code_Point`
+* `Pattern_Syntax`
+* `Pattern_White_Space`
+* `Quotation_Mark`
+* `Regional_Indicator`
+* `Script_Extensions`
+* `Script`
+* `Sentence_Break`
+* `Sentence_Terminal`
+* `Simple_Case_Folding`
 * `Simple_Lowercase_Mapping`
-* `Simple_Uppercase_Mapping`
 * `Simple_Titlecase_Mapping`
-* `Lowercase`
+* `Simple_Uppercase_Mapping`
+* `Terminal_Punctuation`
 * `Uppercase`
 * `White_Space`
+* `Word_Break`
+* `XID_Continue`
+* `XID_Start`
+* `Vertical_Orientation`
 
 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!
 
@@ -39,13 +75,14 @@ Add the following dependency to your project's `lakefile.toml`:
 name = "UnicodeBasic"
 git = "https://github.com/fgdorais/lean4-unicode-basic.git"
 rev = "main" # or any specific revision
+subDir = "lib"
 ```
 
 Or this dependency to your project's `lakefile.lean`:
 
 ```lean4
 require UnicodeBasic from git
-  "https://github.com/fgdorais/lean4-unicode-basic.git" @ "main"
+  "https://github.com/fgdorais/lean4-unicode-basic.git" @ "main" / "lib"
 ```
 
 Then add `import UnicodeBasic` at the top of any Lean file where you plan to use this library.