-
Notifications
You must be signed in to change notification settings - Fork 12
/
paper.tex
669 lines (578 loc) · 25 KB
/
paper.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
\def\paperversiondraft{draft}
\def\paperversionnormal{normal}
% If the paper version is set to 'normal' mode keep it,
% otherwise set it to 'draft' mode.
\ifx\paperversion\paperversionnormal
\else
\def\paperversion{draft}
\fi
\documentclass[review, anonymous, sigplan]{acmart}
\def\acmversionanonymous{anonymous}
\def\acmversionjournal{journal}
\def\acmversionnone{none}
\makeatletter
\if@ACM@anonymous
\def\acmversion{anonymous}
\else
\def\acmversion{journal}
\fi
\makeatother
\usepackage{colortbl}
% 'draftonly' environment
\usepackage{environ}
\ifx\paperversion\paperversiondraft
\newenvironment{draftonly}{}{}
\else
\NewEnviron{draftonly}{}
\fi
% Most PL conferences are edited by conference-publishing.com. Follow their
% advice to add the following packages.
%
% The first enables the use of UTF-8 as character encoding, which is the
% standard nowadays. The second ensures the use of font encodings that support
% accented characters etc. (Why should I use this?). The mictotype package
% enables certain features 'towards typographical perfection
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{microtype}
\usepackage{xargs}
\usepackage{lipsum}
\usepackage{xparse}
\usepackage{xifthen, xstring}
\usepackage{xspace}
\usepackage{marginnote}
\usepackage{etoolbox}
\usepackage[acronym,shortcuts]{glossaries}
\usepackage{amsmath}
\usepackage{thmtools} % required for autoref to lemmas
\usepackage{algorithm}
\usepackage[noend]{algpseudocode}
\input{tex/setup.tex}
\input{tex/acm.tex}
\usemintedstyle{colorful}
% Newer versions of minted require the 'customlexer' argument for custom lexers
% whereas older versions require the '-x' to be passed via the command line.
\makeatletter
\ifcsdef{minted@optlistcl@quote}
{
\newminted[mlir]{tools/MLIRLexer.py:MLIRLexerOnlyOps}{customlexer, mathescape}
\newminted[xdsl]{tools/MLIRLexer.py:MLIRLexer}{customlexer, mathescape, style=murphy}
\newminted[lean4]{tools/Lean4Lexer.py:Lean4Lexer}{customlexer, mathescape}
}
{
\newminted[mlir]{tools/MLIRLexer.py:MLIRLexerOnlyOps -x}{mathescape}
\newminted[xdsl]{tools/MLIRLexer.py:MLIRLexer -x}{mathescape, style=murphy}
\newminted[lean4]{tools/Lean4Lexer.py:Lean4Lexer -x}{mathescape}
}
\makeatother
% We use the following color scheme
%
% This scheme is both print-friendly and colorblind safe for
% up to four colors (including the red tones makes it not
% colorblind safe any more)
%
% https://colorbrewer2.org/#type=qualitative&scheme=Paired&n=4
\definecolor{pairedNegOneLightGray}{HTML}{cacaca}
\definecolor{pairedNegTwoDarkGray}{HTML}{827b7b}
\definecolor{pairedOneLightBlue}{HTML}{a6cee3}
\definecolor{pairedTwoDarkBlue}{HTML}{1f78b4}
\definecolor{pairedThreeLightGreen}{HTML}{b2df8a}
\definecolor{pairedFourDarkGreen}{HTML}{33a02c}
\definecolor{pairedFiveLightRed}{HTML}{fb9a99}
\definecolor{pairedSixDarkRed}{HTML}{e31a1c}
\createtodoauthor{grosser}{pairedOneLightBlue}
\createtodoauthor{authorTwo}{pairedTwoDarkBlue}
\createtodoauthor{authorThree}{pairedThreeLightGreen}
\createtodoauthor{authorFour}{pairedFourDarkGreen}
\createtodoauthor{authorFive}{pairedFiveLightRed}
\createtodoauthor{authorSix}{pairedSixDarkRed}
\newacronym{ir}{IR}{Intermediate Representation}
\graphicspath{{./images/}}
% Define macros that are used in this paper
%
% We require all macros to end with a delimiter (by default {}) to enusure
% that LaTeX adds whitespace correctly.
\makeatletter
\newcommand\requiredelimiter[2][########]{%
\ifdefined#2%
\def\@temp{\def#2#1}%
\expandafter\@temp\expandafter{#2}%
\else
\@latex@error{\noexpand#2undefined}\@ehc
\fi
}
\@onlypreamble\requiredelimiter
\makeatother
\newcommand\newdelimitedcommand[2]{
\expandafter\newcommand\csname #1\endcsname{#2}
\expandafter\requiredelimiter
\csname #1 \endcsname
}
\newdelimitedcommand{toolname}{Tool}
\usepackage{booktabs}
\newcommand{\ra}[1]{\renewcommand{\arraystretch}{#1}}
\usepackage[verbose]{newunicodechar}
\newunicodechar{₁}{\ensuremath{_1}}
\newunicodechar{₂}{\ensuremath{_2}}
\newunicodechar{∀}{\ensuremath{\forall}}
\newunicodechar{α}{\ensuremath{\alpha}}
\newunicodechar{β}{\ensuremath{\beta}}
% \circled command to print a colored circle.
% \circled{1} pretty-prints "(1)"
% This is useful to refer to labels that are embedded within figures.
\DeclareRobustCommand{\circled}[2][]{%
\ifthenelse{\isempty{#1}}%
{\circledbase{pairedOneLightBlue}{#2}}%
{\autoref{#1}: \hyperref[#1]{\circledbase{pairedOneLightBlue}{#2}}}%
}
% listings don't write "Listing" in autoref without this.
\providecommand*{\listingautorefname}{Listing}
\renewcommand{\sectionautorefname}{Section}
\renewcommand{\subsectionautorefname}{Section}
\renewcommand{\subsubsectionautorefname}{Section}
\begin{document}
%% Title information
\title[Short Title]{Full Title} %% [Short Title] is optional;
%% when present, will be used in
%% header instead of Full Title.
\subtitle{Subtitle} %% \subtitle is optional
%% Author information
%% Contents and number of authors suppressed with 'anonymous'.
%% Each author should be introduced by \author, followed by
%% \authornote (optional), \orcid (optional), \affiliation, and
%% \email.
%% An author may have multiple affiliations and/or emails; repeat the
%% appropriate command.
%% Many elements are not rendered, but should be provided for metadata
%% extraction tools.
\author{First1 Last1}
\authornote{with author1 note} %% \authornote is optional;
%% can be repeated if necessary
\orcid{nnnn-nnnn-nnnn-nnnn} %% \orcid is optional
\affiliation{
\position{Position1}
\department{Department1} %% \department is recommended
\institution{Institution1} %% \institution is required
\streetaddress{Street1 Address1}
\city{City1}
\state{State1}
\postcode{Post-Code1}
\country{Country1}
}
\email{[email protected]} %% \email is recommended
\author{First2 Last2}
\authornote{with author2 note} %% \authornote is optional;
%% can be repeated if necessary
\orcid{nnnn-nnnn-nnnn-nnnn} %% \orcid is optional
\affiliation{
\position{Position2a}
\department{Department2a} %% \department is recommended
\institution{Institution2a} %% \institution is required
\streetaddress{Street2a Address2a}
\city{City2a}
\state{State2a}
\postcode{Post-Code2a}
\country{Country2a}
}
\email{[email protected]} %% \email is recommended
\affiliation{
\position{Position2b}
\department{Department2b} %% \department is recommended
\institution{Institution2b} %% \institution is required
\streetaddress{Street3b Address2b}
\city{City2b}
\state{State2b}
\postcode{Post-Code2b}
\country{Country2b}
}
\email{[email protected]} %% \email is recommended
\begin{abstract}
% An abstract should consist of six main sentences:
% 1. Introduction. In one sentence, what’s the topic?
% 2. State the problem you tackle.
% 3. Summarize (in one sentence) why nobody else has adequately answered the research question yet.
% 4. Explain, in one sentence, how you tackled the research question.
% 5. In one sentence, how did you go about doing the research that follows from your big idea.
% 6. As a single sentence, what’s the key impact of your research?
% (http://www.easterbrook.ca/steve/2010/01/how-to-write-a-scientific-abstract-in-six-easy-steps/)
\lipsum[1]
\end{abstract}
% Only add ACM notes and keywords in camera ready version
% Drop citations and footnotes in draft and blind mode.
\ifx\acmversion\acmversionanonymous
\settopmatter{printacmref=false} % Removes citation information below abstract
\renewcommand\footnotetextcopyrightpermission[1]{} % removes footnote with conference information in first column
\fi
\ifx\acmversion\acmversionjournal
%% 2012 ACM Computing Classification System (CSS) concepts
%% Generate at 'http://dl.acm.org/ccs/ccs.cfm'.
\begin{CCSXML}
<ccs2012>
<concept>
<concept_id>10011007.10011006.10011008</concept_id>
<concept_desc>Software and its engineering~General programming languages</concept_desc>
<concept_significance>500</concept_significance>
</concept>
<concept>
<concept_id>10003456.10003457.10003521.10003525</concept_id>
<concept_desc>Social and professional topics~History of programming languages</concept_desc>
<concept_significance>300</concept_significance>
</concept>
</ccs2012>
\end{CCSXML}
\ccsdesc[500]{Software and its engineering~General programming languages}
\ccsdesc[300]{Social and professional topics~History of programming languages}
%% End of generated code
%% Keywords
%% comma separated list
\keywords{keyword1, keyword2, keyword3}
\fi
%% \maketitle
%% Note: \maketitle command must come after title commands, author
%% commands, abstract environment, Computing Classification System
%% environment and commands, and keywords command.
\maketitle
\section{Introduction}
Of this super cool article \ldots
\grosser{A simple comment refering to a particular location}
If there is \authorTwo[some text we want to refer to specifically]{this looks
particularly interesting} we can refer to this text from within our comments.
And here we only mark \authorTwo[text]{} that is \authorTwo[interesting]{}, but do not
actually comment.
Now we have a sequence of comments,
\authorThree{Comment 3}
\authorFour{Comment 4}
\authorFive{Comment 5}
\authorSix{Comment 6}
which should not introduce overlong white space sequences.
Sometimes it is also important to \emph{emphasize} text to understand if it is
underlined or printed in italic.
We sometimes use macros to state that a tool as the name \toolname{} in a
flexible way.
\lipsum[1-3]
\begin{figure}
% Link to figure
%
% https://docs.google.com/drawings/d/1juKp43D3rLC-luBQPwQZ_wCnDK2S_6C1k6USV0wKE0g/edit?usp=sharing
\includegraphics[width=\columnwidth]{overview.pdf}
\caption{Our key idea visualized}
\grosser{Replace this figure with your own drawing.}
\end{figure}
\vspace{.5em}
\noindent
Our contributions are:
\grosser{Always state your contributions explicitly: (A) this makes it
easy for the reader to understand what novelty is presented, and (B)
these contributions help you to focus. In particular, the objective of
the remaining paper should be to support the claims stated here.
}
\begin{itemize}
\item Contribution 1 (\autoref{sec:implementation})
\item Contribution 2
\item Contribution 3
\item Contribution 4
\end{itemize}
\section{Our New Idea}
\lipsum[1-3]
\section{Implementation}
\label{sec:implementation}
\section{Related Work}
\lipsum[1-3]
\grosser{Related work should always be at the end of the document,
as it otherwise becomes an obstacle your reader must
overcome before reaching your idea. For details see:
\url{https://www.microsoft.com/en-us/research/academic-program/write-great-research-paper/}
}
\section{Conclusion}
\lipsum[1]
%% Acknowledgments
\begin{acks} %% acks environment is optional
%% contents suppressed with 'anonymous'
%% Commands \grantsponsor{<sponsorID>}{<name>}{<url>} and
%% \grantnum[<url>]{<sponsorID>}{<number>} should be used to
%% acknowledge financial support and will be used by metadata
%% extraction tools.
This material is based upon work supported by the
\grantsponsor{GS100000001}{National Science
Foundation}{http://dx.doi.org/10.13039/100000001} under Grant
No.~\grantnum{GS100000001}{nnnnnnn} and Grant
No.~\grantnum{GS100000001}{mmmmmmm}. Any opinions, findings, and
conclusions or recommendations expressed in this material are those
of the author and do not necessarily reflect the views of the
National Science Foundation.
\end{acks}
%% Bibliography
\bibliography{references}
%% Appendix
% Move \cleardouble and \appendix out of `draftonly` if you are using the
% appendix
\begin{draftonly}
\cleardoublepage
\appendix
\section{Formatting and Writing Guidelines}
These formatting guidelines aim to standardize our writing. They ensure that
papers with multiple authors have a consistent look and that commonly occurring
items are formatted in ways that are known to work well.
\subsection{Figures}
\label{appendix:figures}
\paragraph{Referencing Figures} When referencing figures from the text we
ensure the following:
\begin{description}
\item [All figures are referenced] A paper with un-referenced figures appears incomplete.
We can check this using the \texttt{refcheck} package.
Issuing \texttt{make refcheck} on the commandline lists all \emph{labeled} elements that are not referenced in the text.
\item [References to figures are brief and easy to skip]~\\
We minimize the number of words needed to refer to a figure. Reducing
the number of non-information-carrying words directly increases
the density of interesting content. When skipping references
becomes easy, reading quickly while ignoring figures remains a
smooth experience. The best and briefest reference to a figure
is a link in parenthesis that is added after the subject
representing the content depicted in a figure:\\
{\color{pairedTwoDarkBlue}\textit{Figure
X shows the design of A, which consists of ...}}\\
$\to$ {\color{pairedFourDarkGreen}
\textit{The design of A (Figure X) consists of ...}}
\item [The text is always self-contained without figures] ~\\ The reader
should be able to read the text without ever looking at any
figure. They should still understand the text and get the key
message of each figure directly from the text. By not forcing
the reader to analyze a figure while reading, we increase
readability as the reader can continue reading without having
to skip between text and figures. Such writing style also helps
to guide the thoughts of the reader, who can (for a moment)
trust our summary of the figure and does not need to develop
their own interpretation on-the-fly, a task which often yields
results that do not fit the flow of our exposition. Readers
typically only feel that their reading is interrupted if there
is no explanation of a figure at all. Hence, we do not need to
discuss all details of a figure, but half a sentence that explains the
core idea is typically sufficient for a reader to continue
reading. By making
our text self-contained even when ignoring figures the reader
experiences a smooth and uninterrupted reading experience.\\
{\color{pairedTwoDarkBlue}
\textit{The speedups are presented in Figure X. < a new topic> }}\\
$\to$ {\color{pairedFourDarkGreen}\textit{Our approach outperforms the state of the art
XXX-library (Figure 3) demonstrating more than 4x speedup on
test case 1 and 2 and a geometric mean speedup of 1.5x over all
20 test cases.}}
\end{description}
We reference figures in text using
\texttt{\symbol{92}autoref\{fig:speedup\}} for a figure with label
\texttt{fig:speedup}. The use of autoref ensures that all references
to figures are formatted consistently, e.g. as \autoref{fig:speedup}.
\paragraph{Color Scheme}
In Figures we use a color scheme that is print-friendly and also visible
with red-green blindness. The following colors are all print-friendly
and red-green save when only using Color 1-4:
\medskip
{
\small
\newcolumntype{a}{>{\columncolor{pairedOneLightBlue}}c}
\newcolumntype{b}{>{\columncolor{pairedTwoDarkBlue}}c}
\newcolumntype{d}{>{\columncolor{pairedThreeLightGreen}}c}
\newcolumntype{e}{>{\columncolor{pairedFourDarkGreen}}c}
\newcolumntype{f}{>{\columncolor{pairedFiveLightRed}}c}
\newcolumntype{g}{>{\columncolor{pairedSixDarkRed}}c}
\begin{tabular}{a b d e f g}
Color 1 & Color 2 & Color 3 & Color 4 & Color 5 & Color 6\\
\#a6cee3 & \#1f78b4 & \#b2df8a & \#33a02c & \#fb9a99 & \#e31a1c
\end{tabular}
}
We de-emphasize components in figures by using additionally two shades of gray.
Especially in complex figures, it is often helpful to de-emphasize visual
elements that we want to represent but that should not be the focus of a
reader's attention.
\medskip
{
\small
\newcolumntype{h}{>{\columncolor{pairedNegOneLightGray}}c}
\newcolumntype{i}{>{\columncolor{pairedNegTwoDarkGray}}c}
\begin{tabular}{h i}
Color -1 & Color -2\\
\#cacaca & \#827b7b\\
\end{tabular}
}
Single-color graphs are plotted in Color 1 - Light Blue.
\paragraph{Labels in Figures}
Complex diagrams often benefit from labels inside the diagrams. We suggest to
use a filled circle (e.g, in light blue) to highlight these numbers and use
these references, e.g., \circled{1} implemented as \texttt{\textbackslash{}circled\{1\}}, in the text to refer to them.
\paragraph{Captions and Core Message}
\label{appendix:captions}
Each figure should have a caption that makes a clear statement about this
figure, as such a statement makes it easier for the reader to (in)validate the
figure as evidence for the claim we make. Traditionally, figures often have a
caption indicating its content:\\ {\color{pairedTwoDarkBlue} \textit{$\cdot$
Speedup of approach A vs approach B on system X}}\\ {\color{pairedTwoDarkBlue}
\textit{$\cdot$ Architecture diagram of our solution}}\\ While these statements
clearly state the content of a figure at the meta-level, they often lack
information about the precise content and the claim a figure is meant to
evidence. While knowing that a figure is an architecture diagram is useful for
the reader when looking at the figure the reader automatically asks two
questions: (a) what properties set this architecture apart and (b) does its
implementation deliver the claimed properties? Or, in more general terms, what
claims do we aim to evidence with this figure and does the figure provide the
needed evidence to support our claims? In theory, this information could be
contained in the text of the paper, but to optimize for readers who skim the
figures first, we want to offer them as part of the caption. Nevertheless, it
makes often sense to word the caption strategically to still document the
meta-level content of a figure.\\ $\to$ {\color{pairedFourDarkGreen}
\textit{$\cdot$ Approach A is consistently faster than approach B, except for
inputs that are not used in practice}}\\ $\to$ {\color{pairedFourDarkGreen}
\textit{$\cdot$ The architecture of our design increases reusability by making
components A, B, \& C independent of the core.}} For example, after reading the
last caption the reader can validate if the architecture design indeed enables
the promised independence, and we can double-check while drafting the paper that
our figure is visualized to facilitate checking if it works as evidence. ! This
does not mean we should mislead with our figure but rather make things easy to
check. If our figure or data would not support our claim, it should be similarly
easy to invalidate our claim!
\subsubsection{Plots} We use matplotlib to create performance
plots such as \autoref{fig:speedup}. We use the following
formatting guidelines:
\begin{itemize}
\item Use a vertical y-label to make it easier to read.
\item Remove top and right frames to reduce visual noise
and allow the reader to focus on the data in the
figure.
\item Provide the concrete data at the top of each bar.
\end{itemize}
\noindent
We also suggest to follow these technical remarks:
\begin{itemize}
\item Create pdf plots and do not use bitmap formats (e.g., png) to
ensure high quality when zooming in.
\item Avoid Type-3 bitmap fonts by
setting fonttype to 42.
\end{itemize}
\begin{figure}
\includegraphics[width=\columnwidth]{plots/speedup}
\caption{Improved running speed after 4 weeks of training.
}
\label{fig:speedup}
\end{figure}
\subsubsection{Tables} We optimize our tables for readability by removing as
much clutter as possible, while highlighting the key structure. Markus Püschel
(see doc/paper-writing/guide-tables.pdf) wrote a nice guide on how to make nice
tables. \autoref{tab:simple_table} illustrates this with a simple
table.
\begin{table}
\ra{1.2}
\centering
\begin{tabular}{l l l r}
\toprule
\textbf{Animal} & \textbf{Size} & \textbf{Biotope} & \textbf{Age}\\
\midrule
Dog & Medium & Ground & 20\\
Cat & Medium & Ground &20 \\
Ant & Small & Ground & 30 \\
Elephant & Large & Ground & 70\\
Whale & Large & Water & 100\\
Salmon & Medium & Water & 13 \\
Eagle & Large & Air & 35 \\
\bottomrule
\end{tabular}
\vspace{1em}
\caption{A table with heigh lines and emphasized header.}
\label{tab:simple_table}
\end{table}
\subsubsection{Listings} We aim to use minted to create listings as much as
possible, as this allows us to edit code quickly. We use syntax highlighting
to make the parts of the code that matter most stand out. Hence, we keep
most code black, comments gray, and highlight just the MLIR operands that
we care about most.
\begin{listing}[H]
% We cannot put '{' on a line after % in draftonly mode, as the hack we used to
% not include the draft section will interpret the listing as normal
% latex where '%' is a comment and {} need to match, which they will
% not if only one is commented.
\begin{mlir}
// This is a comment
def @foo(%0 : !dialect.type)
{
%a = dialect.op(%0) : !dialect.type // $\color{black}\circled{a}$
}
\end{mlir}
\caption{A simple MLIR code example with markers. Markers can also be placed in
captions and refer to labels, e.g. \circled[lst:example]{a}.}
\label{lst:example}
\end{listing}
\begin{listing}[H]
\begin{lean4}
theorem funext {f₁ f₂ : ∀ (x : α), β x}
(h : ∀ x, f₁ x = f₂ x) : f₁ = f₂ := by
show extfunApp (Quotient.mk' f₁) =
extfunApp (Quotient.mk' f₂)
apply congrArg
apply Quotient.sound
exact h
\end{lean4}
\caption{A simple Lean4 code example, taken from
\url{https://lean-lang.org/lean4/doc/syntax\_highlight\_in\_latex.html\#example-with-minted}.}
\end{listing}
The syntax highlighting also works for xDSL-like IRs. Notice that different
minted styles can be used for different environments. The xDSL environment uses
the murphy-style in this case, whereas the MLIR version applies the
colorful-style.
\begin{xdsl*}{fontsize=\scriptsize}
func.func() [sym_name = "main", function_type = !fun<[
!iterators.columnar_batch<!tuple<[!i64]>>
], []>] {
^bb0(%0 : !iterators.columnar_batch<!tuple<[!i64]>>):
%t : !iterators.stream<!llvm.struct<[!i64]>> =
iterators.scan_columnar_batch(%0 : ...)
%filtered : !iterators.stream<!llvm.struct<[!i64]>> =
iterators.filter(%input : …) [predicateRef = @s0]
iterators.sink(%filtered : !iterators.stream<!tuple<[!i64]>>)
func.return()
}
func.func() [sym_name = "s0", function_type = !fun<[
!llvm.struct<[!i64]>], [!i1]>] {
^bb0(%struct : !llvm.struct<[!i64]>):
%id : !i64 = llvm.extractvalue(%struct : ...)
[position = [0 : !index]]
%five : !i64 = arith.constant() [value = 5 : !i64]
%cmp : !i1 = arith.cmpi(%id : !i64, %five : !i64)
[predicate = 4 : !i64]
func.return(%cmp : !i1)
}
\end{xdsl*}
\section{Writing}
A couple of hints with respect to how we write text.
\subsection{Citations}
\label{appendix:citations}
\subsubsection{Do not use numerical citations as nouns}
Especially when working with numerical citations (e.g., [1]) the use of
citations as nouns reduces readability. Hence, we do not use numerical citations
as nouns and instead expand these citations with \texttt{\textbackslash{}citet} to the
authornames.
\\
{\color{pairedTwoDarkBlue}
\textit{[1] showed that .. $\dots$}}\\
$\to$ {\color{pairedFourDarkGreen}\textit{Author et al. [1] showed}}
\subsubsection{Prefer meaningful text over citations as textual content}
While acknowledging authors of work is important, maximizing the amount of technical
content (outside of a historic perspective) typically makes text more direct and
concrete. Hence, we avoid the discussion of who did what in text if the
historic context does not add meaning or empty words can be replaced by an immediate
citation. E.g, in the following the words `introduced in` are not carrying
information and can be dropped.\\
{\color{pairedTwoDarkBlue}
\textit{we extend PreviousIdea introduced in [1] $\dots$ by}}\\
$\to$ {\color{pairedFourDarkGreen}\textit{we extend PreviousIdea [1] by}}
\subsubsection{Managing acronyms automatically}
Managing acronyms manually can lead to situations where the specific term is not properly expanded upon first use or when it is introduced.
The \texttt{acronym} package is useful to avoid such situations and provides full control over acronyms.
The expanded form of an abbreviation should be in lowercase, unless its parts are also capitalized (e.g., United Kingdom for UK).
For example, assume we have defined an acronym with \texttt{\textbackslash{}newacronym\{ir\}\{IR\}\{intermediate representation\}}:
\begin{itemize}
\item Upon first use of \texttt{\textbackslash{}ac\{ir\}} we get: \ac{ir}.
\item On the second reference: \ac{ir}.
\item To force expansion (e.g., for the background section where the term is first described), we use \texttt{\textbackslash{}acf\{ir\}} which gives: \acf{ir}.
\item To force contraction (e.g., to save space for a figure caption), we use \texttt{\textbackslash{}acs\{ir\}} which gives: \acs{ir}.
\item To obtain plural form, we use \texttt{\textbackslash{}acp\{ir\}} giving: \acp{ir}.
\end{itemize}
\end{draftonly}
\end{document}