Documentation now reflects split manifest.json

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

Author: ahelwer

.github/scripts/check_manifest_features.py

@@ -1,6 +1,6 @@
 """
 This script performs whatever validations are possible on the metadata in
-the manifest.json file. Prominent checks include:
+the manifest.json files. Prominent checks include:
  * .tla files containing pluscal or proofs are marked as such
  * .tla files importing community modules have those modules listed
  * .cfg files with certain features are marked as such
@@ -234,7 +234,7 @@ def check_features(parser, queries, manifest, examples_root):
     return success
 
 if __name__ == '__main__':
-    parser = ArgumentParser(description='Checks metadata in tlaplus/examples manifest.json against module and model files in repository.')
+    parser = ArgumentParser(description='Checks metadata in manifest.json files against module and model files in repository.')
     parser.add_argument('--examples_root', help='Root directory of the tlaplus/examples repository', required=True)
     args = parser.parse_args()
 

.github/scripts/check_manifest_files.py

@@ -1,8 +1,8 @@
 """
 Checks to ensure all files in manifest.json exist, that all .tla and .cfg
 files in repo are recorded in manifest.json (except for those in .ciignore),
-and that no files are present twice in the manifest. Also checks to ensure
-no files in .ciignore are in the manifest.json.
+and that no files are present twice in the manifests. Also checks to ensure
+no files in .ciignore are in the manifest.json files.
 """
 
 from argparse import ArgumentParser

.github/scripts/check_markdown_table.py

@@ -1,5 +1,5 @@
 """
-Validates the spec table in README.md, ensuring it matches manifest.json.
+Validates the spec table in README.md, ensuring it matches manifest.json files.
 """
 
 from argparse import ArgumentParser

.github/scripts/check_small_models.py

@@ -1,5 +1,5 @@
 """
-Check all models marked as size "small" in the manifest with TLC. Small
+Check all models marked as size "small" in each manifest with TLC. Small
 models should finish executing in less than ten seconds on the GitHub CI
 machines.
 """

.github/scripts/generate_manifest.py

@@ -1,5 +1,5 @@
 """
-Generates a best-effort manifest.json file. This is done by scanning all
+Generates best-effort manifest.json files. This is done by scanning all
 .tla and .cfg files in the specifications dir then attempting to sort them
 into a spec/module/model hierarchy. Files are parsed to check for features
 and imports. Human-written fields (title/description/source/authors for

.github/scripts/parse_modules.py

@@ -1,5 +1,5 @@
 """
-Parse all modules in the manifest with SANY.
+Parse all modules in the manifests with SANY.
 """
 
 from argparse import ArgumentParser

.github/scripts/record_model_state_space.py

@@ -1,6 +1,6 @@
 """
 Records the number of unique & total states encountered by TLC for each small
-model where that info is not present, then writes it to the manifest.json.
+model where that info is not present, then writes it to a manifest.json file.
 """
 
 from argparse import ArgumentParser

.github/scripts/smoke_test_large_models.py

@@ -1,5 +1,5 @@
 """
-Smoke-test all models not marked as size "small" in the manifest. This
+Smoke-test all models not marked as size "small" in each manifest. This
 entails running them for five seconds to ensure they can actually start
 and work with the spec they're supposed to be modeling.
 """

.github/scripts/unicode_number_set_shim.py

@@ -2,7 +2,7 @@
 While Unicode support in the Java tools goes through a trial period, the core
 Naturals/Integers/Reals modules will remain Unicode-free. So, the Unicode
 number sets ℕ, ℤ, and ℝ must be defined in any module that wishes to use
-them. This script iterates through all modules in the manifest and replaces
+them. This script iterates through all modules in the manifests and replaces
 their imports of the Naturals/Integers/Reals modules with shims containing
 a definition of the Unicode number sets.
 """

CONTRIBUTING.md

@@ -22,26 +22,25 @@ Licensing your contributed specs under MIT is most appreciated, for consistency;
    This makes it clear which model files are associated with which spec.
 1. Include a `README.md` in the spec directory explaining the significance of the spec with links to any relevant websites or publications, or integrate this info as comments in the spec itself.
 
-At this point, you have the option of adding your spec directory to the [`.ciignore`](.ciignore) file to simply contribute the spec files & exclude it from automated validation.
+At this point, you have the option of adding your spec directory to the [`.ciignore`](.ciignore) file to simply contribute the spec files & exclude it from automated validation, although this precludes your spec from the table of CI-validated specs in [`README.md`](README.md).
 Contribution volume is low enough that maintainers will be able to onboard your spec to the validation process eventually.
 However, if you are willing to put in the addition work of onboarding your spec to continuous integration yourself, follow the steps below.
 
 ## Adding Spec to Continuous Integration
 
 All specs & models in this repository are subject to many validation checks; for a full listing, see [`DEVELOPING.md`](DEVELOPING.md).
-While many of these checks concern basic properties like whether the spec parses properly and its models do not crash, they also check whether the spec correctly reflects metadata stored about it in [`manifest.json`](manifest.json) and a table in [`README.md`](README.md).
+While many of these checks concern basic properties like whether the spec parses properly and its models do not crash, they also check whether the spec correctly reflects metadata stored about it in the spec's `manifest.json` file and a table in [`README.md`](README.md).
 
-The central file containing metadata about all specs is [`manifest.json`](manifest.json).
-You will need to add an entry to it for your spec & model files.
+CI validation requires creating a `manifest.json` metadata file in your specification's root directory.
 This can either be done manually (by looking at existing examples) or largely automated using the instructions below; note that if done manually you are very likely to miss tagging your spec with some feature flags detected & enforced by the CI.
-Before submitted your changes to run in the CI, you can quickly check your [`manifest.json`](manifest.json) against the schema [`manifest-schema.json`](manifest-schema.json) at https://www.jsonschemavalidator.net/.
+Before submitted your changes to run in the CI, you can quickly check your `manifest.json` against the schema [`manifest-schema.json`](manifest-schema.json) at https://www.jsonschemavalidator.net/.
 Steps:
 
 1. Ensure you have Python 3.11+ installed; open a terminal in the root of this repository
 1. It is considered best practice to create & initialize a Python virtual environment so the required packages are not installed globally; 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` to auto-generate your spec entry in [`manifest.json`](manifest.json) with as many details as possible
-1. Locate your spec's entry in the [`manifest.json`](manifest.json) file and ensure the following fields are filled out:
+1. Run `python .github/scripts/generate_manifest.py` to auto-generate your spec's `manifest.json` file with as many details as possible
+1. Locate your spec directory's `manifest.json` file and ensure the following fields are filled out:
    - Spec title: an appropriate title for your specification
    - Spec description: a short description of your specification
    - Spec sources: links relevant to the source of the spec (papers, blog posts, repositories)
@@ -69,18 +68,18 @@ Steps:
      - Recording these turns your model into a powerful regression test for TLC
    - Other fields are auto-generated by the script; if you are adding an entry manually, ensure their values are present and correct (see other entries or the [`manifest-schema.json`](manifest-schema.json) file)
 1. Add your spec somewhere in the **topmost** table (not the bottom one, don't get them mixed up!) in [`README.md`](README.md); this must have:
-   - The spec name as a link to the spec's directory, matching the name in the [`manifest.json`](manifest.json)
-   - A comma-separated list of authors, which must also match the list of authors in [`manifest.json`](manifest.json)
+   - The spec name as a link to the spec's directory, matching the name in the `manifest.json`
+   - A comma-separated list of authors, which must also match the list of authors in the `manifest.json`
    - A checkmark indicating whether the spec is appropriate for beginners
-     - Checked IFF (if and only if) `beginner` is present in the `tags` field of your spec in [`manifest.json`](manifest.json)
+     - Checked IFF (if and only if) `beginner` is present in the `tags` field of your spec in `manifest.json`
    - A checkmark indicating whether the spec contains a formal proof
-     - Checked IFF a `proof` tag is present in the `features` field of least one module under your spec in [`manifest.json`](manifest.json)
+     - Checked IFF a `proof` tag is present in the `features` field of least one module under your spec in `manifest.json`
    - A checkmark indicating whether the spec contains PlusCal
-     - Checked IFF a `pluscal` tag is present in the `features` field of least one module under your spec in [`manifest.json`](manifest.json)
+     - Checked IFF a `pluscal` tag is present in the `features` field of least one module under your spec in `manifest.json`
    - A checkmark indicating whether the spec contains a TLC-checkable model
-     - Checked IFF `exhaustive search`, `generate`, or `simulate` tags are present in the `mode` field of at least one model under your spec in [`manifest.json`](manifest.json)
+     - Checked IFF `exhaustive search`, `generate`, or `simulate` tags are present in the `mode` field of at least one model under your spec in `manifest.json`
    - A checkmark indicating whether the spec contains an Apalache-checkable model
-     - Checked IFF `symbolic` tag is present in the `mode` field of at least one model under your spec in [`manifest.json`](manifest.json)
+     - Checked IFF `symbolic` tag is present in the `mode` field of at least one model under your spec in `manifest.json`
 
 At this point you can open a pull request and the CI will run against your spec, alerting you to any details that you missed.
 These scripts can be run locally for a faster development loop; see [`DEVELOPING.md`](DEVELOPING.md) for details.