Il s'agit de la commande coqdoc qui peut être exécutée dans le fournisseur d'hébergement gratuit OnWorks en utilisant l'un de nos multiples postes de travail en ligne gratuits tels que Ubuntu Online, Fedora Online, l'émulateur en ligne Windows ou l'émulateur en ligne MAC OS
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).
Connection Linguistique 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