| Thank you for your report. Please file an issue on https://github.com/tlaplus/v2-tlapm/issues so that we are reminded that we need to fix this for the next release.
As you say, the "Bags" module included with TLAPS is badly named and should be called BagTheorems.
Some of the modules associated with TLAPS indeed introduce additional operators (such as Reverse in SequenceTheorems) that may lead to clashes with operator names introduced by users, and the clash may become apparent only when you start doing proofs and therefore import modules such as SequenceTheorems that you don't need for your specification. TLA+ has so far eschewed associating name spaces with modules. Conceivably, one could move the definitions of these operators to the existing standard modules because they may be useful independently of proofs, but the standard modules have been stable for a long time, so there is some reluctance to changing them. Defining an operator such as Reverse is easy enough, but proofs of its properties are not automatic, so it makes sense to provide such theorems in standard proof modules. Perhaps the additional operators and their properties should be moved to separate modules – I believe that the proofs of theorems about operators defined in the existing standard modules do not depend on the additional operators.
Regards, Stephan
There appears to be some "weirdness", for lack of a better term, going on with the Bags module when using TLAPS.
\* What happened ***
Extending "Bags" in an own module resulted in a duplication error with a "Reverse" operator that I had defined. This was unexpected, since the Standard Module bags shouldn't define such an operator.
\* The problem with Bags and TLAPS ***
For some reason, TLAPS includes a "Bags" module. This module consists of an exact copy of the standard "Bags" plus some extras, the latter consisting of:
1. extension of modules: TLAPS, FiniteSetTheorems, SequenceTheorems
2. definition of a SeqToBag operator
3. proofs of various properties on Bags
The extended "SequenceTheorems" module in particular, defines "Reverse" as well as various other common operations on Sequences (likewise for FiniteSetTheorems). These definitions are therefore, by extension, in TLAPS' "Bags" module.
The TLA+ library path locations, in the toolbox "preference" settings, appear to take precedence over the Standard Modules toolbox itself provides. Therefore, when the TLAPS library is included, extending "Bags" means extending TLAPS' "Bags", which includes various operations on lists and sets.
\* Other Standard Modules in TLAPS ***
"RealTime" and "FiniteSets" are also provided by TLAPS. However these are exact copies (except for comments).
Note that unlike with "Bags", the theorems and proofs for "FiniteSets" are in the "FiniteSetTheorems" and "FiniteSetTheorems_proofs" modules (which extend FiniteSets).
Note also that no "Sequences" module is provided by TLAPS, yet there is a "SequenceTheorems" module that extends the standard "Sequences" module provided by toolbox.
\* Possible fixes ***
This situation seems easily avoidable:
Firstly, the extra (non-standard) content of TLAPS "Bags" should be moved to a "BagTheorems" module (and possibly "BagTheorems_proof"), matching the approach followed in "FiniteSets" and "RealTime". Secondly, should there be no need for copies of standard modules in TLAPS these should be removed, matching the approach followed in "SequenceTheorems".
Finally, a couple of points regarding toolbox:
It doesn't seem quite right that toolbox would allow for standard modules to be overridden silently. Maybe a warning should be provided? Regarding usability. The error message I got did include a line indicating that "Reverse" was duplicating a declaration in "SequenceTheorems". It would be nice if one could access this source by clicking this line in the error message (instead it takes us to the duplication in one's own file).
--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.
|