Este é o comando coqchk.opt 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
coqchk - O verificador de bibliotecas compiladas do Coq Proof Checker
SINOPSE
coqchk [ opções ] módulos
DESCRIÇÃO
coqchk é o verificador autônomo de bibliotecas compiladas (arquivos .vo produzidos por coqc) para
o Coq Proof Assistant. Consulte o Manual de Referência para obter mais informações. Retorna com
código de saída 0 se todas as tarefas solicitadas foram bem-sucedidas. Um código de retorno diferente de zero significa que
algo deu errado: alguma biblioteca não foi encontrada, conteúdo corrompido, verificação de tipo
falha etc.
módulos é uma lista de módulos a serem verificados. Os módulos podem ser referidos por um curto ou
nome qualificado.
OPÇÕES
-I é, --incluir dir
adicionar diretório dir no caminho de inclusão
-R dir coqdir
mapear recursivamente físico dir para lógico coqdir
- silencioso
torna o coqchk menos prolixo.
-Admitem módulo
marcar o módulo especificado e todas as suas dependências como confiáveis, e não será
verificado novamente, a menos que explicitamente solicitado por outras opções.
-norec módulo
especifica que o módulo dado deve ser verificado sem a solicitação para verificar seu
dependências.
-m, --memória
exibe um resumo da memória usada pelo verificador.
-ó, --contexto de saída
exibe um resumo do conteúdo lógico que foi verificado: suposições e
uso de impredicatividade.
-conjunto impredicativo
permite que o verificador aceite bibliotecas que foram compiladas com este sinalizador.
-v imprimir a versão coqchk e sair.
-coqlib dir
substitui o local padrão da biblioteca padrão.
-Onde imprimir localização da biblioteca padrão coqchk e sair.
-h, --Socorro
imprimir lista de opções
Use coqchk.opt online usando serviços onworks.net
