Simplify contribution process

まず、#164 のコントリビューションドキュメント、generate_manifest.py、manifest.json、README の表、およびここで説明されている CI チェックを読んでください。方向性を提案する前に、どのバリデーションが中央のマニフェストと表の形式に依存しているかを整理してください。完了の条件は、列挙されているバリデーション、フィルタリング、マニフェスト、README の一貫性という利点を維持した、より簡単なコントリビューションプロセスについて合意することです。

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).