Skip to content

Conversation

@ahelwer
Copy link
Collaborator

@ahelwer ahelwer commented Dec 17, 2025

macOS runners also seem to be getting slower, so skip checking one of the CoffeeCan models.

-and -not -wholename "*/LeastCircularSubstring/*" \
-and -not -wholename "*/diskpaxos/*" \
-and -not -wholename "*/ewd998/*" \
-and -not -wholename "*/ewd840/*" \
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If I understand correctly, you pass all TLA+ modules to tlapm, except those mentioned here. Up to now, the logic was "positive" in the sense that only specifications that declared containing a proof were checked. For ewd840, the incriminated "ToString" operator is used only in EWD840_anim.tla, whereas as far as I can tell the exception list also contains EWD840_proof.tla, which it would be great to check. Similarly, ewd998/EWD998_proof.tla should pass the check but is excluded here?

Copy link
Collaborator Author

@ahelwer ahelwer Dec 17, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yeah I think I am leaning against this approach after seeing how large the list will grow (probably at least double this size). There are a lot of examples that use the RECURSIVE keyword. All those EWD directories also have lots of files, most of which fail parsing since they use nonstandard TLC modules.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Development

Successfully merging this pull request may close these issues.

2 participants