Commit c99edd11 authored by Marco Perronet's avatar Marco Perronet Committed by Björn Brandenburg

Add pretty documentation generation

Add the `htmlpretty` target to the Makefile to generate prettier documentation,
based on the CoqdocJS project.

     https://www.ps.uni-saarland.de/~ttebbi/coqdocjs/

     https://github.com/tebbi/coqdocjs

Many thanks to Tobias Tebbi for creating CoqdocJS.
parent 0ac14e20
......@@ -60,15 +60,18 @@ doc:
dependencies:
- 1.9.0-coq-8.9
script:
- make html
- make html -j ${NJOBS}
- mv html with-proofs
- make gallinahtml
- make gallinahtml -j ${NJOBS}
- mv html without-proofs
- make htmlpretty -j ${NJOBS}
- mv html pretty
artifacts:
name: "prosa-spec-$CI_COMMIT_REF_NAME"
paths:
- "with-proofs/"
- "without-proofs/"
- "pretty/"
expire_in: 1 week
proof-length:
......
......@@ -45,7 +45,11 @@ For example, the schedulability analysis for global scheduling with release jitt
The Coqdoc documentation (as shown on the [webpage](http://prosa.mpi-sws.org/documentation.html)) can be easily generated with `Make`:
```$ make gallinahtml -j4```
```$ make html -j 4``` *Documentation with proofs*
```$ make gallinahtml -j 4``` *Documentation without proofs*
```$ make htmlpretty -j 4``` *Pretty documentation (can also hide/show proofs)*
Since Coqdoc requires object files as input, please make sure that the code is compilable.
......
......@@ -36,3 +36,5 @@ else
sed -i 's|rm -f $(VOFILES) $(VOFILES:.vo=.vio) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old)|find . -name "*.vo" -delete -o -name "*.glob" -delete -o -name "*.v.d" -delete -o -name "*.vio" -delete -o -name "*.old" -delete -o -name "*.beautified" -delete|g' Makefile
fi
# Patch Makefile.coqdocjs for pretty documentation targets
printf "\n# Include pretty documentation targets\ninclude scripts/coqdocjs/Makefile.coqdocjs" >> Makefile
htmlpretty: $(GLOBFILES) $(VFILES)
$(SHOW)'COQDOC -d html $(GAL) --with-header scripts/coqdocjs/header.html --with-footer scripts/coqdocjs/footer.html'
$(HIDE)mkdir -p html
$(HIDE)$(COQDOC) \
-toc $(COQDOCFLAGS) \
--with-header scripts/coqdocjs/header.html --with-footer scripts/coqdocjs/footer.html \
-html $(GAL) $(COQDOCLIBS) -d html $(VFILES)
$(HIDE)cp scripts/coqdocjs/resources/* html
$(HIDE)mv html/index.html html/indexpage.html
</div>
<div id="footer">
Generated by <a href="http://coq.inria.fr/">coqdoc</a> and improved with <a href="https://github.com/tebbi/coqdocjs">CoqdocJS</a>
</div>
</div>
</body>
</html>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html;charset=utf-8" />
<link href="coqdoc.css" rel="stylesheet" type="text/css" />
<link href="coqdocjs.css" rel="stylesheet" type="text/css"/>
<script type="text/javascript" src="config.js"></script>
<script type="text/javascript" src="coqdocjs.js"></script>
</head>
<body onload="document.getElementById('content').focus()">
<div id="header">
<span class="left">
<span class="modulename"> <script> document.write(document.title) </script> </span>
</span>
<span class="button" id="toggle-proofs"></span>
<span class="right">
<a href="../">Project Page</a>
<a href="./indexpage.html"> Index </a>
<a href="./toc.html"> Table of Contents </a>
</span>
</div>
<div id="content" tabindex="-1" onblur="document.getElementById('content').focus()">
<div id="main">
Copyright (c) 2016, Tobias Tebbi
All rights reserved.
Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are met:
* Redistributions of source code must retain the above copyright
notice, this list of conditions and the following disclaimer.
* Redistributions in binary form must reproduce the above copyright
notice, this list of conditions and the following disclaimer in the
documentation and/or other materials provided with the distribution.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDERS BE LIABLE FOR ANY
DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
var coqdocjs = coqdocjs || {};
coqdocjs.repl = {
"forall": "",
"exists": "",
"~": "¬",
"/\\": "",
"\\/": "",
"->": "",
"<-": "",
"<->": "",
"=>": "",
"<>": "",
"<=": "",
">=": "",
"el": "",
"nel": "",
"<<=": "",
"|-": "",
">>": "»",
"<<": "",
"++": "",
"===": "",
"=/=": "",
"=~=": "",
"==>": "",
"lhd": "",
"rhd": "",
"nat": "",
"alpha": "α",
"beta": "β",
"gamma": "γ",
"delta": "δ",
"epsilon": "ε",
"eta": "η",
"iota": "ι",
"kappa": "κ",
"lambda": "λ",
"mu": "μ",
"nu": "ν",
"omega": "ω",
"phi": "ϕ",
"pi": "π",
"psi": "ψ",
"rho": "ρ",
"sigma": "σ",
"tau": "τ",
"theta": "θ",
"xi": "ξ",
"zeta": "ζ",
"Delta": "Δ",
"Gamma": "Γ",
"Pi": "Π",
"Sigma": "Σ",
"Omega": "Ω",
"Xi": "Ξ"
};
coqdocjs.subscr = {
"0" : "",
"1" : "",
"2" : "",
"3" : "",
"4" : "",
"5" : "",
"6" : "",
"7" : "",
"8" : "",
"9" : "",
};
coqdocjs.replInText = ["==>","<=>", "=>", "->", "<-", ":="];
@import url(https://fonts.googleapis.com/css?family=Open+Sans:400,700);
body{
font-family: 'Open Sans', sans-serif;
font-size: 14px;
color: #2D2D2D
}
a {
text-decoration: none;
border-radius: 3px;
padding-left: 3px;
padding-right: 3px;
margin-left: -3px;
margin-right: -3px;
color: inherit;
font-weight: bold;
}
#main .code a, #main .inlinecode a, #toc a {
font-weight: inherit;
}
a[href]:hover, [clickable]:hover{
background-color: rgba(0,0,0,0.1);
cursor: pointer;
}
h, h1, h2, h3, h4, h5 {
line-height: 1;
color: black;
text-rendering: optimizeLegibility;
font-weight: normal;
letter-spacing: 0.1em;
text-align: left;
}
div + br {
display: none;
}
div:empty{ display: none;}
#main h1 {
font-size: 2em;
}
#main h2 {
font-size: 1.667rem;
}
#main h3 {
font-size: 1.333em;
}
#main h4, #main h5, #main h6 {
font-size: 1em;
}
#toc h2 {
padding-bottom: 0;
}
#main .doc {
margin: 0;
text-align: justify;
}
.inlinecode, .code, #main pre {
font-family: monospace;
}
.code > br:first-child {
display: none;
}
.doc + .code{
margin-top:0.5em;
}
.block{
display: block;
margin-top: 5px;
margin-bottom: 5px;
padding: 10px;
text-align: center;
}
.block img{
margin: 15px;
}
table.infrule {
border: 0px;
margin-left: 50px;
margin-top: 10px;
margin-bottom: 10px;
}
td.infrule {
font-family: "Droid Sans Mono", "DejaVu Sans Mono", monospace;
text-align: center;
padding: 0;
line-height: 1;
}
tr.infrulemiddle hr {
margin: 1px 0 1px 0;
}
.infrulenamecol {
color: rgb(60%,60%,60%);
padding-left: 1em;
padding-bottom: 0.1em
}
.id[type="constructor"], .id[type="projection"], .id[type="method"],
.id[title="constructor"], .id[title="projection"], .id[title="method"] {
color: #A30E16;
}
.id[type="var"], .id[type="variable"],
.id[title="var"], .id[title="variable"] {
color: inherit;
}
.id[type="definition"], .id[type="record"], .id[type="class"], .id[type="instance"], .id[type="inductive"], .id[type="library"],
.id[title="definition"], .id[title="record"], .id[title="class"], .id[title="instance"], .id[title="inductive"], .id[title="library"] {
color: #A6650F;
}
.id[type="lemma"],
.id[title="lemma"]{
color: #188B0C;
}
.id[type="keyword"], .id[type="notation"], .id[type="abbreviation"],
.id[title="keyword"], .id[title="notation"], .id[title="abbreviation"]{
color : #2874AE;
}
.comment {
color: #808080;
}
/* TOC */
#toc h2{
letter-spacing: 0;
font-size: 1.333em;
}
/* Index */
#index {
margin: 0;
padding: 0;
width: 100%;
}
#index #frontispiece {
margin: 1em auto;
padding: 1em;
width: 60%;
}
.booktitle { font-size : 140% }
.authors { font-size : 90%;
line-height: 115%; }
.moreauthors { font-size : 60% }
#index #entrance {
text-align: center;
}
#index #entrance .spacer {
margin: 0 30px 0 30px;
}
ul.doclist {
margin-top: 0em;
margin-bottom: 0em;
}
#toc > * {
clear: both;
}
#toc > a {
display: block;
float: left;
margin-top: 1em;
}
#toc a h2{
display: inline;
}
/* replace unicode */
.id[repl] .hidden {
font-size: 0;
}
.id[repl]:before{
content: attr(repl);
}
/* folding proofs */
@keyframes show-proof {
0% {
max-height: 1.2em;
opacity: 1;
}
99% {
max-height: 1000em;
}
100%{
}
}
@keyframes hide-proof {
from {
visibility: visible;
max-height: 10em;
opacity: 1;
}
to {
max-height: 1.2em;
}
}
.proof {
cursor: pointer;
}
.proof * {
cursor: pointer;
}
.proof {
overflow: hidden;
position: relative;
transition: opacity 1s;
display: inline-block;
}
.proof[show="false"] {
max-height: 1.2em;
visibility: hidden;
opacity: 0;
}
.proof[show="false"][animate] {
animation-name: hide-proof;
animation-duration: 0.25s;
}
.proof[show=true] {
animation-name: show-proof;
animation-duration: 10s;
}
.proof[show="false"]:before {
position: absolute;
visibility: visible;
width: 100%;
height: 100%;
display: block;
opacity: 0;
content: "M";
}
.proof[show="false"]:hover:before {
content: "";
}
.proof[show="false"] + br + br {
display: none;
}
.proof[show="false"]:hover {
visibility: visible;
opacity: 0.5;
}
#toggle-proofs[proof-status="no-proofs"] {
display: none;
}
#toggle-proofs[proof-status="some-hidden"]:before {
content: "Show Proofs";
}
#toggle-proofs[proof-status="all-shown"]:before {
content: "Hide Proofs";
}
/* page layout */
html, body {
height: 100%;
margin:0;
padding:0;
}
body {
display: flex;
flex-direction: column
}
#content {
flex: 1;
overflow: auto;
display: flex;
flex-direction: column;
}
#content:focus {
outline: none; /* prevent glow in OS X */
}
#main {
display: block;
padding: 16px;
padding-top: 1em;
padding-bottom: 2em;
margin-left: auto;
margin-right: auto;
max-width: 60em;
flex: 1 0 auto;
}
.libtitle {
display: none;
}
/* header */
#header {
width:100%;
padding: 0;
margin: 0;
display: flex;
align-items: center;
background-color: rgb(21,57,105);
color: white;
font-weight: bold;
overflow: hidden;
}
.button {
cursor: pointer;
}
#header * {
text-decoration: none;
vertical-align: middle;
margin-left: 15px;
margin-right: 15px;
}
#header > .right, #header > .left {
display: flex;
flex: 1;
align-items: center;
}
#header > .left {
text-align: left;
}
#header > .right {
flex-direction: row-reverse;
}
#header a, #header .button {
color: white;
box-sizing: border-box;
}
#header a {
border-radius: 0;
padding: 0.2em;
}
#header .button {
background-color: rgb(63, 103, 156);
border-radius: 1em;
padding-left: 0.5em;
padding-right: 0.5em;
margin: 0.2em;
}
#header a:hover, #header .button:hover {
background-color: rgb(181, 213, 255);
color: black;
}
#header h1 { padding: 0;
margin: 0;}
/* footer */
#footer {
text-align: center;
opacity: 0.5;
font-size: 75%;
}
/* hyperlinks */
@keyframes highlight {
50%{
background-color: black;
}
}
:target * {
animation-name: highlight;
animation-duration: 1s;
}
a[name]:empty {
float: right;
}
var coqdocjs = coqdocjs || {};
(function(){
function replace(s){
var m;
if (m = s.match(/^(.+)'/)) {
return replace(m[1])+"'";
} else if (m = s.match(/^([A-Za-z]+)_?(\d+)$/)) {
return replace(m[1])+m[2].replace(/\d/g, function(d){return coqdocjs.subscr[d]});
} else if (coqdocjs.repl.hasOwnProperty(s)){
return coqdocjs.repl[s]
} else {
return s;
}
}
function toArray(nl){
return Array.prototype.slice.call(nl);
}
function replInTextNodes() {
coqdocjs.replInText.forEach(function(toReplace){
toArray(document.getElementsByClassName("code")).concat(toArray(document.getElementsByClassName("inlinecode"))).forEach(function(elem){
toArray(elem.childNodes).forEach(function(node){
if (node.nodeType != Node.TEXT_NODE) return;
var fragments = node.textContent.split(toReplace);
node.textContent = fragments[fragments.length-1];
for (var k = 0; k < fragments.length - 1; ++k) {
node.parentNode.insertBefore(document.createTextNode(fragments[k]),node);
var replacement = document.createElement("span");
replacement.appendChild(document.createTextNode(toReplace));
replacement.setAttribute("class", "id");
replacement.setAttribute("type", "keyword");
node.parentNode.insertBefore(replacement, node);
}
});
});
});
}
function replNodes() {
toArray(document.getElementsByClassName("id")).forEach(function(node){
if (["var", "variable", "keyword", "notation", "definition", "inductive"].indexOf(node.getAttribute("type"))>=0){
var text = node.textContent;
var replText = replace(text);
if(text != replText) {
node.setAttribute("repl", replText);
node.setAttribute("title", text);
var hidden = document.createElement("span");
hidden.setAttribute("class", "hidden");
while (node.firstChild) {
hidden.appendChild(node.firstChild);
}
node.appendChild(hidden);
}
}
});
}
function isProofStart(s){
return s == "Proof";
}
function isProofEnd(s){
return ["Qed", "Admitted", "Defined"].indexOf(s) > -1;
}
function proofStatus(){
var proofs = toArray(document.getElementsByClassName("proof"));
if(proofs.length) {
for(proof of proofs) {
if (proof.getAttribute("show") === "false") {
return "some-hidden";
}
}
return "all-shown";
}
else {
return "no-proofs";
}
}
function updateView(){
document.getElementById("toggle-proofs").setAttribute("proof-status", proofStatus());
}
function foldProofs() {
toArray(document.getElementsByClassName("id")).forEach(function(node){
if(isProofStart(node.textContent)) {
var proof = document.createElement("span");
proof.setAttribute("class", "proof");
node.parentNode.insertBefore(proof, node);
if(proof.previousSibling.nodeType === Node.TEXT_NODE)
proof.appendChild(proof.previousSibling);
while(node && !isProofEnd(node.textContent)) {
proof.appendChild(node);
node = proof.nextSibling;
}
if (proof.nextSibling) proof.appendChild(proof.nextSibling); // the Qed
if (proof.nextSibling) proof.appendChild(proof.nextSibling); // the dot after the Qed
proof.addEventListener("click", function(proof){return function(e){
console.log(e.target.parentNode.tagName);
if (e.target.parentNode.tagName.toLowerCase() === "a")
return;
proof.setAttribute("show", proof.getAttribute("show") === "true" ? "false" : "true");
proof.setAttribute("animate", "");
updateView();
};}(proof));
proof.setAttribute("show", "false");
}
});