Use prebuilt python package for tree-sitter-tlaplus

.github/scripts/check_manifest_features.py

@@ -15,6 +15,8 @@
 from typing import Any
 import re
 import tla_utils
+import tree_sitter_tlaplus
+from tree_sitter import Language, Parser
 
 logging.basicConfig(level=logging.INFO)
 
@@ -228,14 +230,16 @@ def check_features(parser, queries, manifest, examples_root):
 if __name__ == '__main__':
     parser = ArgumentParser(description='Checks metadata in tlaplus/examples manifest.json against module and model files in repository.')
     parser.add_argument('--manifest_path', help='Path to the tlaplus/examples manifest.json file', required=True)
-    parser.add_argument('--ts_path', help='Path to tree-sitter-tlaplus directory', required=True)
+    parser.add_argument('--ts_path', help='[DEPRECATED, UNUSED] Path to tree-sitter-tlaplus directory', required=False)
     args = parser.parse_args()
 
     manifest_path = normpath(args.manifest_path)
     manifest = tla_utils.load_json(manifest_path)
     examples_root = dirname(manifest_path)
 
-    (TLAPLUS_LANGUAGE, parser) = tla_utils.build_ts_grammar(normpath(args.ts_path))
+    TLAPLUS_LANGUAGE = Language(tree_sitter_tlaplus.language(), 'tlaplus')
+    parser = Parser()
+    parser.set_language(TLAPLUS_LANGUAGE)
     queries = build_queries(TLAPLUS_LANGUAGE)
 
     if check_features(parser, queries, manifest, examples_root):

.github/scripts/generate_manifest.py

@@ -13,6 +13,8 @@
 from pathlib import PureWindowsPath
 import glob
 import tla_utils
+import tree_sitter_tlaplus
+from tree_sitter import Language, Parser
 
 def to_posix(path):
     """
@@ -165,15 +167,17 @@ def integrate_old_manifest_into_new(old_manifest, new_manifest):
     parser = ArgumentParser(description='Generates a new manifest.json derived from files in the repo.')
     parser.add_argument('--manifest_path', help='Path to the current tlaplus/examples manifest.json file', default='manifest.json')
     parser.add_argument('--ci_ignore_path', help='Path to the CI ignore file', default='.ciignore')
-    parser.add_argument('--ts_path', help='Path to tree-sitter-tlaplus directory', default='tree-sitter-tlaplus')
+    parser.add_argument('--ts_path', help='[DEPRECATED, UNUSED] Path to tree-sitter-tlaplus directory', required=False)
     args = parser.parse_args()
 
     manifest_path = normpath(args.manifest_path)
     examples_root = dirname(manifest_path)
     ci_ignore_path = normpath(args.ci_ignore_path)
     ignored_dirs = tla_utils.get_ignored_dirs(ci_ignore_path)
 
-    (TLAPLUS_LANGUAGE, parser) = tla_utils.build_ts_grammar(normpath(args.ts_path))
+    TLAPLUS_LANGUAGE = Language(tree_sitter_tlaplus.language(), 'tlaplus')
+    parser = Parser()
+    parser.set_language(TLAPLUS_LANGUAGE)
     queries = build_queries(TLAPLUS_LANGUAGE)
 
     old_manifest = tla_utils.load_json(manifest_path)

.github/scripts/linux-setup.sh

@@ -37,10 +37,6 @@ main() {
   fi
   # Put all dependencies in their own directory to ensure they aren't included implicitly
   mkdir -p "$DEPS_DIR"
-  # Get tree-sitter-tlaplus
-  wget -nv https://github.com/tlaplus-community/tree-sitter-tlaplus/archive/main.tar.gz -O /tmp/tree-sitter-tlaplus.tar.gz
-  tar -xzf /tmp/tree-sitter-tlaplus.tar.gz --directory "$DEPS_DIR"
-  mv "$DEPS_DIR/tree-sitter-tlaplus-main" "$DEPS_DIR/tree-sitter-tlaplus"
   # Get TLA⁺ tools
   mkdir -p "$DEPS_DIR/tools"
   wget -nv http://nightly.tlapl.us/dist/tla2tools.jar -P "$DEPS_DIR/tools"

.github/scripts/requirements.txt

@@ -1,4 +1,5 @@
-jsonschema == 4.20.0
-tree-sitter==0.20.4
+jsonschema==4.20.0
 mistletoe==1.2.1
+tree-sitter
+tree-sitter-tlaplus
 

.github/scripts/tla_utils.py

@@ -1,7 +1,6 @@
 from datetime import datetime
 import json
 from os.path import join, normpath, pathsep
-from tree_sitter import Language, Parser
 import subprocess
 import re
 
@@ -51,17 +50,6 @@ def write_json(data, path):
     with open(path, 'w', encoding='utf-8') as file:
         json.dump(data, file, indent=2, ensure_ascii=False)
 
-def build_ts_grammar(ts_path):
-    """
-    Builds the tree-sitter-tlaplus grammar and constructs the parser.
-    """
-    ts_build_path = join(ts_path, 'build', 'tree-sitter-languages.so')
-    Language.build_library(ts_build_path, [ts_path])
-    TLAPLUS_LANGUAGE = Language(ts_build_path, 'tlaplus')
-    parser = Parser()
-    parser.set_language(TLAPLUS_LANGUAGE)
-    return (TLAPLUS_LANGUAGE, parser)
-
 def parse_module(examples_root, parser, path):
     """
     Parses a .tla file; returns the parse tree along with whether a parse

.github/scripts/unicode_number_set_shim.py

@@ -13,6 +13,8 @@
 from os.path import dirname, normpath, join
 import tla_utils
 from typing import List
+import tree_sitter_tlaplus
+from tree_sitter import Language, Parser
 
 logging.basicConfig(level=logging.INFO)
 
@@ -115,7 +117,7 @@ def write_module(examples_root, module_path, module_bytes):
 if __name__ == '__main__':
     parser = ArgumentParser(description='Adds ℕ/ℤ/ℝ Unicode number set shim definitions to modules as needed.')
     parser.add_argument('--manifest_path', help='Path to the tlaplus/examples manifest.json file', required=True)
-    parser.add_argument('--ts_path', help='Path to tree-sitter-tlaplus directory', required=True)
+    parser.add_argument('--ts_path', help='[DEPRECATED, UNUSED] Path to tree-sitter-tlaplus directory', required=False)
     parser.add_argument('--skip', nargs='+', help='Space-separated list of .tla modules to skip', required=False, default=[])
     parser.add_argument('--only', nargs='+', help='If provided, only modify models in this space-separated list', required=False, default=[])
     args = parser.parse_args()
@@ -126,7 +128,9 @@ def write_module(examples_root, module_path, module_bytes):
     skip_modules = [normpath(path) for path in args.skip]
     only_modules = [normpath(path) for path in args.only]
 
-    (TLAPLUS_LANGUAGE, parser) = tla_utils.build_ts_grammar(normpath(args.ts_path))
+    TLAPLUS_LANGUAGE = Language(tree_sitter_tlaplus.language(), 'tlaplus')
+    parser = Parser()
+    parser.set_language(TLAPLUS_LANGUAGE)
     imports_query = build_imports_query(TLAPLUS_LANGUAGE)
 
     modules = [

.github/scripts/windows-setup.sh

@@ -34,11 +34,6 @@ main() {
   fi
   # Put all dependencies in their own directory to ensure they aren't included implicitly
   mkdir -p "$DEPS_DIR"
-  # Get tree-sitter-tlaplus
-  curl -L https://github.com/tlaplus-community/tree-sitter-tlaplus/archive/main.zip --output tree-sitter-tlaplus.zip
-  7z x tree-sitter-tlaplus.zip
-  mv tree-sitter-tlaplus-main "$DEPS_DIR/tree-sitter-tlaplus"
-  rm tree-sitter-tlaplus.zip
   # Get TLA⁺ tools
   mkdir -p "$DEPS_DIR/tools"
   curl http://nightly.tlapl.us/dist/tla2tools.jar --output "$DEPS_DIR/tools/tla2tools.jar"

.github/workflows/CI.yml

@@ -56,8 +56,7 @@ jobs:
       - name: Check manifest feature flags
         run: |
           python "$SCRIPT_DIR/check_manifest_features.py" \
-            --manifest_path manifest.json                 \
-            --ts_path $DEPS_DIR/tree-sitter-tlaplus
+            --manifest_path manifest.json
       - name: Check README spec table
         run: |
           python "$SCRIPT_DIR/check_markdown_table.py"  \
@@ -73,7 +72,6 @@ jobs:
         if: matrix.unicode
         run: |
           python "$SCRIPT_DIR/unicode_number_set_shim.py" \
-            --ts_path "$DEPS_DIR/tree-sitter-tlaplus"     \
             --manifest_path manifest.json
       - name: Translate PlusCal
         if: (!matrix.unicode) # PlusCal does not yet support unicode
@@ -171,10 +169,8 @@ jobs:
             --skip "${SKIP[@]}"
       - name: Smoke-test manifest generation script
         run: |
-          rm -r $DEPS_DIR/tree-sitter-tlaplus/build
           python $SCRIPT_DIR/generate_manifest.py \
             --manifest_path manifest.json         \
-            --ci_ignore_path .ciignore            \
-            --ts_path $DEPS_DIR/tree-sitter-tlaplus
+            --ci_ignore_path .ciignore
           git diff -a
 

README.md

@@ -157,11 +157,8 @@ Follow these instructions:
 To combat bitrot, it is important to add your spec and model to the continuous integration system.
 To do this, you'll have to update the [`manifest.json`](manifest.json) file with machine-readable records of your spec files.
 If this process doesn't work for you, you can alternatively modify the [`.ciignore`](.ciignore) file to exclude your spec from validation.
-Otherwise, follow these directions:
+Modifying the `manifest.json` can be done manually or (recommended) following these directions:
 1. Ensure you have Python 3.11+ installed
-1. Download & extract tree-sitter-tlaplus ([zip](https://github.com/tlaplus-community/tree-sitter-tlaplus/archive/refs/heads/main.zip), [tar.gz](https://github.com/tlaplus-community/tree-sitter-tlaplus/archive/refs/heads/main.tar.gz)) to the root of the repository; ensure the extracted folder is named `tree-sitter-tlaplus`
-1. Open a shell and navigate to the repo root; ensure a C++ compiler is installed and on your path
-   - On Windows, this might entail running the below script from the visual studio developer command prompt
 1. It is considered best practice to create & initialize a Python virtual environment to preserve your system package store; run `python -m venv .` then `source ./bin/activate` on Linux & macOS or `.\Scripts\activate.bat` on Windows (run `deactivate` to exit)
 1. Run `pip install -r .github/scripts/requirements.txt`
 1. Run `python .github/scripts/generate_manifest.py`