Como gerar um pdf a partir de um arquivo do Coq?
1. Gerando um pdf a partir de um arquivo do Coq via \LaTeX
Existem diversas maneiras de gerar um pdf a partir de um arquivo do Coq. Assumimos que você tem o \LaTeX instalado no seu computador.
- Crie um diretório contendo um arquivo inicial do \LaTeX, digamos
relatorio.tex
(um exemplo encontra-se disponível em http://flaviomoura.info/files/relatorio.tex); o arquivo de configuraçãocoqdoc.sty
(disponível em http://flaviomoura.info/files/coqdoc.sty); e o seu arquivo do Coq, digamosfileCoq.v
. - Digite em um terminal (no diretório que contém o arquivo Coq): coqdoc –latex –body-only -s fileCoq.v
- Em seguida, digite: pdflatex relatorio.tex
- Abra o arquivo relatorio.pdf com o aplicativo de sua preferência.
- Para mais informações sobre o CoqDoc, consulte https://coq.inria.fr/refman/using/tools/coqdoc.html