Re: [tlaplus] path of `tlapm` files

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

On 10.07.20 10:15, Ioannis Filippidis wrote:
> 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


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

-- 
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/17d89c72-71b2-efe2-43ec-497422eae46a%40lemmster.de.