chore: restore history

Author: fgdorais

.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-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,8 +33,7 @@ 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
@@ -43,5 +43,6 @@ jobs:
           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

@@ -58,6 +58,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

@@ -22,6 +22,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 -/
@@ -386,4 +389,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,6 +3,8 @@ Copyright © 2023-2025 François G. Dorais. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 -/
 
+import Std.Data.HashMap
+
 /-- Low-level conversion from `UInt32` to `Char` (*unsafe*)
 
   This function translates to a no-op in the compiler. However, it does not
@@ -1011,4 +1013,64 @@ 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

UnicodeCLib/basic.c

@@ -1,5 +1,9 @@
 #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) {

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

UnicodeData.lean

@@ -6,3 +6,4 @@ Released under Apache 2.0 license as described in the file LICENSE.
 import UnicodeData.Aliases
 import UnicodeData.Basic
 import UnicodeData.PropList
+import UnicodeData.Scripts

lakefile.lean

@@ -62,4 +62,5 @@ script updateUCD do downloadUCD [
     "PropList.txt",
     "PropertyAliases.txt",
     "PropertyValueAliases.txt",
+    "Scripts.txt",
   ]

makeCLib.lean

@@ -191,7 +191,45 @@ static const unicode_data_t table[] = {"
       file.putStrLn s!"\{UINT32_C({c₀}),UINT32_C({c₁}),UINT64_C({d})},"
     file.putStrLn "};"
 
+def scriptTable : Array (UInt32 × UInt32 × UInt64) :=
+  let t := Scripts.data.toArray.flatMap fun (sc, t) =>
+    let sc := Script.ofAbbrev! <| PropertyValueAliases.getShortName! "sc" sc
+    t.map fun (c₀, c₁) => (c₀, c₁, sc.code.toUInt64)
+  t.qsort fun (a, _) (b, _) => a < b
+
+def makeScriptC : IO Unit :=
+  IO.FS.withFile (clibDir / "script.c") .write fun file => do
+    file.putStrLn s!"/* THIS IS A GENERATED FILE - DO NOT EDIT */
+#include \"basic.h\"
+
+#define TABLE_SIZE {scriptTable.size}
+#define SCRIPT_UNKNOWN UINT32_C({Script.ofAbbrev! "Zzzz" |>.code})"
+    file.putStrLn "
+static const unicode_data_t table[TABLE_SIZE];
+
+uint32_t unicode_script_lookup(uint32_t c) {
+  unicode_data_t v;
+  if (c >= table[0].cmin) {
+    unsigned int lo = 0;
+    unsigned int hi = TABLE_SIZE;
+    unsigned int i = (lo + hi)/2;
+    while (i != lo) {
+      if (c < table[i].cmin) hi = i;
+      else lo = i;
+      i = (lo + hi)/2;
+    }
+    if (c <= table[i].cmax) return (uint32_t)table[i].data;
+  }
+  return SCRIPT_UNKNOWN;
+}
+
+static const unicode_data_t table[] = {"
+    for (c₀, c₁, d) in scriptTable do
+      file.putStrLn s!"\{UINT32_C({c₀}),UINT32_C({c₁}),UINT64_C({d})},"
+    file.putStrLn "};"
+
 def main : IO UInt32 := do
   makeCaseC
   makePropC
+  makeScriptC
   return 0