`Functions.tla` here clashes with `Functions.tla` in TLAPM

[lemmy]

There is a name clash between the Functions.tla in CommunityModules and Functions.tla in TLAPM, with the Functions.tla in CommunityModules (CM!Functions.tla) having a superset of operators compared to the version in TLAPM. Users who open specs that depend on CM!Functions.tla but who have PM!Functions.tla on the library path (first) end up with an unparsable spec.

/cc @muenchnerkindl @xxyzzn

Likely related: tlaplus/tlapm#3

[lemmy]

To continue the discussion about moving modules out of TLAPS:

• Agreement that the CommunityModules repo is a good home for most TLA+ modules (some modules might later graduate to the standard modules)

• Requiring TLAPS users to install the CommunityModules is acceptable

• TLAPS cannot yet read TLA+ modules from the CommunityModules.jar (zip) file: Accept archives (zip) in search path tlapm#3

• What to do about the related *_theorems.tla and *_theorems_proofs.tla modules in TLAPS?

• The TLAPS modules should remain under the control of TLAPS (non-TLAPS users can just remove a proof from a spec that they downloaded)

/cc @johnyf @damiendoligez @quicquid

[muenchnerkindl]

I think the *_theorems(_proofs) modules should also be moved to the CommunityModules so that everything is in one place and that they get better visibility. Obviously, they only need to be imported by users who write proofs.

[lemmy]

We could move *_theorems(_proofs) into a subdirectory to reduce clutter. Also, to catch regressions, the CM Github action can check the proofs with the latest TLAPS release (https://github.com/lemmy/BlockingQueue/blob/4fa409b020725631d8fa0fa99ea9c813c3cd40dc/.github/workflows/main.yml#L18-L29 for inspiration).

[lemmy]

/cc @kape1395 for visibility

[kape1395]

From the build perspective. The current tests in TLAPS depend on the files in the standard library, including the Functions.tla. E.g.

./test/fast/regression/consensus/consensus_test.tla -> FiniteSetTheorems -> Functions.

But I haven't checked if the backends (Isabelle, ...) are tied to these modules. If the relations exist there, the related modules should be kept in the TLAPM repo, IMO.

Considering the tests. Maybe these dependencies should be reorganized somehow to avoid loops across the repositories.
The tests could be split to

• those depending on the modules (that will be) moved to the community modules repo (regression/integration tests)
• and those that don't (core test suite).

The core test suite could be run without dependencies from the community modules. These should be enough to build/install/release the TLAPS.

And the regression/integration" test suite would not be tied to the build/install/release procedures. They

• should be invoked separately from the core test suite.
• would download the latest versions of the proofs from the community and examples repositories, etc.
• can be run by the GitHub actions as a separate workflow. All of the tlapm/examples/community-modules should have such workflows to ensure cross-checks.

While trying to check this, I found that test/fast/regression/MiniProducerConsumer_test.tla depends on Sequences, but there is no Sequences.tla file in the repository. I wonder how it works.

[damiendoligez]

While trying to check this, I found that test/fast/regression/MiniProducerConsumer_test.tla depends on Sequences, but there is no Sequences.tla file in the repository. I wonder how it works.

It is, like most of the standard modules, implemented internally within tlapm in src/module/m_standard.ml. This is important because tlapm has to implement special treatment of some of the operators defined in these modules (to translate them into the corresponding back-end provers' features).