search

tlaplus / tlapm

The TLA Proof Manager
https://proofs.tlapl.us/
BSD 2-Clause "Simplified" License
67 stars 20 forks source link

Run corpus of TLA+ syntax tests in simple pass/fail manner #159

Closed ahelwer closed 2 weeks ago

ahelwer commented 4 weeks ago

This adds a preexisting set of approximately 200 syntax tests for TLAPM's parser. Future work will build on this to examine the actual parse tree output by TLAPM, but for now we just see whether the parser successfully parses all the things it is expected to. This effort uncovered a fair number of bugs which will be opened as issues in this repository.

Commits were generally made for the purpose of tracking work so I recommend doing a squash-commit if this is merged.

This work was funded by a grant from the TLA+ Foundation.

ahelwer commented 3 weeks ago

@kape1395 this is good to merge. Would appreciate a lookover of my OCaml code, this is my first time writing anything in the language!