이것은 Ubuntu Online, Fedora Online, Windows 온라인 에뮬레이터 또는 MAC OS 온라인 에뮬레이터와 같은 여러 무료 온라인 워크스테이션 중 하나를 사용하여 OnWorks 무료 호스팅 공급자에서 실행할 수 있는 명령 coqide입니다.
프로그램:
이름
coqide - Coq Proof Assistant 그래픽 인터페이스
개요
코키드 [ 옵션 ]
기술
코키드 Coq 증명 도우미를 위한 gtk 그래픽 인터페이스입니다.
Coq의 명령줄 기반 사용에 대해서는 다음을 참조하십시오. 콕탑(1) ; Coq의 배치 지향 사용에 대해서는 다음을 참조하십시오.
coqc(1).
옵션
-h 에서 허용하는 전체 옵션 목록 표시 코키드.
-I DIR, -포함 DIR
포함 경로에 디렉토리 dir을 추가하십시오.
-R DIR 콕디르
재귀적으로 물리적 매핑 DIR 논리적으로 콕디르.
-src 포함 경로에 소스 디렉토리를 추가하십시오.
-는 f, -입력 상태 f
상태 읽기 f.coq.
-소음 빈 상태로 시작하십시오.
-출력 상태 f
파일에 상태 쓰기 f.coq.
-load-ml-개체 f
ML 개체 파일 로드 f.
-load-ml-소스 f
ML 파일 로드 f.
-l f, -로드-버낙-소스 f
Coq 파일 로드 f.v(로드 f..)
-lv f, -로드-베르낙-소스-상세 f
Coq 파일 로드 f.v(상세 로드 f..)
-로드 버낙 객체 f
Coq 개체 파일 로드 f.보.
-필요하다 f
Coq 개체 파일 로드 f.vo 및 가져오기(필수 f..)
-엮다 f
Coq 파일 컴파일 f.v(의미 -일괄).
-컴파일 장황 f
Coq 파일을 장황하게 컴파일 f.v(의미 -일괄).
-고르다 Coq 또는 Coq_SearchIsos의 네이티브 코드 버전을 실행합니다.
-바이트 Coq 또는 Coq_SearchIsos의 바이트코드 버전을 실행합니다.
-어디 Coq의 표준 라이브러리 위치를 인쇄하고 종료합니다.
-v Coq 버전을 인쇄하고 종료합니다.
-q rcfile의 로드를 건너뜁니다.
-초기화 파일 f
rcfile을 다음과 같이 설정하십시오. f.
-일괄 배치 모드(인수 구문 분석 직후 종료).
-신병 부팅 모드( -q 및 -일괄).
-이맥스 Coq에게 Emacs에서 실행된다고 알려줍니다.
-덤프 글로브 f
파일의 덤프 세계화 f (에 의해 사용 coqdoc(삼)).
- 암시적 집합
정렬 설정 암시적 설정.
-내하중 방지
메모리에 불투명한 증명을 로드하지 마십시오.
-xml 디렉토리를 기반으로 하는 계층 구조로 XML 파일 내보내기
COQ_XML_LIBRARY_ROOT (설정된 경우) 또는 stdout으로 (설정되지 않은 경우).
onworks.net 서비스를 사용하여 온라인에서 coqide 사용