# Get the raw LaTeX from the spec instead of an exported PDF?

54 views

### thomas...@gmail.com

Aug 25, 2020, 12:06:27 PM8/25/20
to tlaplus
Hello! I have a spec that I designed in the Toolbox, and I want to take the spec and include it into a paper I'm writing.  Is there a way to export the raw LaTeX code from the toolbox instead of just the PDF?

### Willy Schultz

Aug 25, 2020, 1:12:57 PM8/25/20
to tlaplus
I'm not sure if there's an officially supported way to get the TeX source directly from inside the Toolbox, but if you click "File > Produce PDF Version", the TeX output from the PDF generation should be placed in the *.toolbox directory of your spec. For example, if your module is named "Spec", you should find a .tex file at "Spec.toolbox/Spec.tex". You could retrieve it manually from that location. If you want to bypass the Toolbox entirely, you can generate the TeX source from the command line using the java tla2tex.TLA tool directly.

### thomas...@gmail.com

Aug 25, 2020, 4:29:54 PM8/25/20
to tlaplus
That works, I was able to grab it from the .toolbox folder.

I can't imagine it would be too hard to add this as an official feature for the toolbox, would it? It has to produce the TeX anyway to create the PDF, I would think it would be pretty straightforward to add an option to have a little menu-item underneath saying "export TeX" or something.

### Willy Schultz

Aug 25, 2020, 5:47:45 PM8/25/20
to tlaplus
It sounds reasonable. Feel free to open a Github issue for it here.

### Christian Barthel

Aug 27, 2020, 3:37:03 AM8/27/20
to thomas...@gmail.com, tlaplus
Hello,
I think you can embed TLA+ code within a LaTeX document and
generate the pretty printed version of it. To do so: create a
document like this:

%< %< %< %< %< %< %< %< %< %< %< %< %< %< %< %< %< %< %< %<
% filename: test.tex
\documentclass[11pt]{article}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{graphicx}
\usepackage{tlatex}
\usepackage{color}
\newcommand{\figscale}{.65}
\begin{document}
\title{Testing}
\author{Christian Barthel}

\section{My test}
\begin{figure}[!h]
\begin{tla}
------------------------------- MODULE HC ------------------
EXTENDS Naturals
VARIABLES hr

vars == <<hr>>

Init == /\ hr \in 1..12
Next == /\ hr' = IF hr = 12 THEN 1 ELSE hr + 1

Spec == Init /\ [][Next]_vars

Invariant == [](hr \in (1..12))
===========================================================
\end{tla}
\begin{tlatex}
\end{tlatex}
\end{figure}
\end{document}
%< %< %< %< %< %< %< %< %< %< %< %< %< %< %< %< %< %< %< %<

Then, it is possible to generate pretty printed TLA+ code
with:

java -cp tla2tools.jar tla2tex.TeX test.tex

This will basically fill in the LaTeX code between
"\begin{tlatex}" and "\end{tlatex}". And finally compile it to a
PDF file:

pdflatex test.tex