From 8bd86579f242760c99ba03c1b06e0dd640df11af Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Fri, 6 May 2022 11:52:36 +0100
Subject: Add mode around problematic sections

---
 chapters/hls.tex | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)

(limited to 'chapters/hls.tex')

diff --git a/chapters/hls.tex b/chapters/hls.tex
index dcdf2b2..1a5374c 100644
--- a/chapters/hls.tex
+++ b/chapters/hls.tex
@@ -1317,6 +1317,29 @@ $B_1$ and $B_2$ must be the same.
 
 \subsection[coq-mechanisation]{Coq Mechanisation}
 
+\startnotmode[nolmtx]
+\startplacetable[reference={tab:proof-statistics},title={Statistics about the numbers of lines of
+    code in the proof and implementation of Vericert.}]
+  \starttabulate[|l|r|r|r|r|r|]
+    \FL
+    \NC \NS[1][c] {\bf Coq code} \NS[1][c] {\bf Spec} \NC {\bf Total} \NC \NR
+    \ML
+    \NC Data structures and libraries \NC 280 \NC --- \NC --- \NC 500 \NC 780 \NC \NR
+    \NC Integers and values \NC 98 \NC --- \NC 15 \NC 968 \NC 1081 \NC \NR
+    \NC HTL semantics \NC 50 \NC --- \NC 181 \NC 65 \NC 296 \NC \NR
+    \NC HTL generation \NC 590 \NC --- \NC 66 \NC 3069 \NC 3725 \NC \NR
+    \NC RAM generation \NC 253 \NC --- \NC --- \NC 2793 \NC 3046 \NC \NR
+    \NC Verilog semantics \NC 78 \NC --- \NC 431 \NC 235 \NC 744 \NC \NR
+    \NC Verilog generation \NC 104 \NC --- \NC --- \NC 486 \NC 590 \NC \NR
+    \NC Top-level driver, pretty printers \NC 318 \NC 775 \NC --- \NC 189 \NC 1282 \NC \NR
+    \LL
+    \NC {\bf Total} \NC 1721 \NC 775 \NC 693 \NC 8355 \NC 11544 \NC \NR
+    \BL
+  \stoptabulate
+\stopplacetable
+\stopnotmode
+
+\startmode[nolmtx]
 \startplacetable[reference={tab:proof-statistics},title={Statistics about the numbers of lines of
     code in the proof and implementation of Vericert.}]
   \starttabulate[|l|r|r|r|r|r|]
@@ -1336,6 +1359,7 @@ $B_1$ and $B_2$ must be the same.
     \HL
   \stoptabulate
 \stopplacetable
+\stopmode
 
 The lines of code for the implementation and proof of can be found in
 \in{Table}[tab:proof-statistics]. Overall, it took about 1.5 person-years to build -- about three
-- 
cgit 

