Feature: add `-I` flag to SANY to define include directories for specs

[ahelwer]

SANY has somewhat weird behavior for deciding where to look for specs; you have to put it as part of the classpath, like:

java -cp spec/search/path:tla2tools.jar tla2sany.SANY SpecName.tla

It would be nice to formalize this with a simple -I spec/search/path commandline parameter, similar to the SANY XML exporter. This seems like a good beginner issue.

[lemmy]

The main spec (the root module and its submodules) is usually located in the same directory. Typically, we only include auxiliary modules that provide common operators, such as the CommunityModules. Since these auxiliary modules frequently include Java module overrides, the use of the classpath becomes necessary.

[ahelwer]

For things like parsing TLAPS specs I think the -I flag would be fairly useful.

[lemmy]

No doubt, but please work out a sensible order of precedence for cases where both the classpath and -I are used together.

[ahelwer]

I learned during the tlaplus/examples work that the jar paths must go first in the classpath if I want them & the non-jar includes to work, so we can maintain that relationship and have the classpath override -I I think.

On the other hand that might violate the principle of least surprise, since I suspect people who use SANY from the command line like myself usually define an alias in their bashrc, which has a baked-in classpath. And one would expect a command-specific -I flag to override whatever is the default.