Re: [tlaplus] path of `tlapm` files

I like the idea of having one "tlacache" directory for these auxiliary files corresponding to one directory containing TLA+ modules rather than having one directory per module. And like Markus, I am not a big fan of Python naming conventions and don't see why we should follow them. I think that users who have a need to inspect files generated by "--debug tempfiles" etc. will be able to find them even if the directory is hidden by the file manager. In my opinion, the main disadvantage of a hidden directory is that it may accumulate cruft without users being easily aware of this.

Note that TLC has the "-metadir" command line option for telling it where to store generated states, which defaults to specdir/states but can be set to a different directory (I used to set this to /tmp during many years). This could be generalized so that the user would be able to specify the position of the tlacache directory (perhaps also through a Toolbox preference), but it could still default to specdir/.tlacache or whatever. And it should probably be organized in subdirectories corresponding to the different tools such as tlacache/tlapm etc.

Stephan

On 11 Jul 2020, at 21:47, Ioannis Filippidis <jfilippidis@xxxxxxxxx> wrote:

Hi Markus,

In Python, two leading and two trailing underscores are used in names of
special methods [1,2], which are implicitly called by Python to execute certain
operations, for example the method named `__str__` implements the conversion of
an object to a string. A leading underscore signifies a non-public part
of the API [3], and names that start with an underscore are not imported by
`from modulename import *` [4] (and not shown in introspection with `ipython`,
unless an underscore is typed before pressing tab).
So `__pycache__` indicates a builtin mechanism, and alludes to internal details.
Adopting the Python scheme for `__tlacache__` would have the benefit of
following this convention, and its similarity to `__pycache__` could suggest
similar purpose, of storing auxiliary files.

About using a dot in the directory name, in PEP 3147 the reasons listed for not
using a dot are that dot-files are special on only some platforms and that
the `__pycache__` directory is not intended to be completely hidden from users [5].
The `*.tlaps` directories can contain input files for solvers when the
`--debug=tempfiles` option is passed to `tlapm`, and those files could be used
for debugging. I was not sure whether the directory would be intended to be
completely hidden (instead of explicitly hidden via `.gitignore`), and followed
the Python convention, hence the name `__tlacache__`.

Within a `git` repository, and using a program that is aware of `.gitignore`
settings, the file view would hide the `__tlacache__` directory (for example
within the editor Atom).

[1] https://docs.python.org/3/glossary.html?highlight=underscore (entry: "special method")
[2] https://www.python.org/dev/peps/pep-0008/#descriptive-naming-styles
[3] https://docs.python.org/3/tutorial/classes.html#private-variables
[4] https://docs.python.org/3/tutorial/modules.html?highlight=underscore#more-on-modules
[5] https://www.python.org/dev/peps/pep-3147/#pyc

Best regards,
Ioannis

--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/65d38d0f-2753-4917-b882-b5a2d8198dbao%40googlegroups.com.