如何通过 TLA+ 工具箱有效地使用 git答案

【问题标题】：How to use git effectively with TLA+ toolbox如何通过 TLA+ 工具箱有效地使用 git
【发布时间】：2022-07-10 01:00:43
【问题描述】：

TLA+ 工具箱创建了大量文件和目录。使用规范和模型并将它们保持在 git 中的版本以及使用工具箱的好方法是什么？正常的工作流程是什么样的？

【问题讨论】：

标签： tla+

【解决方案1】：

我在.gitignore 中完全忽略了*.toolbox。这意味着模型配置没有保存在不理想的 repo 中。

使用 VS Code 插件可以实现良好的工作流程，该插件依赖于配置模型常量和检查哪些不变量/属性的顶级 .cfg 文件。

这是我的.gitignore

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

我保留了一个 Makefile，用于执行一些有用的任务，例如清理这些辅助文件并将打印精美的 PDF 保存在单独的 dist/ 文件夹中。

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

【讨论】：

【解决方案2】：

将此添加到.gitignore 将仅保留模型参数文件，例如MySpec.toolbox/MySpec__Model_1.lauch，我发现如果所有其他文件丢失，我只需要恢复模型：

# TLA+ Toolbox files, this will keep <spec_name>__<model_name>.launch
/*.toolbox/.settings
/*.toolbox/.project
/*.toolbox/*/*
/*.toolbox/*_SnapShot_*.launch
# TLA+ Toolbox PDF production artifacts
/*.toolbox/*.aux
/*.toolbox/*.log
/*.toolbox/*.tex
/*.toolbox/*.pdf
/*.pdf

您可以通过这些步骤验证它是否足够：

提交MySpec.toolbox/MySpec__Model_1.lauch
关闭工具箱中的规范（如果您不这样做，工具箱将显示错误，您可以在下次打开时将其关闭）
退出工具箱
删除MySpec.toolbox/ 中除MySpec__Model_1.lauch 之外的所有内容
重新打开工具箱
使用Add New Spec... 重新打开您的规范
重新创建一个与以前同名的模型，在此示例中为 Model_1
保存并关闭模型
退出工具箱
保存模型时删除工具箱对MySpec.toolbox/MySpec__Model_1.lauch所做的更改
重新打开工具箱

目前唯一的缺点是MySpec.toolbox/MySpec__Model_1.lauch 中存储的参数调用fpIndex 在每次模型执行时都会发生变化，请参阅https://tla.msr-inria.inria.fr/tlatoolbox/doc/model/tlc-options-page.html 中的指纹种子索引。这会导致该文件每次都出现在 git 中更改的文件中。

【讨论】：