[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: change font size of latex pretty-printed TLA spec

Hi Giulio,

PFA the script. A few things:

0) It will only work on Linux (because I'm not using python's Path for file handling)
1) The filename and directory name are hard-coded strings on lines 31 and 32. You can easily change them to be taken as arguments when invoking the script.
2) The alignment will be off for the following:

Action == /\ A
          /\ B
          /\ C

will print as

Action == /\ A
         /\ B
         /\ C

I remember fixing it but I can't seem to find the version of the script which had that fix.
But the following will print with correct alignment:

Action ="">
  /\ A
  /\ B
  /\ C

Feel free to ask any questions you might have.


On Friday, January 11, 2019 at 2:29:59 AM UTC-5, Giulio Salierno wrote:
Il giorno giovedì 10 gennaio 2019 18:48:15 UTC+1, saks...@xxxxxxxxxxxxxx ha scritto:
> I have a python script that helps me pretty print my proofs, for example the specs and proofs in the appendices of https://arxiv.org/abs/1606.01387. I can share it if you like the formatting.
> Best,
> Saksham Chand
> On Thursday, January 10, 2019 at 12:16:51 PM UTC-5, sali...@xxxxxxxxx wrote:Dear everyone,
>  I'm creating a pretty-printed version of my tla specs using the tla2tex.TeX tool. Does anyone know how to modify the font size so that those fit properly in a paper? I've already had a look if the tool provides this option with no results.
> Thanks in advance

Dear Saksham,
I've seen the formatting style used in the appendices and I would be very happy if you could share the script.  Thank you!


#!/usr/bin/env python
import sys
import os
import tempfile
import re

def footnotify (line):
  # Make font size footnotesize
  line = line.replace('\\mbox{', '\\mbox{\\footnotesize')

  # Convert all horizontal spacing to footnotesize
  x = line
  z = ''
  while '@s{' in x:
    y = x.split('@s{', 1)
    z += y[0]
    z += '@s{'
    a = y[1].split('}', 1)
      z += str(round(float(a[0]) * 4.0 / 5.0, 2)) # This is where the size is changed
      z += '}'
      x = a[1]
      z = ''
  line = z + x

  return line

#TODO: add sys.argv
dirname = '/home/saksham/Desktop/journal/'
fname = 'MultiPaxosCha'
os.system('java tla2tex.TLA ' + dirname + fname + '.tla')
f = fname + '.tex'
insert_amssymb_if_not_already_present = False
assume_in_line = False

with open(f) as fd1, open(tmp[1],'w') as fd2:
  for line in fd1:
    # Lines of original Latex to skip
    if 'setlength{\\textwidth}' in line or 'setlength{\\textheight}' in line:

    # Add sty files needed for our Latex additions
    if insert_amssymb_if_not_already_present:
      if 'amssymb' not in line:
        # Add any sty file your latex needs here but the first has to be amssymb
        # because that is what the if-condition is checking
      insert_amssymb_if_not_already_present = False

    if 'documentclass' in line:
      insert_amssymb_if_not_already_present = True

    # Replace \not \exists with \nexists
    # TODO: This wouldn't work if the \not and \exists are in separate lines :(
    line = line.replace('{\\lnot} \E', '{\\nexists}')

    # Replace {} with \emptyset
    line = line.replace('\\{ \\}', '{\\emptyset}')

    # All TLA+ keywords to be colored Purple in Latex
    if 'textsc' in line and 'purple' not in line:
      line = line.replace('textsc','textcolor{purple}{{\\textsc')
      if '%' in line:
        line = line.split('%', 1)[0]
        line += '}}\n'
        line = line.replace('\n','}}\n')

      if 'case' in line:
        line = line.replace('case ', ' case ')

    # All string constants to be colored blue in Latex
    if 'textsf' in line and 'blue' not in line:
      line = line.replace('textsf','textcolor{blue}{{\\textsf')
      line = line.replace('\n','}}\n')

    # Enable shading in comments by default
    if "setboolean" in line and "shading" in line and "false" in line:
      line = line.replace('false', 'true')

    # Change font size
    line = footnotify(line)

    # Remove extra space in front of `PROVE' keyword
    line = line.replace('{\\PROVE}\\@s{2.0}', '{\\PROVE}')
    if assume_in_line:  # ASSUME in previous line
      if 'PROVE' in line and '\\@x{' not in line:
        line = line.replace('{\\PROVE}', '{\\PROVE}\\@s{-4.1}')
    if 'ASSUME' in line: assume_in_line = True
    else: assume_in_line = False


os.rename(tmp[1], f)
os.system('pdflatex ' + fname + '.tex')