diff --git a/Main.lean b/Main.lean
index e35991d..ebdbd29 100644
--- a/Main.lean
+++ b/Main.lean
@@ -11,7 +11,8 @@ where
   config := {
     extraFiles := [("static", "static")],
     extraCss := ["/static/colors.css", "/static/theme.css", "/static/print.css", "/static/fonts/source-serif/source-serif-text.css", "/static/fonts/source-code-pro/source-code-pro.css", "/static/katex/katex.min.css"],
-    extraJs := ["/static/katex/katex.min.js", "/static/math.js", "/static/print.js"]
-    emitTeX := false
-    emitHtmlSingle := true -- for proofreading
+    extraJs := ["/static/katex/katex.min.js", "/static/math.js", "/static/print.js"],
+    emitTeX := false,
+    emitHtmlSingle := true, -- for proofreading
+    logo := some "/static/lean_logo.svg"
   }
diff --git a/lake-manifest.json b/lake-manifest.json
index 8d0c4ca..472115a 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "4c7f449c296461794d5260dd044f2629e53e8532",
+   "rev": "625054ef9e53e3b9167252f59fd55589aa56e196",
    "name": "verso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
diff --git a/static/lean_logo.svg b/static/lean_logo.svg
new file mode 100644
index 0000000..98b0913
--- /dev/null
+++ b/static/lean_logo.svg
@@ -0,0 +1,90 @@
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<svg xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns:cc="http://creativecommons.org/ns#" xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#" xmlns:svg="http://www.w3.org/2000/svg" xmlns="http://www.w3.org/2000/svg" xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd" xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape" width="300" height="150" viewBox="0 0 240 120" version="1.1" id="svg2" inkscape:version="1.0.2 (e86c870879, 2021-01-15)" sodipodi:docname="lean_logo.svg">
+  <metadata id="metadata113">
+    <rdf:RDF>
+      <cc:Work rdf:about="">
+        <dc:format>image/svg+xml</dc:format>
+        <dc:type rdf:resource="http://purl.org/dc/dcmitype/StillImage"/>
+      </cc:Work>
+    </rdf:RDF>
+  </metadata>
+  <sodipodi:namedview pagecolor="#ffffff" bordercolor="#666666" borderopacity="1" objecttolerance="10" gridtolerance="10" guidetolerance="10" inkscape:pageopacity="0" inkscape:pageshadow="2" inkscape:window-width="2560" inkscape:window-height="1418" id="namedview111" showgrid="false" inkscape:zoom="4" inkscape:cx="223.20569" inkscape:cy="58.300704" inkscape:window-x="0" inkscape:window-y="0" inkscape:window-maximized="1" inkscape:current-layer="surface1" inkscape:document-rotation="0" showguides="true" inkscape:guide-bbox="true">
+    <sodipodi:guide position="70.622896,28.982703" orientation="0,-1" id="guide193"/>
+    <sodipodi:guide position="55.91963,99.309873" orientation="0,-1" id="guide205"/>
+    <sodipodi:guide position="63.7,64.3" orientation="0,-1" id="guide207"/>
+    <sodipodi:guide position="57.515625,28.982703" orientation="0,-1" id="guide209"/>
+    <sodipodi:guide position="57.403125,27.453125" orientation="0,-1" id="guide211"/>
+    <sodipodi:guide position="9.834375,27.071875" orientation="1,0" id="guide213"/>
+    <sodipodi:guide position="11.771875,28.396875" orientation="1,0" id="guide215"/>
+  </sodipodi:namedview>
+  <defs id="defs4">
+    <g id="g6">
+      <symbol overflow="visible" id="glyph0-0" style="overflow:visible">
+        <path style="stroke:none" d="m -5.140625,0 -180.499995,0 0,-262.4375 180.499995,0 z M -178.125,-250.15625 l 0,237.09375 79.171875,-118.75 z m 5.14063,243.03125 154.781245,0 -77.1875,-117.5625 z m 77.593745,-131.8125 77.1875,-116.375 -154.781245,0 z m 3.5625,7.125 79.15625,118.75 0,-237.09375 z" id="path9" inkscape:connector-curvature="0"/>
+      </symbol>
+      <symbol overflow="visible" id="glyph0-1" style="overflow:visible">
+        <path style="stroke:none" d="m -24.9375,-135.375 -143.29687,0 0,-6.32812 143.29687,0 0,-129.04688 -146.45312,0 0,-5.9375 152.781245,0 0,276.6875 -153.578125,0 0,-5.9375 147.25,0 z" id="path12" inkscape:connector-curvature="0"/>
+      </symbol>
+      <symbol overflow="visible" id="glyph1-0" style="overflow:visible">
+        <path style="stroke:none" d="m 5.140625,0 180.499995,0 0,-262.4375 -180.499995,0 z M 178.125,-250.15625 l 0,237.09375 -79.171875,-118.75 z m -5.14063,243.03125 -154.781245,0 77.1875,-117.5625 z m -77.593745,-131.8125 -77.1875,-116.375 154.781245,0 z m -3.5625,7.125 -79.15625,118.75 0,-237.09375 z" id="path15" inkscape:connector-curvature="0"/>
+      </symbol>
+      <symbol overflow="visible" id="glyph1-1" style="overflow:visible">
+        <path style="stroke:none" d="m 24.9375,0 0,-264.40625 L 207.8125,0 l 6.32812,0 0,-277.07812 -5.9375,0 0,265.999995 -184.062495,-265.999995 -5.53125,-0.39063 0,277.46875 z" id="path18" inkscape:connector-curvature="0"/>
+      </symbol>
+      <symbol overflow="visible" id="glyph1-2" style="overflow:visible">
+        <path style="stroke:none" d="m 24.9375,-276.6875 -6.328125,0 0,276.6875 C 70.453125,0 121.92188,0 173.76562,0 l 0,-6.328125 -148.82812,0 z" id="path21" inkscape:connector-curvature="0"/>
+      </symbol>
+      <symbol overflow="visible" id="glyph2-0" style="overflow:visible">
+        <path style="stroke:none" d="m 1.21875,0 42.5,0 0,-61.796875 -42.5,0 z m 40.734375,-58.921875 0,55.84375 -18.640625,-27.96875 z m -1.21875,57.25 -36.453125,0 18.1875,-27.6875 z M 22.46875,-32.71875 4.28125,-60.125 l 36.453125,0 z m -0.84375,1.671875 -18.640625,27.96875 0,-55.84375 z" id="path24" inkscape:connector-curvature="0"/>
+      </symbol>
+      <symbol overflow="visible" id="glyph2-1" style="overflow:visible">
+        <path style="stroke:none" d="m 24.796875,0.28125 0,-64.046875 22.5625,0 0,-1.484375 -46.515625,0 0,1.484375 22.546875,0 0,64.046875 z" id="path27" inkscape:connector-curvature="0"/>
+      </symbol>
+      <symbol overflow="visible" id="glyph2-2" style="overflow:visible">
+        <path style="stroke:none" d="m 5.78125,-65.15625 -1.40625,0 0,65.15625 1.40625,0 0,-32.34375 40.921875,0 0,32.34375 1.484375,0 0,-65.15625 -1.484375,0 0,31.40625 -40.921875,0 z" id="path30" inkscape:connector-curvature="0"/>
+      </symbol>
+      <symbol overflow="visible" id="glyph2-3" style="overflow:visible">
+        <path style="stroke:none" d="m 5.875,-31.875 33.75,0 0,-1.5 -33.75,0 0,-30.390625 34.484375,0 0,-1.390625 -35.984375,0 0,65.15625 36.171875,0 0,-1.390625 -34.671875,0 z" id="path33" inkscape:connector-curvature="0"/>
+      </symbol>
+      <symbol overflow="visible" id="glyph2-4" style="overflow:visible">
+        <path style="stroke:none" d="m 67.765625,-32.625 c 0,8.859375 -3.53125,16.78125 -9.21875,22.5625 -5.78125,5.875 -13.796875,9.5 -22.5625,9.5 -8.765625,0 -16.6875,-3.625 -22.46875,-9.5 C 7.828125,-15.84375 4.1875,-23.765625 4.1875,-32.625 c 0,-8.859375 3.640625,-16.78125 9.328125,-22.5625 5.78125,-5.875 13.703125,-9.5 22.46875,-9.5 8.765625,0 16.78125,3.625 22.5625,9.5 5.6875,5.78125 9.21875,13.703125 9.21875,22.5625 z m -65.0625,0 c 0,9.234375 3.828125,17.609375 9.78125,23.671875 5.96875,6.15625 14.359375,9.890625 23.5,9.890625 9.234375,0 17.515625,-3.734375 23.578125,-9.890625 5.96875,-6.0625 9.796875,-14.4375 9.796875,-23.671875 0,-9.234375 -3.828125,-17.625 -9.796875,-23.671875 C 53.5,-62.453125 45.21875,-66.1875 35.984375,-66.1875 c -9.140625,0 -17.53125,3.734375 -23.5,9.890625 C 6.53125,-50.25 2.703125,-41.859375 2.703125,-32.625 z" id="path36" inkscape:connector-curvature="0"/>
+      </symbol>
+      <symbol overflow="visible" id="glyph2-5" style="overflow:visible">
+        <path style="stroke:none" d="m 5.78125,-63.765625 21.15625,0 c 24.234375,0 24.234375,35.234375 0,35.234375 l -12.671875,0 0,1.40625 L 44.28125,0 46.421875,0 16.40625,-27.125 l 10.53125,0 c 26.109375,0 26.109375,-38.125 0,-38.125 l -22.5625,0 0,65.25 1.40625,0 z" id="path39" inkscape:connector-curvature="0"/>
+      </symbol>
+      <symbol overflow="visible" id="glyph2-6" style="overflow:visible">
+        <path style="stroke:none" d="m 5.78125,-63.109375 26.5625,39.53125 1.21875,0 26.5625,-39.53125 0,63.109375 1.40625,0 0,-65.25 -1.5,0 -27.125,39.984375 L 5.875,-65.25 l -1.5,0 0,65.25 1.40625,0 z" id="path42" inkscape:connector-curvature="0"/>
+      </symbol>
+      <symbol overflow="visible" id="glyph2-7" style="overflow:visible">
+        <path style="stroke:none" d="" id="path45" inkscape:connector-curvature="0"/>
+      </symbol>
+      <symbol overflow="visible" id="glyph2-8" style="overflow:visible">
+        <path style="stroke:none" d="m 4.375,-64.5 c 0,21.53125 0,42.96875 0,64.5 l 1.5,0 0,-24.796875 21.0625,0 c 26.109375,0 26.109375,-40.453125 0,-40.453125 l -22.5625,0 z m 1.5,38.3125 0,-37.578125 21.0625,0 c 24.234375,0 24.234375,37.578125 0,37.578125 z" id="path48" inkscape:connector-curvature="0"/>
+      </symbol>
+      <symbol overflow="visible" id="glyph2-9" style="overflow:visible">
+        <path style="stroke:none" d="m 5.78125,-63.765625 21.15625,0 c 24.234375,0 24.234375,35.234375 0,35.234375 l -12.671875,0 0,1.40625 L 44.28125,0 46.421875,0 16.40625,-27.125 l 10.53125,0 c 26.109375,0 26.109375,-38.125 0,-38.125 l -22.5625,0 0,65.25 1.40625,0 z" id="path51" inkscape:connector-curvature="0"/>
+      </symbol>
+      <symbol overflow="visible" id="glyph2-10" style="overflow:visible">
+        <path style="stroke:none" d="m 67.03125,-32.625 c 0,8.859375 -3.546875,16.78125 -9.234375,22.5625 -5.78125,5.875 -13.796875,9.5 -22.5625,9.5 -8.765625,0 -16.6875,-3.625 -22.46875,-9.5 -5.6875,-5.78125 -9.3125,-13.703125 -9.3125,-22.5625 0,-8.859375 3.625,-16.78125 9.3125,-22.5625 5.78125,-5.875 13.703125,-9.5 22.46875,-9.5 8.765625,0 16.78125,3.625 22.5625,9.5 5.6875,5.78125 9.234375,13.703125 9.234375,22.5625 z m -65.078125,0 c 0,9.234375 3.828125,17.609375 9.796875,23.671875 5.96875,6.15625 14.34375,9.890625 23.484375,9.890625 9.234375,0 17.53125,-3.734375 23.59375,-9.890625 5.953125,-6.0625 9.78125,-14.4375 9.78125,-23.671875 0,-9.234375 -3.828125,-17.625 -9.78125,-23.671875 -6.0625,-6.15625 -14.359375,-9.890625 -23.59375,-9.890625 -9.140625,0 -17.515625,3.734375 -23.484375,9.890625 C 5.78125,-50.25 1.953125,-41.859375 1.953125,-32.625 z" id="path54" inkscape:connector-curvature="0"/>
+      </symbol>
+      <symbol overflow="visible" id="glyph2-11" style="overflow:visible">
+        <path style="stroke:none" d="m 27.5,-0.84375 -25.359375,-64.3125 -1.578125,0 26.1875,66.1875 1.59375,0 26.1875,-66.1875 -1.578125,0 z" id="path57" inkscape:connector-curvature="0"/>
+      </symbol>
+      <symbol overflow="visible" id="glyph2-12" style="overflow:visible">
+        <path style="stroke:none" d="m 5.875,-31.875 33.75,0 0,-1.5 -33.75,0 0,-30.390625 34.484375,0 0,-1.390625 -35.984375,0 0,65.15625 36.171875,0 0,-1.390625 -34.671875,0 z" id="path60" inkscape:connector-curvature="0"/>
+      </symbol>
+    </g>
+    <clipPath clipPathUnits="userSpaceOnUse" id="clipPath3094">
+      <rect style="fill:#0000ff;fill-rule:evenodd;stroke:#000000;stroke-width:0.80000001px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1" id="rect3096" width="754.1781" height="300.61642" x="13.184932" y="8.90411"/>
+    </clipPath>
+  </defs>
+  <g id="surface1" clip-path="url(#clipPath3094)" transform="matrix(0.30563256,0,0,0.25971391,2.2768141,14.142563)">
+    <g style="fill:#000000;fill-opacity:1" id="g71"/>
+    <g id="g1226">
+      <path style="fill:#000000;fill-opacity:1;stroke:none" d="M 323.2793,166.51926 H 179.98243 v -6.32812 H 323.2793 V 31.14426 H 176.82618 v -5.9375 h 152.78124 v 276.6875 h -304.879816 V 25.210709 h 6.339311 v 270.787071 h 292.212385 z" id="path188" inkscape:connector-curvature="0" sodipodi:nodetypes="ccccccccccccccc"/>
+      <path style="fill:#000000;fill-opacity:1;stroke:none" d="M 554.58618,301.89426 V 37.48801 l 182.875,264.40625 h 6.32812 V 25.303323 h -5.9375 V 290.81613 L 553.78931,25.303323 h -5.53125 V 301.89426 Z" id="path196" inkscape:connector-curvature="0" sodipodi:nodetypes="ccccccccccc"/>
+      <path style="fill:none;stroke:#000000;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-opacity:1" d="m 493.91087,342.7146 35.08932,83.78546 35.25165,-83.75238" transform="matrix(3.192199,0,0,3.192199,-1250.002,-1067.559)" id="path75" inkscape:connector-curvature="0" sodipodi:nodetypes="ccc"/>
+      <path style="fill:none;stroke:#000000;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-opacity:1" d="m 511.6195,385.54515 34.93019,0.0" transform="matrix(3.192199,0,0,3.192199,-1250.002,-1067.559)" id="path77" inkscape:connector-curvature="0" sodipodi:nodetypes="cc"/>
+    </g>
+  </g>
+<script xmlns=""/></svg>
\ No newline at end of file
diff --git a/static/theme.css b/static/theme.css
index 6468d92..f0b8d64 100644
--- a/static/theme.css
+++ b/static/theme.css
@@ -105,7 +105,7 @@ figcaption {
 
 /** Temporary measures until the real release **/
 
-body::before {
+main::before {
     content: 'Preview Release';
     position: fixed;
     top: 0;
@@ -122,13 +122,13 @@ body::before {
     background-color: var(--lean-compl-yellow);
     font-family: var(--verso-structure-font-family);
     font-size: large;
-    z-index: -1; /* don't show under marginal notes*/
 }
 
-span.TODO, .marginalia .note {
-    z-index: -2;
-}
 
 #print {
     display: none;
 }
+
+#top-menu {
+
+}