chore: merge main

Author: fgdorais

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

@@ -0,0 +1,28 @@
+# Push every commit to `main` into `nightly-testing`
+
+name: Push to Nightly
+
+on:
+  push:
+    branches: ["main"]
+
+jobs:
+  push-to-nightly:
+    runs-on: ubuntu-latest
+    steps:
+
+      - name: checkout repo
+        uses: actions/checkout@v6
+        with:
+          ref: nightly-testing
+          fetch-depth: 0
+          token: ${{ secrets.UNICODE_BASIC_TOKEN }}
+
+      - name: merge main
+        run: |
+          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 commit --allow-empty -m "chore: merge main into nightly-testing"
+          git push origin nightly-testing

.github/workflows/release.yml

@@ -37,7 +37,7 @@ jobs:
           zip -rq docs-${TAG_NAME}.zip doc doc-data
 
       - name: Release
-        uses: softprops/action-gh-release@v2
+        uses: softprops/action-gh-release@v3
         with:
           files: |
             docs/docs-${{ github.ref_name }}.tar.gz

.github/workflows/update-nightly.yml …b/workflows/update-nightly-toolchain.yml.github/workflows/update-nightly.yml renamed to .github/workflows/update-nightly-toolchain.yml .github/workflows/update-nightly.yml renamed to .github/workflows/update-nightly-toolchain.yml

@@ -1,9 +1,9 @@
-name: Update Nightly Testing
+name: Update Nightly Toolchain
 
 on:
+  workflow_dispatch:
   schedule:
     - cron: '0 9 * * *'
-  workflow_dispatch:
 
 jobs:
   update:
@@ -22,22 +22,20 @@ jobs:
       - name: set user
         run: |
           git config user.name "${{ github.actor }}"
-          git config user.email "${{ github.actor_id}}+${{ github.actor }}@users.noreply.github.com"
-
-      - name: merge main
-        run: |
-          git fetch origin
-          git merge origin/main --strategy-option theirs --no-commit --allow-unrelated-histories
+          git config user.email "${{ github.actor_id }}+${{ github.actor }}@users.noreply.github.com"
 
-      - name: update lean-toolchain
+      - name: get toochain 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')
           echo "lean_tag=$LEAN_TAG" >> $GITHUB_OUTPUT
-          echo "leanprover/lean4:$LEAN_TAG" > lean-toolchain
-          git add lean-toolchain
+          echo "repo_tag=$REPO_TAG" >> $GITHUB_OUTPUT
 
       - 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 commit -m "chore: update toolchain ${{ steps.toolchain-tag.outputs.lean_tag }}"
           git push origin nightly-testing

.github/workflows/update-toolchain.yml

@@ -14,6 +14,7 @@ jobs:
       - name: checkout
         uses: actions/checkout@v6
         with:
+          ref: nightly-testing
           fetch-depth: 0
 
       - name: install jq
@@ -22,7 +23,7 @@ jobs:
       - name: get toolchain tags
         id: toolchain-tag
         run: |
-          REPO_TAG=$(sed 's/.*://1' lean-toolchain | tr -d '\n')
+          REPO_TAG=$(git show main: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
@@ -32,15 +33,16 @@ jobs:
         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"
-          git merge -X theirs origin/nightly-testing
+          git config user.email "${{ github.actor_id }}+${{ github.actor }}@users.noreply.github.com"
           echo "leanprover/lean4:${{ steps.toolchain-tag.outputs.lean_tag }}" > lean-toolchain
 
       - 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:
           token: ${{ secrets.UNICODE_BASIC_TOKEN }}
           commit-message: "chore: update toolchain ${{ steps.toolchain-tag.outputs.lean_tag }}"
           branch: update-toolchain-${{ steps.toolchain-tag.outputs.lean_tag }}
+          base: main
           delete-branch: true
           title: "chore: update toolchain ${{ steps.toolchain-tag.outputs.lean_tag }}"

UnicodeBasic.lean

@@ -51,7 +51,7 @@ namespace Unicode
 /-- Get character name
 
   When the Unicode property `Name` is empty, a unique code label is returned
-  as described in Unicode Standard, section 4.8. These labels start with
+  as recommended in Unicode Standard, section 4.8. These labels start with
   `'<'` (U+003C) and end with `'>'` (U+003E) so they are distinguishable from
   actual name values.
 
@@ -60,6 +60,27 @@ namespace Unicode
 @[inline]
 def getName (char : Char) : String := lookupName char.val
 
+/-!
+  ## Script ##
+-/
+
+/-- Get character script
+
+  Unicode property: `Script`
+-/
+@[inline]
+def getScript (char : Char) : Script := lookupScript char.val
+
+/-- Get script name
+
+  Returns `none` if the script code is unassigned.
+
+  Unicode property: `Script`
+-/
+@[inline]
+def getScriptName? (s : Script) : Option String :=
+  lookupScriptName s |>.map toString
+
 /-!
   ## Bidirectional Properties ##
 -/

UnicodeBasic/TableLookup.lean

@@ -23,6 +23,9 @@ protected abbrev oMath  : UInt64 := 0x800000000
 @[extern "unicode_prop_lookup"]
 protected opaque lookupProp (c : UInt32) : UInt64
 
+@[extern "unicode_script_lookup"]
+protected opaque lookupScript (c : UInt32) : Script
+
 end CLib
 
 /-- Binary search -/
@@ -387,4 +390,22 @@ where
   str : String := include_str "../data/table/White_Space.txt"
   table : Thunk <| Array (UInt32 × UInt32) := parsePropTable str
 
+/-- Get the script of a code point using lookup table
+
+  Unicode property: `Script` -/
+@[inline]
+def lookupScript (c : UInt32) : Script := CLib.lookupScript c
+
+/-- Get the name of a script
+
+  Unicode property: `Script` -/
+def lookupScriptName (s : Script) : Option String.Slice :=
+  let table := table.get
+  if s.code < table[0]!.1 then none else
+    match table[find s.code (fun i => table[i]!.1) 0 table.size.toUSize]! with
+    | (c, v) => if s.code = c then some v else none
+where
+  str : String := include_str "../data/table/Script_Name.txt"
+  table : Thunk <| Array (UInt32 × String.Slice) := parseTable str fun _ n => n[0]!
+
 end Unicode

UnicodeBasic/Types.lean

@@ -3,7 +3,10 @@ Copyright © 2023-2025 François G. Dorais. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 -/
 module
+public import Std.Data.HashMap
+
 public section
+
 /-- Low-level conversion from `UInt32` to `Char` (*unsafe*)
 
   This function translates to a no-op in the compiler. However, it does not
@@ -1014,5 +1017,65 @@ def BidiClass.ofAbbrev! (abbr : String.Slice) : BidiClass :=
 instance : Repr BidiClass where
   reprPrec bc _ := s!"Unicode.BidiClass.{bc.toAbbrev}"
 
+/-!
+  ## Scripts ##
+-/
+
+/-- Check if valid script identifier -/
+@[inline]
+def Script.isValid (c : UInt32) : Bool :=
+  let c0 := (c >>> 24).toUInt8
+  let c1 := (c >>> 16).toUInt8
+  let c2 := (c >>> 8).toUInt8
+  let c3 := c.toUInt8
+  (c0 ≤ 'Z'.toUInt8 && 'A'.toUInt8 ≤ c0)
+    && (c1 ≤ 'z'.toUInt8 && 'a'.toUInt8 ≤ c1)
+      && (c2 ≤ 'z'.toUInt8 && 'a'.toUInt8 ≤ c2)
+        && (c3 ≤ 'z'.toUInt8 && 'a'.toUInt8 ≤ c3)
+
+/-- Script identifier type -/
+structure Script where
+  code : UInt32
+  is_valid : Script.isValid code
+deriving DecidableEq, Hashable
+
+namespace Script
+
+/-- Default value is `Zzzz` (`Unknown`) -/
+instance : Inhabited Script where
+  default := {
+    code := (((('Z'.val <<< 8 ||| 'z'.val) <<< 8) ||| 'z'.val) <<< 8) ||| 'z'.val
+    is_valid := by decide
+  }
+
+/-- String abbreviation of script -/
+@[extern "unicode_script_to_abbrev"]
+def toAbbrev : Script → String
+  | ⟨c, _⟩ =>
+    let c0 := Char.ofUInt8 (c >>> 24).toUInt8
+    let c1 := Char.ofUInt8 (c >>> 16).toUInt8
+    let c2 := Char.ofUInt8 (c >>> 8).toUInt8
+    let c3 := Char.ofUInt8 c.toUInt8
+    String.ofList [c0, c1, c2, c3]
+
+@[extern "unicode_script_of_abbrev"]
+private opaque ofAbbrevAux (abbr : String) : UInt32
+
+/-- Get script from abbreviation -/
+def ofAbbrev? (abbr : String.Slice) : Option Script :=
+  if abbr.utf8ByteSize = 4 then
+    let code := ofAbbrevAux abbr.toString
+    if h : Script.isValid code then
+      some ⟨code, h⟩
+    else
+      none
+  else
+    none
+
+@[inline, inherit_doc ofAbbrev?]
+def ofAbbrev! (abbr : String.Slice) : Script := ofAbbrev? abbr |>.get!
+
+end Script
+
 end Unicode
 end

UnicodeCLib/basic.c

@@ -0,0 +1,34 @@
+#include <lean/lean.h>
+#ifdef _WIN32
+#include <winsock2.h>
+#else
+#include <arpa/inet.h>
+#endif
+#include "basic.h"
+
+static inline int unicode_script_is_valid(uint32_t c) {
+  int c0 = (int)(c >> 24 & 0xff);
+  int c1 = (int)(c >> 16 & 0xff);
+  int c2 = (int)(c >> 8 & 0xff);
+  int c3 = (int)(c & 0xff);
+  return
+    c0 <= 'Z' && 'A' <= c0 &&
+    c1 <= 'z' && 'a' <= c1 &&
+    c2 <= 'z' && 'a' <= c2 &&
+    c3 <= 'z' && 'a' <= c3;
+}
+
+uint32_t unicode_script_of_abbrev(b_lean_obj_arg abbr) {
+  lean_string_object * str = lean_to_string(abbr);
+  assert(str->m_size > 4);
+  uint32_t val = *((uint32_t*)(str->m_data));
+  return ntohl(val);
+}
+
+lean_obj_res unicode_script_to_abbrev(uint32_t scr) {
+  assert(unicode_script_is_valid(scr));
+  lean_object * abbr = lean_alloc_string(5, 5, 4);
+  lean_to_string(abbr)->m_data[4] = 0;
+  *((uint32_t*)lean_to_string(abbr)->m_data) = htonl(scr);
+  return abbr;
+}

UnicodeCLib/basic.h

@@ -69,6 +69,12 @@ LEAN_EXPORT uint64_t unicode_prop_lookup(uint32_t c);
 
 LEAN_EXPORT uint64_t unicode_case_lookup(uint32_t c);
 
+LEAN_EXPORT uint32_t unicode_script_lookup(uint32_t c);
+
+LEAN_EXPORT uint32_t unicode_script_of_abbrev(b_lean_obj_arg abbr);
+
+LEAN_EXPORT lean_obj_res unicode_script_to_abbrev(uint32_t scr);
+
 #ifdef __cplusplus
 }
 #endif