From e8027cbeac9e4fc0efe5a0b661bcc2e2a89dab35 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Wed, 25 Nov 2020 15:47:30 +0000
Subject: Fix documentation for docs website

---
 docs/.nojekyll               |    0
 docs/building.org            |   68 --
 docs/css/org.css             | 1552 ++++++++++++++++--------------------------
 docs/documentation.org       |   70 ++
 docs/index.org               |    8 +-
 docs/publish.el              |   97 ++-
 docs/publish.setup           |    2 +
 docs/setup.org               |    7 -
 scripts/download_artifact.sh |    6 +-
 9 files changed, 760 insertions(+), 1050 deletions(-)
 create mode 100644 docs/.nojekyll
 delete mode 100644 docs/building.org
 create mode 100644 docs/documentation.org
 create mode 100644 docs/publish.setup
 delete mode 100644 docs/setup.org

diff --git a/docs/.nojekyll b/docs/.nojekyll
new file mode 100644
index 0000000..e69de29
diff --git a/docs/building.org b/docs/building.org
deleted file mode 100644
index 48a6a90..0000000
--- a/docs/building.org
+++ /dev/null
@@ -1,68 +0,0 @@
-#+SETUPFILE: setup.org
-#+TITLE: Building
-
-To build Vericert, the provided Makefile can be used. External dependencies are needed to build the project, which can be pulled in automatically with [[https://nixos.org/nix/][nix]] using the provided ~default.nix~ and ~shell.nix~ files.
-
-The project is written in Coq, a theorem prover, which is extracted to OCaml so that it can then be compiled and executed. The dependencies of this project are the following:
-
-- [[https://coq.inria.fr/][Coq]]: theorem prover that is used to also program the HLS tool.
-- [[https://ocaml.org/][OCaml]]: the OCaml compiler to compile the extracted files.
-- [[https://github.com/mit-plv/bbv][bbv]]: an efficient bit vector library.
-- [[https://github.com/ocaml/dune][dune]]: build tool for ocaml projects to gather all the ocaml files and compile them in the right order.
-- [[http://gallium.inria.fr/~fpottier/menhir/][menhir]]: parser generator for ocaml.
-- [[https://github.com/ocaml/ocamlfind][findlib]] to find installed OCaml libraries.
-- [[https://gcc.gnu.org/][GCC]]: compiler to help build CompCert.
-
-These dependencies can be installed manually, or automatically through Nix.
-
-* Downloading CompCert
-
-CompCert is added as a submodule in the ~lib/CompCert~ directory. It is needed to run the build process below, as it is the one dependency that is not downloaded by nix, and has to be downloaded together with the repository. To clone CompCert together with this project, you can run:
-
-#+begin_src shell
-git clone --recursive https://github.com/ymherklotz/vericert
-#+end_src
-
-If the repository is already cloned, you can run the following command to make sure that CompCert is also downloaded:
-
-#+begin_src shell
-git submodule update --init
-#+end_src
-
-* Setting up Nix
-
-Nix is a package manager that can create an isolated environment so that the builds are reproducible. Once nix is installed, it can be used in the following way.
-
-To open a shell which includes all the necessary dependencies, one can use:
-
-#+begin_src shell
-nix-shell
-#+end_src
-
-which will open a shell that has all the dependencies loaded.
-
-* Makefile build
-
-If the dependencies were installed manually, or if one is in the ~nix-shell~, the project can be built by running:
-
-#+begin_src shell
-make -j8
-#+end_src
-
-and installed locally, or under the ~PREFIX~ location using:
-
-#+begin_src shell
-make install
-#+end_src
-
-Which will install the binary in ~./bin/vericert~ by default. However, this can be changed by changing the ~PREFIX~ environment variable, in which case the binary will be installed in ~$PREFIX/bin/vericert~.
-
-* Running
-
-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
diff --git a/docs/css/org.css b/docs/css/org.css
index aa713ec..99008e7 100644
--- a/docs/css/org.css
+++ b/docs/css/org.css
@@ -1,1058 +1,696 @@
-@media all
-{
-    body {
-        font-family: "Helvetica Neue", "Lucida Grande", "Lucida Sans Unicode", Helvetica, Arial, sans-serif !important;
-        font-size: 14px;
-        line-height: 21px;
-        color: #333;
+body {
+    width: 95%;
+    font-size: 14px;
+    margin: 2% auto;
+    line-height: 1.4em;
+    font-family: "Alegreya", serif;
+    color: #333;
+    background-color: #fdf6e3;
+}
 
-        max-width: 62em;
-        margin: auto;
-    }
-    body #content {
-        padding-top: 30px;
-    }
-    body .title {
-        margin-left: 0;
-    }
+#table-of-contents li, #toc li {
+    list-style-type: none;
+}
 
-    #org-div-home-and-up{
-        position: fixed;
-        right: 0;
-        top: 4em;
-    }
+.is-active-link::before {
+  background-color: #A5573E;
+}
 
-    /* TOC inspired by http://jashkenas.github.com/coffee-script */
-    #table-of-contents {
-        z-index: 100;
-        font-size: 10pt;
-        position: fixed;
-        right: 0em;
-        top: 0em;
-        background: white;
-        -webkit-box-shadow: 0 0 0.5em #777777;
-        -moz-box-shadow: 0 0 0.5em #777777;
-        -webkit-border-bottom-left-radius: 5px;
-        -moz-border-radius-bottomleft: 5px;
-        text-align: right;
-        /* ensure doesn't flow off the screen when expanded */
-        max-height: 80%;
-        overflow: auto; 
-    }
-    #table-of-contents h2 {
-        font-size: 10pt;
-        max-width: 9em;
-        font-weight: normal;
-        padding-left: 0.5em;
-        padding-left: 0.5em;
-        padding-top: 0.05em;
-        padding-bottom: 0.05em; 
+@media screen and (min-width: 600px) {
+    body {
+        font-size: 18px;
     }
+}
 
-    #table-of-contents #text-table-of-contents {
-        display: none;
-        text-align: left; 
-    }
-    #table-of-contents:hover #text-table-of-contents {
-        display: block;
-        padding: 0.5em;
-        margin-top: -1.5em; 
+@media screen and (min-width: 1200px) {
+    body {
+        margin: 2% 0;
+        margin-left: 27rem;
     }
 
-    #table-of-contents #text-table-of-contents ul {
-        list-style-position: outside;
+    #left-bar {
+        float: left;
+        position: fixed;
+        left: 0px;
+        top: 0px;
+        padding: 25px;
+        width: 20rem;
+        height: 100%;
+        background-color: #A5573E;
     }
 
-    /* #license { */
-    /*   padding: .3em; */
-    /*   border: 1px solid gray; */
-    /*   background-color: #eeeeee; */
-    /* } */
+    .logo > a {
+        color: #fdf6e3;
+        font-size: 5rem;
+        font-weight: bold;
+        text-decoration: none;
+    }
 
-    h1 {
-        /*
-          font-family:Sans;
-          font-weight:bold; */
-        font-size:2.1em;
-        padding:0 0 30px 0;
-        margin-top: 10px;
+    .logo {
+        text-align: center;
         margin-bottom: 10px;
-        color: #333;
     }
 
-    h2 {
-        font-family:Arial,sans-serif;
-        font-size:1.45em;
-        line-height:16px;
-        padding:7px 0 0 0;
-        color: #666;
+    .logo > a:hover {
+        border-bottom: none;
     }
 
-    .outline-text-2 {
-        margin-left: 0.1em
+    #navbar {
+        text-align: center;
     }
 
-    .title {
-
+    #navbar > span {
+        padding: 0 1em;
     }
 
-    h3 {
-        font-family:Arial,sans-serif;
-        font-size:1.3em;
-        color: #666;
-        margin-left: 0.6em;
+    #navbar > span > a {
+        color: #fdf6e3;
+        font-size: 1.5rem;
+        font-weight: bold;
     }
 
-    .outline-text-3 {
-        margin-left: 0.9em;
+    #navbar > span > a:hover {
+        border-bottom: none;
     }
 
-    h4 {
-        font-family:Arial,sans-serif;
-        font-size:1.2em;
-        margin-left: 1.2em;
-        color: #666;
+    a.toc-link {
+        color: #fdf6e3;
     }
 
-    .outline-text-4 {
-        margin-left: 1.45em;
+    header > p {
+        color: #fdf6e3;
+        line-height: 1.3;
     }
 
-    a {
-        text-decoration: none; 
-        color: #3399cc;
-    }
-    /* a:visited {text-decoration: none; color: #224444} */ /* Taken out because color too similar to text. */
-    a:visited {
-        text-decoration: none; 
-        color: #3399cc;
-    }  /* this is now the color of the Unicorns horn */
-    a:hover {
-        text-decoration: underline; 
-        color: #3399cc;
+    #postamble {
+        float: left;
+        position: fixed;
+        left: 50px;
+        bottom: 0;
+        max-width: 20rem;
     }
+}
 
-    ul, ol {
-        padding-left: 2em;
+@media screen and (min-width: 810px) {
+    body {
+        max-width: 800px;
     }
+}
 
-    ul {
-	list-style-type: square;
-	list-style-image: inherit;
-	list-style-position: outside;
-    }
-    ol {
-	list-style-type: decimal;
-	list-style-position: outside;
-    }
-    ol ol {
-	list-style-type: lower-alpha;
-    }
+::selection {
+    background: #D6EDFF;
+}
 
-    .todo {
-        color: #CA0000;
-    }
+p {
+    margin: 1em auto;
+}
 
-    .done {
-        color: #006666;
-    }
+ol,ul {
+    margin: 0 auto;
+}
 
-    .timestamp-kwd {
-        color: #444;
-    }
+dl {
+    margin: 0 auto;
+}
 
-    .tag {
+.title {
+    text-align: center;
+    margin: 0.8em auto;
+    color: black;
+}
 
-    }
+.subtitle {
+    text-align: center;
+    font-size: 0.7em;
+    line-height: 1.4;
+    font-weight: bold;
+    color: grey;
+    margin: 1em auto;
+}
 
-    li {
-        margin: .4em;
-    }
+.abstract {
+    margin: auto;
+    width: 80%;
+    font-style: italic;
+}
 
-    table {
-        border: none;
-        margin: auto;
-        margin-top: 10px;
-        margin-bottom: 10px;
-    }
+.abstract p:last-of-type:before {
+    content: "    ";
+    white-space: pre;
+}
 
-    td {
-        border: none;
-        border-left: 1px solid black;
-    }
+.status {
+    font-size: 90%;
+    margin: 2em auto;
+}
 
-    th {
-        border: none;
-    }
+[class^="section-number-"] {
+    margin-right: .5em;
+}
 
-    table.full {
-    }
+[id^="orgheadline"] {
+    clear: both;
+}
 
-    table.full td {
-	border: 1px solid black;
-	padding: 5px;
-    }
+#footnotes {
+    font-size: 90%;
+}
 
-    code {
-        font-size: 100%;
-        color: black;
-        border: 1px solid #DEDEDE;
-        padding: 0px 0.2em;
-    }
+.footpara {
+    display: inline;
+    margin: .2em auto;
+}
 
-    img {
-        border: none;
-    }
+.footdef {
+    margin-bottom: 1em;
+}
 
-    .share img {
-        opacity: .4;
-        -moz-opacity: .4;
-        filter: alpha(opacity=40);
-    }
+.footdef sup {
+    padding-right: .5em;
+}
 
-    .share img:hover {
-        opacity: 1;
-        -moz-opacity: 1;
-        filter: alpha(opacity=100);
-    }
+a {
+    color: #527d9a;
+    text-decoration: none;
+}
 
-    /* pre {border: 1px solid #555; */
-    /*      background: #EEE; */
-    /*      font-size: 9pt; */
-    /*      padding: 1em; */
-    /*     } */
-
-    /* pre { */
-    /*     color: #e5e5e5; */
-    /*     background-color: #000000; */
-    /*     padding: 1.4em; */
-    /*     border: 2px solid gray; */
-    /* } */
-
-    /* pre { */
-    /*     background-color: #2b2b2b; */
-    /*     border: 4px solid gray; */
-    /*     color: #EEE; */
-    /*     overflow: auto; */
-    /*     padding: 1em; */
-    /*  } */
-
-    pre {
-        font-family: Monaco, Consolas, "Lucida Console", monospace;
-        color: black;
-        background-color: #ffffff;
-        padding: 1.2em;
-        /* border: 1px solid #dddddd; */
-        overflow: auto;
-
-        /*
-        -webkit-box-shadow: 0px 0px 4px rgba(0,0,0,0.23);
-        -moz-box-shadow: 0px 0px 4px rgba(0,0,0,0.23);
-        box-shadow: 0px 0px 4px rgba(0,0,0,0.23);
-        */
-    }
+a:hover {
+    color: #003355;
+    border-bottom: 1px dotted;
+}
 
-    div.summary {
-        padding: 15px;
-        border:1px solid #CCC;
-        border-radius:10px;
-        -moz-border-radius:10px;
-        -webkit-box-shadow: 0px 0px 4px rgba(0,0,0,0.23);
-        -moz-box-shadow: 0px 0px 4px rgba(0,0,0,0.23);
-        box-shadow: 0px 0px 4px rgba(0,0,0,0.23);
-    }
+figure {
+    padding: 0px;
+    margin: 1em auto;
+    text-align: center;
+}
 
-    div.summary h2 {
-        padding: 0;
-        margin: 0;
-    }
+img {
+    max-width: 100%;
+    vertical-align: middle;
+}
 
-    .org-info-box {
-        clear:both;
-        margin-left:auto;
-        margin-right:auto;
-        padding:0.7em;
-    /* border:1px solid #CCC; */
-    /* border-radius:10px; */
-    /* -moz-border-radius:10px; */
-    }
-    .org-info-box img {
-        float:left;
-        margin:0em 0.5em 0em 0em;
-    }
-    .org-info-box p {
-        margin:0em;
-        padding:0em;
-    }
+.MathJax_Display {
+    margin: 0!important;
+    width: 90%!important;
+}
+
+h1,h2,h3,h4,h5,h6 {
+    color: #A5573E;
+    line-height: 1em;
+    font-family: "Iosevka", sans-serif;
+}
 
+h1,h2,h3 {
+    line-height: 1.4em;
+}
 
-    .builtin {
-        /* font-lock-builtin-face */
-        color: #f4a460;
-    }
-    .comment {
-        /* font-lock-comment-face */
-        color: #737373;
-    }
-    .comment-delimiter {
-        /* font-lock-comment-delimiter-face */
-        color: #666666;
-    }
-    .constant {
-        /* font-lock-constant-face */
-        color: #db7093;
-    }
-    .doc {
-        /* font-lock-doc-face */
-        color: #b3b3b3;
-    }
-    .function-name {
-        /* font-lock-function-name-face */
-        color: #5f9ea0;
-    }
-    .headline {
-        /* headline-face */
-        color: #ffffff;
-        background-color: #000000;
-        font-weight: bold;
-    }
-    .keyword {
-        /* font-lock-keyword-face */
-        color: #4682b4;
-    }
-    .negation-char {
-    }
-    .regexp-grouping-backslash {
-    }
-    .regexp-grouping-construct {
-    }
-    .string {
-        /* font-lock-string-face */
-        color: #ccc79a;
-    }
-    .todo-comment {
-        /* todo-comment-face */
-        color: #ffffff;
-        background-color: #000000;
-        font-weight: bold;
+h4,h5,h6 {
+    font-size: 1em;
+}
+
+@media screen and (min-width: 600px) {
+    h1 {
+        font-size: 2em;
     }
-    .variable-name {
-        /* font-lock-variable-name-face */
-        color: #ff6a6a;
+    h2 {
+        font-size: 1.5em;
     }
-    .warning {
-        /* font-lock-warning-face */
-        color: #ffffff;
-        background-color: #cd5c5c;
-        font-weight: bold;
+    h3 {
+        font-size: 1.3em;
     }
-    pre.a {
-        color: inherit;
-        background-color: inherit;
-        font: inherit;
-        text-decoration: inherit;
+    h1,h2,h3 {
+        line-height: 1.4em;
     }
-    pre.a:hover {
-        text-decoration: underline;
+    h4,h5,h6 {
+        font-size: 1.1em;
     }
+}
 
-    /* Styles for org-info.js */
+dt {
+    font-weight: bold;
+}
 
-    .org-info-js_info-navigation
-    {
-        border-style:none;
-    }
+/* table */
 
-    #org-info-js_console-label
-    {
-        font-size:10px;
-        font-weight:bold;
-        white-space:nowrap;
-    }
+table {
+    margin: 1em auto;
+    border-top: 2px solid;
+    border-bottom: 2px solid;
+    border-collapse: collapse;
+}
 
-    .org-info-js_search-highlight
-    {
-        background-color:#ffff00;
-        color:#000000;
-        font-weight:bold;
-    }
+thead {
+    border-bottom: 2px solid;
+}
 
-    #org-info-js-window
-    {
-        border-bottom:1px solid black;
-        padding-bottom:10px;
-        margin-bottom:10px;
-    }
+table td + td, table th + th {
+    border-left: 1px solid gray;
+}
 
+table tr {
+    border-top: 1px solid lightgray;
+}
 
+td,th {
+    padding: 0.3em 0.6em;
+    vertical-align: middle;
+}
 
-    .org-info-search-highlight
-    {
-        background-color:#adefef; /* same color as emacs default */
-        color:#000000;
-        font-weight:bold;
-    }
+caption.t-above {
+    caption-side: top;
+}
 
-    .org-bbdb-company {
-        /* bbdb-company */
-        font-style: italic;
-    }
-    .org-bbdb-field-name {
-    }
-    .org-bbdb-field-value {
-    }
-    .org-bbdb-name {
-        /* bbdb-name */
-        text-decoration: underline;
-    }
-    .org-bold {
-        /* bold */
-        font-weight: bold;
-    }
-    .org-bold-italic {
-        /* bold-italic */
-        font-weight: bold;
-        font-style: italic;
-    }
-    .org-border {
-        /* border */
-        background-color: #000000;
-    }
-    .org-buffer-menu-buffer {
-        /* buffer-menu-buffer */
-        font-weight: bold;
-    }
-    .org-builtin {
-        /* font-lock-builtin-face */
-        color: #da70d6;
-    }
-    .org-button {
-        /* button */
-        text-decoration: underline;
-    }
-    .org-c-nonbreakable-space {
-        /* c-nonbreakable-space-face */
-        background-color: #ff0000;
-        font-weight: bold;
-    }
-    .org-calendar-today {
-        /* calendar-today */
-        text-decoration: underline;
-    }
-    .org-comment {
-        /* font-lock-comment-face */
-        color: #b22222;
-    }
-    .org-comment-delimiter {
-        /* font-lock-comment-delimiter-face */
-        color: #b22222;
-    }
-    .org-constant {
-        /* font-lock-constant-face */
-        color: #5f9ea0;
-    }
-    .org-cursor {
-        /* cursor */
-        background-color: #000000;
-    }
-    .org-default {
-        /* default */
-        color: #000000;
-        background-color: #ffffff;
-    }
-    .org-diary {
-        /* diary */
-        color: #ff0000;
-    }
-    .org-doc {
-        /* font-lock-doc-face */
-        color: #bc8f8f;
-    }
-    .org-escape-glyph {
-        /* escape-glyph */
-        color: #a52a2a;
-    }
-    .org-file-name-shadow {
-        /* file-name-shadow */
-        color: #7f7f7f;
-    }
-    .org-fixed-pitch {
-    }
-    .org-fringe {
-        /* fringe */
-        background-color: #f2f2f2;
-    }
-    .org-function-name {
-        /* font-lock-function-name-face */
-        color: #0000ff;
-    }
-    .org-header-line {
-        /* header-line */
-        color: #333333;
-        background-color: #e5e5e5;
-    }
-    .org-help-argument-name {
-        /* help-argument-name */
-        font-style: italic;
-    }
-    .org-highlight {
-        /* highlight */
-        background-color: #b4eeb4;
-    }
-    .org-holiday {
-        /* holiday */
-        background-color: #ffc0cb;
-    }
-    .org-info-header-node {
-        /* info-header-node */
-        color: #a52a2a;
-        font-weight: bold;
-        font-style: italic;
-    }
-    .org-info-header-xref {
-        /* info-header-xref */
-        color: #0000ff;
-        text-decoration: underline;
-    }
-    .org-info-menu-header {
-        /* info-menu-header */
-        font-weight: bold;
-    }
-    .org-info-menu-star {
-        /* info-menu-star */
-        color: #ff0000;
-    }
-    .org-info-node {
-        /* info-node */
-        color: #a52a2a;
-        font-weight: bold;
-        font-style: italic;
-    }
-    .org-info-title-1 {
-        /* info-title-1 */
-        font-size: 172%;
-        font-weight: bold;
-    }
-    .org-info-title-2 {
-        /* info-title-2 */
-        font-size: 144%;
-        font-weight: bold;
-    }
-    .org-info-title-3 {
-        /* info-title-3 */
-        font-size: 120%;
-        font-weight: bold;
-    }
-    .org-info-title-4 {
-        /* info-title-4 */
-        font-weight: bold;
-    }
-    .org-info-xref {
-        /* info-xref */
-        color: #0000ff;
-        text-decoration: underline;
-    }
-    .org-isearch {
-        /* isearch */
-        color: #b0e2ff;
-        background-color: #cd00cd;
-    }
-    .org-italic {
-        /* italic */
-        font-style: italic;
-    }
-    .org-keyword {
-        /* font-lock-keyword-face */
-        color: #a020f0;
-    }
-    .org-lazy-highlight {
-        /* lazy-highlight */
-        background-color: #afeeee;
-    }
-    .org-link {
-        /* link */
-        color: #0000ff;
-        text-decoration: underline;
-    }
-    .org-link-visited {
-        /* link-visited */
-        color: #8b008b;
-        text-decoration: underline;
-    }
-    .org-match {
-        /* match */
-        background-color: #ffff00;
-    }
-    .org-menu {
-    }
-    .org-message-cited-text {
-        /* message-cited-text */
-        color: #ff0000;
-    }
-    .org-message-header-cc {
-        /* message-header-cc */
-        color: #191970;
-    }
-    .org-message-header-name {
-        /* message-header-name */
-        color: #6495ed;
-    }
-    .org-message-header-newsgroups {
-        /* message-header-newsgroups */
-        color: #00008b;
-        font-weight: bold;
-        font-style: italic;
-    }
-    .org-message-header-other {
-        /* message-header-other */
-        color: #4682b4;
-    }
-    .org-message-header-subject {
-        /* message-header-subject */
-        color: #000080;
-        font-weight: bold;
-    }
-    .org-message-header-to {
-        /* message-header-to */
-        color: #191970;
-        font-weight: bold;
-    }
-    .org-message-header-xheader {
-        /* message-header-xheader */
-        color: #0000ff;
-    }
-    .org-message-mml {
-        /* message-mml */
-        color: #228b22;
-    }
-    .org-message-separator {
-        /* message-separator */
-        color: #a52a2a;
-    }
-    .org-minibuffer-prompt {
-        /* minibuffer-prompt */
-        color: #0000cd;
-    }
-    .org-mm-uu-extract {
-        /* mm-uu-extract */
-        color: #006400;
-        background-color: #ffffe0;
-    }
-    .org-mode-line {
-        /* mode-line */
-        color: #000000;
-        background-color: #bfbfbf;
-    }
-    .org-mode-line-buffer-id {
-        /* mode-line-buffer-id */
-        font-weight: bold;
-    }
-    .org-mode-line-highlight {
-    }
-    .org-mode-line-inactive {
-        /* mode-line-inactive */
-        color: #333333;
-        background-color: #e5e5e5;
-    }
-    .org-mouse {
-        /* mouse */
-        background-color: #000000;
-    }
-    .org-negation-char {
-    }
-    .org-next-error {
-        /* next-error */
-        background-color: #eedc82;
-    }
-    .org-nobreak-space {
-        /* nobreak-space */
-        color: #a52a2a;
-        text-decoration: underline;
-    }
-    .org-org-agenda-date {
-        /* org-agenda-date */
-        color: #0000ff;
-    }
-    .org-org-agenda-date-weekend {
-        /* org-agenda-date-weekend */
-        color: #0000ff;
-        font-weight: bold;
-    }
-    .org-org-agenda-restriction-lock {
-        /* org-agenda-restriction-lock */
-        background-color: #ffff00;
-    }
-    .org-org-agenda-structure {
-        /* org-agenda-structure */
-        color: #0000ff;
-    }
-    .org-org-archived {
-        /* org-archived */
-        color: #7f7f7f;
-    }
-    .org-org-code {
-        /* org-code */
-        color: #7f7f7f;
-    }
-    .org-org-column {
-        /* org-column */
-        background-color: #e5e5e5;
-    }
-    .org-org-column-title {
-        /* org-column-title */
-        background-color: #e5e5e5;
-        font-weight: bold;
-        text-decoration: underline;
-    }
-    .org-org-date {
-        /* org-date */
-        color: #a020f0;
-        text-decoration: underline;
-    }
-    .org-org-done {
-        /* org-done */
-        color: #228b22;
-        font-weight: bold;
-    }
-    .org-org-drawer {
-        /* org-drawer */
-        color: #0000ff;
-    }
-    .org-org-ellipsis {
-        /* org-ellipsis */
-        color: #b8860b;
-        text-decoration: underline;
-    }
-    .org-org-formula {
-        /* org-formula */
-        color: #b22222;
-    }
-    .org-org-headline-done {
-        /* org-headline-done */
-        color: #bc8f8f;
-    }
-    .org-org-hide {
-        /* org-hide */
-        color: #e5e5e5;
-    }
-    .org-org-latex-and-export-specials {
-        /* org-latex-and-export-specials */
-        color: #8b4513;
-    }
-    .org-org-level-1 {
-        /* org-level-1 */
-        color: #0000ff;
-    }
-    .org-org-level-2 {
-        /* org-level-2 */
-        color: #b8860b;
-    }
-    .org-org-level-3 {
-        /* org-level-3 */
-        color: #a020f0;
-    }
-    .org-org-level-4 {
-        /* org-level-4 */
-        color: #b22222;
-    }
-    .org-org-level-5 {
-        /* org-level-5 */
-        color: #228b22;
-    }
-    .org-org-level-6 {
-        /* org-level-6 */
-        color: #5f9ea0;
-    }
-    .org-org-level-7 {
-        /* org-level-7 */
-        color: #da70d6;
-    }
-    .org-org-level-8 {
-        /* org-level-8 */
-        color: #bc8f8f;
-    }
-    .org-org-link {
-        /* org-link */
-        color: #a020f0;
-        text-decoration: underline;
-    }
-    .org-org-property-value {
-    }
-    .org-org-scheduled-previously {
-        /* org-scheduled-previously */
-        color: #b22222;
-    }
-    .org-org-scheduled-today {
-        /* org-scheduled-today */
-        color: #006400;
-    }
-    .org-org-sexp-date {
-        /* org-sexp-date */
-        color: #a020f0;
-    }
-    .org-org-special-keyword {
-        /* org-special-keyword */
-        color: #bc8f8f;
-    }
-    .org-org-table {
-        /* org-table */
-        color: #0000ff;
-    }
-    .org-org-tag {
-        /* org-tag */
-        font-weight: bold;
-    }
-    .org-org-target {
-        /* org-target */
-        text-decoration: underline;
-    }
-    .org-org-time-grid {
-        /* org-time-grid */
-        color: #b8860b;
-    }
-    .org-org-todo {
-        /* org-todo */
-        color: #ff0000;
-    }
-    .org-org-upcoming-deadline {
-        /* org-upcoming-deadline */
-        color: #b22222;
-    }
-    .org-org-verbatim {
-        /* org-verbatim */
-        color: #7f7f7f;
-        text-decoration: underline;
-    }
-    .org-org-warning {
-        /* org-warning */
-        color: #ff0000;
-        font-weight: bold;
-    }
-    .org-outline-1 {
-        /* outline-1 */
-        color: #0000ff;
-    }
-    .org-outline-2 {
-        /* outline-2 */
-        color: #b8860b;
-    }
-    .org-outline-3 {
-        /* outline-3 */
-        color: #a020f0;
-    }
-    .org-outline-4 {
-        /* outline-4 */
-        color: #b22222;
-    }
-    .org-outline-5 {
-        /* outline-5 */
-        color: #228b22;
-    }
-    .org-outline-6 {
-        /* outline-6 */
-        color: #5f9ea0;
-    }
-    .org-outline-7 {
-        /* outline-7 */
-        color: #da70d6;
-    }
-    .org-outline-8 {
-        /* outline-8 */
-        color: #bc8f8f;
-    }
-    .outline-text-1, .outline-text-2, .outline-text-3, .outline-text-4, .outline-text-5, .outline-text-6 {
-    /* Add more spacing between section. Padding, so that folding with org-info.js works as expected. */
+caption.t-bottom {
+    caption-side: bottom;
+}
 
-    }
+caption {
+    margin-bottom: 0.3em;
+}
 
-    .org-preprocessor {
-        /* font-lock-preprocessor-face */
-        color: #da70d6;
-    }
-    .org-query-replace {
-        /* query-replace */
-        color: #b0e2ff;
-        background-color: #cd00cd;
-    }
-    .org-regexp-grouping-backslash {
-        /* font-lock-regexp-grouping-backslash */
-        font-weight: bold;
-    }
-    .org-regexp-grouping-construct {
-        /* font-lock-regexp-grouping-construct */
-        font-weight: bold;
-    }
-    .org-region {
-        /* region */
-        background-color: #eedc82;
-    }
-    .org-rmail-highlight {
-    }
-    .org-scroll-bar {
-        /* scroll-bar */
-        background-color: #bfbfbf;
-    }
-    .org-secondary-selection {
-        /* secondary-selection */
-        background-color: #ffff00;
-    }
-    .org-shadow {
-        /* shadow */
-        color: #7f7f7f;
-    }
-    .org-show-paren-match {
-        /* show-paren-match */
-        background-color: #40e0d0;
-    }
-    .org-show-paren-mismatch {
-        /* show-paren-mismatch */
-        color: #ffffff;
-        background-color: #a020f0;
-    }
-    .org-string {
-        /* font-lock-string-face */
-        color: #bc8f8f;
-    }
-    .org-texinfo-heading {
-        /* texinfo-heading */
-        color: #0000ff;
-    }
-    .org-tool-bar {
-        /* tool-bar */
-        color: #000000;
-        background-color: #bfbfbf;
-    }
-    .org-tooltip {
-        /* tooltip */
-        color: #000000;
-        background-color: #ffffe0;
-    }
-    .org-trailing-whitespace {
-        /* trailing-whitespace */
-        background-color: #ff0000;
-    }
-    .org-type {
-        /* font-lock-type-face */
-        color: #228b22;
-    }
-    .org-underline {
-        /* underline */
-        text-decoration: underline;
-    }
-    .org-variable-name {
-        /* font-lock-variable-name-face */
-        color: #b8860b;
-    }
-    .org-variable-pitch {
-    }
-    .org-vertical-border {
-    }
-    .org-warning {
-        /* font-lock-warning-face */
-        color: #ff0000;
-        font-weight: bold;
-    }
-    .rss_box {
-    }
-    .rss_title, rss_title a {
-    }
-    .rss_items {
-    }
-    .rss_item a:link, .rss_item a:visited, .rss_item a:active {
-    }
-    .rss_item a:hover {
-    }
-    .rss_date {
-    }
+figcaption {
+    margin-top: 0.3em;
+}
 
-    #postamble {
-        padding: .3em;
-        margin-bottom: 1em;
-        border: 1px solid gray;
-        background-color: #eeeeee;
-    }
+th.org-right {
+    text-align: center;
+}
 
-    #show_source {
-        float: right; 
-        margin: .7em;
-    }
-    
+th.org-left {
+    text-align: center;
+}
+
+th.org-center {
+    text-align: center;
+}
+
+td.org-right {
+    text-align: right;
+}
 
-} /* END OF @media all */
+td.org-left {
+    text-align: left;
+}
 
+td.org-center {
+    text-align: center;
+}
 
+blockquote {
+    margin: 1em 2em;
+    padding-left: 1em;
+    border-left: 3px solid #ccc;
+}
 
-@media screen
-{
-  #table-of-contents {
-    float: right;
-    padding-right: 5px;
-    border: 1px solid #CCC;
-    max-width: 50%;
-    overflow: auto;
-  }
-} /* END OF @media screen */
+kbd {
+    background-color: #f7f7f7;
+    font-size: 80%;
+    margin: 0 .1em;
+    padding: .1em .6em;
+}
+
+.todo {
+    background-color: red;
+    color: white;
+    padding: .1em 0.3em;
+    border-radius: 3px;
+    background-clip: padding-box;
+    font-size: 80%;
+    font-family: "Iosevka", monospace;
+    line-height: 1;
+}
 
-.due {
+.done {
+    background-color: green;
+    color: white;
+    padding: .1em 0.3em;
+    border-radius: 3px;
+    background-clip: padding-box;
     font-size: 80%;
-    margin: 0 1em 0 1em;
+    font-family: "Iosevka", monospace;
+    line-height: 1;
+}
+
+.priority {
+    color: orange;
+    font-family: "Iosevka", monospace;
+}
+
+/* Because tag span is set to float.  This is more like a hacking.  Maybe we
+   need a cleaner solution. */
+#table-of-contents li {
+    clear: both;
+}
+
+.tag {
+    font-family: "Iosevka", monospace;
+    font-size: 0.7em;
+    font-weight: normal;
+}
+
+.tag span {
+    padding: 0.3em 0.3em;
+    float: right;
+    margin-right: .5em;
+    border: 1px solid #bbb;
+    border-radius: 3px;
+    background-clip: padding-box;
+    color: #333;
+    background-color: #eee;
+    line-height: 1;
+}
+
+.timestamp {
+    color: #bebebe;
+    font-size: 90%;
 }
 
-#contact-front p {
+.timestamp-kwd {
+    color: #5f9ea0;
+}
+
+.org-right {
+    margin-left: auto;
+    margin-right: 0px;
+    text-align: right;
+}
+
+.org-left {
+    margin-left: 0px;
+    margin-right: auto;
     text-align: left;
 }
 
-ul.index-links {
-    padding-left: 0;
-    margin-left: 0;
+.org-center {
+    margin-left: auto;
+    margin-right: auto;
+    text-align: center;
 }
 
-ul.index-links li {
-    list-style-type: none;
-    margin-left: 0;
+.underline {
+    text-decoration: underline;
+}
+
+#postamble p, #preamble p {
+    font-size: 90%;
+    margin: .2em;
+}
+
+p.verse {
+    margin-left: 3%;
 }
 
-div#preamble div#plupperButton a img {
-    height: 16px;
+:not(pre) > code {
+    padding: 2px 5px;
+    margin: auto 1px;
+    border: 1px solid #DDD;
+    border-radius: 3px;
+    background-clip: padding-box;
+    color: #333;
+    font-size: 80%;
+}
+
+.org-src-container {
+    border: 1px solid #ccc;
+    box-shadow: 3px 3px 3px #eee;
+    font-family: "Iosevka", monospace;
+    font-size: 80%;
+    margin: 1em auto;
+    padding: 0.1em 0.5em;
+    position: relative;
+}
+
+.org-src-container>pre {
+    overflow: auto;
+}
+
+.org-src-container>pre:before {
+    display: block;
     position: absolute;
-    top: 4px;
+    background-color: #b3b3b3;
+    top: 0;
+    right: 0;
+    padding: 0 0.5em;
+    border-bottom-left-radius: 8px;
+    border: 0;
+    color: white;
+    font-size: 80%;
 }
 
-blockquote {
-    background: #fbfbfb;
+/* from http://demo.thi.ng/org-spec/ */
+
+.org-src-container>pre.src-sh:before {
+    content: 'sh';
+}
+.org-src-container>pre.src-bash:before {
+    content: 'bash';
+}
+.org-src-container>pre.src-emacs-lisp:before {
+    content: 'Emacs Lisp';
+}
+.org-src-container>pre.src-R:before {
+    content: 'R';
+}
+.org-src-container>pre.src-org:before {
+    content: 'Org';
+}
+.org-src-container>pre.src-cpp:before {
+    content: 'C++';
+}
+.org-src-container>pre.src-c:before {
+    content: 'C';
+}
+.org-src-container>pre.src-html:before {
+    content: 'HTML'
+}
+.org-src-container>pre.src-js:before {
+    content: 'Javascript'
+}
+.org-src-container>pre.src-javascript:before {
+    content: 'Javascript'
+}
+
+// More languages from http://orgmode.org/worg/org-contrib/babel/languages.html
+
+.org-src-container>pre.src-abc:before {
+    content: 'ABC';
+}
+.org-src-container>pre.src-asymptote:before {
+    content: 'Asymptote';
+}
+.org-src-container>pre.src-awk:before {
+    content: 'Awk';
+}
+.org-src-container>pre.src-C:before {
+    content: 'C';
+}
+.org-src-container>pre.src-calc:before {
+    content: 'Calc';
+}
+.org-src-container>pre.src-clojure:before {
+    content: 'Clojure';
+}
+.org-src-container>pre.src-comint:before {
+    content: 'comint';
+}
+.org-src-container>pre.src-css:before {
+    content: 'CSS';
+}
+.org-src-container>pre.src-D:before {
+    content: 'D';
+}
+.org-src-container>pre.src-ditaa:before {
+    content: 'Ditaa';
+}
+.org-src-container>pre.src-dot:before {
+    content: 'Dot';
+}
+.org-src-container>pre.src-ebnf:before {
+    content: 'ebnf';
+}
+.org-src-container>pre.src-forth:before {
+    content: 'Forth';
+}
+.org-src-container>pre.src-F90:before {
+    content: 'Fortran';
+}
+.org-src-container>pre.src-gnuplot:before {
+    content: 'Gnuplot';
+}
+.org-src-container>pre.src-haskell:before {
+    content: 'Haskell';
+}
+.org-src-container>pre.src-io:before {
+    content: 'Io';
+}
+.org-src-container>pre.src-java:before {
+    content: 'Java';
+}
+.org-src-container>pre.src-latex:before {
+    content: 'LaTeX';
+}
+.org-src-container>pre.src-ledger:before {
+    content: 'Ledger';
+}
+.org-src-container>pre.src-ly:before {
+    content: 'Lilypond';
+}
+.org-src-container>pre.src-lisp:before {
+    content: 'Lisp';
+}
+.org-src-container>pre.src-makefile:before {
+    content: 'Make';
+}
+.org-src-container>pre.src-matlab:before {
+    content: 'Matlab';
+}
+.org-src-container>pre.src-max:before {
+    content: 'Maxima';
+}
+.org-src-container>pre.src-mscgen:before {
+    content: 'Mscgen';
+}
+.org-src-container>pre.src-Caml:before {
+    content: 'Objective';
+}
+.org-src-container>pre.src-octave:before {
+    content: 'Octave';
+}
+.org-src-container>pre.src-org:before {
+    content: 'Org';
+}
+.org-src-container>pre.src-perl:before {
+    content: 'Perl';
+}
+.org-src-container>pre.src-picolisp:before {
+    content: 'Picolisp';
+}
+.org-src-container>pre.src-plantuml:before {
+    content: 'PlantUML';
+}
+.org-src-container>pre.src-python:before {
+    content: 'Python';
+}
+.org-src-container>pre.src-ruby:before {
+    content: 'Ruby';
+}
+.org-src-container>pre.src-sass:before {
+    content: 'Sass';
+}
+.org-src-container>pre.src-scala:before {
+    content: 'Scala';
+}
+.org-src-container>pre.src-scheme:before {
+    content: 'Scheme';
+}
+.org-src-container>pre.src-screen:before {
+    content: 'Screen';
+}
+.org-src-container>pre.src-sed:before {
+    content: 'Sed';
+}
+.org-src-container>pre.src-shell:before {
+    content: 'shell';
+}
+.org-src-container>pre.src-shen:before {
+    content: 'Shen';
+}
+.org-src-container>pre.src-sql:before {
+    content: 'SQL';
+}
+.org-src-container>pre.src-sqlite:before {
+    content: 'SQLite';
+}
+.org-src-container>pre.src-stan:before {
+    content: 'Stan';
+}
+.org-src-container>pre.src-vala:before {
+    content: 'Vala';
+}
+.org-src-container>pre.src-axiom:before {
+    content: 'Axiom';
+}
+.org-src-container>pre.src-browser:before {
+    content: 'HTML';
+}
+.org-src-container>pre.src-cypher:before {
+    content: 'Neo4j';
+}
+.org-src-container>pre.src-elixir:before {
+    content: 'Elixir';
+}
+.org-src-container>pre.src-request:before {
+    content: 'http';
+}
+.org-src-container>pre.src-ipython:before {
+    content: 'iPython';
+}
+.org-src-container>pre.src-kotlin:before {
+    content: 'Kotlin';
+}
+.org-src-container>pre.src-Flavored Erlang  lfe:before {
+    content: 'Lisp';
+}
+.org-src-container>pre.src-mongo:before {
+    content: 'MongoDB';
+}
+.org-src-container>pre.src-prolog:before {
+    content: 'Prolog';
+}
+.org-src-container>pre.src-rec:before {
+    content: 'rec';
+}
+.org-src-container>pre.src-ML  sml:before {
+    content: 'Standard';
+}
+.org-src-container>pre.src-Translate  translate:before {
+    content: 'Google';
+}
+.org-src-container>pre.src-typescript:before {
+    content: 'Typescript';
+}
+.org-src-container>pre.src-rust:before {
+    content: 'Rust';
+}
+
+.inlinetask {
+    background: #ffffcc;
+    border: 2px solid gray;
+    margin: 10px;
     padding: 10px;
-    border-radius: 10px;
-    -moz-border-radius: 10px;
 }
 
-.figure img {
-    background: white;
-    padding: 5px;
-    -moz-box-shadow: 0px 0px 5px #c7c7c7;
-    -webkit-box-shadow: 0px 0px 5px #c7c7c7;
-    box-shadow: 0px 0px 5px #c7c7c7;
+#org-div-home-and-up {
+    font-size: 70%;
+    text-align: right;
+    white-space: nowrap;
 }
 
-div.hidden > strong {
-    margin-left: 0;
-    cursor: pointer;
-    color: #aaa;
+.linenr {
+    font-size: 90%;
 }
 
-div.hidden > strong > small {
-    margin-left: 1em;
+.code-highlighted {
+    background-color: #ffff00;
+}
+
+#bibliography {
     font-size: 90%;
-    font-weight: normal;
-    font-style: italic;
 }
 
-div.hidden div.hidden-content {
-    padding-left: 10px;
-    margin-bottom: 4em;
-    border-left: 3px solid #999;
+#bibliography table {
+    width: 100%;
 }
 
-div.hidden {
-    margin-bottom: 1em;
-    margin-left: 2em;
+.creator {
+    display: block;
+
+}
+
+@media screen and (min-width: 600px) {
+    .creator {
+        display: inline;
+        float: right;
+    }
 }
diff --git a/docs/documentation.org b/docs/documentation.org
new file mode 100644
index 0000000..09c3ffe
--- /dev/null
+++ b/docs/documentation.org
@@ -0,0 +1,70 @@
+#+SETUPFILE: publish.setup
+#+TITLE: Vericert Documentation
+
+* Building
+
+To build Vericert, the provided Makefile can be used. External dependencies are needed to build the project, which can be pulled in automatically with [[https://nixos.org/nix/][nix]] using the provided ~default.nix~ and ~shell.nix~ files.
+
+The project is written in Coq, a theorem prover, which is extracted to OCaml so that it can then be compiled and executed. The dependencies of this project are the following:
+
+- [[https://coq.inria.fr/][Coq]]: theorem prover that is used to also program the HLS tool.
+- [[https://ocaml.org/][OCaml]]: the OCaml compiler to compile the extracted files.
+- [[https://github.com/mit-plv/bbv][bbv]]: an efficient bit vector library.
+- [[https://github.com/ocaml/dune][dune]]: build tool for ocaml projects to gather all the ocaml files and compile them in the right order.
+- [[http://gallium.inria.fr/~fpottier/menhir/][menhir]]: parser generator for ocaml.
+- [[https://github.com/ocaml/ocamlfind][findlib]] to find installed OCaml libraries.
+- [[https://gcc.gnu.org/][GCC]]: compiler to help build CompCert.
+
+These dependencies can be installed manually, or automatically through Nix.
+
+** Downloading CompCert
+
+CompCert is added as a submodule in the ~lib/CompCert~ directory. It is needed to run the build process below, as it is the one dependency that is not downloaded by nix, and has to be downloaded together with the repository. To clone CompCert together with this project, you can run:
+
+#+begin_src shell
+git clone --recursive https://github.com/ymherklotz/vericert
+#+end_src
+
+If the repository is already cloned, you can run the following command to make sure that CompCert is also downloaded:
+
+#+begin_src shell
+git submodule update --init
+#+end_src
+
+** Setting up Nix
+
+Nix is a package manager that can create an isolated environment so that the builds are reproducible. Once nix is installed, it can be used in the following way.
+
+To open a shell which includes all the necessary dependencies, one can use:
+
+#+begin_src shell
+nix-shell
+#+end_src
+
+which will open a shell that has all the dependencies loaded.
+
+** Makefile build
+
+If the dependencies were installed manually, or if one is in the ~nix-shell~, the project can be built by running:
+
+#+begin_src shell
+make -j8
+#+end_src
+
+and installed locally, or under the ~PREFIX~ location using:
+
+#+begin_src shell
+make install
+#+end_src
+
+Which will install the binary in ~./bin/vericert~ by default. However, this can be changed by changing the ~PREFIX~ environment variable, in which case the binary will be installed in ~$PREFIX/bin/vericert~.
+
+** Running
+
+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
diff --git a/docs/index.org b/docs/index.org
index 6ec0130..7a92650 100644
--- a/docs/index.org
+++ b/docs/index.org
@@ -1,5 +1,5 @@
-#+SETUPFILE: setup.org
-#+TITLE: VeriCert
+#+SETUPFILE: publish.setup
+#+TITLE: Vericert
 
 A formally verified high-level synthesis (HLS) tool written in Coq, building on top of [[https://github.com/AbsInt/CompCert][CompCert]].  This ensures the correctness of the C to Verilog translation according to our Verilog semantics and CompCert's C semantics, removing the need to check the resulting hardware for behavioural correctness.
 
@@ -14,5 +14,5 @@ The project is currently a work in progress, so proofs remain to be finished.  C
 
 * Content
 
-- [[./docs/toc.html][Vericert Coq Documentation]]
-- [[./building.org][Building Vericert]]
+- [[./proof/toc.html][Vericert Proof]]
+- [[./documentation.org][Vericert Documentation]]
diff --git a/docs/publish.el b/docs/publish.el
index e7a27d7..df7235d 100644
--- a/docs/publish.el
+++ b/docs/publish.el
@@ -1,14 +1,89 @@
 ;; Publishing projects, this one is for the zettelkasten
+(require 'package)
+(package-initialize)
+(add-to-list 'package-archives '("org" . "https://orgmode.org/elpa/") t)
+(add-to-list 'package-archives '("melpa" . "https://melpa.org/packages/") t)
+(package-refresh-contents)
+(package-install 'org-plus-contrib)
+(package-install 'htmlize)
+
 (require 'org)
+(require 'ox-publish)
+
+(defvar vericert/header "")
+(defvar vericert/site-attachments nil)
+(defvar vericert/base "")
+
+(setq vericert/base "/vericert")
+
+(setq vericert/header (concat "<div id=\"left-bar\">
+<header id=\"header\" class=\"status\">
+<div class=\"logo\"><a href=\"" vericert/base "\">Vericert</a></div>
+<nav id=\"navbar\">
+<span><a href=\"" vericert/base "/documentation.html\">Documentation</a></span>
+<span><a href=\"" vericert/base "/proof/toc.html\">Proof</a></span>
+</nav>
+<p>Vericert is the first formally verified high-level synthesis tool.</p>
+</header>
+<div id=\"toc\"></div>
+</div>"))
+
+(setq vericert/site-attachments
+  (regexp-opt '("jpg" "jpeg" "gif" "png" "svg"
+                "ico" "cur" "css" "js" "woff" "html" "pdf")))
+
+(setq user-full-name nil)
+
+(setq org-export-with-smart-quotes t
+      org-export-with-section-numbers t
+      org-export-with-toc t)
+
+(setq org-html-divs '((preamble "header" "header")
+                      (content "main" "content")
+                      (postamble "footer" "postamble"))
+      org-html-container-element "section"
+      org-html-metadata-timestamp-format "%Y-%m-%d"
+      org-html-checkbox-type 'html
+      org-html-html5-fancy t
+      org-html-validation-link nil
+      org-html-doctype "html5"
+      org-html-coding-system 'utf-8-unix
+      org-html-head-include-default-style nil
+      org-html-head-include-scripts nil)
+
 (setq org-publish-project-alist
-      '(("orgfiles"
-         :base-directory "./"
-         :base-extension "org"
-         :publishing-directory "./html/"
-         :publishing-function org-html-publish-to-html)
-        ("assets"
-         :base-directory "./css/"
-         :base-extension "css"
-         :publishing-directory "./html/css/"
-         :publishing-function org-publish-attachment)
-        ("documentation" :components ("orgfiles" "assets"))))
+      (list
+       (list "vericert-org"
+             :base-directory "./"
+             :base-extension "org"
+             :exclude (regexp-opt '("README" "draft"))
+             :html-head-extra
+             (concat "<script src=\"https://cdnjs.cloudflare.com/ajax/libs/tocbot/4.11.1/tocbot.min.js\"></script>
+<link rel=\"stylesheet\" href=\"https://cdnjs.cloudflare.com/ajax/libs/tocbot/4.11.1/tocbot.css\">
+<link rel=\"stylesheet\" href=\"" vericert/base "/css/org.css\" type=\"text/css\" media=\"screen\" />")
+             :html-preamble t
+             :html-preamble-format (list (list "en" vericert/header))
+             :html-postamble t
+             :html-postamble-format '(("en" "<script>tocbot.init({
+  tocSelector: '#toc',
+  contentSelector: '#content',
+  headingSelector: 'h2, h3',
+  hasInnerContainers: true,
+});</script>"))
+             :publishing-directory "./html"
+             :publishing-function 'org-html-publish-to-html
+             :recursive t)
+       (list "vericert-assets"
+             :base-directory "."
+             :base-extension vericert/site-attachments
+             :include '(".nojekyll")
+             :exclude "html/"
+             :publishing-directory "./html"
+             :publishing-function 'org-publish-attachment
+             :recursive t)
+       (list "vericert" :components '("vericert-org" "vericert-assets"))))
+
+(defun publish-vericert-docs ()
+  "Publish Vericert documentation."
+  (interactive)
+  (org-publish "vericert" t))
diff --git a/docs/publish.setup b/docs/publish.setup
new file mode 100644
index 0000000..a3e7255
--- /dev/null
+++ b/docs/publish.setup
@@ -0,0 +1,2 @@
+#+MACRO: begin-summary #+HTML: <div class="summary"><h2>Summary</h2>
+#+MACRO: end-summary #+HTML: </div>
diff --git a/docs/setup.org b/docs/setup.org
deleted file mode 100644
index 969fdf9..0000000
--- a/docs/setup.org
+++ /dev/null
@@ -1,7 +0,0 @@
-#+HTML_HEAD: <link rel="stylesheet" href="css/org.css" type="text/css" media="screen" />
-
-#+MACRO: begin-summary #+HTML: <div class="summary"><h2>Summary</h2>
-#+MACRO: end-summary #+HTML: </div>
-
-#+MACRO: begin-hidden #+HTML: <div class="hidden"><strong>$1 <small>click to toggle</small></strong><div class="hidden-content">
-#+MACRO: end-hidden #+HTML: </div></div>
diff --git a/scripts/download_artifact.sh b/scripts/download_artifact.sh
index 5ba8b4d..cac69f6 100755
--- a/scripts/download_artifact.sh
+++ b/scripts/download_artifact.sh
@@ -1,8 +1,8 @@
 #!/bin/sh
 
-mkdir -p docs/html/docs
-cd docs/html/docs
-curl -v -L -H "Accept: application/vnd.github.v3+json" -H "Authorization: token $GITHUB_TOKEN" https://api.github.com/repos/ymherklotz/vericert/actions/artifacts/14069960/zip -o html-documentation.zip
+mkdir -p docs/html/proof
+cd docs/html/proof
+curl -v -L -H "Accept: application/vnd.github.v3+json" -H "Authorization: token $GITHUB_TOKEN" https://api.github.com/repos/ymherklotz/vericert/actions/artifacts/26286264/zip -o html-documentation.zip
 unzip html-documentation.zip
 rm html-documentation.zip
 cp ../../css/coqdoc.css .
-- 
cgit