To jest polecenie coqchk.opt, które można uruchomić u dostawcy bezpłatnego hostingu OnWorks przy użyciu jednej z naszych wielu darmowych stacji roboczych online, takich jak Ubuntu Online, Fedora Online, emulator online Windows lub emulator online MAC OS
PROGRAM:
IMIĘ
coqchk - weryfikator skompilowanych bibliotek Coq Proof Checker
STRESZCZENIE
coqchk [ Opcje ] Moduły
OPIS
coqchk jest samodzielnym narzędziem do sprawdzania skompilowanych bibliotek (plików .vo produkowanych przez coqc) dla
Asystenta Coq Proof. Więcej informacji można znaleźć w instrukcji obsługi. Wraca z
kod zakończenia 0, jeśli wszystkie żądane zadania powiodły się. Niezerowy kod powrotu oznacza, że
coś poszło nie tak: nie znaleziono jakiejś biblioteki, uszkodzona zawartość, sprawdzanie typu
awaria itp.
Moduły to lista modułów do sprawdzenia. Do modułów można się odwoływać krótkim lub
kwalifikowana nazwa.
OPCJE
-I reż, --włączać reż
dodaj katalog reż w ścieżce dołączania
-R reż koqdir
rekursywnie mapować fizyczne reż do logicznego koqdir
-cichy
sprawia, że coqchk jest mniej gadatliwy.
-przyznawać moduł
oznacz określony moduł i wszystkie jego zależności jako zaufane i nie będzie
ponownie sprawdzane, chyba że wyraźnie zażądają tego inne opcje.
-norek moduł
określa, że dany moduł będzie weryfikowany bez żądania sprawdzenia jego
zależności.
-M, --pamięć
wyświetla podsumowanie pamięci używanej przez sprawdzarkę.
-o, --kontekst-wyjściowy
wyświetla podsumowanie logicznych treści, które zostały zweryfikowane: założenia i
wykorzystanie nierespektywności.
-zestaw imperatywny
pozwala sprawdzającemu akceptować biblioteki, które zostały skompilowane z tą flagą.
-v wydrukuj wersję coqchk i wyjdź.
-koqlib reż
nadpisuje domyślną lokalizację biblioteki standardowej.
-gdzie wydrukuj lokalizację i wyjdź z biblioteki standardowej coqchk.
-H, --help
wydrukuj listę opcji
Korzystaj z coqchk.opt online za pomocą usług onworks.net
