search

tlaplus / Examples

A collection of TLA⁺ specifications of varying complexities
Other
1.27k stars 198 forks source link

Enforce correspondence between manifest.json and README.md table in CI #70

Closed ahelwer closed 8 months ago

ahelwer commented 1 year ago

This isn't work I'm planning to do anytime soon but it would be a nice little project if someone else wants to take it on. Markdown is a very difficult language to work with, tooling-wise, but there are nice full-featured parsers like goldmark (used by the Hugo static site generator, for example) which make it tractable. A CI script could parse the README.md file with goldmark, find the table & its entries, and check its correspondence to the manifest.json file. This would include not only the existence of specs in the table but also whether they are properly labeled as including proofs, pluscal, TLC models, and whatever other traits we care to define. This could also implement whatever clustering & categorization is desired in #15. This could all possibly be implemented as a goldmark extension. Alternatively, there are a number of python markdown parsers of varying quality levels that could be used.

ahelwer commented 8 months ago

There are some pretty good python markdown parsing packages now and I'm playing around at this. It seems pretty viable to actually enforce correspondence between the README.md table and the manifest.json file. I think we should do the following checks:

  1. Ensure top-level spec directories are isomorphic with entries in table
  2. Ensure each Name column entry links to appropriate directory (the directory link will be the foreign key matching that row to an entry in manifest.json)
  3. Ensure authors match
  4. Ensure TLAPS proof is indicated if present
  5. Ensure TLC model is indicated if present
  6. Ensure PlusCal is indicated if present
  7. Ensure Apalache is indicated if present (I don't actually know how to check for this)

I also propose making the following changes to the table itself:

  1. Remove the # column, not sure what the use of it is
  2. Remove the Module Dependencies column, existing data seems very inconsistent and it would be quite difficult to make complete

@lemmy thoughts?

lemmy commented 8 months ago

LGTM

ahelwer commented 8 months ago

While transforming the table I found these links which I cannot yet map to a spec in the repo:

https://github.com/neoschizomer/Paxos
https://github.com/tlaplus/tlaplus/blob/master/tlatools/org.lamport.tlatools/src/tlc2/tool/fp/OpenAddressing.tla
https://github.com/Alexander-N/tla-specs/tree/main/crdt-bug
https://github.com/Alexander-N/tla-specs/tree/main/asyncio-lock
https://github.com/dranov/raft-tla
https://github.com/elem-azar-unis/CRDT-Redis/tree/master/MET/TLA
https://github.com/Cjen1/tla_increment
https://www.losa.fr/blog/streamlet-in-tla+
https://github.com/elh/petri-tlaplus
https://github.com/JYwellin/CRDT-TLA