Jest to polecenie coqmktop, które można uruchomić u dostawcy bezpłatnego hostingu OnWorks przy użyciu jednej z naszych wielu bezpłatnych stacji roboczych online, takich jak Ubuntu Online, Fedora Online, emulator online systemu Windows lub emulator online systemu MAC OS
PROGRAM:
IMIĘ
coqmktop — linker taktyki użytkownika Coq Proof Assistant
STRESZCZENIE
coqmktop [ Opcje ] pliki
OPIS
coqmktop buduje nowy najwyższy poziom Coq rozszerzony o taktykę użytkownika. pliki są Celem
Pliki obiektów lub bibliotek Caml (tj. z przyrostkiem .cmo, .cmx, .cma lub .cmxa) do połączenia z
System Coq. Linker tworzy wykonywalny najwyższy poziom Coq, który można wywołać bezpośrednio
lub przez kok(1), używając opcji -image.
OPCJE
-h Pomoc. Lista dostępnych opcji.
-srcdir reż
Określ, gdzie znajdują się pliki źródłowe Coq
-o plik-exec
Określ nazwę wynikowego najwyższego poziomu
-optować Kompiluj w kodzie natywnym
-pełny Połącz taktykę wysokiego poziomu
-Top Zbuduj Coq na najwyższym poziomie ocaml (niekompatybilny z -optować)
-R reż Określ rekursywnie katalogi dla Ocaml
-v8 Link do gramatyki V8
Korzystaj z coqmktop online, korzystając z usług onworks.net
