如何在Sublime Text自定义构建中嵌入子命令指定Tamarin引理？

1. 创建自定义构建系统文件 #

打开Sublime Text，依次点击Tools > Build System > New Build System，将默认内容替换为以下配置：

{
    "shell_cmd": "tamarin-prover --diff $file $(python3 extract_lemma_cmd.py $file)",
    "shell": true,
    "working_dir": "${file_path}",
    "file_regex": "^(.*?)(\\((\\d+),(\\d+)\\))?: (.*)$",
    "selector": "source.spthy"
}

2. 关键配置解析 #

• shell_cmd：直接复用你在终端中使用的命令格式，其中$file是Sublime内置变量，会自动替换为当前打开的模型文件路径；$(python3 extract_lemma_cmd.py $file)会先执行Python脚本提取用户定义引理，将输出结果作为参数传递给tamarin-prover。
• shell: true：必须开启此选项，让Sublime调用系统默认shell（如bash）执行命令，这样才能支持$()这种命令替换语法。
• working_dir：设置为当前文件所在目录，确保脚本和模型文件的路径解析不会出错。
• file_regex：用于匹配Tamarin输出的错误信息，方便Sublime快速跳转到对应代码行。
• selector：指定该构建系统仅对.spthy文件生效，打开这类文件时会自动选中此构建系统。

3. 保存并使用 #

将文件保存为Tamarin-Prove-Custom.sublime-build，保存位置选择Sublime的User目录（保存时会自动定位到该目录）。之后打开你的.spthy模型文件，按下Ctrl+B（Linux/Windows）或Cmd+B（Mac）即可执行自定义命令，仅证明用户定义的引理。

注意事项 #

• 确保python3和tamarin-prover已加入系统PATH，Sublime能正常找到这两个命令。
• 如果extract_lemma_cmd.py不在当前工作目录，需在命令中填写脚本的绝对路径（例如/home/your-username/scripts/extract_lemma_cmd.py）。

内容的提问来源于stack exchange，提问作者Mohit Kumar Jangid