# Re: [tlaplus] embed PlusCal and TLA+ specs in latex papers

You must have downloaded the tools sometime in the past and Java is finding the wrong version.  Go to the page http://research.microsoft.com/en-us/um/people/lamport/tla/tools.html and read the section "Downloading and Installing the Tools" to find out how to set an environment variable to tell Java where to find the tools.  Instead of setting the environment variable to c:\user\myfolder\tla, you can run the program by typing something like

java -cp "c:\user\myfolder\tla" tla2tex.TeX

Leslie

On Sun, Jun 2, 2013 at 10:10 AM, Hai Zhou wrote:
I believe that I downloaded at the new location. However, I am not sure how java find those files; it may get the old one somewhere...
$java tla2tex.TeX tla2tex.TeX Version .9 created 19 Sep 2007 On Sunday, June 2, 2013 12:55:48 PM UTC-5, Leslie Lamport wrote: You seem to be using an old version of TLATeX. Did you download the latest version of the tools? They are no longer distributed from the Microsoft site, but rather from https://tla.msr-inria.inria.fr/tlatoolbox/dist/ . If you did download them from there, tell me what version number and date the program prints. Leslie On Sun, Jun 2, 2013 at 9:36 AM, Hai Zhou wrote: Thanks very much for the info. There is no mention of pcal in the -info documents. I use the following but get nothing:$ java tla2tex.TeX -info |grep "pcal"
Also, when I use \begin{pcal} \end{pcal}, no tlatex environment is generated. But if I use tla environment, it did generate.
--
Hai

On Sunday, June 2, 2013 12:26:22 PM UTC-5, Leslie Lamport wrote:
Could you explain what you mean by "doing PlusCal"?  Are the instructions you get by running "tla2tex.TeX -info" unclear?  (Note the instructions at the beginning to use a pcal or ppcal environment for PlusCal code and a tla environment for plain TLA+.)  What may not be clear is that in the pcal environment, you put PlusCal code, not a comment containing PlusCal code.

If you need to know how to use PlusCal,  the PlusCal manual is on the PlusCal web page.

Leslie
On Sun, Jun 2, 2013 at 6:56 AM, Hai Zhou wrote:
Leslie: Thanks for the quick reply. I got the tool and started to use it. However, it is not clear how to do PlusCal. Could you explain a bit?
--
Hai

On Sunday, June 2, 2013 4:10:40 AM UTC-5, Leslie Lamport wrote:

You will have to download the stand-alone tools (http://research.microsoft.com/en-us/um/people/lamport/tla/tools.html) and run the tla2tex.TeX Java program (which is not mentioned on the Web page, but probably should be).  Run it with the –info option to get the documentation.

Leslie

On Sat, Jun 1, 2013 at 8:43 PM, Hai Zhou wrote:
I would like to embed PlusCal algorithms and TLA+ specs in my paper in latex.
What is the style file I need to use for that, and where can I find it?

Thanks very much.
--
Hai

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.