Including TLA+ in a Pandoc paper.

68 views
Skip to first unread message

thomas...@gmail.com

unread,
Nov 24, 2020, 8:32:31 PM11/24/20
to tlaplus
Hi!

I am attempting to write an academic paper for a project which has been formally verified with TLA+. 

The paper is written in markdown with Pandoc, and for the life of me I have not been able import the TLA+ -generated.tex file into my document.

Has anyone here had any success importing their TLA+ stuff into a Pandoc paper? 
Obviously I could recreate the math within the vanilla LaTeX, but I was hoping something semi-automated.

thomas...@gmail.com

unread,
Nov 24, 2020, 9:44:01 PM11/24/20
to tlaplus


Ok so it's not perfect, or even "good", but an update of what I have that's sort of working.

If I write a document in Markdown like this:

```
######################################################################## 100.0%
---
title: "Test Thing"
header-includes: |
 \usepackage{subfiles}
---

# The Design
Lorem Ipsum Ipsum Lorem
\subfileinclude{equations/XORDistance}

```
(With XORDistance.tex being the generated TLA+ LaTeX file)

And then I render the document with Pandoc into TeX first:

`pandoc -s  input.md -o output.tex`

And then manually render using XeLaTeX:

`xelatex output.tex`

I get a PDF that resembles close to what I want.  However, it seems to be placing all the includes as text into the document.

Screen Shot 2020-11-24 at 9.41.49 PM.png


Any idea on how to fix that?

Leslie Lamport

unread,
Nov 25, 2020, 12:02:19 PM11/25/20
to tlaplus
The place to find information about TLA+ and its tools is its home page:

 
On that home page is a link to the Tools page.  On the Tools page is a 
subsection titled TLATeX Pretty-Printer.  If you open that subsection
you will find instructions on including TLA+ and PlusCal code in a
LaTeX document.

thomas...@gmail.com

unread,
Nov 25, 2020, 4:15:09 PM11/25/20
to tlaplus
I managed to get it working a bit better, by exporting my adding adding custom begin/end tags for TLA in my document, exporting to TeX, running LaTeX on the TeX, running the tla2tex program, then compiling with pdflatex. 

This mostly works, except when I try and use curly braces, it appears that Pandoc is trying to escape them, leading tla2tex to double-escape:


Anyone here have an idea on how to tell Pandoc to avoid escaping within a specific context.

thomas...@gmail.com

unread,
Nov 25, 2020, 4:37:21 PM11/25/20
to tlaplus
Ugh, sorry, bad copypaste with the image:
Screen Shot 2020-11-25 at 4.36.23 PM.png
Reply all
Reply to author
Forward
0 new messages