Include TLA+ in LyX documents and export it pretty-printed to PDF

Create a wrapper script for tla2tex.TeX (part of tlatools), put it onto $PATH and name it



## Creating dummy file ${OUTPUT%.*}.tex for tla2tex to remove. It apparently needs this.
touch ${OUTPUT%.*}.tex

## Running tla2tex.TeX on $INPUT and writing output to ${OUTPUT%.*}.tex. Expects the TLA+Toolbox to
## be installed to /opt/TLA+Toolbox
java -cp /opt/TLA+Toolbox/plugins/org.lamport.tlatools_1.0.0.*/ tla2tex.TeX -out ${OUTPUT%.*}.tex $INPUT

## Converting ${OUTPUT%.*}.tex back to $OUTPUT for LyX to read it
#cp ${OUTPUT%.*}.tex $OUTPUT
## tla2tex.TeX does not accept "\label{...}" as a lexem and fails. To still be able to use \label
## within algorithms, they get wrapped into a TLA+ line comment ("\*..."). Despite being an empty
## comment, the resulting PDF shows a grayish box for each \label iff comment shading is enabled.
## The regexp below removes all boxes created by TLA+ line comments with \label{...}.
cat ${OUTPUT%.*}.tex |perl -0777 -pe 's/\\\@y\{%\n (\\label\{[:a-zA-Z0-9]+})\n}%/$1/igs' > $OUTPUT

Open up LyX and create two new "File Formats" under Tools > Preferences > File Handling > File Formats:

Format: LaTeX (tla2tex)
Short name: tla2tex
Extensions: tex

Format: PDF (tla2tex)
(Check "Document format", "Show in export menu", "Vector graphics format")
Short name: pdf4tla2tex
Extensions: pdf
Shortcut: T
Viewer: qpdfview --unique

Also create two new LyX "Converters" under Tools > Preferences > File Handling > Converters:

From/To: LaTeX (plain) -> LaTeX (tla2tex)
Converter: $$o $$i

From/To: LaTeX (tla2tex) -> PDF (tla2tex)
Converter: pdflatex $$i
Extra flag: latex=pdflatex

Afterwards run Tools > reconfigure and restart LyX. TLA+ statements can then be included in LyX documents inside LyX's \ERT within a "tla" or "pcal" environment provided the document's LaTeX preamble declares a \usepackage{tlatex} as explained in the tla2tex help and be exported via File > Export > PDF (tla2tex):

(* A standard definition of spec.              *)
Spec == Init /\ [][Next]_vars /\ WF_vars(Next)

Ideally, the excerpts were sourced from the .tla file directly so that one wouldn't need to copy&paste parts of a specification into the .tex document. Someone might want to look into This. The catchfilebetweentags packages seems to be a viable candidate.

An incompatibility with the algorithm2e package surfaced that screws up \ref pointing to a \label whichis attached to a section/subsection. If secnumdepth is set to be lower than the label'ed section/subsection, the \ref fails to show the number of the parent secton if interleaved with a TLA+/PlusCal algorithm. Instead, it shows the last line number of the interleaved algorithm. If anybody cares about it, the .tex below reproduces it.







\@x{ Line}%
\@x{ Line}%
\@x{ Line}%


\chapter{Broken Ref Below}

\ref{subsec:subsection} <= incorrectly shows last line number of
algorithm instead of ``1.1''.
\item If line numbers are omitted (no \textbackslash{}LinesNumbered in Preamble),
the bug disappears.
\item If secnumdepth includes subsections, the bug disappears.


Last posts

  1. Forcefully re-resolve a stale PDE target definition
  2. Cross-compile kernel module (ext2) for Samsung nx300 on Ubuntu 14.04
  3. Auto backup files from the Samsung NX300 camera in the background
  4. SWTError: No more handles [gtk_init_check() failed] running platform tests (on Linux)
  5. Apache Felix HTTP whiteboard pattern on Equinox