diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2022-05-06 10:49:36 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2022-05-06 10:49:36 +0100 |
| commit | 4e29d51567c76ff07fe4add711f61b896a9cccf1 (patch) | |
| tree | 30eb7f7699921de4ffcdeb059f00a6aec8d75e46 | |
| parent | c3e4847d73dac078f31381aa6c4f41928a191e7d (diff) | |
| download | lsr22_fvhls-4e29d51567c76ff07fe4add711f61b896a9cccf1.tar.gz lsr22_fvhls-4e29d51567c76ff07fe4add711f61b896a9cccf1.zip | |
Update build
| -rw-r--r-- | .build.yml | 3 | ||||
| -rw-r--r-- | Makefile | 3 | ||||
| -rw-r--r-- | chapters/hls.tex | 10 |
3 files changed, 8 insertions, 8 deletions
@@ -4,7 +4,7 @@ packages: - context-modules - texlive-pictures - vim - - texlive-fonts-extra + - fonts-texgyre sources: - git@git.sr.ht:~ymherklotz/lsr22_fvhls secrets: @@ -12,7 +12,6 @@ secrets: tasks: - build: | cd lsr22_fvhls - mtxrun --generate make REBUILD_DEPS=no main.pdf artifacts: - lsr22_fvhls/main.pdf @@ -1,6 +1,7 @@ MODE ?= main REBUILD_DEPS ?= yes DEPS := +CONTEXT ?= context ifeq ($(REBUILD_DEPS), yes) DEPS += figures/timing-1.pdf figures/timing-2.pdf figures/timing-3.pdf @@ -20,5 +21,5 @@ chapters/scheduling.pdf: figures/timing-3.pdf # silent structure,structures,pages,resolvers,open source,close source,loading,modules %.pdf: %.tex - context --mode=$(MODE) --nonstopmode --silent='*' $< + $(CONTEXT) --mode=$(MODE) --nonstopmode --silent='*' $< cp $(notdir $@) $@ || true diff --git a/chapters/hls.tex b/chapters/hls.tex index f39afd3..dcdf2b2 100644 --- a/chapters/hls.tex +++ b/chapters/hls.tex @@ -1320,9 +1320,9 @@ $B_1$ and $B_2$ must be the same. \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 + \HL + \NC \NC {\bf Coq code} \NC \NC {\bf Spec} \NC \NC {\bf Total} \NC \NR + \HL \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 @@ -1331,9 +1331,9 @@ $B_1$ and $B_2$ must be the same. \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 + \HL \NC {\bf Total} \NC 1721 \NC 775 \NC 693 \NC 8355 \NC 11544 \NC \NR - \BL + \HL \stoptabulate \stopplacetable |