coqchk.opt - Online in de cloud

PROGRAMMA:

NAAM

coqchk - De Coq Proof Checker gecompileerde bibliothekenverificatie

KORTE INHOUD

coqchk [ opties ] modules

PRODUCTBESCHRIJVING

coqchk is de zelfstandige controleur van gecompileerde bibliotheken (.vo-bestanden geproduceerd door coqc) voor
de Coq Proof Assistent. Zie de Naslaggids voor meer informatie. Het keert terug met
exit code 0 als alle gevraagde taken zijn geslaagd. Een retourcode die niet nul is, betekent dat
er is iets misgegaan: een bibliotheek is niet gevonden, de inhoud is beschadigd, er is een typecontrole uitgevoerd
mislukking, etc.

modules is een lijst met modules die moeten worden gecontroleerd. Naar modules kan worden verwezen met een korte of
gekwalificeerde naam.

OPTIES

-I richt, --erbij betrekken dir
map toevoegen dir in het include-pad

-R dir coqdir
recursief fysiek in kaart brengen dir logisch coqdir

-stil
maakt coqchk minder uitgebreid.

-toegeven module
tag de opgegeven module en al zijn afhankelijkheden als vertrouwd, en dat zal niet zo zijn
opnieuw gecontroleerd, tenzij expliciet gevraagd door andere opties.

-norec module
specificeert dat de gegeven module moet worden geverifieerd zonder te vragen om deze te controleren
afhankelijkheden.

-M, --geheugen
geeft een samenvatting weer van het geheugen dat door de checker wordt gebruikt.

-O, --uitvoer-context
geeft een samenvatting weer van de logische inhoud die is geverifieerd: aannames en
gebruik van impredicativiteit.

-impredicatieve-set
staat de controleur toe om bibliotheken te accepteren die met deze vlag zijn gecompileerd.

-v druk de coqchk-versie af en sluit af.

-coqlib dir
overschrijft de standaardlocatie van de standaardbibliotheek.

-waar print coqchk standaard bibliotheeklocatie en sluit af.

-H, --help
lijst met opties afdrukken

Gebruik coqchk.opt online met behulp van onworks.net-services