path of `tlapm` files

[Ioannis Filippidis]

Hi all,

I would like to suggest a change to the path where `tlapm` saves auxiliary files,

to the path `__tlacache__/filename.tlaps/`, for an input file

named `filename.tla`. The current path is `filename.tlaps/`.

With this change, the generated files for all the TLA+ files in a directory

would be placed under a single directory named `__tlacache__`,

so that the `*.tlaps` directories would not be listed in the working directory.

This change would imply that to load fingerprints from previous

`tlapm` versions, existing `*.tlaps` directories would need to be moved

to the `__tlacache__/` directory.

Using a common directory named `__tlacache__` is inspired by

the directory `__pycache__` [1] in Python 3, which stores `.pyc` files.

[1] https://www.python.org/dev/peps/pep-3147/

Best regards,

Ioannis

[Markus Kuppe]

What is the benefit of adopting the python scheme (four underscores)?
For me, such a folder name has the opposite effect and draws attention
(elevated by the fact that it's shown at the top of file managers).
Have you considered a hidden directory [1] that usually is, well, hidden?

The change is currently only limited to TLAPS, which is why I'd suggest
adding an additional sub-folder ".tlacache/tlapm/filename.tlaps" should
other tools such as Apalache, TLC, or the Toolbox adopt the change.

Markus

[1] https://en.wikipedia.org/wiki/Hidden_file_and_hidden_directory

[Ioannis Filippidis]

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

[Stephan Merz]

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.

My 2 cents,

Stephan

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

[Markus Kuppe]

On 12.07.20 01:32, Stephan Merz wrote:
> In my opinion, the main disadvantage of a hidden directory is that it
> may accumulate cruft without users being easily aware of this.

The Toolbox already shows a warning at the bottom status bar if the size
of the ".toolbox" folder exceeds a (configure) threshold. It wouldn't
be difficult to also include the new directory.

Markus