이것은 Ubuntu Online, Fedora Online, Windows 온라인 에뮬레이터 또는 MAC OS 온라인 에뮬레이터와 같은 여러 무료 온라인 워크스테이션 중 하나를 사용하여 OnWorks 무료 호스팅 제공업체에서 실행할 수 있는 명령 coqmktop입니다.
프로그램:
이름
coqmktop - Coq Proof Assistant 사용자 전술 링커
개요
coqmktop [ 옵션 ] 파일
기술
coqmktop 사용자 전술로 확장된 새로운 Coq 최상위 레벨을 구축합니다. 파일 목표입니다
Caml 개체 또는 라이브러리 파일(예: 접미사 .cmo, .cmx, .cma 또는 .cmxa 포함)
콕 시스템. 링커는 직접 호출할 수 있는 실행 가능한 Coq 최상위 레벨을 생성합니다.
또는을 통해 coqc(1) -image 옵션을 사용합니다.
옵션
-h 돕다. 사용 가능한 옵션을 나열합니다.
-srcdir DIR
Coq 소스 파일의 위치 지정
-o 실행 파일
결과 최상위 레벨의 이름을 지정하십시오.
-고르다 네이티브 코드로 컴파일
-완전한 높은 수준의 전술 연결
-상단 ocaml 최상위 레벨에서 Coq 빌드(호환되지 않음 -고르다)
-R DIR Ocaml에 대해 재귀적으로 디렉토리 지정
-v8 V8 문법과 연결
onworks.net 서비스를 사용하여 온라인 coqmktop 사용
