Este é o comando coqmktop que pode ser executado no provedor de hospedagem gratuita OnWorks usando uma de nossas várias estações de trabalho online gratuitas, como Ubuntu Online, Fedora Online, emulador online do Windows ou emulador online do MAC OS
PROGRAMA:
NOME
coqmktop - O vinculador de táticas de usuário do Coq Proof Assistant
SINOPSE
coqmktop [ opções ] arquivos
DESCRIÇÃO
coqmktop constrói um novo nível superior do Coq estendido com táticas de usuário. arquivos são o objetivo
Objeto Caml ou arquivos de biblioteca (ou seja, com sufixo .cmo, .cmx, .cma ou .cmxa) para vincular com o
Sistema Coq. O vinculador produz um Coq de nível superior executável que pode ser chamado diretamente
Ou através de coqc(1), usando a opção -image.
OPÇÕES
-h Ajuda. Liste as opções disponíveis.
-srcdir dir
Especifique onde estão os arquivos de origem Coq
-o arquivo exec
Especifique o nome do nível superior resultante
-optar Compilar em código nativo
-cheio Vincule táticas de alto nível
-topo Construir Coq em um nível superior ocaml (incompatível com -optar)
-R dir Especifique diretórios recursivamente para Ocaml
-v8 Link com gramática V8
Use coqmktop online usando serviços onworks.net
