search

tlaplus / tlaplus

TLC is a model checker for specifications written in TLA+. The TLA+Toolbox is an IDE for TLA+.
https://lamport.azurewebsites.net/tla/tla.html
MIT License
2.33k stars 197 forks source link

Do not store TLC generated and runtime data in spec's subdirectories #196

Closed nomothetis closed 4 years ago

nomothetis commented 6 years ago

Hi,

I'm working with the TLA+ Toolbox, and for complicated reasons cannot ignore files in a subdirectory when checking in code. I would like to redirect the TLA+ output files (snapshots, etc) to a different location, but was unable to find a setting for that. Is this an option?

Thanks.

lemmy commented 6 years ago

@nomothetis You can turn snapshots off entirely by setting the numbers to keep in the preferences to zero. You cannot redirect the output though.

Can you elaborate on what you check in and what you want to ignore (related to github issue #157)?

nomothetis commented 6 years ago

Thanks for the tip on turning off snapshots.

Honestly, reading issue #157, covers exactly what I would like for production use; I can live with PlusCal translations being in the same file (though since it's in essence the same information twice, it would be nicer not to have that), but the others make working as a team difficult.

lemmy commented 6 years ago

In other words a cleverly crafted .gitignore file can satisfy your use case?

nomothetis commented 6 years ago

If I used git, it would. :-) Unfortunately, we use...complicated infrastructure at work.

lemmy commented 6 years ago

@nomothetis Do you know that you can recreate the MC.out and MC.cfg from the .launch config that resides in their parent directory?

nomothetis commented 6 years ago

I did not know that, but I'm not sure how helpful it is.

Our system automatically saves all and any writes as snapshots to make them accessible across machines. Therefore any generated code is stored ~forever. So even if we find a way to ignore files from commits, we would still have unnecessary space consumption problems. Of course, I'm just toying with TLA+ for myself right now, but if we were to seriously adopt it, we'd need to be able to separate generated from source code.

lemmy commented 4 years ago

Please reopen if this remains an issue (with latest and greatest).