Add unicode testing to CI (#135)

* Add unicode testing to CI

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

.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

.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,28 +63,62 @@ 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
           # before termination or else it fails. This makes it not amenable to
           # 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