Repository navigation
Simplify contribution process #171
Description
While the contribution process gives us some nice testing & consistency benefits, currently it is too complicated. As evidence for this, at least one contributor has given up instead of trying to add their spec (see #147). While this is before I wrote in-depth contribution documentation in #164, writing that document made me realize the process is quite complicated and likely more than we can expect from most users.
Here is some consideration about the value we get from the current process, which would ideally be maintained when transitioning to an easier process:
- Ensuring all specs parse correctly and all models model-check correctly, so users who want to look at TLA+ examples can be assured they will not be misled by incorrect specs or models.
- Ability to programmatically filter specs & models according to various properties, enabling ease of scripting additional tests (both within this repository and for users developing their own tools who consume this repository) without having to create & maintain a bash file hard-coding the desired behavior for each spec
- A largely automatically-validated manifest file containing many interesting spec traits that can be searched through, for users desiring particular examples
- Automated correspondence checking between the table in the README and the specs in the repo
In general I do not believe going back to hardcoding desired behavior (commands, etc.) for each spec is a good approach. This will inevitably drift out of sync with the actual contents of the repository, as evidenced by the state of the README table before #105. We've accumulated a good number of tests and many of them would not have been tractable to write without the nice manifest filtering capabilities.
One obvious improvement we could make is devolving the large central manifest.json file to smaller manifest.json files in each spec directory. As is, manifest.json has become too large (at 5000+ lines) to be human readable except for searching for keywords using ctrl+f in the browser or text search in a local editor. It also suffers from some amount of rot as users add their entries manually in an order different from the one produced by the generate_manifest.py script. If we devolve this to individual directories, it becomes a much nicer experience for users to write their own JSON file. Users can use github's repository search function to look for keywords, or grep through all json files locally.
A perpetual thorn in peoples' sides is making their README table entry satisfy the desired constraints of the CI. While automated conformance checking for the README table is absolutely necessary as it will surely drift otherwise, I am open to ideas about how this can be made simpler. @hwayne suggested scripting the modifications to the README table, which is certainly possible, but experience has shown that most users want to just add their entry by hand instead of running a python script. Some ideas:
- The CI itself could modify the README table using GitHub's write privilege, if it is incorrect; it is a projection of all information available in the manifest.json file(s), so can be readily automatically generated from that source of truth
- We could remove the authors field from the README table. While it is nice to give credit as often & prominently as possible, every field in the table increases the likelihood of users entering data in a way inconsistent with the manifest.json file(s).
- We could remove the table of external specs in the README, changing it into a simple list of links for example. Having two spec tables in the README with different formats is confusing for users, and they might modify the wrong one (this did happen in Add b-tree example #147).
Activity
lemmy commentedon May 21, 2025
This repository is for TLA+ examples—not JSON examples. No one wants to read or write JSON here. The primary audience consists of TLA+ users looking to learn and explore TLA+ through practical examples. A distant second, by several orders of magnitude, are contributors who want to add their own specs to this repo or link their upstream repos. The smallest audience are tool builders, who can be counted on two hands.
ahelwer commentedon May 21, 2025
Okay, so replace JSON with some other data format that will be included in TLA+ file preamble and postambles and have to be parsed by machines. What is that data format? What do we gain by not making it JSON?
lemmy commentedon May 21, 2025
JSON, YAML, XML—pick your poison. The real issue is that there's complex machinery (Python scripts coupled with JSON) that creates friction for the second biggest audience of this repo and has a bus factor of one.
ahelwer commentedon May 21, 2025
The bus factor is a real concern, so I have put a bunch of effort into documenting the current CI setup. My understanding is that you are much more familiar with bash than python, so would prefer to have as much CI logic as possible in bash; is this correct? Of course we should build our systems using languages that maintainers know.
lemmy commentedon May 21, 2025
I have no preference—I dislike all programming languages equally. 🙂 That said, the TLA+ project shouldn't turn into a programming language zoo. As much as possible, we stick to OCaml or Java (besides TLA+).
ahelwer commentedon Jul 31, 2025
A good incremental step here is just to split the central manifest file into files in each specifications/SpecName directory, without making any other changes. This has many benefits and will also reduce git merge conflicts.
ahelwer commentedon Aug 8, 2025
One manifest field that would be good to de-duplicate is the model size/model runtime field. Model runtime will of course vary quite a bit by computer, but I still find it fairly useful to know just how long a model ran on some computer, as opposed to just small/medium/large. Like does a model run for 45 minutes or three days? So my preference would be to get rid of the model size field instead of the model runtime field, and then the
check_small_models.pyscript just runs all models with less than a 30 second run time. This design decision is also relevant for #123 where proof checking time would similarly be recorded & filtered upon, which is more relevant now that proofs have been fixed.Manifest: remove path, title, and description fields
Manifest: remove path, title, and description fields
Manifest: remove path, title, and description fields
Manifest: remove path, title, and description fields
younes-io commentedon Apr 2, 2026
I may be missing some context, but after reading through the workflow and the related issues, I think the main point is that this repo appears to have one primary validation gate for normal development: the
Check Specs & Metadataworkflow:Examples/.github/workflows/CI.yml
Line 1 in dc6470a
That gate is doing two different jobs at the same time:
Job 1:
decide whether a PR is basically sound and safe to merge as an example contribution
Job 2:
verify that the repository as a whole still behaves as a polished cross-platform regression corpus for multiple tools
Those are both useful jobs, but are not the same job.
Today, the primary gate tries to answer both questions at once. That is why a PR can be perfectly reasonable at the TLA+ level and still fail for reasons that are real, but of a different kind: platform differences, Unicode mode, dependency downloads, proof timing, full-repo metadata consistency, README synchronization, and so on.
We could have a simple way to keep the standards high while making the intent clearer:
Lane A: this is the required PR gate : is this change valid enough to merge?
For example:
Lane B: corpus/infrastructure validation : is the repository still healthy as a full corpus?
For example:
Lane B could run on a schedule, on demand, or automatically only for PRs that touch CI/tooling/metadata infrastructure or make broad changes (to be defined).
This would not lower the bar. It would make the bar more precise.
It would also make failures easier to interpret. A red required PR gate would mean "this change is not ready". A red corpus/infrastructure job would mean "the repository ecosystem needs attention". Those are both important, but they are different signals and are best treated as such.
If the goal is to preserve the repo’s value both as an examples collection and as a corpus, this seems like the simplest and most practical way to do it, imo.
ahelwer commentedon Apr 2, 2026
That puts all the work of keeping this repo consistent on the maintainers.
younes-io commentedon Apr 2, 2026
We’re balancing two goals: low contributor friction and strong corpus-wide guarantees. We can’t maximize both at once; we can only choose where to pay.
I don't think there is a zero-cost design here. Either every contributor pays for corpus-wide guarantees up front in CI, or maintainers/reviewers pay more of that cost later through judgment and follow-up.
lemmy commentedon Apr 2, 2026
I will repeat what I said earlier: This repository is for TLA+ examples [...]. The primary audience consists of (human and artificial) TLA+ users looking to learn and explore TLA+ through practical examples. A distant second, by several orders of magnitude, are contributors who want to add their own specs to this repo or link their upstream repos. The smallest audience are tool builders, who can be counted on two hands.
The first (and third) groups benefit from having as many examples as possible. The second group is what makes that possible. Therefore, contributions should be made as easy and frictionless as possible.
ahelwer commentedon Apr 2, 2026
Numerically, but the value is much harder to quantify. It would be just as valid to count every CI run consuming these examples as a separate use, in which case the tool builders surely outnumber any other use case.
ahelwer commentedon Apr 2, 2026
Anyway! I think there are two things to do before considering splitting up the functionality:
find | jq | xargs command. The tricky thing here is that some of the specs have special cases to handle. Which leads into...lemmy commentedon Apr 6, 2026
A data point: While working on #204, the build fails because of a TLAPS proof.