Holmake to build LaTeX (with HOL inclusions)

[hol-theorem-prover]

Holmake to build LaTeX (with HOL inclusions)

[xrchz]

Doesn't this work already? I use Holmake to build my PDFs...
I use it in combination with Chris Monsoon's LaTeX Makefile.

[mn200]

Presumably you have Holmake call make? I'd like a solution that doesn't depend on external tools.

[xrchz]

I understand that desire, but we need to be reasonable about the cut-off point. I presume you don't want to re-implement pdflatex or xetex or latex and dvi2pdf or whatever the right command to invoke LaTeX is. The LaTeX Makefile abstracts away from all this and just builds a pdf with as many invocations to TeX wrappers underneath as required. But it depends on make. Should Holmake be able to interpret it?

[mn200]

It's always struck me that the latex-makefile makes too alarming a use of all the tricks of GNU make to want to be able to do it myself. I only recently learnt of the existence of the latexmk; perhaps this would be as good a thing to tell people to use. It has the advantage that it apparently works on Windows without requiring a make implementation.

[xrchz]

So it's a choice between depending on perl or depending on make. Both seem reasonable to me. I haven't tried latexmk so can't vouch for it. Should HOL ship with latexmk or LateX Makefile or neither, in order to close this issue?

[mn200]

I think if people have a TeX installation at all, there's a strong chance they'll have latexmk. The issue is that they may not have perl. And I certainly don't want to distribute perl. I'll close this and remember that our standard advice is for people to call latexmk