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 tla2tex.sh:

#!/bin/bash

OUTPUT=$1
INPUT=$2

## 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: tla2tex.sh $$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 and be exported via File > Export > PDF (tla2tex):

\begin{tla}
(***********************************************)
(* A standard definition of spec.              *)
(***********************************************)
Spec == Init /\ [][Next]_vars /\ WF_vars(Next)
\end{tla}

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] (https://www.ctan.org/pkg/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.

\batchmode
\makeatletter
\def\input@path{{/home/foobar/}}
\makeatother
\documentclass[english]{scrreprt}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\setcounter{secnumdepth}{1}
\setcounter{tocdepth}{1}
\usepackage{algorithm2e}

\makeatletter
\usepackage{tlatex}
\RestyleAlgo{ruled}
\LinesNumbered

\makeatother

\usepackage{babel}
\begin{document}

\chapter{Chap}

\section{Sec}

\begin{algorithm}
\begin{tla}
Line
Line
Line
\end{tla}
\begin{tlatex}
\@x{ Line}%
\@x{ Line}%
\@x{ Line}%
\end{tlatex}
\centering{}\caption{caption}
\end{algorithm}


\subsection{Subsec\label{subsec:subsection}}

\chapter{Broken Ref Below}

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

\end{document}

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

Published

Category

Contact