From 2445ae9f7085ba1317d41bfd1bf81fd3243cba7b Mon Sep 17 00:00:00 2001
From: Andrew Helwer <ahelwer@users.noreply.github.com>
Date: Wed, 10 Apr 2024 16:42:59 -0400
Subject: [PATCH] Add unicode testing to CI (#135)

* Add unicode testing to CI

Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>
---
 .github/scripts/parse_modules.py | 18 +++++++-----
 .github/workflows/CI.yml         | 50 ++++++++++++++++++++++++++------
 2 files changed, 52 insertions(+), 16 deletions(-)

diff --git a/.github/scripts/parse_modules.py b/.github/scripts/parse_modules.py
index bc76ee17..1d61ad97 100644
--- a/.github/scripts/parse_modules.py
+++ b/.github/scripts/parse_modules.py
@@ -38,13 +38,17 @@ def parse_module(path):
     # Jar paths must go first
     search_paths = pathsep.join([tools_jar_path, dirname(path), community_modules, tlaps_modules])
     sany = subprocess.run([
-        'java',
-        '-cp', search_paths,
-        'tla2sany.SANY',
-        '-error-codes',
-        path
-    ], capture_output=True)
-    output = ' '.join(sany.args) + '\n' + sany.stdout.decode('utf-8')
+            'java',
+            '-cp', search_paths,
+            'tla2sany.SANY',
+            '-error-codes',
+            path
+        ],
+        stdout=subprocess.PIPE,
+        stderr=subprocess.STDOUT,
+        text=True
+    )
+    output = ' '.join(sany.args) + '\n' + sany.stdout
     if 0 == sany.returncode:
         logging.debug(output)
         return True
diff --git a/.github/workflows/CI.yml b/.github/workflows/CI.yml
index 4b1749b2..a338c9c2 100644
--- a/.github/workflows/CI.yml
+++ b/.github/workflows/CI.yml
@@ -15,11 +15,9 @@ jobs:
     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,20 +63,54 @@ 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 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 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
+            --manifest_path manifest.json                                \
+            --skip "${SKIP[@]}"
       - 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                     \
             --community_modules_jar_path $DEPS_DIR/community/modules.jar \
-            --manifest_path manifest.json
+            --manifest_path manifest.json                                \
+            --skip "${SKIP[@]}"
       - name: Smoke-test large models
         run: |
           # SimKnuthYao requires certain number of states to have been generated
@@ -86,7 +118,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 +128,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