이는 Ubuntu Online, Fedora Online, Windows 온라인 에뮬레이터 또는 MAC OS 온라인 에뮬레이터와 같은 여러 무료 온라인 워크스테이션 중 하나를 사용하여 OnWorks 무료 호스팅 공급자에서 실행할 수 있는 coqdoc 명령입니다.
프로그램:
이름
coqdoc - Coq 증명 도우미를 위한 문서화 도구
개요
coqdoc [ 옵션 ] 파일
기술
coqdoc Coq 교정 지원을 위한 문서화 도구입니다. LaTeX 또는 HTML을 생성합니다.
Coq 파일 세트의 문서. 문서는 Coq 참조 설명서를 참조하십시오(url
아래).
옵션
사무용 겉옷 옵션
-h 돕다. coqdoc에서 허용하는 전체 옵션 목록을 제공합니다.
--html HTML 출력을 선택합니다.
--유액
LATEX 출력을 선택합니다.
--dvi DVI 출력을 선택합니다.
--추신 PostScript 출력을 선택합니다.
--texmacs
TeXmacs 출력을 선택합니다.
--stdout
출력을 stdout으로 리디렉션
-o 파일--산출 파일
출력을 파일로 리디렉션 파일.
-d 디렉토리, --예배 규칙서 DIR
파일을 디렉토리로 출력 DIR 현재 디렉토리 대신(옵션 -d는
-o 옵션으로 지정된 파일 이름을 변경하십시오(있는 경우).
-에스, --짧은
파일의 제목을 삽입하지 마십시오. 기본 동작은 다음과 같은 제목을 삽입하는 것입니다.
각 파일에 대한 ``라이브러리 Foo''.
-t 끈, --제목 현
문서 제목을 설정합니다.
--몸만
최종 문서의 헤더와 트레일러를 억제합니다. 따라서 다음을 삽입할 수 있습니다.
결과 문서를 더 큰 문서로 만듭니다.
-p 끈, --전문 현
\begin{document} 바로 앞에 LATEX 서문에 내용을 삽입한다.
(-html에서는 의미 없음).
--vernac 파일 파일 --tex 파일 파일
파일 `file'을 각각 .v(또는 .g) 파일 또는 .tex 파일로 간주합니다.
--파일-출처 파일
명령에 주어진 것처럼 파일 `file'에서 처리할 파일 이름을 읽습니다.
선. 여러 디렉토리로 분할된 프로그램 소스에 유용합니다.
-NS, --조용한
조용히 해. 오류를 제외하고는 아무 것도 인쇄하지 마십시오.
-시간, --도움
옵션에 대한 간략한 요약을 제공하고 종료합니다.
-V, --번역
버전을 인쇄하고 종료합니다.
색인 옵션
기본 동작은 HTML 출력 전용 인덱스를 index.html로 빌드하는 것입니다.
--인덱스 없음
인덱스를 출력하지 마십시오.
--다중 인덱스
색인의 각 카테고리 및 각 문자에 대해 한 페이지를 생성합니다.
톱 페이지 index.html.
작업대 of 내용 선택권
-톡, --목차
목차를 삽입합니다. LATEX 출력의 경우 다음 위치에 \tableofcontents를 삽입합니다.
문서의 시작. HTML 출력의 경우 목차를 작성합니다.
toc.html로.
하이퍼 링크 옵션
--glob-from 파일
파일 파일에서 Coq 세계화를 사용하여 참조를 만듭니다. (이러한 세계화는
Coq 옵션 -dump-glob으로 획득).
--외부 없음
Coq 표준 라이브러리에 대한 링크를 삽입하지 마십시오.
--외부의 URL libroot
루트 접두사가 libroot인 외부 라이브러리의 기본 URL을 설정합니다.
--coqlib URL
Coq 표준 라이브러리의 기본 URL을 설정합니다(기본값은
http://coq.inria.fr/library/).
--coqlib_path DIR
Coq 파일, 특히 스타일 파일이 설치된 기본 경로를 설정합니다.
coqdoc.sty 및 coqdoc.css.
-R DIR 콕디르
물리적 디렉토리 dir을 Coq 논리 디렉토리 coqdir에 매핑(Coq 옵션과 유사)
-아르 자형). 참고 : 옵션 -R은 명령에서 다음 파일에만 영향을 미칩니다.
줄이므로 이 옵션을 먼저 넣어야 할 것입니다.
내용 옵션
-NS, --갈리나
교정을 인쇄하지 마십시오.
-엘, --빛
라이트 모드. 증명 억제(-g 사용) 및 다음 명령:
* [재귀] 전술 정의
* 힌트 / 힌트
* 필요하다
* 투명/불투명
* 암시적 인수/암시적
* 섹션 / 변수 / 가설 / 종료
옵션 -g 및 -l의 동작은 (* begin show를 사용하여 로컬에서 재정의할 수 있습니다.
*) ... (* end show *) 환경(위 참조).
지원하는 언어 옵션
기본 동작은 ASCII 7비트 입력 파일을 가정하는 것입니다.
-latin1, --latin1
ISO-8859-1 입력 파일을 선택합니다. --inputenc latin1 --charset과 동일합니다.
iso-8859-1.
-utf8, --utf8
UTF-8(유니코드) 입력 파일을 선택합니다. --inputenc utf8 --charset과 동일합니다.
UTF-8. LATEX UTF-8 지원은 다음에서 찾을 수 있습니다.
http://www.ctan.org/tex-archive/macros/latex/contrib/supported/unicode/.
--입력 현
LATEX 패키지 inputenc에 대한 옵션으로 LATEX 입력 인코딩을 제공한다.
--문자셋 현
HTML 헤더에 삽입할 HTML 문자 집합을 지정합니다.
onworks.net 서비스를 사용하여 온라인에서 coqdoc 사용