From 11d6215f265d0dbcfd0048819a614f318a0775a4 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sat, 26 Mar 2022 21:08:23 +0000 Subject: Add sphinx documentation --- docs/Makefile | 39 -- docs/README.org | 7 - docs/common.org | 15 - docs/documentation.org | 562 --------------------- docs/images/toolflow.pdf | Bin 20490 -> 0 bytes docs/images/toolflow.png | Bin 26864 -> 0 bytes docs/images/toolflow.svg | 1250 ---------------------------------------------- docs/man.org | 89 ---- docs/res/coqdoc.css | 867 -------------------------------- docs/res/fdl.org | 489 ------------------ docs/res/install-deps.el | 11 - docs/res/publish.el | 23 - 12 files changed, 3352 deletions(-) delete mode 100644 docs/Makefile delete mode 100644 docs/README.org delete mode 100644 docs/common.org delete mode 100644 docs/documentation.org delete mode 100644 docs/images/toolflow.pdf delete mode 100644 docs/images/toolflow.png delete mode 100644 docs/images/toolflow.svg delete mode 100644 docs/man.org delete mode 100644 docs/res/coqdoc.css delete mode 100644 docs/res/fdl.org delete mode 100644 docs/res/install-deps.el delete mode 100644 docs/res/publish.el (limited to 'docs') diff --git a/docs/Makefile b/docs/Makefile deleted file mode 100644 index 9d4f361..0000000 --- a/docs/Makefile +++ /dev/null @@ -1,39 +0,0 @@ -all: manual src man-html - -install-deps: - emacs --batch --load ./res/install-deps.el - -%.man: %.org - emacs --batch --file $< --load ./res/publish.el --funcall org-man-export-to-man - -%.html: %.org - emacs --batch --file $< --load ./res/publish.el --funcall org-html-export-to-html - -manual: - mkdir -p manual - emacs --batch --file documentation.org --load ./res/publish.el --funcall org-texinfo-export-to-texinfo - makeinfo --html --number-sections --no-split \ - --css-ref "https://www.gnu.org/software/emacs/manual.css" \ - vericert.texi -o ./manual/index.html - cp -r images ./manual/. - -man-html: man.html - mkdir -p man - cp man.html ./man/vericert.1.html - -vericert.1: man.man - cp $< $@ - -src: - $(MAKE) -C .. doc - cp -r ../html src - -upload: - tar caf docs.tar.xz manual man src - rsync docs.tar.xz "zk@leika.ymhg.org:~" - -.PHONY: all upload manual man src install-deps man-html - -clean: - rm -rf manual man src - rm -f docs.tar.xz diff --git a/docs/README.org b/docs/README.org deleted file mode 100644 index 4113ed9..0000000 --- a/docs/README.org +++ /dev/null @@ -1,7 +0,0 @@ -#+title: Vericert Documentation - -The documentation for [[https://github.com/ymherklotz/vericert][Vericert]], which is written in the [[/documentation.org][documentation.org]] file. - -* How to develop on documentation - -The documentation uses =hugo= to generate the website, diff --git a/docs/common.org b/docs/common.org deleted file mode 100644 index aa27264..0000000 --- a/docs/common.org +++ /dev/null @@ -1,15 +0,0 @@ -#+author: Yann Herklotz -#+email: git@ymhg.org - -#+macro: version 1.2.2 -#+macro: modified 2022-02-24 - -#+macro: base_url https://vericert.ymhg.org - -#+macro: link src_emacs-lisp[:results raw]{(ymhg/link "$1" "$2")} - -#+macro: texinfo_head (eval (if (eq org-export-current-backend 'texinfo) "#+exclude_tags: noexport_texinfo" "#+exclude_tags: onlyexport_texinfo")) -#+macro: latex_head (eval (if (eq org-export-current-backend 'latex) "#+exclude_tags: noexport_latex" "#+exclude_tags: onlyexport_latex")) -#+macro: hugo_head (eval (if (eq org-export-current-backend 'hugo) "#+exclude_tags: noexport_hugo" "#+exclude_tags: onlyexport_hugo")) -{{{texinfo_head}}} -{{{latex_head}}} diff --git a/docs/documentation.org b/docs/documentation.org deleted file mode 100644 index 85bc8fd..0000000 --- a/docs/documentation.org +++ /dev/null @@ -1,562 +0,0 @@ -#+title: Vericert Manual -#+subtitle: Release {{{version}}} -#+author: Yann Herklotz -#+email: git@ymhg.org -#+language: en - -* Introduction -:PROPERTIES: -:EXPORT_FILE_NAME: _index -:EXPORT_HUGO_SECTION: docs -:CUSTOM_ID: docs -:END: - -Vericert translates C code into a hardware description language called Verilog, which can then be -synthesised into hardware, to be placed onto a field-programmable gate array (FPGA) or -application-specific integrated circuit (ASIC). - -#+attr_html: :width "600px" -#+caption: Current design of Vericert, where HTL is an intermediate language representing a finite state machine with data-path (FSMD) and Verilog is the target language. -#+name: fig:design -[[./images/toolflow.png]] - -The design shown in Figure [[fig:design]] shows how Vericert leverages an existing verified C compiler -called [[https://compcert.org/compcert-C.html][CompCert]] to perform this translation. - -#+texinfo: @insertcopying - -* COPYING -:PROPERTIES: -:COPYING: t -:END: - -Copyright (C) 2019-2022 Yann Herklotz. - -#+begin_quote -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_quote - -* Building Vericert -:PROPERTIES: -:EXPORT_FILE_NAME: building -:EXPORT_HUGO_SECTION: docs -:CUSTOM_ID: building -:END: - -#+transclude: [[file:~/projects/vericert/README.org::#building][file:../README.org::#building]] :only-contents :exclude-elements "headline property-drawer" -#+transclude: [[file:~/projects/vericert/README.org::#downloading-compcert][file:../README.org::#downloading-compcert]] :level 2 -#+transclude: [[file:~/projects/vericert/README.org::#setting-up-nix][file:../README.org::#setting-up-nix]] :level 2 -#+transclude: [[file:~/projects/vericert/README.org::#makefile-build][file:../README.org::#makefile-build]] :level 2 - -** Testing - -To test out ~vericert~ you can try the following examples which are in the test folder using the -following: - -#+begin_src shell -./bin/vericert test/loop.c -o loop.v -./bin/vericert test/conditional.c -o conditional.v -./bin/vericert test/add.c -o add.v -#+end_src - -Or by running the test suite using the following command: - -#+begin_src shell -make test -#+end_src - -* Using Vericert -:PROPERTIES: -:CUSTOM_ID: using-vericert -:END: - -Vericert can be used to translate a subset of C into Verilog. As a simple example, consider the -following C file (~main.c~): - -#+begin_src C -void matrix_multiply(int first[2][2], int second[2][2], int multiply[2][2]) { - int sum = 0; - for (int c = 0; c < 2; c++) { - for (int d = 0; d < 2; d++) { - for (int k = 0; k < 2; k++) { - sum = sum + first[c][k]*second[k][d]; - } - multiply[c][d] = sum; - sum = 0; - } - } -} - -int main() { - int f[2][2] = {{1, 2}, {3, 4}}; - int s[2][2] = {{5, 6}, {7, 8}}; - int m[2][2] = {{0, 0}, {0, 0}}; - - matrix_multiply(f, s, m); - return m[1][1]; -} -#+end_src - -It can be compiled using the following command, assuming that vericert is somewhere on the path. - -#+begin_src shell -vericert main.c -o main.v -#+end_src - -The Verilog file contains a top-level test-bench, which can be given to any Verilog simulator to -simulate the hardware, which should give the same result as executing the C code. Using [[http://iverilog.icarus.com/][Icarus -Verilog]] as an example: - -#+begin_src shell -iverilog -o main_v main.v -#+end_src - -When executing, it should therefore print the following: - -#+begin_src shell -$ ./main_v -finished: 50 -#+end_src - -This gives the same result as executing the C in the following way: - -#+begin_src shell -$ gcc -o main_c main.c -$ ./main_c -$ echo $? -50 -#+end_src - -** Man pages - -#+transclude: [[file:man.org][file:man.org]] :exclude-elements "keyword" :level 3 - -* Unreleased Features -:PROPERTIES: -:EXPORT_FILE_NAME: unreleased -:EXPORT_HUGO_SECTION: docs -:CUSTOM_ID: unreleased-features -:END: - -The following are unreleased features in Vericert that are currently being worked on and have not -been completely proven correct yet. Currently this includes features such as: - -- [[#scheduling][scheduling]], -- [[#operation-chaining][operation chaining]], -- [[#if-conversion][if-conversion]], and -- [[#functions][functions]]. - -This page gives some preliminary information on how the features are implemented and how the proofs -for the features are being done. Once these features are properly implemented, they will be added -to the proper documentation. - -** Scheduling -:PROPERTIES: -:CUSTOM_ID: scheduling -:END: -#+cindex: scheduling - -Scheduling is an optimisation which is used to run various instructions in parallel that are -independent to each other. - -** Operation Chaining -:PROPERTIES: -:CUSTOM_ID: operation-chaining -:END: - -Operation chaining is an optimisation that can be added on to scheduling and allows for the -sequential execution of instructions in a clock cycle, while executing other instructions in -parallel in the same clock cycle. - -** If-conversion -:PROPERTIES: -:CUSTOM_ID: if-conversion -:END: - -If-conversion is an optimisation which can turn code with simple control flow into a single block -(called a hyper-block), using predicated instructions. - -** Functions -:PROPERTIES: -:CUSTOM_ID: functions -:END: - -Functions are currently only inlined in Vericert, however, we are working on a proper interface to -integrate function calls into the hardware. - -* Coq Style Guide - :PROPERTIES: - :CUSTOM_ID: coq-style-guide - :EXPORT_FILE_NAME: coq-style-guide - :EXPORT_HUGO_SECTION: docs - :END: - -This style guide was taken from [[https://github.com/project-oak/silveroak][Silveroak]], it outlines code style for Coq code in this -repository. There are certainly other valid strategies and opinions on Coq code style; this is laid -out purely in the name of consistency. For a visual example of the style, see the [[#example][example]] at the -bottom of this file. - -** Code organization - :PROPERTIES: - :CUSTOM_ID: code-organization - :END: -*** Legal banner - :PROPERTIES: - :CUSTOM_ID: legal-banner - :END: - -- Files should begin with a copyright/license banner, as shown in the example above. - -*** Import statements - :PROPERTIES: - :CUSTOM_ID: import-statements - :END: - -- =Require Import= statements should all go at the top of the file, followed by file-wide =Import= - statements. - - - =Import=s often contain notations or typeclass instances that might override notations or - instances from another library, so it's nice to highlight them separately. - -- One =Require Import= statement per line; it's easier to scan that way. -- =Require Import= statements should use "fully-qualified" names (e.g. =Require Import - Coq.ZArith.ZArith= instead of =Require Import ZArith=). - - - Use the =Locate= command to find the fully-qualified name! - -- =Require Import='s should go in the following order: - - 1. Standard library dependencies (start with =Coq.=) - 2. External dependencies (anything outside the current project) - 3. Same-project dependencies - -- =Require Import='s with the same root library (the name before the first =.=) should be grouped - together. Within each root-library group, they should be in alphabetical order (so =Coq.Lists.List= - before =Coq.ZArith.ZArith=). - -*** Notations and scopes - :PROPERTIES: - :CUSTOM_ID: notations-and-scopes - :END: - -- Any file-wide =Local Open Scope='s should come immediately after the =Import=s (see example). - - - Always use =Local Open Scope=; just =Open Scope= will sneakily open the scope for those who import - your file. - -- Put notations in their own separate modules or files, so that those who import your file can - choose whether or not they want the notations. - - - Conflicting notations can cause a lot of headache, so it comes in very handy to leave this - flexibility! - -** Formatting - :PROPERTIES: - :CUSTOM_ID: formatting - :END: -*** Line length - :PROPERTIES: - :CUSTOM_ID: line-length - :END: - -- Maximum line length 80 characters. - - - Many Coq IDE setups divide the screen in half vertically and use only half to display source - code, so more than 80 characters can be genuinely hard to read on a laptop. - -*** Whitespace and indentation - :PROPERTIES: - :CUSTOM_ID: whitespace-and-indentation - :END: - -- No trailing whitespace. - -- Spaces, not tabs. - -- Files should end with a newline. - - - Many editors do this automatically on save. - -- Colons may be either "English-spaced", with no space before the colon and one space after (=x: nat=) - or "French-spaced", with one space before and after (=x : nat=). - -- Default indentation is 2 spaces. - - - Keeping this small prevents complex proofs from being indented ridiculously far, and matches IDE - defaults. - -- Use 2-space indents if inserting a line break immediately after: - - - =Proof.= - - =fun <...> =>= - - =forall <...>,= - - =exists <....>,= - -- The style for indenting arguments in function application depends on where you make a line - break. If you make the line break immediately after the function name, use a 2-space - indent. However, if you make it after one or more arguments, align the next line with the first - argument: - - #+begin_src coq - (Z.pow - 1 2) - (Z.pow 1 2 3 - 4 5 6) - #+end_src - -- =Inductive= cases should not be indented. Example: - - #+begin_src coq - Inductive Foo : Type := - | FooA : Foo - | FooB : Foo - . - #+end_src - -- =match= or =lazymatch= cases should line up with the "m" in =match= or "l" in =lazymatch=, as in the - following examples: - - #+begin_src coq - match x with - | 3 => true - | _ => false - end. - - lazymatch x with - | 3 => idtac - | _ => fail "Not equal to 3:" x - end. - - repeat match goal with - | _ => progress subst - | _ => reflexivity - end. - - do 2 lazymatch goal with - | |- context [eq] => idtac - end. - #+end_src - -** Definitions and Fixpoints - :PROPERTIES: - :CUSTOM_ID: definitions-and-fixpoints - :END: - -- It's okay to leave the return type of =Definition='s and =Fixpoint='s implicit (e.g. ~Definition x := 5~ - instead of ~Definition x : nat := 5~) when the type is very simple or obvious (for instance, the - definition is in a file which deals exclusively with operations on =Z=). - -** Inductives - :PROPERTIES: - :CUSTOM_ID: inductives - :END: - -- The =.= ending an =Inductive= can be either on the same line as the last case or on its own line - immediately below. That is, both of the following are acceptable: - - #+begin_src coq - Inductive Foo : Type := - | FooA : Foo - | FooB : Foo - . - Inductive Foo : Type := - | FooA : Foo - | FooB : Foo. - #+end_src - -** Lemma/Theorem statements - :PROPERTIES: - :CUSTOM_ID: lemmatheorem-statements - :END: - -- Generally, use =Theorem= for the most important, top-level facts you prove and =Lemma= for everything - else. -- Insert a line break after the colon in the lemma statement. -- Insert a line break after the comma for =forall= or =exist= quantifiers. -- Implication arrows (=->=) should share a line with the previous hypothesis, not the following one. -- There is no need to make a line break after every =->=; short preconditions may share a line. - -** Proofs and tactics - :PROPERTIES: - :CUSTOM_ID: proofs-and-tactics - :END: - -- Use the =Proof= command (lined up vertically with =Lemma= or =Theorem= it corresponds to) to open a - proof, and indent the first line after it 2 spaces. - -- Very small proofs (where =Proof. Qed.= is <= 80 characters) can go all in one line. - -- When ending a proof, align the ending statement (=Qed=, =Admitted=, etc.) with =Proof=. - -- Avoid referring to autogenerated names (e.g. =H0=, =n0=). It's okay to let Coq generate these names, - but you should not explicitly refer to them in your proof. So =intros; my_solver= is fine, but - =intros; apply H1; my_solver= is not fine. - - - You can force a non-autogenerated name by either putting the variable before the colon in the - lemma statement (=Lemma foo x : ...= instead of =Lemma foo : forall x, ...=), or by passing - arguments to =intros= (e.g. =intros ? x= to name the second argument =x=) - -- This way, the proof won't break when new hypotheses are added or autogenerated variable names - change. - -- Use curly braces ={}= for subgoals, instead of bullets. - -- /Never write tactics with more than one subgoal focused./ This can make the proof very confusing to - step through! If you have more than one subgoal, use curly braces. - -- Consider adding a comment after the opening curly brace that explains what case you're in (see - example). - - - This is not necessary for small subgoals but can help show the major lines of reasoning in large - proofs. - -- If invoking a tactic that is expected to return multiple subgoals, use =[ | ... | ]= before the =.= to - explicitly specify how many subgoals you expect. - - - Examples: =split; [ | ].= =induction z; [ | | ].= - - This helps make code more maintainable, because it fails immediately if your tactic no longer - solves as many subgoals as expected (or unexpectedly solves more). - -- If invoking a string of tactics (composed by =;=) that will break the goal into multiple subgoals - and then solve all but one, still use =[ ]= to enforce that all but one goal is solved. - - - Example: =split; try lia; [ ]=. - -- Tactics that consist only of =repeat=-ing a procedure (e.g. =repeat match=, =repeat first=) should - factor out a single step of that procedure a separate tactic called =_step=, because - the single-step version is much easier to debug. For instance: - - #+begin_src coq - Ltac crush_step := - match goal with - | _ => progress subst - | _ => reflexivity - end. - Ltac crush := repeat crush_step. - #+end_src - -** Naming - :PROPERTIES: - :CUSTOM_ID: naming - :END: - -- Helper proofs about standard library datatypes should go in a module that is named to match the - standard library module (see example). - - - This makes the helper proofs look like standard-library ones, which is helpful for categorizing - them if they're genuinely at the standard-library level of abstraction. - -- Names of modules should start with capital letters. -- Names of inductives and their constructors should start with capital letters. -- Names of other definitions/lemmas should be snake case. - -** Example - :PROPERTIES: - :CUSTOM_ID: example - :END: -A small standalone Coq file that exhibits many of the style points. - -#+begin_src coq -(* - * Vericert: Verified high-level synthesis. - * Copyright (C) 2021 Name - * - * - *) - - Require Import Coq.Lists.List. - Require Import Coq.micromega.Lia. - Require Import Coq.ZArith.ZArith. - Import ListNotations. - Local Open Scope Z_scope. - - (* Helper proofs about standard library integers (Z) go within [Module Z] so - that they match standard-library Z lemmas when used. *) - Module Z. - Lemma pow_3_r x : x ^ 3 = x * x * x. - Proof. lia. Qed. (* very short proofs can go all on one line *) - - Lemma pow_4_r x : x ^ 4 = x * x * x * x. - Proof. - change 4 with (Z.succ (Z.succ (Z.succ (Z.succ 0)))). - repeat match goal with - | _ => rewrite Z.pow_1_r - | _ => rewrite Z.pow_succ_r by lia - | |- context [x * (?a * ?b)] => - replace (x * (a * b)) with (a * b * x) by lia - | _ => reflexivity - end. - Qed. - End Z. - (* Now we can access the lemmas above as Z.pow_3_r and Z.pow_4_r, as if they - were in the ZArith library! *) - - Definition bar (x y : Z) := x ^ (y + 1). - - (* example with a painfully manual proof to show case formatting *) - Lemma bar_upper_bound : - forall x y a, - 0 <= x <= a -> 0 <= y -> - 0 <= bar x y <= a ^ (y + 1). - Proof. - (* avoid referencing autogenerated names by explicitly naming variables *) - intros x y a Hx Hy. revert y Hy x a Hx. - (* explicitly indicate # subgoals with [ | ... | ] if > 1 *) - cbv [bar]; refine (natlike_ind _ _ _); [ | ]. - { (* y = 0 *) - intros; lia. } - { (* y = Z.succ _ *) - intros. - rewrite Z.add_succ_l, Z.pow_succ_r by lia. - split. - { (* 0 <= bar x y *) - apply Z.mul_nonneg_nonneg; [ lia | ]. - apply Z.pow_nonneg; lia. } - { (* bar x y < a ^ y *) - rewrite Z.pow_succ_r by lia. - apply Z.mul_le_mono_nonneg; try lia; - [ apply Z.pow_nonneg; lia | ]. - (* For more flexible proofs, use match statements to find hypotheses - rather than referring to them by autogenerated names like H0. In this - case, we'll take any hypothesis that applies to and then solves the - goal. *) - match goal with H : _ |- _ => apply H; solve [auto] end. } } - Qed. - - (* Put notations in a separate module or file so that importers can - decide whether or not to use them. *) - Module BarNotations. - Infix "#" := bar (at level 40) : Z_scope. - Notation "x '##'" := (bar x x) (at level 40) : Z_scope. - End BarNotations. -#+end_src - -* Index - Features -:PROPERTIES: -:CUSTOM_ID: cindex -:APPENDIX: t -:INDEX: cp -:DESCRIPTION: Key concepts & features -:END: - -* Export Setup :noexport: - -#+setupfile: common.org - -#+export_file_name: vericert.texi - -#+texinfo_dir_category: High-level synthesis tool -#+texinfo_dir_title: Vericert -#+texinfo_dir_desc: Formally verified high-level synthesis tool - -* GNU Free Documentation License -:PROPERTIES: -:appendix: t -:END: - -#+include: res/fdl.org diff --git a/docs/images/toolflow.pdf b/docs/images/toolflow.pdf deleted file mode 100644 index 5fcee67..0000000 Binary files a/docs/images/toolflow.pdf and /dev/null differ diff --git a/docs/images/toolflow.png b/docs/images/toolflow.png deleted file mode 100644 index 601d6be..0000000 Binary files a/docs/images/toolflow.png and /dev/null differ diff --git a/docs/images/toolflow.svg b/docs/images/toolflow.svg deleted file mode 100644 index 0d8f39f..0000000 --- a/docs/images/toolflow.svg +++ /dev/null @@ -1,1250 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/docs/man.org b/docs/man.org deleted file mode 100644 index cb6143f..0000000 --- a/docs/man.org +++ /dev/null @@ -1,89 +0,0 @@ -#+title: vericert -#+man_class_options: :section-id "1" -#+options: toc:nil num:nil -#+html_head_extra: - -* NAME - -vericert - A formally verified high-level synthesis tool. - -* SYNOPSYS - -*vericert* [ *OPTION* ]... [ *FILE* ]... - -* DESCRIPTION - -** HLS Options: - -- --no-hls :: Do not use HLS and generate standard flow -- --simulate :: Simulate the result with the Verilog semantics -- --debug-hls :: Add debug logic to the Verilog -- --initialise-stack :: initialise the stack to all 0s - -** HLS Optimisations: - -- -fschedule :: Schedule the resulting hardware [off] -- -fif-conversion :: If-conversion optimisation [off] - -** General options: - -- -stdlib :: Set the path of the Compcert run-time library -- -v :: Print external commands before invoking them -- -timings :: Show the time spent in various compiler passes -- -version :: Print the version string and exit -- -target :: Generate code for the given target -- -conf :: Read configuration from file -- @ :: Read command line options from - -** Tracing Options: - -- -dprepro :: Save C file after preprocessing in .i -- -dparse :: Save C file after parsing and elaboration in .parsed.c -- -dc :: Save generated C in .compcert.c -- -dclight :: Save generated Clight in .light.c -- -dcminor :: Save generated Cminor in .cm -- -drtl :: Save RTL at various optimization points in .rtl. -- -drtlblock :: Save RTLBlock .rtlblock -- -dhtl :: Save HTL before Verilog generation .htl -- -dltl :: Save LTL after register allocation in .ltl -- -dmach :: Save generated Mach code in .mach -- -dasm :: Save generated assembly in .s -- -dall :: Save all generated intermediate files in . -- -sdump :: Save info for post-linking validation in .json -- -o :: Generate output in - -** Diagnostic options: - -- -Wall :: Enable all warnings -- -W :: Enable the specific -- -Wno- :: Disable the specific -- -Werror :: Make all warnings into errors -- -Werror= :: Turn into an error -- -Wno-error= :: Turn into a warning even if -Werror is specified -- -Wfatal-errors :: Turn all errors into fatal errors aborting the compilation -- -fdiagnostics-color :: Turn on colored diagnostics -- -fno-diagnostics-color :: Turn of colored diagnostics -- -fmax-errors= :: Maximum number of errors to report -- -fdiagnostics-show-option :: Print the option name with mappable diagnostics -- -fno-diagnostics-show-option :: Turn of printing of options with mappable diagnostics - -* AUTHOR - -Written by Yann Herklotz, Michalis Pardalos, James Pollard, Nadesh Ramanathan and John Wickerson. - -* COPYRIGHT - -Copyright (C) 2019-2022 Yann Herklotz - -This program is free software: you can redistribute it and/or modify -it under the terms of the GNU General Public License as published by -the Free Software Foundation, either version 3 of the License, or -(at your option) any later version. - -This program is distributed in the hope that it will be useful, -but WITHOUT ANY WARRANTY; without even the implied warranty of -MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -GNU General Public License for more details. - -You should have received a copy of the GNU General Public License -along with this program. If not, see . diff --git a/docs/res/coqdoc.css b/docs/res/coqdoc.css deleted file mode 100644 index 5572aaa..0000000 --- a/docs/res/coqdoc.css +++ /dev/null @@ -1,867 +0,0 @@ -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/docs/res/fdl.org b/docs/res/fdl.org deleted file mode 100644 index 81e2cd9..0000000 --- a/docs/res/fdl.org +++ /dev/null @@ -1,489 +0,0 @@ -# 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/docs/res/install-deps.el b/docs/res/install-deps.el deleted file mode 100644 index 09cf4ae..0000000 --- a/docs/res/install-deps.el +++ /dev/null @@ -1,11 +0,0 @@ -(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/docs/res/publish.el b/docs/res/publish.el deleted file mode 100644 index c083eb0..0000000 --- a/docs/res/publish.el +++ /dev/null @@ -1,23 +0,0 @@ -(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) -- cgit