이는 Ubuntu Online, Fedora Online, Windows 온라인 에뮬레이터 또는 MAC OS 온라인 에뮬레이터와 같은 여러 무료 온라인 워크스테이션 중 하나를 사용하여 OnWorks 무료 호스팅 공급자에서 실행할 수 있는 coqchk.opt 명령입니다.
프로그램:
이름
coqchk - Coq Proof Checker 컴파일된 라이브러리 검증기
개요
코크치크 [ 옵션 ] 모듈
기술
코크치크 컴파일된 라이브러리(coqc에서 생성한 .vo 파일)의 독립 실행형 검사기입니다.
Coq 증명 도우미. 자세한 내용은 참조 설명서를 참조하십시오. 다음과 같이 반환됩니다.
요청된 모든 작업이 성공한 경우 종료 코드 0. XNUMX이 아닌 반환 코드는 다음을 의미합니다.
문제 발생: 일부 라이브러리를 찾을 수 없음, 손상된 콘텐츠, 유형 확인
고장 등
모듈 확인할 모듈 목록입니다. 모듈은 짧은 또는
정규화된 이름.
옵션
-I 디렉토리, --포함하다 DIR
디렉토리 추가 DIR 포함 경로에서
-R DIR 콕디르
재귀적으로 물리적 매핑 DIR 논리적으로 콕디르
-조용한
coqchk를 덜 장황하게 만듭니다.
-인정하다 모듈
지정된 모듈과 모든 종속성을 신뢰할 수 있는 것으로 태그 지정하고
다른 옵션에서 명시적으로 요청하지 않는 한 다시 확인합니다.
-노렉 모듈
지정된 모듈이 확인 요청 없이 확인되도록 지정합니다.
종속성.
-미디엄, --메모리
검사기가 사용한 메모리 요약을 표시합니다.
-영형, --출력 컨텍스트
검증된 논리적 내용의 요약 표시: 가정 및
예측 불가능성 사용.
- 암시적 집합
검사기가 이 플래그로 컴파일된 라이브러리를 수락할 수 있습니다.
-v coqchk 버전을 인쇄하고 종료합니다.
-coqlib DIR
표준 라이브러리의 기본 위치를 재정의합니다.
-어디 coqchk 표준 라이브러리 위치를 인쇄하고 종료합니다.
-시간, --도움
옵션 목록 인쇄
onworks.net 서비스를 사용하여 coqchk.opt 온라인 사용
