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,
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/512895B8-2492-413F-A3FC-BF171B99B215%40gmail.com.