coqdoc - En ligne dans le Cloud

PROGRAMME:

Nom

coqdoc - Un outil de documentation pour l'assistant de preuve Coq

SYNOPSIS

coqdoc [ Options ] fichiers

DESCRIPTION

coqdoc est un outil de documentation pour l'assistant de preuve Coq. Il crée LaTeX ou HTML
documents à partir d'un ensemble de fichiers Coq. Voir le manuel de référence Coq pour la documentation (url
ci-dessous).

OPTIONS

En Conclusion: Options
-h Aider. Vous donnera la liste complète des options acceptées par coqdoc.

--html Sélectionnez une sortie HTML.

--latex
Sélectionnez une sortie LATEX.

--dvi Sélectionnez une sortie DVI.

--PS Sélectionnez une sortie PostScript.

--texmacs
Sélectionnez une sortie TeXmacs.

--stdout
Rediriger la sortie vers stdout

-o fichier,--output filet
Rediriger la sortie dans le fichier fichier.

-d d, --annuaire dir
Fichiers de sortie dans le répertoire dir au lieu du répertoire courant (l'option -d ne
changer le nom de fichier spécifié avec l'option -o, le cas échéant).

-Oui, --court
N'insérez pas de titres pour les fichiers. Le comportement par défaut est d'insérer un titre comme
``Library Foo'' pour chaque fichier.

-t chaîne, --Titre un magnifique
Définissez le titre du document.

--corps uniquement
Supprimer l'en-tête et la fin du document final. Ainsi, vous pouvez insérer le
document résultant dans un plus grand.

-p chaîne, --préambule un magnifique
Insérez du matériel dans le préambule LATEX, juste avant \begin{document}
(sans signification avec -html).

--vernac-fichier fichier, --tex-fichier filet
Considére le fichier `file' respectivement comme un fichier .v (ou .g) ou un fichier .tex.

--files-de filet
Lire les noms de fichiers à traiter dans le fichier « fichier » comme s'ils étaient donnés sur la commande
ligne. Utile pour les sources de programme réparties dans plusieurs répertoires.

-q, --silencieux
Soyez silencieux. N'imprimez rien d'autre que des erreurs.

-h, --Aidez-moi
Donnez un bref résumé des options et quittez.

-dans, --version
Imprimez la version et quittez.

Sommaire Options
Le comportement par défaut consiste à créer un index, pour la sortie HTML uniquement, dans index.html.

--pas d'index
Ne pas sortir l'index.

--multi-index
Générez une page pour chaque catégorie et chaque lettre de l'index, ainsi qu'un
première page index.html.

lampe de table of contenu option
-toc, --table des matières
Insérer une table des matières. Pour une sortie LATEX, il insère une \tableofcontents à
le début du document. Pour une sortie HTML, il construit une table des matières
dans toc.html.

Liens hypertextes Options
--glob-de filet
Faire des références en utilisant les globalisations Coq à partir du fichier fichier. (De telles mondialisations sont
obtenu avec l'option Coq -dump-glob).

--pas d'externes
N'insérez pas de liens vers la bibliothèque standard Coq.

--externe url Libroot
Définissez l'URL de base pour la bibliothèque externe dont le préfixe racine est libroot.

--coqlib url
Définir l'URL de base pour la bibliothèque standard Coq (la valeur par défaut est
http://coq.inria.fr/library/).

--coqlib_path dir
Définir le chemin de base où les fichiers Coq sont installés, en particulier les fichiers de style
coqdoc.sty et coqdoc.css.

-R dir coqdir
Mappez le répertoire physique dir vers le répertoire logique Coq coqdir (de la même manière que l'option Coq
-R). Remarque: l'option -R n'a d'effet que sur les fichiers qui la suivent sur la commande
ligne, vous devrez donc probablement mettre cette option en premier.

Table des matières Options
-g, --galline
N'imprimez pas d'épreuves.

-l, --léger
Mode lumière. Supprimez les preuves (comme avec -g) et les commandes suivantes :

* [Récursif] Définition de la tactique
* Indice / Indices
* Exiger
* Transparente / Opaque
* Argument implicite / Implicites
* Section / Variable / Hypothèse / Fin

Le comportement des options -g et -l peut être modifié localement en utilisant le (* begin show
*) ... (* end show *) environnement (voir ci-dessus).

Langue Options
Le comportement par défaut est de supposer des fichiers d'entrée ASCII 7 bits.

-latin1, --latin1
Sélectionnez les fichiers d'entrée ISO-8859-1. C'est équivalent à --inputenc latin1 --charset
iso-8859-1.

-utf8, --utf8
Sélectionnez les fichiers d'entrée UTF-8 (Unicode). C'est équivalent à --inputenc utf8 --charset
utf-8. La prise en charge de LATEX UTF-8 est disponible sur
http://www.ctan.org/tex-archive/macros/latex/contrib/supported/unicode/.

--entrée un magnifique
Donnez un codage d'entrée LATEX, en option au package LATEX inputenc.

--jeu de caractères un magnifique
Spécifiez le jeu de caractères HTML à insérer dans l'en-tête HTML.

Utiliser coqdoc en ligne en utilisant les services onworks.net