-
Notifications
You must be signed in to change notification settings - Fork 0
/
AEC.html
110 lines (110 loc) · 9.98 KB
/
AEC.html
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
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml" lang="" xml:lang="">
<head>
<meta charset="utf-8" />
<meta name="generator" content="pandoc" />
<meta name="viewport" content="width=device-width, initial-scale=1.0, user-scalable=yes" />
<meta name="author" content="Yufei Cai" />
<meta name="author" content="Paolo G. Giarrusso" />
<meta name="author" content="Tillmann Rendel" />
<meta name="author" content="Klaus Ostermann" />
<title>Incremental λ-Calculus: Artifact Evaluation</title>
<style>
code{white-space: pre-wrap;}
span.smallcaps{font-variant: small-caps;}
span.underline{text-decoration: underline;}
div.column{display: inline-block; vertical-align: top; width: 50%;}
div.hanging-indent{margin-left: 1.5em; text-indent: -1.5em;}
ul.task-list{list-style: none;}
</style>
<link rel="stylesheet" href="ilc.css" />
<!--[if lt IE 9]>
<script src="//cdnjs.cloudflare.com/ajax/libs/html5shiv/3.7.3/html5shiv-printshiv.min.js"></script>
<![endif]-->
</head>
<body>
<header id="title-block-header">
<h1 class="title">Incremental λ-Calculus: Artifact Evaluation</h1>
<p class="author">Yufei Cai</p>
<p class="author">Paolo G. Giarrusso</p>
<p class="author">Tillmann Rendel</p>
<p class="author">Klaus Ostermann</p>
<p class="date">University of Marburg</p>
</header>
<p>This is the submission to the PLDI 2014 Artifact Evaluation Committee for the paper:</p>
<ul class="incremental">
<li>Yufei Cai, Paolo G. Giarrusso, Tillmann Rendel, Klaus Ostermann.<br />
<a href="http://www.informatik.uni-marburg.de/~pgiarrusso/papers/pldi14-ilc-author-final.pdf"><strong>A Theory of Changes for Higher-Order Languages:</strong><br />
<strong>Incrementalizing λ-Calculi by Static Differentiation.</strong></a><br />
<em>To appear</em> at PLDI, ACM 2014.</li>
</ul>
<p>We submit three artifacts:</p>
<ol class="incremental" type="1">
<li><p>A <strong>machine-checked formalizations</strong> of our theoretical results, in the dependently-typed programming language Agda.</p></li>
<li><p>A <strong>prototype implementation</strong> of our ideas in Scala.</p></li>
<li><p>The <strong>raw data</strong> and <strong>detailed graphs</strong> of our benchmark.</p></li>
</ol>
<h1 id="quick-start">Quick Start</h1>
<ul class="incremental">
<li><p>Download the <a href="http://www.informatik.uni-marburg.de/~pgiarrusso/ILC/AEC/ilc-vm.ova">Virtual Machine Image</a> (~1.8GiB).</p></li>
<li><p>Install <a href="https://www.virtualbox.org/wiki/Downloads">VirtualBox</a> version 4.3.6 (<a href="#why-virtualbox-4.3.6">why?</a>).</p></li>
<li><p>Boot the downloaded virtual machine with VirtualBox.<br />
(You need 1.5GB of RAM and ~4.5GiB of disk space).</p></li>
<li><p>You will be automatically logged in on a Ubuntu system.</p></li>
</ul>
<p>The virtual machine contains everything you need to interact with our artifacts:</p>
<ul class="incremental">
<li><p>A local copy of this website (<code>start-here.html</code> on the desktop).</p></li>
<li><p>Our artifacts (subfolders of <code>ilc</code> on the desktop, links to the READMEs on the desktop).</p></li>
<li><p>Necessary software (Emacs, Eclipse, …) and configuration.</p></li>
</ul>
<p>More information about the virtual machine image is available <a href="#virtual-machine-image">below</a>.</p>
<h1 id="other-download-options">Other Download Options</h1>
<p>The Virtual Machine image (see <a href="#virtual-machine-image">below</a>) is probably the easiest way to interact with our artifacts, but we also provide the following alternatives:</p>
<ul class="incremental">
<li><p>Formalization in Agda.</p>
<p>Reviewers can <a href="http://www.informatik.uni-marburg.de/~pgiarrusso/ILC/AEC/ilc-agda.zip">download the Agda code</a>, <a href="http://www.informatik.uni-marburg.de/~pgiarrusso/ILC/AEC/agda/README.html">view Agda code in their browser</a> or use the virtual machine image (see below). More information about this artifact is in <a href="http://www.informatik.uni-marburg.de/~pgiarrusso/ILC/AEC/agda/README.html"><code>agda/README.agda</code></a>.</p>
<p>Note that the virtual machine image includes Agda (for type checking) and Emacs (for viewing and editing). We are not aware of any other Agda IDE. If you don’t want to use Emacs, you can <a href="http://www.informatik.uni-marburg.de/~pgiarrusso/ILC/AEC/agda/README.html">view the Agda code in your browser</a>. It is fully syntax-highlighted and cross-referenced, so for just reading the code, you don’t lose much over using Emacs.</p></li>
<li><p>Implementation in Scala.</p>
<p>Reviewers can <a href="http://www.informatik.uni-marburg.de/~pgiarrusso/ILC/AEC/ilc-scala-prototype.zip">download the Scala code</a> or use the virtual machine image (see below). More information about this artifact is in <a href="http://www.informatik.uni-marburg.de/~pgiarrusso/ILC/AEC/scala-prototype/README.html"><code>scala-prototype/README.md</code></a>.</p>
<p>Note that the virtual machine image includes SBT (for compilation) and the Eclipse-bases Scala IDE (for viewing and editing). If you want to use a different IDE for Scala, you have to <a href="http://www.informatik.uni-marburg.de/~pgiarrusso/ILC/AEC/ilc-scala-prototype.zip">download the Scala code</a> and set up SBT and the IDE of your choice.</p>
<p>If you install SBT on your own machine, make sure to run it with at least 8M of stack space and 1G of heap size (by passing <code>-Xss8M -Xmx1024m</code> to the JVM running SBT, or equivalently <code>-J-Xss8M -J-Xmx1024m</code> to SBT itself).</p></li>
<li><p>Benchmark results.</p>
<p>Reviewers can <a href="http://www.informatik.uni-marburg.de/~pgiarrusso/ILC/AEC/ilc-graphs.zip">download the data</a>, <a href="http://www.informatik.uni-marburg.de/~pgiarrusso/ILC/AEC/graphs/README.html">view the data in their browser</a> or use the virtual machine image (see below). More information about this artifact is in <a href="http://www.informatik.uni-marburg.de/~pgiarrusso/ILC/AEC/graphs/README.html"><code>graphs/README.md</code></a>.</p></li>
</ul>
<h1 id="virtual-machine-image">Virtual Machine Image</h1>
<p>The following virtual machine image contains all artifacts as well as the software we used to create and use the artifacts. Except maybe for Agda or Scala power users, this is probably the easiest way to interact with the artifacts.</p>
<ul class="incremental">
<li><a href="http://www.informatik.uni-marburg.de/~pgiarrusso/ILC/AEC/ilc-vm.ova">Virtual Machine Image</a> (~1.8GiB)</li>
</ul>
<p>This virtual machine contains a Ubuntu system. Inside the virtual machine, you will also find on the desktop:</p>
<ul class="incremental">
<li>a copy of this website inside the <code>ilc-website</code> folder (minus the VM image itself)</li>
<li>our artifacts in the <code>ilc</code> folder</li>
<li>support software inside <code>support-software</code></li>
</ul>
<h2 id="how-to-interact-with-the-agda-codebase">How to interact with the Agda codebase</h2>
<p>On the left-hand side you will also find links for Emacs and a terminal; Emacs is already set up for working with Agda, and the Agda README contains basic instructions for working with Emacs and for finding more information.</p>
<p>On the desktop, there’s a link to the Agda README which will open in Emacs.</p>
<h2 id="how-to-interact-with-the-scala-codebase">How to interact with the Scala codebase</h2>
<p>For compiling the Scala codebase and running tests, we preinstalled SBT and configured it to have enough memory (1G) and stack (8M) to compile and run our code with the big datasets we use. We reduced the maximum benchmark size to fit the virtual machine memory - we originally ran them with 4G of RAM on a 64bit virtual machine, but we preferred creating a 32bit VM with less RAM. Details on how to change the configuration are in the README for the Scala codebase.</p>
<p>We also preloaded Eclipse with the correct version of the Scala plugin (Scala IDE 3.0.2) on the virtual machine, and preloaded our project for it. However, Eclipse cannot compile the project from scratch unless SBT has already compiled the source code before. So for example, you have to compile with SBT once after each “clean” in Eclipse.</p>
<h2 id="virtual-machine-survival-guide">Virtual machine survival guide</h2>
<p>The VM is a mostly standard Ubuntu Linux 12.04 LTS system. Should you be unfamiliar with Ubuntu, or should you need info on the configuration, here is some survival information which might get you started.</p>
<ul class="incremental">
<li><p>Icons for programs you need should be either on the left or on the desktop; if not, click on the icon on the top left corner to access the “Dash” and follow instructions.</p></li>
<li><p>After you maximize a window, you need to hover over the left-hand corner to see the close/minimize/demaximize buttons.</p></li>
<li><p>This virtual machine is set up for:</p>
<ul class="incremental">
<li>Timezone: UTC.</li>
<li>Keyboard layout: US (apparently your layout does not make a difference).</li>
</ul>
<p>To change those settings, use the “System Settings” icon (on the left).</p></li>
<li><p>The main user has username <code>vagrant</code> and password <code>vagrant</code>. To perform privileged operations, you might be asked for password of this user.</p></li>
<li><p>Should you need Haskell (for the Agda codebase), you should just need to install haskell-platform.</p></li>
</ul>
<h2 id="why-virtualbox-4.3.6">Why VirtualBox 4.3.6?</h2>
<p>We package the virtual machine in the standardized OVF format. Therefore, at least in <em>theory</em> the virtual machine should work with other versions of VirtualBox. It should even work with VMWare, though the guest contains optimized drivers for VirtualBox (VirtualBox Guest Additions 4.3.6) but not for VMWare (so it will at least be less performant on VMWare).</p>
<p>However, we have only tested running the VM on OS X, Windows and Linux systems with VirtualBox 4.3.6, and workarounded the VirtualBox bugs we did find (we had to disable 3D acceleration to ensure scrolling would work in Emacs). Whether other VirtualBox versions will work depends entirely on VirtualBox and is outside of our control — even though usually VirtualBox does work.</p>
</body>
</html>