Re: [tlaplus] TLAPM from command line

[Martin <martin...@xxxxxxxxxxxxxx>]

Hi Amira,

Yes, you can run tlapm on the commandline, by default it should be
installed in /usr/local/lib/bin/tlapm . It seems you are trying to
install from source, but there are also binary packages available at:

http://tla.msr-inria.inria.fr/tlaps/content/Download/Binaries.html

They also provide the binaries for Zenon, Isabelle 2011 and other
theorem provers. If you would like to compile from source, I would
advise to install the binary package first to have all the backends
ready ( they are by default installed to /usr/local/lib/tlapm ) and then
install your self-compiled copy of tlapm to /usr/local/bin . That should
also solve your problems with PolyML, which is only necessary for
compiling (and running) Isabelle.

I hope that helps a bit,
cheers Martin

On 03/10/2017 03:52 PM, Amira Methni wrote:
> Hi, 
> 
> I have a set of TLA+ modules containing several lemma and proofs. I want
> to write a script that launches TLAPs for all these modules instead of
> launching TLAPS for each TLA+ file separately. 
> Can I use TLAPM from command line to do this? 
> 
> PS: I tried to install TLAPS source code by following instructions on
> the web site, but polyml is no longer available.
> 
> Thanks  
> Amira
>