☰

将 coq-tex 与 latexmk 集成

tag-icon • tag-icon latexmk
将 coq-tex 与 latexmk 集成

coq-tex可以使用特殊环境预处理 LaTeX 文件，将 Coq 交互放入输出文件中；结果即可用于pdflatex。

我喜欢latexmk，最近才发现它，并希望它自动运行 coq-tex。怎么做？

答案1

基于latexmk：多个自定义生成的文件和 \input，我设法使以下设置基本正常工作。latexmk配置

add_cus_dep('tex', 'v_tex', 0, 'coqtex');
sub coqtex {
    system("coq-tex -sl \"$_[0].tex\" -o \"$_[0].v_tex\"");
}
push @generated_exts, 'v_tex';

然后，使用以下宏input在 Coq 环境中对 tex 文件进行操作：

\newcommand{\inputcoq}[1]{\InputIfFileExists{#1.v_tex}{}{\typeout{No file #1.v_tex.}}}

例如，\inputcoq{foo}.latexmk应该会自动重新生成正确的文件。

但是，有一个问题是，无论是latexmk -c还是latexmk -C都不会删除生成的v_tex文件。第二个问题是，它coq-tex会自动使用扩展名，当我用它配置它（并相应地更改其余代码）时.v.tex，它似乎会卡住。这是因为将最后一个点之后的所有内容都视为扩展名。latexmkadd_cus_dep('tex', 'v.tex', 0, 'coqtex');latexmk

相关内容