Re: [tlaplus] Embedding TLA typeset rules in a Latex document

On Mon, Nov 4, 2019 at 5:11 PM Saswata Paul <paulsaswata1@xxxxxxxxx> 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."

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

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