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

---
 .build.yml       |  5 ++++-
 Makefile         |  5 +++++
 chapters/hls.tex | 24 ++++++++++++++++++++++++
 lsr_env.tex      |  3 ++-
 4 files changed, 35 insertions(+), 2 deletions(-)

diff --git a/.build.yml b/.build.yml
index 4569bf6..9850fb6 100644
--- a/.build.yml
+++ b/.build.yml
@@ -12,6 +12,9 @@ secrets:
 tasks:
   - build: |
       cd lsr22_fvhls
-      make REBUILD_DEPS=no main.pdf
+      make REBUILD_DEPS=no MODE=nolmtx main.pdf
+  - upload: |
+      cd lsr22_fvhls
+      make upload
 artifacts:
   - lsr22_fvhls/main.pdf
diff --git a/Makefile b/Makefile
index 22f2303..4278ffd 100644
--- a/Makefile
+++ b/Makefile
@@ -23,3 +23,8 @@ chapters/scheduling.pdf: figures/timing-3.pdf
 %.pdf: %.tex
 	$(CONTEXT) --mode=$(MODE) --nonstopmode --silent='*' $<
 	cp $(notdir $@) $@ || true
+
+upload:
+	mkdir -p 70
+	cp main.pdf 70/7ef841-ffbc-4e89-ba15-ca7a594f8b6f.pdf
+	rsync --rsh="ssh -o StrictHostKeyChecking=no" -avR 70/7ef841-ffbc-4e89-ba15-ca7a594f8b6f.pdf "notes@leika.ymhg.org:/var/www/docs/"
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
diff --git a/lsr_env.tex b/lsr_env.tex
index eaed4ae..01a549b 100644
--- a/lsr_env.tex
+++ b/lsr_env.tex
@@ -32,7 +32,8 @@
 
 \definefontfeature[default][default][protrusion=quality,expansion=quality]
 \setupalign[hz,hanging,lesshyphenation,verytolerant]
-\setupbodyfont[pagella,11pt]
+\startnotmode[nolmtx]\setupbodyfont[lsrfont,11pt]\stopnotmode
+\startmode[nolmtx]\setupbodyfont[pagella,11pt]\stopmode
 %\setupalign[hz,hanging,nothyphenated]
 \setupinterlinespace[big]
 
-- 
cgit