Simplify contribution process

[ahelwer]

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:

1. 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.
2. 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
3. A largely automatically-validated manifest file containing many interesting spec traits that can be searched through, for users desiring particular examples
4. 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 #147).

[lemmy]

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.

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]

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]

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]

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]

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]

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]

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.py script 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.