You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: DEVELOPING.md
+1-1Lines changed: 1 addition & 1 deletion
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -13,7 +13,7 @@ Here is a brief overview of each script in the order they are run in [the CI](.g
13
13
1.[`check_manifest_files.py`](.github/scripts/check_manifest_files.py): this ensures the modules & models recorded in [`manifest.json`](manifest.json) concord with the set of modules & models found under the [`specifications`](specifications) directory, while also respecting the exclusion of any specs in the [`.ciignore`](.ciignore) file.
14
14
1.[`check_manifest_features.py`](.github/scripts/check_manifest_features.py`): this uses the [tree-sitter-tlaplus](https://pypi.org/project/tree-sitter-tlaplus/) python package to run queries on all the `.tla` files and ensure their features (`proof`, `pluscal`, `action composition`) are correctly recorded in [`manifest.json`](manifest.json); it also does best-effort regex parsing of all `.cfg` files to ensure their features (`view`, `alias`, etc.) are similarly correctly recorded.
15
15
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 [`manifest.json`](manifest.json); before this script was developed the table tended to diverge wildly from the actual content of this repo.
16
-
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](https://github.com/tlaplus/tlaplus-standard/tree/652a8eb5d5838b9712be3502cb36dbae826d5689/unicode) form to ensure TLA⁺ tooling functions identically on ASCII & Unicode specs.
16
+
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.
17
17
The CI spawns separate runs with and without conversion of specs to Unicode.
18
18
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.
19
19
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 `ℝ`.
0 commit comments