# Integrate coq-tex with latexmk

`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?

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.

• 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