Suffix module names with 'Fork' to avoid conflicts with newer versions of the same modules included in CommunityModules

[lemmy]

Workaround for Github issue #171
#171

[Bug]

[ahelwer]

I don't think this is a good approach and seems downstream of the general lack of a well-thought-out versioning or packaging system for the community modules.

Perhaps these should be moved out of the TLAPM standard library and into the community modules themselves?

[lemmy]

Right now, the main issue is that the outdated SequencesExt and Functions modules in TLAPM are breaking the TLA+ VSCode extension for users. Moreover, since 2022, there has been consensus to move these modules (and their proofs) out of TLAPM and into CommunityModules. If the community decides to design and build a more advanced module system, that will take significant time.

[ahelwer]

I think moving the modules out of TLAPM into the community modules sounds good.

[lemmy]

This is blocked because the proofs fail for the latest versions of SequencesExt and Functions.

[ahelwer]

Perhaps they can be commented out then turned into an OMITTED?

[lemmy]

This PR does not block any of that work or make fixing the proofs more difficult. The specific names of these two models should not matter. If anything, the *Fork prefix more clearly indicates that these modules are forks (of the ones in CM). Most importantly, it ensures that VSCode users are not broken.

[ahelwer]

It will break the proofs of anybody who uses these modules. As would moving these modules to the community modules, but then users are presented the upgrade path of moving to a new version of the community modules instead of renaming their imports temporarily.

Since the goal state has these modules named the same as they are now, switching their names back and forth adds an unnecessary migration step.

[lemmy]

Good point — those users (if they exist) would also be affected by #171
if their setup happens to prioritize the newer versions of Functions and SequenceExt from the CommunityModules. The new module names give them a way to pin the older version of those modules.

[ahelwer]

See comment about upgrade paths. Fundamentally I see this as a shortcut that makes the situation worse when a bit more work (moving the modules to the community repo and commenting out proofs that no longer currently work) would lead to a better outcome.

[lemmy]

See comment about upgrade paths. Fundamentally I see this as a shortcut that makes the situation worse when a bit more work (moving the modules to the community repo and commenting out proofs that no longer currently work) would lead to a better outcome.

Are you volunteering? I’m afraid I won’t be able to do more than this PR.

[lemmy]

By the way, even if Functions and SequencesExt were moved to CommunityModules, existing TLAPS proofs would still break until authors explicitly include CommunityModules.