Embedding TLA typeset rules in a Latex document

[Saswata Paul]

Hi,

    I have been trying to embed TLA typeset formulas in a Latex document. I have gone through the instructions for downloading and installing the tools at https://lamport.azurewebsites.net/tla/standalone-tools.html?back-link=tools.html#tlatex?unhideBut@EQhide-tlatex@AMPunhideDiv@EQtlatex 

 

     I am using Windows.  The instructions in the page includes the following - 

                                                   "Let's suppose that your folder is  c:\user\myfolder .   This will create a subfolder of  myfolder  named  tla  that has three subfolders, each containing one of the tools.  You must then add  c:\user\myfolder\tla  to your CLASSPATH variable." 

     However, after extracting thetla2tools.jar file, instead of a folder named tla with three subfolders, three separate folders for each tool called tla2sany, tla2tex and tlc2 were created, along with some other folders.

  I tried adding tla2latex to my CLASSPATH and then running the following in the directory where my tex file is present (as described in https://lamport.azurewebsites.net/tla/texinfo.txt):

java tla2tex.TeX My_file.tex

I also tried the above by adding the tla2latex folder to my Path variable in windows.

However, it seems that the tla2tex folder does not have any class named tla2tex.TeX.

I will appreciate any help regarding this. If there is some other way to embed tla+ into a latex document, that will be helpful as well.

Thanks

[Saksham Chand]

There should be a file named "TeX.class" in the folder tla2tex, hence "tla2tex.TeX". The directory that should be added in CLASSPATH is the parent directory of tla2tex and not tla2tex itself.

Hope this resolves the issue,

Saksham

--
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 view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/e2148915-e55c-4909-bb7d-a855ece0d001%40googlegroups.com.

[Saswata Paul]

       This worked perfectly. 

Thank you !

You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/quIUFoR9thM/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAJSuO-8b83QE7K1MZ1ZxV_P%2Bh0Y%3DP2nEdag_n%3Douo%2Bmpq9-S%3DQ%40mail.gmail.com.

[Markus Kuppe]

On 04.11.19 14:07, Saswata Paul wrote:
> Hi,
>
>     I have been trying to embed TLA typeset formulas in a Latex
> document. I have gone through the instructions for downloading and
> installing the tools
> at https://lamport.azurewebsites.net/tla/standalone-tools.html?back-link=tools.html#tlatex?unhideBut@EQhide-tlatex@AMPunhideDiv@EQtlatex 
>  
>
>      I am using Windows.  The instructions in the page includes the
> following - 
>                                                    "Let's suppose that
> your folder is  c:\user\myfolder .   This will create a subfolder of 
>  myfolder  named  tla  that has three subfolders, each containing one of
> the tools.  You must then add  c:\user\myfolder\tla  to your CLASSPATH
> variable." 

Don't unzip and forget CLASSPATH. Instead try:

$ java -cp /path/to/tla2tools.jar tla2tex.TeX My_file.tex

Best
Markus

[Saswata Paul]

   I will try this out as well. Thank you!

--
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/quIUFoR9thM/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/e89b3bfb-0b78-abfc-bca7-8245f447d711%40lemmster.de.