Il s'agit de la commande coqmktop 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
coqmktop - L'éditeur de liens tactiques utilisateur Coq Proof Assistant
SYNOPSIS
ordinateur de bureau [ Options ] fichiers
DESCRIPTION
ordinateur de bureau construit un nouveau niveau supérieur Coq étendu avec des tactiques utilisateur. fichiers sont l'objectif
Objets Caml ou fichiers de bibliothèque (c'est-à-dire avec le suffixe .cmo, .cmx, .cma ou .cmxa) à lier avec le
Système Coq. L'éditeur de liens produit un toplevel Coq exécutable qui peut être appelé directement
Ou à travers coqc(1), en utilisant l'option -image.
OPTIONS
-h Aider. Lister les options disponibles.
-srcdir dir
Précisez où se trouvent les fichiers sources Coq
-o fichier-exec
Spécifiez le nom du niveau supérieur résultant
-opter Compiler en code natif
-full Reliez les tactiques de haut niveau
-Haut Construire Coq sur un toplevel ocaml (incompatible avec -opter)
-R dir Spécifier récursivement les répertoires pour Ocaml
-v8 Lien avec la grammaire V8
Utilisez coqmktop en ligne en utilisant les services onworks.net
