Il s'agit de la commande coq-tex 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
coq-tex - Traiter des phrases Coq intégrées dans des fichiers LaTeX
SYNOPSIS
coq tex [ -o fichier de sortie ] [ -n largeur de ligne ] [ -image image-coq ] [ -w ] [ -v ] [ -sl ] [
-hrule ] [ -petit ] fichier-entrée
DESCRIPTION
La coq tex le filtre extrait les phrases Coq intégrées dans les fichiers LaTeX, les évalue et
insérer le résultat de l'évaluation après chaque phrase.
Trois environnements LaTeX sont fournis pour inclure le code Coq dans les fichiers d'entrée :
coq_exemple
Les phrases entre \begin{coq_example} et \end{coq_example} sont évaluées et
copié dans le fichier de sortie. Chaque phrase est suivie de la réponse du
boucle de niveau supérieur.
coq_exemple*
Les phrases entre \begin{coq_example*} et \end{coq_example*} sont évaluées et
copié dans le fichier de sortie. Les réponses de la boucle de niveau supérieur sont rejetées.
coq_eval
Les phrases entre \begin{coq_eval} et \end{coq_eval} sont évaluées en silence.
Elles ne sont pas copiées dans le fichier de sortie, et les réponses de la boucle toplevel
sont mis au rebut.
Le code LaTeX résultant est stocké dans le fichier filet.v.tex si le fichier d'entrée porte le nom
la forme filet.tex, sinon le nom du fichier de sortie est le nom du fichier d'entrée
avec `.v.tex' ajouté.
Les fichiers produits par coq tex peut être directement traité par LaTeX. Les deux phrases Coq
et la sortie de niveau supérieur sont composées en police de machine à écrire.
OPTIONS
-o fichier de sortie
Spécifiez le nom d'un fichier où la sortie LaTeX doit être stockée. Un tiret "-"
provoque l'impression de la sortie LaTeX sur la sortie standard.
-n largeur de ligne
Définissez la largeur de ligne. La valeur par défaut est de 72 caractères. Les réponses du plus haut niveau
boucle sont pliés s'ils sont plus longs que la largeur de la ligne. Aucun pliage n'est effectué sur
le texte d'entrée Coq.
-image image-coq
Parce que le fichier image-coq à exécuter pour évaluer les phrases Coq. Par défaut,
c'est la commande coq sans spécifier de chemin utilisé pour évaluer
les phrases du Coq.
-w Faire en sorte que les lignes soient pliées sur un caractère espace dans la mesure du possible, en évitant les coupures de mots
dans la sortie. Par défaut, le pliage se produit à la largeur de la ligne, quel que soit le mot
coupes.
-v Mode verbeux. Imprime les réponses Coq sur la sortie standard. Utile pour détecter
erreurs dans les phrases Coq.
-sl Mode incliné. Les réponses Coq sont écrites dans une police inclinée.
-hrule Mode lignes horizontales. Les parties Coq sont écrites entre deux lignes horizontales.
-petit Mode petite police. Les parties Coq sont écrites dans une police plus petite.
MISES EN GARDE
Les phrases \begin... et \end... doivent se trouver sur une ligne par elles-mêmes, sans caractères
avant la barre oblique inverse ou après l'accolade fermante. Chaque phrase Coq doit se terminer par
`.' à la fin d'une ligne. Les espaces vides sont acceptés entre `.' et la nouvelle ligne, mais tout
un autre caractère fera que coq-tex ignore la fin de la phrase, ce qui entraîne un
mélange incorrect des réponses dans les phrases. (Les réponses « à la traîne ».)
Utilisez coq-tex en ligne en utilisant les services onworks.net
