Add TLA_PATH environment variable to load modules from

[konnov]

Run TLC with -DTLA-Library=/path/to/lib/archive or add the library archive to the Toolbox (File > Preferences > TLA+ Preferences > TLA+ library path locations).

It would be great to have a standard environment variable, e.g., called TLA_PATH. Similar to PATH, PYTHON_PATH, JAVA_LIBRARY_PATH, etc., it would list directories, from which the TLA+ tools would pull the library modules.

[lemmy]

Does @informalsystems have the resources to provide a pull request?

[konnov]

In principle, yes, but I am not sure about the whereabouts of the file reading operations in the SANY parser.

[lemmy]

util.FilenameToStream and its subclasses such as util.SimpleFilenameToStream

Since TLA_PATH is an alternative to "TLA-Library", it should work for SANY and the other tools such as TLC.

[konnov]

Thanks! I will have a look.

[lemmy]

@konnov Are you still pushing this?

[konnov]

Not really. I was stuck at how Eclipse handles filenames. So I guess the related PR #493 needs some expertise in Eclipse.

[ahelwer]

@lemmy what do you think about also adding this as a TLC command line option? You can define additional directories to search for TLA files when running TLC. This would also help when outputting TE specs to a subdirectory; you can switch working directory to that subdirectory, then run TLC on the TE spec while asking TLC to look for the original spec in the parent directory via a command line option. This is also nice because running TLC on a spec identified by absolute path (rather than in current working directory) does not seem to be currently supported.