Re: [tlaplus] How to build Codeplex Tlaplus Tools?

[Markus Alexander Kuppe <tlaplus-go...@xxxxxxxxxxx>]

On 08.03.2015 11:50, marc magrans de abril wrote:
> I have performed the following steps:
> * Cloned the Git repo in https://tlaplus.codeplex.com/
> * Compile the default target of the customBuild.xml file under
> tlaplus/tlatools
> * This generates a tla2tools.jar
> 
> I wonder if that's all I need to compile all the tools. Is it?
> 
> Do you have any instructions on the procedure to compile and run a new
> version?
> 
> Have I compiled all the tools (i.e. TLC, SANY, etc.)?
> 
> What should I do to run this new version in my OSX?

Hi Marc,

if you just want the tools [1] but don't want the TLA Toolbox [2],
tla2tools.jar is all you really need (you could have downloaded [1] the
tools from the web instead of compiling manually).

In order to run the individual tools, just add tla2tools.jar to java's
classpath:

java -cp tla2tools.jar tlc2.TLC
java -cp tla2tools.jar tla2sany.SANY
java -cp tla2tools.jar pcal.trans
java -cp tla2tools.jar tla2tex.TLA

When it comes to the tools' arguments, the source files directly are a
good source of information. See tlc2.TLC [3], pcal.trans [4],
tla2sany.SANY [5] and tla2tex.TLA [6].


May I ask why you don't want to use the Toolbox [2]? It provides an easy
entry into TLA+ and a graphical front-end for the tools.

Cheers
Markus

[1] http://research.microsoft.com/en-us/um/people/lamport/tla/tools.html
[2] http://research.microsoft.com/en-us/um/people/lamport/tla/toolbox.html
[3]
http://tlaplus.codeplex.com/SourceControl/latest#tlatools/src/tlc2/TLC.java
[4]
http://tlaplus.codeplex.com/SourceControl/latest#tlatools/src/pcal/trans.java
[5]
http://tlaplus.codeplex.com/SourceControl/latest#tlatools/src/tla2sany/drivers/SANY.java
[6]
http://tlaplus.codeplex.com/SourceControl/latest#tlatools/src/tla2tex/TLA.java