Add to documentation

5 files changed, 68 insertions, 29 deletions

diff --git a/doc/Makefile b/doc/Makefile
index 5662645..8a34845 100644
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -9,7 +9,7 @@ SOURCEDIR         = .
 BUILDDIR          = _build
 SOURCE_DATE_EPOCH = $(shell git log -1 --format=%ct)
 
-VS_DOCS := ../src/Compiler.v ../src/hls/RTLBlockInstr.v
+VS_DOCS := Compiler.v hls/RTLBlockInstr.v hls/RTLBlockgen.v hls/RTLBlockgenproof.v
 
 # Put it first so that "make" without argument is like "make help".
 help:
@@ -20,5 +20,5 @@ help:
 # Catch-all target: route all unknown targets to Sphinx using the new
 # "make mode" option.  $(O) is meant as a shortcut for $(SPHINXOPTS).
 %: Makefile
-	$(foreach d,$(VS_DOCS),cp $(d) $(patsubst ../%,%,$(d));)
+	$(foreach d,$(VS_DOCS),cp ../src/$(d) src/$(d);)
 	@$(SPHINXBUILD) -M $@ "$(SOURCEDIR)" "$(BUILDDIR)" $(SPHINXOPTS) $(O)
diff --git a/doc/_static/css/custom.css b/doc/_static/css/custom.css
index 66a1e35..e899c8f 100644
--- a/doc/_static/css/custom.css
+++ b/doc/_static/css/custom.css
@@ -3,9 +3,29 @@
 .alectryon-coqdoc .doc .inlinecode,
 .alectryon-mref,
 .alectryon-block, .alectryon-io,
-.alectryon-toggle-label, .alectryon-banner, pre, tt, code {
+.alectryon-toggle-label, .alectryon-banner, pre, tt, code,
+.rst-content kbd, .rst-content pre, .rst-content samp,
+.rst-content .linenodiv pre, .rst-content div[class^="highlight"] pre, .rst-content pre.literal-block {
     font-family: 'Iosevka Fixed Slab', 'Iosevka Slab Web', 'Iosevka Web', 'Iosevka Slab',
                  'Iosevka', 'Fira Code', monospace;
     font-feature-settings: "COQX" 1 /* Coq ligatures */, "XV00" 1 /* Legacy */, "calt" 1 /* Fallback */;
     line-height: initial;
+    font-size: 0.9em;
+}
+
+img { width: 100%; }
+a { color: #469369; }
+a:hover { color: #60b386; }
+
+.wy-menu-vertical header, .wy-menu-vertical p.caption {
+    color:  #fff5db;
+}
+
+.wy-nav-content, .wy-menu-vertical li.current > a, .wy-menu-vertical li.on a {
+    background-color: #fffbf2;
+    color: #2a3e40;
+}
+
+.wy-side-nav-search .wy-dropdown > a, .wy-side-nav-search > a {
+    color: #2a3e40;
 }
diff --git a/doc/conf.py b/doc/conf.py
index c7a9970..7000f7b 100644
--- a/doc/conf.py
+++ b/doc/conf.py
@@ -48,25 +48,12 @@ pygments_style = "emacs"
 # The theme to use for HTML and HTML Help pages.  See the documentation for
 # a list of builtin themes.
 #
-html_theme = 'alabaster'
+html_theme = 'sphinx_rtd_theme'
 
-html_theme_options = {
-    'logo': 'images/vericert-main.svg',
-    'github_user': 'ymherklotz',
-    'github_repo': 'vericert',
-    'description': 'A formally verified high-level synthesis tool written in Coq.',
-    'github_button': False,
-    'show_powered_by': False,
-}
+html_logo = "_static/images/vericert-main.svg"
 
-html_sidebars = {
-    '**': [
-        'about.html',
-        'searchbox.html',
-        'navigation.html',
-        'relations.html',
-        'donate.html',
-    ]
+html_theme_options = {
+    'style_nav_header_background': '#fff5db'
 }
 
 # Add any paths that contain custom static files (such as style sheets) here,
diff --git a/doc/index.rst b/doc/index.rst
index ebb99df..06aa509 100644
--- a/doc/index.rst
+++ b/doc/index.rst
@@ -6,21 +6,57 @@
 Vericert's Documentation
 ========================
 
+A formally verified high-level synthesis (HLS) tool written in Coq, building on top of `CompCert
+<https://github.com/AbsInt/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.
+
+Features
+--------
+
+The project is currently a work in progress.  Currently, the following C features are supported and
+have all been proven correct, providing a verified translation from C to Verilog:
+
+- all int operations,
+- non-recursive function calls,
+- local arrays and pointers, and
+- control-flow structures such as if-statements, for-loops, etc...
+
 .. toctree::
    :maxdepth: 2
-   :caption: Content:
+   :caption: Content
 
    vericert
 
 .. toctree::
    :maxdepth: 1
-   :caption: Sources:
+   :caption: Sources
 
    src/Compiler
    src/hls/RTLBlockInstr
+   src/hls/RTLBlockgen
+   src/hls/RTLBlockgenproof
+
+Publications
+------------
+
+:OOPSLA '21: Yann Herklotz, James D. Pollard, Nadesh Ramanathan, and John Wickerson. Formal
+             Verification of High-Level Synthesis. In *Proc. ACM Program. Lang.* 5, OOPSLA, 2021.
+
+:LATTE '21: Yann Herklotz and John Wickerson. High-level synthesis tools should be proven
+            correct. In *Workshop on Languages, Tools, and Techniques for Accelerator
+            Design*, 2021.
+
+Mailing lists
+-------------
+
+For discussions, you can join the following mailing list: `lists.sr.ht/~ymherklotz/vericert-discuss <https://lists.sr.ht/~ymherklotz/vericert-discuss>`_.
+
+For contributing patches to the `sourcehut <https://sr.ht/~ymherklotz/vericert/>`_ repository:
+`lists.sr.ht/~ymherklotz/vericert-devel <https://lists.sr.ht/~ymherklotz/vericert-devel>`_.
 
 Indices
-==================
+=======
 
 * :ref:`genindex`
 * :ref:`search`
diff --git a/doc/vericert.rst b/doc/vericert.rst
index 3c8eaeb..19ac28f 100644
--- a/doc/vericert.rst
+++ b/doc/vericert.rst
@@ -12,7 +12,7 @@ application-specific integrated circuit (ASIC).
 
 .. _fig:design:
 
-.. figure:: /_static/images/toolflow.png
+.. figure:: /_static/images/toolflow.svg
 
     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.
@@ -20,8 +20,6 @@ application-specific integrated circuit (ASIC).
 The design shown in Figure `fig:design`_ shows how Vericert leverages an existing verified C
 compiler called `CompCert <https://compcert.org/compcert-C.html>`_ to perform this translation.
 
-.. index:: vericert
-
 .. _building:
 
 Building Vericert
@@ -48,8 +46,6 @@ Or by running the test suite using the following command:
 
 .. _using-vericert:
 
-.. index:: vericert
-
 Using Vericert
 --------------
 
@@ -454,7 +450,7 @@ Example
 
 A small standalone Coq file that exhibits many of the style points.
 
-.. code:: coq
+.. coq:: no-out
 
     (*
      * Vericert: Verified high-level synthesis.