Generate HTML for sum8 ILA capture

cava/Cava2HDL/Setup.hs

@@ -0,0 +1,17 @@
+{- Copyright 2020 The Project Oak Authors
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.
+-}
+
+import Distribution.Simple
+main = defaultMain

demos/tutorial.v

@@ -941,10 +941,9 @@ Definition sum8_tb :=
 
 (*|
 The circuit netlist and testbench can be converted in SystemVerilog and
-simulated using a SystemVerilog simulator like Verilator:
+simulated using a SystemVerilog simulator like Verilator::
 
-clang++ -L/usr/local/opt/sqlite/lib    sum8_tb.o verilated.o verilated_vcd_c.o Vsum8_tb__ALL.a    -o Vsum8_tb -lm -lstdc++
-obj_dir/Vsum8_tb
+  clang++ -L/usr/local/opt/sqlite/lib    sum8_tb.o verilated.o verilated_vcd_c.o Vsum8_tb__ALL.a    -o Vsum8_tb -lm -lstdc++ obj_dir/Vsum8_tb
                   10: tick = 0,  i = 3,  o = 3
                   20: tick = 1,  i = 5,  o = 8
                   30: tick = 2,  i = 7,  o = 15
@@ -970,7 +969,7 @@ run and observe this actually running on an FPGA and capture its output:
    :width: 70%
    :alt: Logic analyzer trace capture for the sum8 circuit.
 
-Reassuring the actual circuit behaves as predicted by the Cava model
+Reassuringly, the actual circuit behaves as predicted by the Cava model
 in Coq and the SystemVerilog simulation.
 |*)
 

docs/demo/alectryon.css

@@ -105,7 +105,7 @@ In any case, make an exception for comments:
 .alectryon-toggle-label,
 .alectryon-extra-goal-label {
     display: block;
-    font-size: 0.8rem;
+    font-size: 0.8em;
 }
 
 .alectryon-io .alectryon-input {
@@ -122,33 +122,33 @@ In any case, make an exception for comments:
 .alectryon-io label.alectryon-input:after,
 .alectryon-io .alectryon-extra-goal-label:before {
     border: 1px solid #babdb6;
-    border-radius: 1rem;
+    border-radius: 1em;
     box-sizing: border-box;
     content: '';
     display: inline-block;
     font-weight: bold;
-    height: 0.25rem;
-    margin-bottom: 0.15rem;
+    height: 0.25em;
+    margin-bottom: 0.15em;
     vertical-align: middle;
-    width: 0.75rem;
+    width: 0.75em;
 }
 
 .alectryon-toggle-label:before,
 .alectryon-io .alectryon-extra-goal-label:before {
-    margin-right: 0.25rem;
+    margin-right: 0.25em;
 }
 
 .alectryon-io .alectryon-extra-goal-label::before {
-    margin-top: -0.35rem;
+    margin-top: -0.35em;
 }
 
 .alectryon-io label.alectryon-input {
-    padding-right: 1rem; /* Prevent line wraps before the checkbox bubble */
+    padding-right: 1em; /* Prevent line wraps before the checkbox bubble */
 }
 
 .alectryon-io label.alectryon-input:after {
-    margin-left: 0.25rem;
-    margin-right: -1rem; /* Compensate for the anti-wrapping space */
+    margin-left: 0.25em;
+    margin-right: -1em; /* Compensate for the anti-wrapping space */
 }
 
 .alectryon-failed {
@@ -158,7 +158,7 @@ In any case, make an exception for comments:
     text-decoration: red dotted underline;
     text-decoration-skip-ink: none;
     /* Chrome prints background images in low resolution, yielding a blurry underline */
-    /* background: bottom / 0.3rem auto repeat-x url(data:image/svg+xml;base64,PHN2ZyB4bWxucz0iaHR0cDovL3d3dy53My5vcmcvMjAwMC9zdmciIHZpZXdCb3g9IjAgMCAyLjY0NiAxLjg1MiIgaGVpZ2h0PSI4IiB3aWR0aD0iMTAiPjxwYXRoIGQ9Ik0wIC4yNjVjLjc5NCAwIC41MyAxLjMyMiAxLjMyMyAxLjMyMi43OTQgMCAuNTMtMS4zMjIgMS4zMjMtMS4zMjIiIGZpbGw9Im5vbmUiIHN0cm9rZT0icmVkIiBzdHJva2Utd2lkdGg9Ii41MjkiLz48L3N2Zz4=); */
+    /* background: bottom / 0.3em auto repeat-x url(data:image/svg+xml;base64,PHN2ZyB4bWxucz0iaHR0cDovL3d3dy53My5vcmcvMjAwMC9zdmciIHZpZXdCb3g9IjAgMCAyLjY0NiAxLjg1MiIgaGVpZ2h0PSI4IiB3aWR0aD0iMTAiPjxwYXRoIGQ9Ik0wIC4yNjVjLjc5NCAwIC41MyAxLjMyMiAxLjMyMyAxLjMyMi43OTQgMCAuNTMtMS4zMjIgMS4zMjMtMS4zMjIiIGZpbGw9Im5vbmUiIHN0cm9rZT0icmVkIiBzdHJva2Utd2lkdGg9Ii41MjkiLz48L3N2Zz4=); */
 }
 
 /* Wrapping :hover rules in a media query ensures that tapping a Coq sentence
@@ -208,7 +208,7 @@ In any case, make an exception for comments:
     left: 0;
     right: 0;
     position: absolute;
-    padding: 0.25rem 0;
+    padding: 0.25em 0;
     overflow: visible; /* Let box-shadows overflow */
     z-index: 1; /* Default to an index lower than that used by :hover */
 }
@@ -256,7 +256,7 @@ In any case, make an exception for comments:
     background: #eeeeec;
 	border: thin solid #d3d7cf; /* Convenient when pre's background is already #EEE */
     display: block;
-    padding: 0.25rem;
+    padding: 0.25em;
 }
 
 .alectryon-message::before {
@@ -279,7 +279,7 @@ In any case, make an exception for comments:
     position: static;
     width: unset;
     background: unset; /* Override the backgrounds set in floating in windowed mode */
-    padding: 0.25rem 0; /* Re-assert so that later :hover rules don't override this padding */
+    padding: 0.25em 0; /* Re-assert so that later :hover rules don't override this padding */
 }
 
 .alectryon-toggle:checked + label + .alectryon-container label.alectryon-input + .alectryon-output .goal-hyps,
@@ -314,12 +314,12 @@ In any case, make an exception for comments:
 .alectryon-io .alectryon-goal,
 .alectryon-io .goal-hyp,
 .alectryon-io .goal-conclusion {
-    border-radius: 0.15rem;
+    border-radius: 0.15em;
 }
 
 .alectryon-io .alectryon-goal,
 .alectryon-io .alectryon-message {
-    margin: 0.25rem;
+    margin: 0.25em;
 }
 
 .alectryon-io .alectryon-goal,
@@ -328,7 +328,7 @@ In any case, make an exception for comments:
     background: #d3d7cf;
     display: block;
     flex-direction: column;
-    padding: 0.5rem;
+    padding: 0.5em;
     position: relative;
 }
 
@@ -339,21 +339,21 @@ In any case, make an exception for comments:
     flex-flow: column nowrap; /* re-stated in windowed mode */
     justify-content: space-around;
     /* LATER use a ‘gap’ property instead of margins once supported */
-    margin: -0.15rem -0.25rem; /* -0.15rem to cancel the item spacing */
-    padding-bottom: 0.5rem;
+    margin: -0.15em -0.25em; /* -0.15em to cancel the item spacing */
+    padding-bottom: 0.5em;
 }
 
 .alectryon-io .goal-hyp,
 .alectryon-io .goal-conclusion {
     background: #eeeeec;
     display: inline-block;
-    padding: 0.15rem 0.35rem;
+    padding: 0.15em 0.35em;
 }
 
 .alectryon-io .goal-hyp {
     align-items: baseline;
     display: inline-flex;
-    margin: 0.15rem 0.25rem;
+    margin: 0.15em 0.25em;
 }
 
 .alectryon-io .hyp-names {
@@ -365,7 +365,7 @@ In any case, make an exception for comments:
 
 .alectryon-io .hyp-punct {
     font-weight: 600;
-    margin: 0 0.5rem;
+    margin: 0 0.5em;
 }
 
 .alectryon-io .hyp-body-block,
@@ -387,7 +387,7 @@ In any case, make an exception for comments:
     display: block;
     flex-grow: 1;
     height: 0;
-    margin: 0 0 0.5rem 0;
+    margin: 0 0 0.5em 0;
 }
 
 .alectryon-io .goal-separator .goal-name {
@@ -403,9 +403,9 @@ In any case, make an exception for comments:
     background: #eeeeec;
     border: 1px solid #babcbd;
     font-size: 0.75em;
-    padding: 0.25rem;
+    padding: 0.25em;
     text-align: center;
-    margin: 1rem 0;
+    margin: 1em 0;
 }
 
 .alectryon-banner a {
@@ -443,7 +443,7 @@ In any case, make an exception for comments:
         top: 0;
         left: 100%;
         right: -100%;
-        padding: 0 0.5rem;
+        padding: 0 0.5em;
         position:  absolute;
     }
 
@@ -503,7 +503,7 @@ In any case, make an exception for comments:
 /* See note about specificity below */
 .alectryon-windowed .alectryon-sentence:hover .alectryon-output,
 .alectryon-windowed .alectryon-sentence.alectryon-target .alectryon-toggle ~ .alectryon-output {
-    padding: 0.5rem;
+    padding: 0.5em;
     overflow-y: auto; /* Windowed contents may need to scroll */
 }
 
@@ -562,7 +562,7 @@ In any case, make an exception for comments:
 }
 
 .alectryon-coqdoc .doc .paragraph {
-    height: 0.75rem;
+    height: 0.75em;
 }
 
 /* Centered, Floating */
@@ -591,7 +591,7 @@ In any case, make an exception for comments:
     margin: 0;
     overflow-y: auto;
     position: absolute;
-    padding: 0 1rem;
+    padding: 0 1em;
 }
 
 .alectryon-standalone .alectryon-windowed > * {