CI: Use TLAUC --skip numsets instead of unicode_number_set_shim.py

Use feature introduced in tlaplus-community/tlauc#23

Before these changes, the unicode_number_set_shim.py script was needed to rewrite all specs so they would import a shim version of the Naturals, Integers, and Reals standard modules that defined the ℕ, ℤ, and ℝ number sets. This was a very involved and brittle process, although it did showcase the power of the tree-sitter grammar queries. Now we can simply skip translating those number sets until tlaplus/tlaplus#1020 is fixed. Thus there is no need for the shim script.

Signed-off-by: Andrew Helwer <ahelwer@pm.me>

Author: ahelwer

.github/scripts/unicode_conversion.py

@@ -45,7 +45,7 @@
 def convert_module(module_path):
     logging.info(f'Converting {module_path}')
     result = subprocess.run(
-        [tlauc_path, module_path] + (['--ascii'] if to_ascii else []),
+        [tlauc_path, module_path, '--skip', 'numsets'] + (['--ascii'] if to_ascii else []),
         stdout=subprocess.PIPE,
         stderr=subprocess.STDOUT,
         text=True

.github/scripts/unicode_number_set_shim.py

@@ -67,11 +67,6 @@ jobs:
           python "$SCRIPT_DIR/unicode_conversion.py"  \
             --tlauc_path "$DEPS_DIR/tlauc/tlauc"      \
             --examples_root .
-      - name: Add unicode shims
-        if: matrix.unicode
-        run: |
-          python "$SCRIPT_DIR/unicode_number_set_shim.py" \
-            --examples_root .
       - name: Translate PlusCal
         # PlusCal translations will be reverted at the end of this step,
         # since we want to support people manually editing the generated TLA+

.github/workflows/CI.yml

@@ -15,9 +15,6 @@ Here is a brief overview of each script in the order they are run in [the CI](.g
 1. [`check_markdown_table.py`](.github/scripts/check_markdown_table.py): this uses the [mistletoe](https://pypi.org/project/mistletoe/) markdown parser python package to parse [`README.md`](README.md), extract the spec table, then validate its format & contents against each `manifest.json`; before this script was developed the table tended to diverge wildly from the actual content of this repo.
 1. [`unicode_conversion.py`](.github/scripts/unicode_conversion.py): this script uses [tlauc](https://github.com/tlaplus-community/tlauc) to convert each spec into its Unicode form to ensure TLA⁺ tooling functions identically on ASCII & Unicode specs.
    The CI spawns separate runs with and without conversion of specs to Unicode.
-1. [`unicode_number_set_shim.py`](.github/scripts/unicode_number_set_shim.py): since Unicode adoption is not yet fully ratified, Unicode definitions like `ℕ`, `ℤ`, and `ℝ` (as synonyms for `Nat`, `Int`, and `Real` respectively) are not yet included in the standard modules.
-   This script works around that by using the [tree-sitter-tlaplus](https://pypi.org/project/tree-sitter-tlaplus/) python package to rewrite all imports of the `Naturals`, `Integers`, and `Reals` modules to import shim modules instead that define `ℕ`, `ℤ`, and `ℝ`.
-   Once TLA⁺ fully adopts Unicode this (quite hackish) script will no longer be necessary.
 1. [`translate_pluscal.py`](.github/scripts/translate_pluscal.py): this script runs the PlusCal translator on all modules containing PlusCal, to ensure their PlusCal syntax is valid.
 1. [`parse_modules.py`](.github/scripts/parse_modules.py): this script runs the SANY parser against all `.tla` files in the repository to ensure they are syntactically & semantically valid.
    This can get quite complicated as many modules import specs defined in Apalache, TLAPM, or the community modules.
@@ -69,14 +66,10 @@ python .github/scripts/check_manifest_features.py --examples_root .
 ```sh
 python .github/scripts/check_markdown_table.py --readme_path README.md
 ```
-**WARNING:** the `unicode_conversion.py`, `unicode_number_set_shim.py`, and `translate_pluscal.py` scripts make large numbers of changes to files in your local repository, so be sure to run them on a clean branch where your own changes can't be clobbered and you can easily revert with `git reset --hard HEAD`.
+**WARNING:** the `unicode_conversion.py` and `translate_pluscal.py` scripts make large numbers of changes to files in your local repository, so be sure to run them on a clean branch where your own changes can't be clobbered and you can easily revert with `git reset --hard HEAD`.
 ```sh
 python .github/scripts/unicode_conversion.py --tlauc_path deps/tlauc/tlauc --examples_root .
 ```
-Delete all the shim files generated by `unicode_number_set_shim.py` with `find . -iname "*_UnicodeShim.tla" -delete`.
-```sh
-python .github/scripts/unicode_number_set_shim.py --examples_root .
-```
 ```sh
 python .github/scripts/translate_pluscal.py --tools_jar_path deps/tools/tla2tools.jar --examples_root .
 ```