diff options
Diffstat (limited to 'doc/res')
| -rw-r--r-- | doc/res/coqdoc.css | 867 | ||||
| -rw-r--r-- | doc/res/fdl.org | 489 | ||||
| -rw-r--r-- | doc/res/install-deps.el | 11 | ||||
| -rw-r--r-- | doc/res/publish.el | 23 |
4 files changed, 1390 insertions, 0 deletions
diff --git a/doc/res/coqdoc.css b/doc/res/coqdoc.css new file mode 100644 index 0000000..5572aaa --- /dev/null +++ b/doc/res/coqdoc.css @@ -0,0 +1,867 @@ +body { + padding: 0px 0px; + margin: 0px 0px; + padding-left: 1em; + background-color: white; + font-family: sans-serif; + background-repeat: no-repeat; + background-size: 100%; +} + +#page { + display: block; + padding: 0px; + margin: 0px; +} + +#header { + min-height: 100px; + max-width: 760px; + margin: 0 auto; + padding-left: 80px; + padding-right: 80px; + padding-top: 30px; +} + +#header h1 { + padding: 0; + margin: 0; +} + +/* Menu */ +ul#menu { + padding: 0; + display: block; + margin: auto; +} + +ul#menu li, div.button { + display: inline-block; + background-color: white; + padding: 5px; + font-size: .70em; + text-transform: uppercase; + width: 30%; + text-align: center; + font-weight: 600; +} + +div.button { + margin-top:5px; + width: 40%; +} + +#button_block {margin-top:50px;} + +ul#menu a.hover li { + background-color: red; +} + +/* Contents */ + +#main, #main_home { + display: block; + padding: 80px; + padding-top: 60px; /* BCP */ + font-size: 100%; + line-height: 100%; + max-width: 760px; + background-color: #ffffff; + margin: 0 auto; +} + +#main_home { + background-color: rgba(255, 255, 255, 0.5); +} + +#index_content div.intro p { + font-size: 12px; +} + +#main h1 { + /* line-height: 80%; */ + line-height: normal; + padding-top: 3px; + padding-bottom: 4px; + /* Demitri: font-size: 22pt; */ + font-size: 200%; /* BCP */ +} + +/* allow for multi-line headers */ +#main a.idref:visited {color : #416DFF; text-decoration : none; } +#main a.idref:link {color : #416DFF; text-decoration : none; } +#main a.idref:hover {text-decoration : none; } +#main a.idref:active {text-decoration : none; } + +#main a.modref:visited {color : #416DFF; text-decoration : none; } +#main a.modref:link {color : #416DFF; text-decoration : none; } +#main a.modref:hover {text-decoration : none; } +#main a.modref:active {text-decoration : none; } + +#main .keyword { color : #697f2f } +#main { color: black } + +/* General section class - applies to all .section IDs */ +.section { + padding-top: 12px; + padding-bottom: 11px; + padding-left: 8px; + margin-top: 5px; + margin-bottom: 3px; + margin-top: 18px; + font-size : 125%; + color: #ffffff; +} + +/* Book title in header */ +.booktitleinheader { + color: #000000; + text-transform: uppercase; + font-weight: 300; + letter-spacing: 1px; + font-size: 125%; + margin-left: 0px; + margin-bottom: 22px; + } + +/* Chapter titles */ +.libtitle { + max-width: 860px; + text-transform: uppercase; + margin: 5px auto; + font-weight: 500; + padding-bottom: 2px; + font-size: 120%; + letter-spacing: 3px; + } + +.subtitle { + display: block; + padding-top: 10px; + font-size: 70%; + line-height: normal; +} + +h2.section { + color: #2a2c71; + background-color: transparent; + padding-left: 0px; + padding-top: 0px; + padding-bottom: 0px; + /* margin-top: 0px; */ + margin-top: 9px; /* BCP 2/20 */ + font-size : 135%; } + +h3.section { + /* background-color: rgb(90%,90%,100%); */ + background-color: white; + /* padding-left: 8px; */ + padding-left: 0px; + /* padding-top: 7px; */ + padding-top: 0px; + /* padding-bottom: 0px; */ + padding-bottom: 0.5em; + /* margin-top: 9px; */ + /* margin-top: 4px; (BCP 2/20) */ + margin-top: 9px; /* BCP 2/20 */ + font-size : 115%; + color:black; +} + +h4.section { + margin-top: .2em; + background-color: white; + color: #2a2c71; + padding-left: 0px; + padding-top: 0px; + padding-bottom: 0.5em; /* 0px; */ + font-size : 100%; + font-style : bold; + text-decoration : underline; +} + +#header p { + font-size: 13px; +} + +/* Sets up Main ID and margins */ + +#main .doc { + margin: 0px auto; + font-size: 14px; + line-height: 22px; + /* max-width: 570px; */ + color: black; + /* text-align: justify; */ + border-style: plain; + /* This might work better after changing back to standard coqdoc: */ + padding-top: 10px; + /* padding-top: 18px; */ +} + +.quote { + margin-left: auto; + margin-right: auto; + width: 40em; + color: darkred; +} + +.loud { + color: darkred; +} + +pre { + margin-top: 0px; + margin-bottom: 0px; +} + +.inlinecode { + display: inline; + /* font-size: 125%; */ + color: #444444; + font-family: monospace } + +.doc .inlinecode { + display: inline; + font-size: 105%; + color: rgb(35%,35%,70%); + font-family: monospace } + +.doc .inlinecode .id { +/* I am changing this to white in style below: + color: rgb(35%,35%,70%); +*/ +} + +h1 .inlinecode .id, h1.section span.inlinecode { + color: #ffffff; +} + +.inlinecodenm { + display: inline; + /* font-size: 125%; */ + color: #444444; +} + +.doc .inlinecodenm { + display: inline; + color: rgb(35%,35%,70%); +} + +.doc .inlinecodenm .id { + color: rgb(35%,35%,70%); +} + +.doc .code { + display: inline; + font-size: 110%; + color: rgb(35%,35%,70%); + font-family: monospace; + padding-left: 0px; +} + +.comment { + display: inline; + font-family: monospace; + color: rgb(50%,50%,80%); +} + +.inlineref { + display: inline; + /* font-family: monospace; */ + color: rgb(50%,50%,80%); +} + +.show::before { + /* content: "more"; */ + content: "+"; +} + +.show { + background-color: rgb(93%,93%,93%); + display: inline; + font-family: monospace; + font-size: 60%; + padding-top: 1px; + padding-bottom: 2px; + padding-left: 4px; + padding-right: 4px; + color: rgb(60%,60%,60%); +} + +/* +.show { + display: inline; + font-family: monospace; + font-size: 60%; + padding-top: 0px; + padding-bottom: 0px; + padding-left: 10px; + border: 1px; + border-style: solid; + color: rgb(75%,75%,85%); +} +*/ + +.proofbox { + font-size: 90%; + color: rgb(75%,75%,75%); +} + +#main .less-space { + margin-top: -12px; +} + +/* Inline quizzes */ +.quiz:before { + color: rgb(40%,40%,40%); + /* content: "- Quick Check -" ; */ + display: block; + text-align: center; + margin-bottom: 5px; +} +.quiz { + border: 4px; + border-color: rgb(80%,80%,80%); + /* + margin-left: 40px; + margin-right: 100px; + */ + padding: 5px; + padding-left: 8px; + padding-right: 8px; + margin-top: 10px; + margin-bottom: 15px; + border-style: solid; +} + +/* For textual ones... */ +.show-old { + display: inline; + font-family: monospace; + font-size: 80%; + padding-top: 0px; + padding-bottom: 0px; + padding-left: 3px; + padding-right: 3px; + border: 1px; + margin-top: 5px; /* doesn't work?! */ + border-style: solid; + color: rgb(75%,75%,85%); +} + +.largebr { + margin-top: 10px; +} + +.code { + padding-left: 20px; + font-size: 14px; + font-family: monospace; + line-height: 17px; + margin-top: 9px; +} + +/* Working: +.code { + display: block; + padding-left: 0px; + font-size: 110%; + font-family: monospace; + } +*/ + +.code-space { + max-width: 50em; + margin-top: 0em; + /* margin-bottom: -.5em; */ + margin-left: auto; + margin-right: auto; +} + +.code-tight { + max-width: 50em; + margin-top: .6em; + /* margin-bottom: -.7em; */ + margin-left: auto; + margin-right: auto; +} + +hr.doublespaceincode { + height: 1pt; + visibility: hidden; + font-size: 10px; +} + +/* +code.br { + height: 5em; +} +*/ + +#main .citation { + color: rgb(70%,0%,0%); + text-decoration: underline; +} + +table.infrule { + border: 0px; + margin-left: 50px; + margin-top: .5em; + margin-bottom: 1.2em; +} + +td.infrule { + font-family: monospace; + text-align: center; + /* color: rgb(35%,35%,70%); */ + padding: 0px; + line-height: 100%; +} + +tr.infrulemiddle hr { + margin: 1px 0 1px 0; +} + +.infrulenamecol { + color: rgb(60%,60%,60%); + font-size: 80%; + padding-left: 1em; + padding-bottom: 0.1em +} + +#footer { + font-size: 65%; + font-family: sans-serif; +} + +.id { display: inline; } + +.id[title="constructor"] { + color: #697f2f; +} + +.id[title="var"], +.id[title="variable"] { + color: rgb(40%,0%,40%); +} + +.id[title="definition"] { + color: rgb(0%,40%,0%); +} + +.id[title="abbreviation"] { + color: rgb(0%,40%,0%); +} + +.id[title="lemma"] { + color: rgb(0%,40%,0%); +} + +.id[title="instance"] { + color: rgb(0%,40%,0%); +} + +.id[title="projection"] { + color: rgb(0%,40%,0%); +} + +.id[title="method"] { + color: rgb(0%,40%,0%); +} + +.id[title="inductive"] { + color: #034764; +} + +.id[title="record"] { + color: rgb(0%,0%,80%); +} + +.id[title="class"] { + color: rgb(0%,0%,80%); +} + +.id[title="keyword"] { + color : #697f2f; + /* color: black; */ +} + +.inlinecode .id { + color: rgb(0%,0%,0%); +} + +.nowrap { + white-space: nowrap; +} + +.HIDEFROMHTML { + display: none; +} + +/* TOC */ + +#toc h2 { +/* padding-top: 13px; */ + padding-bottom: 13px; + padding-left: 8px; + margin-top: 5px; + margin-top: 20px; + /* OLD: padding: 10px; + line-height: 120%; + background-color: rgb(60%,60%,100%); */ +} + +#toc h2.ui-accordion-header { + padding: .5em .5em .5em .7em; + outline: none; +} + +#toc .ui-accordion .ui-accordion-content { + padding: 0.5em 2.5em 0.8em .9em; + border-top: 0; + margin-bottom: 1em; + /* bottom rule */ + border: none; + border-bottom: 1px solid transparent; + transition: border-bottom-color 0.25s ease-in; + transition-delay: 0.15s; +} + +#toc .ui-accordion .ui-accordion-content-active { + border-bottom: 1px solid #9b9b9b; + transition-delay: 0s; +} + +#toc h2.ui-accordion-header-active { + background: silver !important; +} + +#toc h2:not(.ui-accordion-header-active):hover { + background: rgba(0,0,0,0.04) !important; +} + +#toc h2 a:hover { + text-decoration: underline; +} + +#toc h2:hover::after { + content: "expand ▾"; + font-size: 80%; + float: right; + margin-top: 0.2em; + color: silver; + opacity: 1; + transition: opacity .5s ease-in-out; +} + +#toc h2.ui-accordion-header-active:hover::after { + opacity: 0; +} + +#toc h2 .select { background-image: url('media/image/arrow_down.jpg'); } +div#sec1.hide { display: none; } + +#toc ul { + padding-top: 8px; + font-size: 14px; + padding-left: 0; +} + +#toc ul ul { + margin-bottom: -8px; +} + +#toc li { + font-weight: 600; + list-style-type: none; + padding-top: 12px; + padding-bottom: 8px; +} + +#toc li li { + font-weight: 300; + list-style-type: circle; + padding-bottom: 3px; + padding-top: 0px; + margin-left: 19px; +} + + + + +/* Accordion Overrides */ + +/* Widget Bar */ +.ui-state-default, +.ui-widget-content .ui-state-default, +.ui-widget-header .ui-state-default, +.ui-button, +/* We use html here because we need a greater specificity to make sure disabled + works properly when clicked or hovered */ +html .ui-button.ui-state-disabled:hover, +html .ui-button.ui-state-disabled:active { + border: none!important; + /* BCP 3/17: I like it better without the rules... + border-bottom: 1px solid silver!important; */ + background: white !important; + font-weight: normal; + color: #454545!important; + font-weight: 400!important; + margin-top: 0px!important; + +} + +/* Misc visuals +----------------------------------*/ + +/* Corner radius */ +.ui-corner-all, +.ui-corner-top, +.ui-corner-left, +.ui-corner-tl { + border-top-left-radius: 0px!important; +} + +.ui-corner-all, +.ui-corner-top, +.ui-corner-right, +.ui-corner-tr { + border-top-right-radius: 0px!important; +} + +.ui-corner-all, +.ui-corner-bottom, +.ui-corner-left, +.ui-corner-bl { + border-bottom-left-radius: 0px!important; +} + +.ui-corner-all, +.ui-corner-bottom, +.ui-corner-right, +.ui-corner-br { + border-bottom-right-radius: 0px!important; +} + +html .ui-button.ui-state-disabled:focus { + color: red!important; +} + +/* Remove Icon */ +.ui-icon { display: none!important; } + +/* Widget */ +.ui-widget-content { + border: 1px solid #9e9e9e; + border-bottom-color: #b2b2b2; +} + +.ui-widget-content { + background: #ffffff; + color: #333333; +} + + +/* Index */ + +#index { + margin: 0; + padding: 0; + width: 100%; + font-style : normal; +} + +#index #frontispiece { + margin: auto; + padding: 1em; + width: 700px; +} + +.booktitle { + font-size : 300%; line-height: 100%; font-style:bold; + color: white; + padding-top: 70px; + padding-bottom: 20px; } +.authors { font-size : 200%; + line-height: 115%; } +.moreauthors { font-size : 170% } +.buttons { font-size : 170%; + margin-left: auto; + margin-right: auto; + font-style : bold; + } + +/* Link colors never changes */ + +A:link, A:visited, A:active, A:hover { + text-decoration: none; + color: #555555 +} + +/* Special color for the chapter header */ + +.booktitleinheader A:visited, .booktitleinheader A:active, .booktitleinheader A:hover, .booktitleinheader A:link { + text-decoration: none; + color: black; +} + +#index #entrance { + text-align: center; +} + +/* This was removed via CSS but the HTML is still generated */ +#index #footer { + display: none; +} + +.paragraph { + height: 0.6em; +} + +ul.doclist { + margin-top: 0em; + margin-bottom: 0em; +} + +/* Index styles */ + +/* Styles the author box (Intro class) and With (column class) */ + +.column { + float:left; + width: 43%; + margin:0 10px; + text-align: left; + font-size: 15px; + line-height: 25px; + padding-right: 20px; + min-height: 340px; +} + +.smallauthors { + font-size: 19px; + line-height: 25px; +} + +.mediumauthors { + font-size: 23px; + line-height: 33px; +} + +.largeauthors { + font-size: 28px; + line-height: 40px; +} + +.intro { + width: 35%; + font-size: 21px; + line-height: 27px; + font-weight: 600; + padding-right: 20px; +} + +.column.pub { + width: 40%; + margin-bottom: 20px; +} + +#index_content { + width: 100%!important; + display: block; + min-height: 400px; +} + +div.column.pub table tbody tr td { + text-align: center; padding: 10px; +} +div.column.pub table tbody tr td p { + text-align: left; + margin-top: 0; + font-weight: 600; + font-size: 13px!important; + line-height: 18px; +} + +/* Tables */ + +td.tab { + height: 16px; + font-weight: 600; + padding-left: 5px; + text-align: left!important; +} + +/* Styles tables on the index -- body class sf_home is used there */ + +body.sf_home table { + min-height: 450px; + vertical-align: top; +} + +body.sf_home table td { + vertical-align: top; + +} +body.sf_home table td p { + min-height: 100px; + +} + +table.logical { background-color: rgba(144, 160, 209, 0.5); } +table.logical tbody tr td.tab { background-color: #91a1d1; } + +table.language_found { background-color: rgba(178, 88, 88, 0.5); } +table.language_found tbody tr td.tab { background-color: #b25959; } + +table.algo { background-color: rgba(194, 194, 108, 0.5); } +table.algo tbody tr td.tab { background-color: #c2c26c; } + +table.qc { background-color: rgba(185, 170, 185, 0.5); } +table.qc tbody tr td.tab { background-color: #8b7d95; } + +table.vc { background-color: rgba(159, 125, 140, 0.5); } +table.vc tbody tr td.tab { background-color: rgb(159, 125, 140); } + +table.slf { background-color: rgba(219, 178, 127, 0.5); } +table.slf tbody tr td.tab { background-color: rgb(219, 178, 127); } + +/* Suggested background color for next volume */ +/* #c07d62 */ + +.ui-draggable, .ui-droppable { + background-position: top; +} + +/* Chapter dependencies (SVG) */ +.deps a polygon:hover { opacity: 0.6; stroke-width: 2; } +.deps a text { pointer-events: none; } + +/* A few specific things for the top-level SF landing page */ + +body.sf_home {background-color: #ededed; background-image: url(../media/image/core_mem_bg.jpg); } + +body.sf_home #header { + background-image: url(../media/image/core_mem_hdr_bg.jpg); + padding-bottom: 20px; +} + +body.sf_home #main_home { + background-color: transparent; +} + +/* A partial fix to a coqdoc bug... + See https://github.com/DeepSpec/sfdev/issues/236 */ +.inlinecode { white-space: pre; } +.inlinecode br { display: none; } + +#header { background-color: rgba(190, 170, 190, 0.5); } + +/* This volume's color */ +.section, ul#menu li.section_name, div.button { background-color: #8b7d95; } + +.slide img { + border: 2px solid gray; + margin: 1em; +} diff --git a/doc/res/fdl.org b/doc/res/fdl.org new file mode 100644 index 0000000..81e2cd9 --- /dev/null +++ b/doc/res/fdl.org @@ -0,0 +1,489 @@ +# The GNU Free Documentation License. +#+begin_center +Version 1.3, 3 November 2008 +#+end_center + +# This file is intended to be included within another document. + +#+begin_verse +Copyright \copy{} 2000, 2001, 2002, 2007, 2008 Free Software Foundation, Inc. +https://fsf.org/ + +Everyone is permitted to copy and distribute verbatim copies +of this license document, but changing it is not allowed. +#+end_verse + +0. [@0] PREAMBLE + + The purpose of this License is to make a manual, textbook, or other + functional and useful document @@texinfo:@dfn{@@free@@texinfo:}@@ + in the sense of freedom: to assure everyone the effective freedom + to copy and redistribute it, with or without modifying it, either + commercially or noncommercially. Secondarily, this License + preserves for the author and publisher a way to get credit for + their work, while not being considered responsible for + modifications made by others. + + This License is a kind of "copyleft", which means that derivative + works of the document must themselves be free in the same sense. + It complements the GNU General Public License, which is a copyleft + license designed for free software. + + We have designed this License in order to use it for manuals for + free software, because free software needs free documentation: + a free program should come with manuals providing the same freedoms + that the software does. But this License is not limited to + software manuals; it can be used for any textual work, regardless + of subject matter or whether it is published as a printed book. We + recommend this License principally for works whose purpose is + instruction or reference. + +1. APPLICABILITY AND DEFINITIONS + + This License applies to any manual or other work, in any medium, + that contains a notice placed by the copyright holder saying it can + be distributed under the terms of this License. Such a notice + grants a world-wide, royalty-free license, unlimited in duration, + to use that work under the conditions stated herein. The + "Document", below, refers to any such manual or work. Any member + of the public is a licensee, and is addressed as "you". You accept + the license if you copy, modify or distribute the work in a way + requiring permission under copyright law. + + A "Modified Version" of the Document means any work containing the + Document or a portion of it, either copied verbatim, or with + modifications and/or translated into another language. + + A "Secondary Section" is a named appendix or a front-matter section + of the Document that deals exclusively with the relationship of the + publishers or authors of the Document to the Document's overall + subject (or to related matters) and contains nothing that could + fall directly within that overall subject. (Thus, if the Document + is in part a textbook of mathematics, a Secondary Section may not + explain any mathematics.) The relationship could be a matter of + historical connection with the subject or with related matters, or + of legal, commercial, philosophical, ethical or political position + regarding them. + + The "Invariant Sections" are certain Secondary Sections whose + titles are designated, as being those of Invariant Sections, in the + notice that says that the Document is released under this License. + If a section does not fit the above definition of Secondary then it + is not allowed to be designated as Invariant. The Document may + contain zero Invariant Sections. If the Document does not identify + any Invariant Sections then there are none. + + The "Cover Texts" are certain short passages of text that are + listed, as Front-Cover Texts or Back-Cover Texts, in the notice + that says that the Document is released under this License. + A Front-Cover Text may be at most 5 words, and a Back-Cover Text + may be at most 25 words. + + A "Transparent" copy of the Document means a machine-readable copy, + represented in a format whose specification is available to the + general public, that is suitable for revising the document + straightforwardly with generic text editors or (for images composed + of pixels) generic paint programs or (for drawings) some widely + available drawing editor, and that is suitable for input to text + formatters or for automatic translation to a variety of formats + suitable for input to text formatters. A copy made in an otherwise + Transparent file format whose markup, or absence of markup, has + been arranged to thwart or discourage subsequent modification by + readers is not Transparent. An image format is not Transparent if + used for any substantial amount of text. A copy that is not + "Transparent" is called "Opaque". + + Examples of suitable formats for Transparent copies include plain + ASCII without markup, Texinfo input format, LaTeX input format, + SGML or XML using a publicly available DTD, and standard-conforming + simple HTML, PostScript or PDF designed for human modification. + Examples of transparent image formats include PNG, XCF and JPG. + Opaque formats include proprietary formats that can be read and + edited only by proprietary word processors, SGML or XML for which + the DTD and/or processing tools are not generally available, and + the machine-generated HTML, PostScript or PDF produced by some word + processors for output purposes only. + + The "Title Page" means, for a printed book, the title page itself, + plus such following pages as are needed to hold, legibly, the + material this License requires to appear in the title page. For + works in formats which do not have any title page as such, "Title + Page" means the text near the most prominent appearance of the + work's title, preceding the beginning of the body of the text. + + The "publisher" means any person or entity that distributes copies + of the Document to the public. + + A section "Entitled XYZ" means a named subunit of the Document + whose title either is precisely XYZ or contains XYZ in parentheses + following text that translates XYZ in another language. (Here XYZ + stands for a specific section name mentioned below, such as + "Acknowledgements", "Dedications", "Endorsements", or "History".) + To "Preserve the Title" of such a section when you modify the + Document means that it remains a section "Entitled XYZ" according + to this definition. + + The Document may include Warranty Disclaimers next to the notice + which states that this License applies to the Document. These + Warranty Disclaimers are considered to be included by reference in + this License, but only as regards disclaiming warranties: any other + implication that these Warranty Disclaimers may have is void and + has no effect on the meaning of this License. + +2. VERBATIM COPYING + + You may copy and distribute the Document in any medium, either + commercially or noncommercially, provided that this License, the + copyright notices, and the license notice saying this License + applies to the Document are reproduced in all copies, and that you + add no other conditions whatsoever to those of this License. You + may not use technical measures to obstruct or control the reading + or further copying of the copies you make or distribute. However, + you may accept compensation in exchange for copies. If you + distribute a large enough number of copies you must also follow the + conditions in section 3. + + You may also lend copies, under the same conditions stated above, + and you may publicly display copies. + +3. COPYING IN QUANTITY + + If you publish printed copies (or copies in media that commonly + have printed covers) of the Document, numbering more than 100, and + the Document's license notice requires Cover Texts, you must + enclose the copies in covers that carry, clearly and legibly, all + these Cover Texts: Front-Cover Texts on the front cover, and + Back-Cover Texts on the back cover. Both covers must also clearly + and legibly identify you as the publisher of these copies. The + front cover must present the full title with all words of the title + equally prominent and visible. You may add other material on the + covers in addition. Copying with changes limited to the covers, as + long as they preserve the title of the Document and satisfy these + conditions, can be treated as verbatim copying in other respects. + + If the required texts for either cover are too voluminous to fit + legibly, you should put the first ones listed (as many as fit + reasonably) on the actual cover, and continue the rest onto + adjacent pages. + + If you publish or distribute Opaque copies of the Document + numbering more than 100, you must either include a machine-readable + Transparent copy along with each Opaque copy, or state in or with + each Opaque copy a computer-network location from which the general + network-using public has access to download using public-standard + network protocols a complete Transparent copy of the Document, free + of added material. If you use the latter option, you must take + reasonably prudent steps, when you begin distribution of Opaque + copies in quantity, to ensure that this Transparent copy will + remain thus accessible at the stated location until at least one + year after the last time you distribute an Opaque copy (directly or + through your agents or retailers) of that edition to the public. + + It is requested, but not required, that you contact the authors of + the Document well before redistributing any large number of copies, + to give them a chance to provide you with an updated version of the + Document. + +4. MODIFICATIONS + + You may copy and distribute a Modified Version of the Document + under the conditions of sections 2 and 3 above, provided that you + release the Modified Version under precisely this License, with the + Modified Version filling the role of the Document, thus licensing + distribution and modification of the Modified Version to whoever + possesses a copy of it. In addition, you must do these things in + the Modified Version: + + #+attr_texinfo: :enum A + 1. Use in the Title Page (and on the covers, if any) a title + distinct from that of the Document, and from those of previous + versions (which should, if there were any, be listed in the + History section of the Document). You may use the same title as + a previous version if the original publisher of that version + gives permission. + + 2. List on the Title Page, as authors, one or more persons or + entities responsible for authorship of the modifications in the + Modified Version, together with at least five of the principal + authors of the Document (all of its principal authors, if it has + fewer than five), unless they release you from this requirement. + + 3. State on the Title page the name of the publisher of the + Modified Version, as the publisher. + + 4. Preserve all the copyright notices of the Document. + + 5. Add an appropriate copyright notice for your modifications + adjacent to the other copyright notices. + + 6. Include, immediately after the copyright notices, a license + notice giving the public permission to use the Modified Version + under the terms of this License, in the form shown in the + Addendum below. + + 7. Preserve in that license notice the full lists of Invariant + Sections and required Cover Texts given in the Document's + license notice. + + 8. Include an unaltered copy of this License. + + 9. Preserve the section Entitled "History", Preserve its Title, and + add to it an item stating at least the title, year, new authors, + and publisher of the Modified Version as given on the Title + Page. If there is no section Entitled "History" in the Document, + create one stating the title, year, authors, and publisher of + the Document as given on its Title Page, then add an item + describing the Modified Version as stated in the previous + sentence. + + 10. Preserve the network location, if any, given in the Document + for public access to a Transparent copy of the Document, and + likewise the network locations given in the Document for + previous versions it was based on. These may be placed in the + "History" section. You may omit a network location for a work + that was published at least four years before the Document + itself, or if the original publisher of the version it refers + to gives permission. + + 11. For any section Entitled "Acknowledgements" or "Dedications", + Preserve the Title of the section, and preserve in the section + all the substance and tone of each of the contributor + acknowledgements and/or dedications given therein. + + 12. Preserve all the Invariant Sections of the Document, unaltered + in their text and in their titles. Section numbers or the + equivalent are not considered part of the section titles. + + 13. Delete any section Entitled "Endorsements". Such a section may + not be included in the Modified Version. + + 14. Do not retitle any existing section to be Entitled + "Endorsements" or to conflict in title with any Invariant + Section. + + 15. Preserve any Warranty Disclaimers. + + If the Modified Version includes new front-matter sections or + appendices that qualify as Secondary Sections and contain no material + copied from the Document, you may at your option designate some or all + of these sections as invariant. To do this, add their titles to the + list of Invariant Sections in the Modified Version's license notice. + These titles must be distinct from any other section titles. + + You may add a section Entitled "Endorsements", provided it contains + nothing but endorsements of your Modified Version by various + parties---for example, statements of peer review or that the text has + been approved by an organization as the authoritative definition of a + standard. + + You may add a passage of up to five words as a Front-Cover Text, and a + passage of up to 25 words as a Back-Cover Text, to the end of the list + of Cover Texts in the Modified Version. Only one passage of + Front-Cover Text and one of Back-Cover Text may be added by (or + through arrangements made by) any one entity. If the Document already + includes a cover text for the same cover, previously added by you or + by arrangement made by the same entity you are acting on behalf of, + you may not add another; but you may replace the old one, on explicit + permission from the previous publisher that added the old one. + + The author(s) and publisher(s) of the Document do not by this License + give permission to use their names for publicity for or to assert or + imply endorsement of any Modified Version. + +5. COMBINING DOCUMENTS + + You may combine the Document with other documents released under + this License, under the terms defined in section 4 above for + modified versions, provided that you include in the combination all + of the Invariant Sections of all of the original documents, + unmodified, and list them all as Invariant Sections of your + combined work in its license notice, and that you preserve all + their Warranty Disclaimers. + + The combined work need only contain one copy of this License, and + multiple identical Invariant Sections may be replaced with a single + copy. If there are multiple Invariant Sections with the same name + but different contents, make the title of each such section unique + by adding at the end of it, in parentheses, the name of the + original author or publisher of that section if known, or else + a unique number. Make the same adjustment to the section titles in + the list of Invariant Sections in the license notice of the + combined work. + + In the combination, you must combine any sections Entitled + "History" in the various original documents, forming one section + Entitled "History"; likewise combine any sections Entitled + "Acknowledgements", and any sections Entitled "Dedications". You + must delete all sections Entitled "Endorsements." + +6. COLLECTIONS OF DOCUMENTS + + You may make a collection consisting of the Document and other + documents released under this License, and replace the individual + copies of this License in the various documents with a single copy + that is included in the collection, provided that you follow the + rules of this License for verbatim copying of each of the documents + in all other respects. + + You may extract a single document from such a collection, and + distribute it individually under this License, provided you insert + a copy of this License into the extracted document, and follow this + License in all other respects regarding verbatim copying of that + document. + +7. AGGREGATION WITH INDEPENDENT WORKS + + A compilation of the Document or its derivatives with other + separate and independent documents or works, in or on a volume of + a storage or distribution medium, is called an "aggregate" if the + copyright resulting from the compilation is not used to limit the + legal rights of the compilation's users beyond what the individual + works permit. When the Document is included in an aggregate, this + License does not apply to the other works in the aggregate which + are not themselves derivative works of the Document. + + If the Cover Text requirement of section 3 is applicable to these + copies of the Document, then if the Document is less than one half + of the entire aggregate, the Document's Cover Texts may be placed + on covers that bracket the Document within the aggregate, or the + electronic equivalent of covers if the Document is in electronic + form. Otherwise they must appear on printed covers that bracket + the whole aggregate. + +8. TRANSLATION + + Translation is considered a kind of modification, so you may + distribute translations of the Document under the terms of + section 4. Replacing Invariant Sections with translations requires + special permission from their copyright holders, but you may + include translations of some or all Invariant Sections in addition + to the original versions of these Invariant Sections. You may + include a translation of this License, and all the license notices + in the Document, and any Warranty Disclaimers, provided that you + also include the original English version of this License and the + original versions of those notices and disclaimers. In case of + a disagreement between the translation and the original version of + this License or a notice or disclaimer, the original version will + prevail. + + If a section in the Document is Entitled "Acknowledgements", + "Dedications", or "History", the requirement (section 4) to + Preserve its Title (section 1) will typically require changing the + actual title. + +9. TERMINATION + + You may not copy, modify, sublicense, or distribute the Document + except as expressly provided under this License. Any attempt + otherwise to copy, modify, sublicense, or distribute it is void, + and will automatically terminate your rights under this License. + + However, if you cease all violation of this License, then your + license from a particular copyright holder is reinstated (a) + provisionally, unless and until the copyright holder explicitly and + finally terminates your license, and (b) permanently, if the + copyright holder fails to notify you of the violation by some + reasonable means prior to 60 days after the cessation. + + Moreover, your license from a particular copyright holder is + reinstated permanently if the copyright holder notifies you of the + violation by some reasonable means, this is the first time you have + received notice of violation of this License (for any work) from + that copyright holder, and you cure the violation prior to 30 days + after your receipt of the notice. + + Termination of your rights under this section does not terminate + the licenses of parties who have received copies or rights from you + under this License. If your rights have been terminated and not + permanently reinstated, receipt of a copy of some or all of the + same material does not give you any rights to use it. + +10. FUTURE REVISIONS OF THIS LICENSE + + The Free Software Foundation may publish new, revised versions of + the GNU Free Documentation License from time to time. Such new + versions will be similar in spirit to the present version, but may + differ in detail to address new problems or concerns. See + https://www.gnu.org/copyleft/. + + Each version of the License is given a distinguishing version + number. If the Document specifies that a particular numbered + version of this License "or any later version" applies to it, you + have the option of following the terms and conditions either of + that specified version or of any later version that has been + published (not as a draft) by the Free Software Foundation. If + the Document does not specify a version number of this License, + you may choose any version ever published (not as a draft) by the + Free Software Foundation. If the Document specifies that a proxy + can decide which future versions of this License can be used, that + proxy's public statement of acceptance of a version permanently + authorizes you to choose that version for the Document. + +11. RELICENSING + + "Massive Multiauthor Collaboration Site" (or "MMC Site") means any + World Wide Web server that publishes copyrightable works and also + provides prominent facilities for anybody to edit those works. + A public wiki that anybody can edit is an example of such + a server. A "Massive Multiauthor Collaboration" (or "MMC") + contained in the site means any set of copyrightable works thus + published on the MMC site. + + "CC-BY-SA" means the Creative Commons Attribution-Share Alike 3.0 + license published by Creative Commons Corporation, + a not-for-profit corporation with a principal place of business in + San Francisco, California, as well as future copyleft versions of + that license published by that same organization. + + "Incorporate" means to publish or republish a Document, in whole + or in part, as part of another Document. + + An MMC is "eligible for relicensing" if it is licensed under this + License, and if all works that were first published under this + License somewhere other than this MMC, and subsequently + incorporated in whole or in part into the MMC, (1) had no cover + texts or invariant sections, and (2) were thus incorporated prior + to November 1, 2008. + + The operator of an MMC Site may republish an MMC contained in the + site under CC-BY-SA on the same site at any time before August 1, + 2009, provided the MMC is eligible for relicensing. + +#+texinfo: @page + +* ADDENDUM: How to use this License for your documents +:PROPERTIES: +:UNNUMBERED: notoc +:END: + +To use this License in a document you have written, include a copy of +the License in the document and put the following copyright and +license notices just after the title page: + +#+begin_example + Copyright (C) YEAR YOUR NAME. + Permission is granted to copy, distribute and/or modify this document + under the terms of the GNU Free Documentation License, Version 1.3 + or any later version published by the Free Software Foundation; + with no Invariant Sections, no Front-Cover Texts, and no Back-Cover + Texts. A copy of the license is included in the section entitled ``GNU + Free Documentation License''. +#+end_example + +If you have Invariant Sections, Front-Cover Texts and Back-Cover Texts, +replace the "with...Texts."\nbsp{}line with this: + +#+begin_example + with the Invariant Sections being LIST THEIR TITLES, with + the Front-Cover Texts being LIST, and with the Back-Cover Texts + being LIST. +#+end_example + +If you have Invariant Sections without Cover Texts, or some other +combination of the three, merge those two alternatives to suit the +situation. + +If your document contains nontrivial examples of program code, we +recommend releasing these examples in parallel under your choice of +free software license, such as the GNU General Public License, to +permit their use in free software. diff --git a/doc/res/install-deps.el b/doc/res/install-deps.el new file mode 100644 index 0000000..09cf4ae --- /dev/null +++ b/doc/res/install-deps.el @@ -0,0 +1,11 @@ +(require 'package) +(package-initialize) +(add-to-list 'package-archives '("nongnu" . "https://elpa.nongnu.org/nongnu/") t) +(add-to-list 'package-archives '("melpa" . "https://melpa.org/packages/") t) +(add-to-list 'package-archives '("gnu-devel" . "https://elpa.gnu.org/devel/") t) +(package-refresh-contents) + +(package-install 'org) +(package-install 'org-contrib) +(package-install 'org-transclusion) +(package-install 'htmlize) diff --git a/doc/res/publish.el b/doc/res/publish.el new file mode 100644 index 0000000..c083eb0 --- /dev/null +++ b/doc/res/publish.el @@ -0,0 +1,23 @@ +(require 'package) +(package-initialize) + +(require 'org) +(require 'org-transclusion) +(require 'ox) +(require 'ox-html) +(require 'htmlize) +(require 'ox-texinfo) +(require 'ox-man) + +(setq org-transclusion-exclude-elements nil + org-html-head-include-default-style nil + org-html-head-include-scripts nil + org-html-postamble-format '(("en" "")) + org-html-postamble t + org-html-divs '((preamble "header" "header") + (content "article" "content") + (postamble "footer" "postamble")) + org-html-doctype "html5" + org-html-htmlize-output-type 'css) + +(org-transclusion-add-all) |