coqdoc - क्लाउड में ऑनलाइन

कार्यक्रम:

नाम

coqdoc - Coq प्रूफ सहायक के लिए एक दस्तावेज़ीकरण उपकरण

SYNOPSIS

कोकडॉक [ विकल्पों ] फ़ाइलों

वर्णन

कोकडॉक Coq प्रूफ सहायक के लिए एक दस्तावेज़ीकरण उपकरण है। यह LaTeX या HTML बनाता है
Coq फ़ाइलों के एक सेट से दस्तावेज़। दस्तावेज़ीकरण के लिए Coq संदर्भ मैनुअल देखें (url
नीचे).

विकल्प

कुल विकल्पों
-h मदद। आपको coqdoc द्वारा स्वीकृत विकल्पों की पूरी सूची देगा।

--एचटीएमएल एक HTML आउटपुट चुनें।

--लेटेक्स
लेटेक्स आउटपुट चुनें।

--डीवीआई एक डीवीआई आउटपुट चुनें।

--पीएस पोस्टस्क्रिप्ट आउटपुट का चयन करें।

--टेक्समैक्स
एक TeXmacs आउटपुट चुनें।

--stdout
आउटपुट को stdout पर रीडायरेक्ट करें

-o फ़ाइल,--आउटपुट पट्टिका
फ़ाइल में आउटपुट को पुनर्निर्देशित करें फ़ाइल.

-d डीआईआर, --निर्देशिका दीर
निर्देशिका में आउटपुट फ़ाइलें दीर वर्तमान निर्देशिका के बजाय (विकल्प -d नहीं है
विकल्प के साथ निर्दिष्ट फ़ाइल नाम बदलें -ओ, यदि कोई हो)।

-एस, --कम
फाइलों के लिए शीर्षक न डालें। डिफ़ॉल्ट व्यवहार एक शीर्षक सम्मिलित करना है जैसे
प्रत्येक फ़ाइल के लिए ``लाइब्रेरी फू''।

-t स्ट्रिंग, --शीर्षक स्ट्रिंग
दस्तावेज़ का शीर्षक सेट करें।

--केवल शरीर
अंतिम दस्तावेज़ के शीर्षलेख और ट्रेलर को दबाएं। इस प्रकार, आप सम्मिलित कर सकते हैं
परिणामी दस्तावेज़ एक बड़े में।

-p स्ट्रिंग, --प्रस्तावना स्ट्रिंग
\ start {document} से ठीक पहले LATEX प्रस्तावना में कुछ सामग्री डालें
(अर्थहीन -एचटीएमएल के साथ)।

--वर्नाक-फ़ाइल फ़ाइल, --टेक्स-फाइल पट्टिका
फ़ाइल `फ़ाइल' को क्रमशः एक .v (या .g) फ़ाइल या .tex फ़ाइल के रूप में मानता है।

--फ़ाइलें-से पट्टिका
फ़ाइल 'फ़ाइल' में संसाधित करने के लिए फ़ाइल नाम पढ़ें जैसे कि वे कमांड पर दिए गए थे
रेखा। कई निर्देशिकाओं में विभाजित कार्यक्रम स्रोतों के लिए उपयोगी।

-क्यू, --शांत
चुप रहें। त्रुटियों को छोड़कर कुछ भी प्रिंट न करें।

-एच, --मदद
विकल्पों का संक्षिप्त सारांश दें और बाहर निकलें।

-में, --संस्करण
संस्करण प्रिंट करें और बाहर निकलें।

सूची विकल्पों
डिफ़ॉल्ट व्यवहार केवल HTML आउटपुट के लिए index.html में एक इंडेक्स बनाना है।

--नो-इंडेक्स
इंडेक्स आउटपुट न करें।

--मल्टी-इंडेक्स
प्रत्येक श्रेणी के लिए एक पृष्ठ और अनुक्रमणिका में प्रत्येक अक्षर को एक साथ उत्पन्न करें a
शीर्ष पृष्ठ index.html।

तालिका of अंतर्वस्तु विकल्प
-टोक, --विषयसूची
सामग्री की एक तालिका डालें। लेटेक्स आउटपुट के लिए, यह \tableofcontents at . सम्मिलित करता है
दस्तावेज़ की शुरुआत। HTML आउटपुट के लिए, यह सामग्री की एक तालिका बनाता है
toc.html में।

हाइपरलिंक विकल्पों
--ग्लोब-से पट्टिका
फ़ाइल फ़ाइल से Coq वैश्वीकरण का उपयोग करके संदर्भ बनाएं। (ऐसे वैश्वीकरण हैं
Coq विकल्प -डंप-ग्लोब के साथ प्राप्त)।

--नहीं-बाहरी
Coq मानक पुस्तकालय के लिंक न डालें।

--बाहरी यूआरएल लिब्रूट
बाहरी पुस्तकालय के लिए आधार URL सेट करें जिसका मूल उपसर्ग libroot है।

--कोक्लिब यूआरएल
Coq मानक पुस्तकालय के लिए आधार URL सेट करें (डिफ़ॉल्ट है
http://coq.inria.fr/library/).

--coqlib_path दीर
आधार पथ सेट करें जहां Coq फ़ाइलें स्थापित हैं, विशेष रूप से शैली फ़ाइलें
coqdoc.sty और coqdoc.css।

-R दीर कोकदिर
Coq तार्किक निर्देशिका coqdir के लिए भौतिक निर्देशिका dir को मैप करें (इसी तरह Coq विकल्प
-आर)। नोट: विकल्प -R केवल कमांड पर इसका अनुसरण करने वाली फाइलों पर प्रभाव डालता है
लाइन, इसलिए आपको शायद इस विकल्प को पहले रखना होगा।

विषय-सूची विकल्पों
-जी, --गैलिना
सबूत मत छापो।

-एल, --रोशनी
लाइट मोड। सबूतों को दबाएं (जैसे -g के साथ) और निम्न आदेश:

* [पुनरावर्ती] रणनीति परिभाषा
* संकेत / संकेत
* आवश्यकता
* पारदर्शी / अपारदर्शी
*अंतर्निहित तर्क / निहितार्थ
*अनुभाग / चर / परिकल्पना / अंत

विकल्प -g और -l के व्यवहार को स्थानीय रूप से ओवरराइड किया जा सकता है (* start show .)
*) ... (* एंड शो *) पर्यावरण (ऊपर देखें)।

भाषा विकल्पों
डिफ़ॉल्ट व्यवहार ASCII 7 बिट इनपुट फ़ाइलों को ग्रहण करना है।

-लैटिन1, --लैटिन1
ISO-8859-1 इनपुट फ़ाइल चुनें। यह --inputenc latin1 --charset . के बराबर है
आईएसओ-8859-1।

-यूटीएफ8, --utf8
UTF-8 (यूनिकोड) इनपुट फाइल चुनें। यह --inputenc utf8 --charset . के बराबर है
यूटीएफ-8. लेटेक्स यूटीएफ -8 समर्थन यहां पाया जा सकता है
http://www.ctan.org/tex-archive/macros/latex/contrib/supported/unicode/.

--inputenc स्ट्रिंग
LATEX पैकेज inputenc के विकल्प के रूप में एक LATEX इनपुट एन्कोडिंग दें।

--चारसेट स्ट्रिंग
HTML हैडर में डालने के लिए HTML कैरेक्टर सेट निर्दिष्ट करें।

onworks.net सेवाओं का उपयोग करके ऑनलाइन coqdoc का उपयोग करें