Add unicode testing to CI

Signed-off-by: Andrew Helwer <[email protected]>

.github/workflows/CI.yml

@@ -12,14 +12,12 @@ on:
 jobs:
   validate:
     name: Validate Manifest, Specs, & Models
-    runs-on: ${{ matrix.os }}
+    runs-on: matrix.os
     strategy:
       matrix:
-        include:
-        - { os: windows-latest }
-        - { os: ubuntu-latest }
-        # https://github.com/tlaplus/Examples/issues/119
-        #- { os: macos-14 }
+        # macOS not used; see https://github.com/tlaplus/Examples/issues/119
+        os: [windows-latest, ubuntu-latest]
+        unicode: [true, false]
       fail-fast: false
     env:
       SCRIPT_DIR: .github/scripts
@@ -65,15 +63,47 @@ jobs:
           python $SCRIPT_DIR/check_markdown_table.py  \
             --manifest_path manifest.json             \
             --readme_path README.md
+      - name: Convert specs to unicode
+        if: matrix.unicode
+        run: |
+          python "$SCRIPT_DIR/unicode_conversion.py"  \
+            --tlauc_path "$DEPS_DIR/tlauc/tlauc"      \
+            --manifest_path "$EXAMPLES_DIR/manifest.json"
+      - name: Add unicode shims
+        if: matrix.unicode
+        run: |
+          python "$SCRIPT_DIR/unicode_number_set_shim.py" \
+            --ts_path "$DEPS_DIR/tree-sitter-tlaplus"     \
+            --manifest_path "$EXAMPLES_DIR/manifest.json"
       - name: Parse all modules
         run: |
+          # Need to have a nonempty list to pass as a skip parameter
+          SKIP=("does/not/exist")
+          if [ ${{ matrix.unicode }} ]; then
+            # These redefine Nat, Int, or Real so cannot be shimmed
+            SKIP+=(
+              "specifications/SpecifyingSystems/Standard/Naturals.tla"
+              "specifications/SpecifyingSystems/Standard/Peano.tla"
+              "specifications/SpecifyingSystems/Standard/Integers.tla"
+              "specifications/SpecifyingSystems/Standard/Reals.tla"
+              "specifications/SpecifyingSystems/Standard/ProtoReals.tla"
+              "specifications/SpecifyingSystems/RealTime/MCRealTime.tla"
+              "specifications/SpecifyingSystems/RealTime/MCRealTimeHourClock.tla"
+            )
+          fi
           python $SCRIPT_DIR/parse_modules.py                            \
             --tools_jar_path $DEPS_DIR/tools/tla2tools.jar               \
             --tlapm_lib_path $DEPS_DIR/tlapm/library                     \
             --community_modules_jar_path $DEPS_DIR/community/modules.jar \
             --manifest_path manifest.json
       - name: Check small models
         run: |
+          # Need to have a nonempty list to pass as a skip parameter
+          SKIP=("does/not/exist")
+          if [ ${{ matrix.unicode }} ]; then
+            # This redefines Real so cannot be shimmed
+            SKIP+=("specifications/SpecifyingSystems/RealTime/MCRealTimeHourClock.cfg")
+          fi
           python $SCRIPT_DIR/check_small_models.py                       \
             --tools_jar_path $DEPS_DIR/tools/tla2tools.jar               \
             --tlapm_lib_path $DEPS_DIR/tlapm/library                     \
@@ -86,7 +116,7 @@ jobs:
           # smoke testing.
           SKIP=("specifications/KnuthYao/SimKnuthYao.cfg")
           # SimTokenRing does not work on Windows systems.
-          if [[ "${{ runner.os }}" == "Windows" ]]; then
+          if [[ "${{ matrix.os }}" == "windows-latest" ]]; then
             SKIP+=("specifications/ewd426/SimTokenRing.cfg")
           fi
           python $SCRIPT_DIR/smoke_test_large_models.py                  \
@@ -96,7 +126,7 @@ jobs:
             --manifest_path manifest.json                                \
             --skip "${SKIP[@]}"
       - name: Check proofs
-        if: matrix.os != 'windows-latest'
+        if: matrix.os != 'windows-latest' && !matrix.unicode
         run: |
           SKIP=(
             # Failing; see https://github.com/tlaplus/Examples/issues/67