Setting Up Your Development Environment
Relevant source files
The following files were used as context for generating this wiki page:This document provides instructions for setting up a local development environment to work with the TLA⁺ Examples repository. The environment is primarily focused on running the same validation scripts used by the Continuous Integration (CI) system. This allows contributors to validate their TLA⁺ specifications locally before submitting a pull request, ensuring that new specs meet the repository's quality standards.
The setup involves installing Python, creating a virtual environment, installing required packages, and downloading the necessary TLA⁺ tooling. Once set up, you can run a suite of scripts to check everything from manifest.json metadata to model checking and proof validation. For instructions on how to contribute a new specification, please see the Contribution Guide.
Sources: DEVELOPING.md:3-6, CONTRIBUTING.md:8-13
Initial Setup
The local development setup relies on Python scripts to orchestrate the validation tasks. The first step is to prepare your local machine with the necessary dependencies and tooling.
Sources: DEVELOPING.md:78-84
Prerequisites
- Python 3.11+: Ensure you have a compatible version of Python installed.
- TLA⁺ Toolbox: While not strictly required for running the validation scripts, the TLA⁺ Toolbox is essential for writing and debugging the TLA⁺ specifications themselves.
Sources: CONTRIBUTING.md:31, specifications/PaxosHowToWinATuringAward/README.txt:20-22
Environment Configuration
The following diagram illustrates the steps to configure your local environment.
This flowchart shows the sequence of commands to prepare the local development environment.
Sources: DEVELOPING.md:78-90, CONTRIBUTING.md:32-34
-
Create and Activate a Python Virtual Environment: It is best practice to use a virtual environment to avoid installing packages globally.
- Create the environment:
python -m venv . - Activate the environment:
- Linux & macOS:
source ./bin/activate - Windows:
.\Scripts\activate.bat
- Linux & macOS:
Sources: CONTRIBUTING.md:33
- Create the environment:
-
Install Python Dependencies: Install the required Python packages using the provided requirements file.
pip install -r .github/scripts/requirements.txtSources: CONTRIBUTING.md:34
-
Download TLA⁺ Tooling: Run the setup script for your operating system. This will download dependencies like
tla2tools.jar,apalache,tlauc, and community modules into adepsdirectory.- Linux & macOS:
./.github/scripts/linux-setup.sh .github/scripts deps true - Windows:
.\.github\scripts\windows-setup.sh .github\scripts deps true
Sources: DEVELOPING.md:79-84
- Linux & macOS:
Validation and Utility Scripts
The repository contains a suite of Python scripts located in .github/scripts for validation and maintenance. These scripts are the same ones run by the CI pipeline. Running them locally provides a faster development loop.
Sources: DEVELOPING.md:8-10
CI Validation Scripts
These scripts are run in order by the CI to validate every aspect of a contributed specification. Most scripts accept --skip and --only parameters to target specific files, and a --verbose flag for detailed output.
The following diagram shows the sequence of validation checks performed by the CI scripts.
This graph outlines the execution order of the primary validation scripts in the CI pipeline.
Sources: DEVELOPING.md:11-41
| Script | Description | Local Run Command |
|---|---|---|
check_manifest_schema.py | Validates manifest.json files against the manifest-schema.json. | python .github/scripts/check_manifest_schema.py --schema_path manifest-schema.json |
check_manifest_files.py | Ensures modules and models in manifest.json match the files on disk. | python .github/scripts/check_manifest_files.py --ci_ignore_path .ciignore |
check_manifest_features.py | Checks that features (e.g., pluscal, proof) are correctly recorded in manifest.json. | python .github/scripts/check_manifest_features.py --examples_root . |
check_markdown_table.py | Validates the format and content of the spec table in README.md against manifest.json files. | python .github/scripts/check_markdown_table.py --readme_path README.md |
unicode_conversion.py | Converts specs to Unicode form to test tooling. Warning: Modifies local files. | python .github/scripts/unicode_conversion.py --tlauc_path deps/tlauc/tlauc --examples_root . |
translate_pluscal.py | Runs the PlusCal translator on all relevant modules. Warning: Modifies local files. | python .github/scripts/translate_pluscal.py --tools_jar_path deps/tools/tla2tools.jar --examples_root . |
parse_modules.py | Runs the SANY parser on all .tla files to check for syntax and semantic errors. | python .github/scripts/parse_modules.py --tools_jar_path deps/tools/tla2tools.jar ... |
check_small_models.py | Runs TLC or Apalache on models expected to complete within 30 seconds. | python .github/scripts/check_small_models.py --tools_jar_path deps/tools/tla2tools.jar ... |
smoke_test_large_models.py | Runs larger models for 5 seconds to ensure they don't crash immediately. | python .github/scripts/smoke_test_large_models.py --tools_jar_path deps/tools/tla2tools.jar ... |
check_proofs.py | Runs TLAPM against modules containing formal proofs. (Does not run on Windows). | python .github/scripts/check_proofs.py --tlapm_path deps/tlapm --examples_root . |
Sources: DEVELOPING.md:11-76, DEVELOPING.md:91-118
Utility Scripts
These scripts are not part of the standard CI validation but provide helpful automation for developers and contributors.
| Script | Description | Local Run Command |
|---|---|---|
generate_manifest.py | Auto-generates a manifest.json file for a new specification by parsing its files. | python .github/scripts/generate_manifest.py --ci_ignore_path .ciignore |
record_model_state_space.py | Runs small models and records their state space information into the manifest.json. | python .github/scripts/record_model_state_space.py --tools_jar_path deps/tools/tla2tools.jar ... |
format_markdown_table.py | A helper script to format the spec table in README.md. | Not typically run directly by contributors. |
Sources: DEVELOPING.md:43-55, DEVELOPING.md:119-124
Contributing a New Specification
When contributing a new specification, the local development environment is used to prepare the spec and its metadata for the CI checks.
The following diagram shows the workflow for a contributor adding a new spec.
This sequence diagram details the steps for contributing a new specification using the local development scripts.
Sources: CONTRIBUTING.md:16-70
The key steps involve:
- Adding your spec files to a new directory under
specifications/. - Running
generate_manifest.pyto create the initialmanifest.json. - Manually editing
manifest.jsonto add details like authors, tags, and model runtimes/results. - Adding an entry for your spec in the main table in
README.md. - Running the validation scripts locally to catch any inconsistencies before pushing.
Sources: CONTRIBUTING.md:16-70
Summary
Setting up a local development environment that mirrors the CI pipeline is a crucial part of contributing to the TLA⁺ Examples repository. It empowers developers to verify their changes thoroughly, ensuring that all specifications and their associated metadata are consistent and correct. By following the steps to configure the environment and run the validation scripts, contributors can streamline the submission process and help maintain the high quality of this valuable resource for the TLA⁺ community.
Sources: DEVELOPING.md:3-6, CONTRIBUTING.md:8-13