coqdoc - Trực tuyến trên Đám mây

CHƯƠNG TRÌNH:

TÊN

coqdoc - Một công cụ tài liệu cho trợ lý bằng chứng Coq

SYNOPSIS

coqdoc [ lựa chọn ] các tập tin

MÔ TẢ

coqdoc là một công cụ tài liệu cho trợ lý bằng chứng Coq. Nó tạo ra LaTeX hoặc HTML
tài liệu từ một tập hợp các tệp Coq. Xem hướng dẫn sử dụng tham chiếu Coq để biết tài liệu (url
dưới đây).

LỰA CHỌN

Tổng thể lựa chọn
-h Cứu giúp. Sẽ cung cấp cho bạn danh sách đầy đủ các tùy chọn được coqdoc chấp nhận.

--html Chọn một đầu ra HTML.

--mủ cao su
Chọn một đầu ra LATEX.

--dvi Chọn một đầu ra DVI.

--ps Chọn một đầu ra PostScript.

--texmac
Chọn một đầu ra TeXmacs.

--thiết bị xuất chuẩn
Chuyển hướng đầu ra sang stdout

-o tập tin,- đầu ra hồ sơ
Chuyển hướng đầu ra vào tệp tập tin.

-d Là, --danh mục dir
Xuất tệp vào thư mục dir thay vì thư mục hiện tại (tùy chọn -d không
thay đổi tên tệp được chỉ định bằng tùy chọn -o, nếu có).

-S, --ngắn
Không chèn tiêu đề cho tệp. Hành vi mặc định là chèn một tiêu đề như
`` Thư viện Foo '' cho mỗi tệp.

-t dây, --chức vụ chuỗi
Đặt tiêu đề tài liệu.

--chỉ cơ thể
Chặn tiêu đề và đoạn giới thiệu của tài liệu cuối cùng. Do đó, bạn có thể chèn
tài liệu kết quả thành một tài liệu lớn hơn.

-p dây, --lời mở đầu chuỗi
Chèn một số tài liệu vào phần mở đầu LATEX, ngay trước khi \ begin {document}
(vô nghĩa với -html).

--vernac-tệp tập tin, --tex-tệp hồ sơ
Coi tệp `tệp 'tương ứng là tệp .v (hoặc .g) hoặc tệp .tex.

--files-từ hồ sơ
Đọc tên tệp để xử lý trong tệp `` tệp '' như thể chúng được cung cấp trên lệnh
hàng. Hữu ích cho các nguồn chương trình được chia thành nhiều thư mục.

-NS, --Yên lặng
Hãy yên lặng. Không in bất cứ thứ gì ngoại trừ lỗi.

-NS, --Cứu giúp
Đưa ra một bản tóm tắt ngắn về các tùy chọn và thoát.

-v, --phiên bản
In phiên bản và thoát.

Chỉ số lựa chọn
Hành vi mặc định là xây dựng một chỉ mục, chỉ dành cho đầu ra HTML, vào index.html.

- không có chỉ mục
Không xuất chỉ mục.

- chỉ số đa
Tạo một trang cho mỗi danh mục và mỗi chữ cái trong chỉ mục, cùng với một
đầu trang index.html.

Bàn of nội dung tùy chọn
-toc, --mục lục
Chèn mục lục. Đối với đầu ra LATEX, nó sẽ chèn một \ tableofcontents tại
phần đầu của tài liệu. Đối với đầu ra HTML, nó xây dựng một mục lục
thành toc.html.

Các siêu liên kết lựa chọn
--glob-từ hồ sơ
Tạo tham chiếu bằng cách sử dụng Coq globalizations từ tệp tệp. (Toàn cầu hóa như vậy là
thu được với tùy chọn Coq -dump-global).

- không bên ngoài
Không chèn liên kết đến thư viện tiêu chuẩn Coq.

--bên ngoài url thư viện
Đặt URL cơ sở cho thư viện bên ngoài có tiền tố gốc là libroot.

--coqlib url
Đặt URL cơ sở cho thư viện tiêu chuẩn Coq (mặc định là
http://coq.inria.fr/library/).

--coqlib_path dir
Đặt đường dẫn cơ sở nơi các tệp Coq được cài đặt, đặc biệt là các tệp kiểu
coqdoc.sty và coqdoc.css.

-R dir coqdir
Ánh xạ thư mục vật lý dir thành thư mục logic Coq coqdir (tương tự như tùy chọn Coq
-NS). Lưu ý: tùy chọn -R chỉ có hiệu lực đối với các tệp theo sau nó trên lệnh
, vì vậy có thể bạn sẽ cần phải đặt tùy chọn này trước tiên.

Nội dung lựa chọn
-NS, --gallina
Không in bản in thử.

-l, --soi rọi
Chế độ sáng. Loại bỏ các bằng chứng (như với -g) và các lệnh sau:

* [Đệ quy] Định nghĩa chiến thuật
* Gợi ý / gợi ý
* Yêu cầu
* Trong suốt / Đục
* Lập luận / Ngụ ý ngầm
* Phần / Biến / Giả thuyết / Kết thúc

Hành vi của các tùy chọn -g và -l có thể được ghi đè cục bộ bằng cách sử dụng (* begin show
*) ... (* end show *) môi trường (xem ở trên).

Ngôn ngữ lựa chọn
Hành vi mặc định là giả sử các tệp đầu vào ASCII 7 bit.

-latin1, --latin1
Chọn tệp đầu vào ISO-8859-1. Nó tương đương với --inputenc latin1 --charset
iso-8859-1.

-utf8, --utf8
Chọn tệp đầu vào UTF-8 (Unicode). Nó tương đương với --inputenc utf8 --charset
utf-8. Hỗ trợ LATEX UTF-8 có thể được tìm thấy tại
http://www.ctan.org/tex-archive/macros/latex/contrib/supported/unicode/.

--inputenc chuỗi
Cung cấp mã hóa đầu vào LATEX, như một tùy chọn cho đầu vào gói LATEX.

--bộ ký tự chuỗi
Chỉ định bộ ký tự HTML, sẽ được chèn vào tiêu đề HTML.

Sử dụng coqdoc trực tuyến bằng các dịch vụ onworks.net