1

coq-tex can pre-process LaTeX files with special environments to put Coq interactions in the output files; the result is ready for use with, say, pdflatex.

I like latexmk, having only recently discovered it, and want it to automatically run coq-tex. How?

2

Based on latexmk: Multiple custom-generated files and \input, I managed to get the following setup mostly working. Configure latexmk with

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';

Then, use the following macro to input tex files with the Coq environments:

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

e.g., \inputcoq{foo}. latexmk should happily regenerate the correct files automatically.

One issue, however, is that neither latexmk -c nor latexmk -C will remove the generated v_tex files. Of secondary concern, coq-tex automatically uses the extension .v.tex, which seemed to choke latexmk when I configure it with add_cus_dep('tex', 'v.tex', 0, 'coqtex'); (and change the rest of the code accordingly). This is because latexmk considers everything after the last dot to be the extension.

4
  • To get the files generated by custom dependenciess removed when you do a latexmk clean (-c or -C) put the line $cleanup_includes_cusdep_generated = 1; in a configuration file. – John Collins Apr 14 at 19:37
  • About using the extension v.tex: A lot of people define the extension to be what's after the last period, i.e., "tex", and that's the choice made by latexmk. It would need a bit of programming to change that. It's probably better to use v_tex, as you are doing. – John Collins Apr 14 at 19:42
  • @JohnCollins thanks for the insight on the extension; will add. I didn't have to change $cleanup_includes_cusdep_generated for other rules (I have several for glossaries, and this is enough: push @generated_exts, 'glo', 'gls', 'acn', 'acr', 'slo', 'sls', 'ist', 'glg', 'alg', 'slg';), so not sure there – D. Ben Knoble Apr 14 at 21:18
  • The use of @generated_exts is about those files that have the same basename as the tex file. That's why using this variable worked before. The documentation could be clearer about that. – John Collins Apr 15 at 0:17

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.