[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] path of `tlapm` files

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.


[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.