Article latex document class out of a Coq script

Using Coq
1

Hi there,

I would like to know if there exists a direct way to generate a pdf out of a Coq script annotated with coqdoc using a given latex document class, like article or llncs. I usually do it by first generating the latex output of the coq script file with coqdoc, and then compiling the latex output separately (after some editing), but this sequence of repetitive steps is a bit annoying.

Best regards,
Flávio.

2

Hi there,

This is another question related to the previous one. I usually need to insert a tex file generated from a annotated coq file via coq. Suppose my coq file starts with an introduction section:

(** * Introduction *)

The coqdoc generates the tex file via the command:

coqdoc --latex --body-only myfile.v

The generated output is as follows:

\coqlibrary{myfile}{Library }{myfile}
\begin{coqdoccode}
\coqdocemptyline
\end{coqdoccode}
\section{Introduction}

Is it possible to generate the output tex file without these four initial line? I mean, is it possible to generate the output starting with the following line (as in the Coq script)?

\section{Introduction}

Thank you very much in advance.
Flávio.

3

Well, you could pipe the ouput of coqdoc into the command tail -n +5 to skip the first 4 lines.

1 Like