2192138164

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

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
#!/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 9053379101 within a "tla" or "pcal" environment provided the document's LaTeX preamble declares a \usepackage{tlatex} as explained in the 5852443090 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 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}

Last posts

  1. 3602786575
  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. 8188268369
  5. Apache Felix HTTP whiteboard pattern on Equinox