From 984afadf45d42d098a8755662eb337d7a627b6bc Mon Sep 17 00:00:00 2001 From: Andrew Helwer <2n8rn1w1f@mozmail.com> Date: Wed, 10 Apr 2024 14:33:52 -0400 Subject: [PATCH 1/6] Add unicode testing to CI Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com> --- .github/workflows/CI.yml | 46 +++++++++++++++++++++++++++++++++------- 1 file changed, 38 insertions(+), 8 deletions(-) diff --git a/.github/workflows/CI.yml b/.github/workflows/CI.yml index 4b1749b2..5161e3c4 100644 --- a/.github/workflows/CI.yml +++ b/.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,8 +63,34 @@ 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 \ @@ -74,6 +98,12 @@ jobs: --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 From 8adc31bf753c1654ea9b07cb8cd0e907e90cf31b Mon Sep 17 00:00:00 2001 From: Andrew Helwer <2n8rn1w1f@mozmail.com> Date: Wed, 10 Apr 2024 14:36:10 -0400 Subject: [PATCH 2/6] Try fix CI Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com> --- .github/workflows/CI.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/CI.yml b/.github/workflows/CI.yml index 5161e3c4..f7a00d85 100644 --- a/.github/workflows/CI.yml +++ b/.github/workflows/CI.yml @@ -12,7 +12,7 @@ on: jobs: validate: name: Validate Manifest, Specs, & Models - runs-on: matrix.os + runs-on: ${{ matrix.os }} strategy: matrix: # macOS not used; see https://github.com/tlaplus/Examples/issues/119 From 1e6fb310ac7e5a67cb65902431306f4260c799fa Mon Sep 17 00:00:00 2001 From: Andrew Helwer <2n8rn1w1f@mozmail.com> Date: Wed, 10 Apr 2024 15:43:53 -0400 Subject: [PATCH 3/6] Fix path to manifest Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com> --- .github/workflows/CI.yml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/CI.yml b/.github/workflows/CI.yml index f7a00d85..a47b3d1d 100644 --- a/.github/workflows/CI.yml +++ b/.github/workflows/CI.yml @@ -12,7 +12,7 @@ on: jobs: validate: name: Validate Manifest, Specs, & Models - runs-on: ${{ matrix.os }} + runs-on: matrix.os strategy: matrix: # macOS not used; see https://github.com/tlaplus/Examples/issues/119 @@ -68,13 +68,13 @@ jobs: run: | python "$SCRIPT_DIR/unicode_conversion.py" \ --tlauc_path "$DEPS_DIR/tlauc/tlauc" \ - --manifest_path "$EXAMPLES_DIR/manifest.json" + --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 "$EXAMPLES_DIR/manifest.json" + --manifest_path manifest.json - name: Parse all modules run: | # Need to have a nonempty list to pass as a skip parameter From 6dda33831253f6357f9636e2a3fb763ce1244b66 Mon Sep 17 00:00:00 2001 From: Andrew Helwer <2n8rn1w1f@mozmail.com> Date: Wed, 10 Apr 2024 15:46:40 -0400 Subject: [PATCH 4/6] Fix runs-on Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com> --- .github/workflows/CI.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/CI.yml b/.github/workflows/CI.yml index a47b3d1d..3e740990 100644 --- a/.github/workflows/CI.yml +++ b/.github/workflows/CI.yml @@ -12,7 +12,7 @@ on: jobs: validate: name: Validate Manifest, Specs, & Models - runs-on: matrix.os + runs-on: ${{ matrix.os }} strategy: matrix: # macOS not used; see https://github.com/tlaplus/Examples/issues/119 From aa4fc2018bb3d7199047335ab570eb0c038e0eda Mon Sep 17 00:00:00 2001 From: Andrew Helwer <2n8rn1w1f@mozmail.com> Date: Wed, 10 Apr 2024 15:54:55 -0400 Subject: [PATCH 5/6] Skip some modules Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com> --- .github/workflows/CI.yml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/.github/workflows/CI.yml b/.github/workflows/CI.yml index 3e740990..a338c9c2 100644 --- a/.github/workflows/CI.yml +++ b/.github/workflows/CI.yml @@ -95,7 +95,8 @@ jobs: --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 @@ -108,7 +109,8 @@ jobs: --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 From b0b22016a46211564143db4473d299d74312b889 Mon Sep 17 00:00:00 2001 From: Andrew Helwer <2n8rn1w1f@mozmail.com> Date: Wed, 10 Apr 2024 16:04:13 -0400 Subject: [PATCH 6/6] Change sany output encoding Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com> --- .github/scripts/parse_modules.py | 18 +++++++++++------- 1 file changed, 11 insertions(+), 7 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