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.

  1. 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ção coqdoc.sty (disponível em http://flaviomoura.info/files/coqdoc.sty); e o seu arquivo do Coq, digamos fileCoq.v.
  2. Digite em um terminal (no diretório que contém o arquivo Coq): coqdoc –latex –body-only -s fileCoq.v
  3. Em seguida, digite: pdflatex relatorio.tex
  4. Abra o arquivo relatorio.pdf com o aplicativo de sua preferência.
  5. Para mais informações sobre o CoqDoc, consulte https://coq.inria.fr/refman/using/tools/coqdoc.html

Date: 2023-03-29 qua 00:00

Author: Flávio L. C. de Moura

Created: 2024-07-11 qui 17:02