'How to use git effectively with TLA+ toolbox

The TLA+ toolbox creates a lot of files and directories. What's a good way to work with the spec and the model and keep them versioned in git, and also use the toolbox? What does a normal workflow look like?

tla+


Solution 1:[1]

I have completely ignored *.toolbox in my .gitignore. This means model configuration is not preserved in the repo which is not ideal.

A good workflow is possible with the VS Code plugin that relies on top-level .cfg files configuring model constants and which invariants/properties to check.

This is my .gitignore

*.dvi
*.old
*.out
*.pdf
*.tex
*.toolbox

I keep a Makefile with useful tasks like cleaning up these auxiliary files and maintaining pretty-printed PDFs in a separate dist/ folder.

JAVA ?= java
TLA2TOOLS_JAR = "tla2tools.jar"
TLA2TOOLS ?= $(JAVA) --class-path $(TLA2TOOLS_JAR)
TLA2TEX ?= $(JAVA) --class-path ../$(TLA2TOOLS_JAR) \
                                           tla2tex.TLA -latexCommand "pdflatex" -shade -grayLevel 0.9

DISTDIR = dist
PDFS = $(addprefix $(DISTDIR)/, $(patsubst %.tla, %.pdf, $(wildcard *.tla)))

all: dist

pdfs: $(PDFS)

$(DISTDIR)/%.pdf: %.tla
        cd $(DISTDIR) && $(TLA2TEX) ../$^

dist: pdfs clean

clean:
        @echo "Cleaning auxiliary TLA2TeX files"
        @rm -f $(DISTDIR)/*.aux $(DISTDIR)/*.dvi $(DISTDIR)/*.log $(DISTDIR)/*.tex

distclean: clean
        rm -f $(DISTDIR)/*.pdf

.PHONY: pdfs dist clean distclean

Sources

This article follows the attribution requirements of Stack Overflow and is licensed under CC BY-SA 3.0.

Source: Stack Overflow

Solution Source
Solution 1 philix

Related Questions