@font-face {
  font-family: "CMU Sans Serif";
  src: url("fonts/cmunss.otf") format("opentype");
  font-weight: 400;
}
@font-face {
  font-family: "CMU Sans Serif";
  src: url("fonts/cmunsx.otf") format("opentype");
  font-weight: 700;
}

:root {
  /* method colors, as in the paper's figures */
  --docker: #1c39bb;
  --estargz: #b4745e;
  --twodfs: #00a693;
  --mitrafsnap: #cc3333;
  /* dark theme, the default */
  --bg: #111318;
  --panel: #191c23;
  --line: #2b303b;
  --text: #e8eaef;
  --muted: #9aa2b1;
  --accent: var(--mitrafsnap);
  --accent-text: #ef6b6b;
  --video-bg: #0b0c10;
  --upd: #7d95ff;
  --upd-fill: rgba(125, 149, 255, .20);
  --sel-fill: rgba(204, 51, 51, .28);
  color-scheme: dark;
  font: 19px/1.55 "CMU Sans Serif", ui-sans-serif, system-ui, sans-serif;
}
:root[data-theme="light"] {
  --bg: #ffffff;
  --panel: #f5f6f8;
  --line: #dfe2e8;
  --text: #15171c;
  --muted: #5b6270;
  --accent-text: #b82a2a;
  --video-bg: #0f1115;
  --upd: #1c39bb;
  --upd-fill: rgba(28, 57, 187, .10);
  --sel-fill: rgba(204, 51, 51, .14);
  color-scheme: light;
}

* { box-sizing: border-box; }
html, body { margin: 0; }
body { background: var(--bg); color: var(--text); }
a { color: var(--accent-text); }
.wrap { max-width: 1120px; margin: 0 auto; padding: 0 24px; }
section.wrap { margin-top: 64px; }
h2 { font-size: 34px; margin: 0 0 14px; }
h3 { font-size: 23px; margin: 6px 0; }
p { margin: 0 0 14px; text-align: justify; hyphens: auto; }
em { font-style: normal; font-weight: 700; }

.hero { border-bottom: 1px solid var(--line); padding: 24px 0 52px; }
html { scroll-behavior: smooth; scroll-padding-top: 76px; }
.topbar {
  position: sticky; top: 0; z-index: 10; background: var(--bg);
  border-bottom: 1px solid transparent; transition: border-color .3s ease;
}
.topbar.scrolled { border-bottom-color: var(--line); }
.bar { display: flex; justify-content: space-between; align-items: center; gap: 16px; height: 64px; }
.nav { align-items: center; }
/* the name slides in once the title has scrolled away */
.nav .brand {
  color: var(--mitrafsnap); font-weight: 700; font-size: 22px;
  max-width: 0; opacity: 0; overflow: hidden; white-space: nowrap; margin-right: 0;
  transform: translateY(6px); pointer-events: none;
  transition: max-width .4s ease, opacity .3s ease, transform .4s ease, margin-right .4s ease;
}
.topbar.scrolled .nav .brand { max-width: 160px; opacity: 1; margin-right: calc(var(--gap) + 4px); transform: none; pointer-events: auto; }
.nav .brand:hover { color: var(--mitrafsnap); }
.to-top {
  position: fixed; right: 24px; bottom: 24px; z-index: 10; width: 44px; height: 44px;
  display: inline-flex; align-items: center; justify-content: center; padding: 0; cursor: pointer;
  color: var(--text); background: var(--panel); border: 1px solid var(--line); border-radius: 50%;
  opacity: 0; transform: translateY(12px); pointer-events: none; transition: opacity .3s ease, transform .3s ease;
}
.to-top.shown { opacity: 1; transform: none; pointer-events: auto; }
.to-top:hover { border-color: var(--muted); }
.to-top svg { width: 20px; height: 20px; fill: none; stroke: currentColor; stroke-width: 2; stroke-linecap: round; stroke-linejoin: round; }
@media (prefers-reduced-motion: reduce) {
  html { scroll-behavior: auto; }
  .nav .brand, .to-top, .topbar { transition: none; }
}
.nav { display: flex; flex-wrap: nowrap; min-width: 0; --gap: 20px; }
.links { display: flex; }
.links a + a { margin-left: var(--gap); }
.actions { display: flex; gap: 10px; align-items: center; }
.theme.menu { display: none; }
.menu svg { stroke-width: 2; }
.menu .close-icon, .topbar.open .menu .open-icon { display: none; }
.topbar.open .menu .close-icon { display: block; }
.nav a { flex-shrink: 0; }
.nav a { color: var(--muted); text-decoration: none; font-size: 18px; }
.nav a:hover { color: var(--text); }
.theme {
  display: inline-flex; align-items: center; justify-content: center; width: 38px; height: 38px;
  color: var(--text); background: var(--panel); border: 1px solid var(--line); border-radius: 8px;
  padding: 0; cursor: pointer;
}
.theme svg { width: 20px; height: 20px; fill: none; stroke: currentColor; stroke-width: 1.8; stroke-linecap: round; }
.theme .moon { fill: currentColor; stroke: none; }
:root[data-theme="light"] .theme .sun, :root:not([data-theme="light"]) .theme .moon { display: none; }
.theme:hover { border-color: var(--muted); }
.hero h1 { font-size: 76px; margin: 0; line-height: 1.05; color: var(--mitrafsnap); }
.hero .lead { font-size: 32px; margin: 10px 0 20px; text-align: left; hyphens: manual; }
.hero .intro { font-size: 20px; color: var(--muted); }

.feature video, .videos video {
  width: 100%; display: block; border-radius: 10px; border: 1px solid var(--line); background: var(--video-bg);
}
.fig { margin: 8px 0 24px; }
/* figures drawn as inline SVG in the page's own colors */
.dg { width: 100%; height: auto; display: block; }
.dg text { fill: var(--text); font-family: inherit; font-size: 14px; }
.dg .small { font-size: 12.5px; }
.dg .title { font-size: 16px; font-weight: 700; }
.dg .strong { font-weight: 700; }
.dg .muted { fill: var(--muted); }
.dg .mono { font-family: ui-monospace, SFMono-Regular, Menlo, monospace; }
.dg .panel { fill: var(--panel); stroke: var(--line); }
.dg .box, .dg .cell { fill: var(--bg); stroke: var(--muted); stroke-width: 1; }
.dg .frame { fill: none; }
.dg .mfs { stroke: var(--mitrafsnap); stroke-width: 1.8; }
.dg .upd { fill: var(--upd-fill); stroke: var(--upd); stroke-width: 1.6; }
.dg .sel { fill: var(--sel-fill); stroke: var(--mitrafsnap); stroke-width: 1.6; }
.dg .partial { fill: var(--panel); stroke: var(--muted); }
.dg .lazy { stroke-dasharray: 5 4; }
.dg .faded { opacity: .55; }
.dg .toc { fill: var(--mitrafsnap); }
.dg .flow { fill: none; stroke: var(--text); stroke-width: 1.5; }
.dg .ondemand { stroke-dasharray: 2 4; stroke-linecap: round; }
.dg .ah { fill: var(--text); }
.dg .x { stroke: var(--upd); stroke-width: 1.8; }
.dg .step circle { fill: var(--bg); stroke: var(--text); stroke-width: 1.3; }
.dg .step text { font-size: 12px; font-weight: 700; text-anchor: middle; }
.figs { display: grid; grid-template-columns: repeat(2, minmax(0, 1fr)); gap: 24px; align-items: start; margin-top: 8px; }
.figs .fig { margin: 0 0 14px; }
code { font-size: .9em; }
.caption, figcaption { color: var(--muted); font-size: 17px; margin-top: 10px; text-align: center; }

.cards { display: grid; grid-template-columns: repeat(3, minmax(0, 1fr)); gap: 16px; margin: 8px 0 14px; }
.card { background: var(--panel); border: 1px solid var(--line); border-radius: 10px; padding: 18px 20px; }
.card p { font-size: 17px; color: var(--muted); margin: 0; }
.note { color: var(--muted); font-size: 17px; }


.videos { display: grid; grid-template-columns: repeat(2, minmax(0, 1fr)); gap: 20px; margin: 10px 0 20px; }
.videos figure { margin: 0; }

table { border-collapse: collapse; width: 100%; font-size: 17px; margin-top: 8px; }
th, td { padding: 8px 10px; border-bottom: 1px solid var(--line); text-align: right; }
th:first-child, td:first-child { text-align: left; }
thead th { font-weight: 700; }
td.best { font-weight: 700; color: var(--accent-text); }
.key { display: inline-block; width: 26px; height: 14px; border: 1px solid #111; margin-right: 8px; vertical-align: -2px; }
.key.docker { background: url("data:image/svg+xml,%3Csvg%20xmlns%3D%22http%3A//www.w3.org/2000/svg%22%20width%3D%2210%22%20height%3D%2210%22%3E%3Crect%20width%3D%2210%22%20height%3D%2210%22%20fill%3D%22%231c39bb%22/%3E%3Cg%20fill%3D%22none%22%20stroke%3D%22%23111%22%20stroke-width%3D%221.1%22%3E%3Cpath%20d%3D%22M-2.5%2C2.5l5%2C-5M0%2C10l10%2C-10M7.5%2C12.5l5%2C-5%22/%3E%3C/g%3E%3C/svg%3E"); }
.key.estargz { background: url("data:image/svg+xml,%3Csvg%20xmlns%3D%22http%3A//www.w3.org/2000/svg%22%20width%3D%2212%22%20height%3D%2212%22%3E%3Crect%20width%3D%2212%22%20height%3D%2212%22%20fill%3D%22%23b4745e%22/%3E%3Cg%20fill%3D%22none%22%20stroke%3D%22%23111%22%20stroke-width%3D%221.1%22%3E%3Cpolygon%20points%3D%226.00%2C2.60%206.85%2C4.83%209.23%2C4.95%207.38%2C6.45%208.00%2C8.75%206.00%2C7.45%204.00%2C8.75%204.62%2C6.45%202.77%2C4.95%205.15%2C4.83%22/%3E%3C/g%3E%3C/svg%3E"); }
.key.twodfs { background: url("data:image/svg+xml,%3Csvg%20xmlns%3D%22http%3A//www.w3.org/2000/svg%22%20width%3D%2210%22%20height%3D%2210%22%3E%3Crect%20width%3D%2210%22%20height%3D%2210%22%20fill%3D%22%2300a693%22/%3E%3Cg%20fill%3D%22none%22%20stroke%3D%22%23111%22%20stroke-width%3D%221.1%22%3E%3Cpath%20d%3D%22M-2.5%2C2.5l5%2C-5M0%2C10l10%2C-10M7.5%2C12.5l5%2C-5M-2.5%2C7.5l5%2C5M0%2C0l10%2C10M7.5%2C-2.5l5%2C5%22/%3E%3C/g%3E%3C/svg%3E"); }
.key.mitrafsnap { background: url("data:image/svg+xml,%3Csvg%20xmlns%3D%22http%3A//www.w3.org/2000/svg%22%20width%3D%2210%22%20height%3D%2210%22%3E%3Crect%20width%3D%2210%22%20height%3D%2210%22%20fill%3D%22%23cc3333%22/%3E%3Cg%20fill%3D%22none%22%20stroke%3D%22%23111%22%20stroke-width%3D%221.1%22%3E%3Ccircle%20cx%3D%225%22%20cy%3D%225%22%20r%3D%221.9%22/%3E%3C/g%3E%3C/svg%3E"); }
table.results td:last-child { white-space: nowrap; }

.repos { list-style: none; padding: 0; margin: 0; display: grid; gap: 10px; }
.repos li { display: flex; gap: 14px; flex-wrap: wrap; align-items: baseline; }
.repos a, .repos .private { font-weight: 700; min-width: 190px; }
.repos .private { color: var(--muted); }
.repos span:last-child { color: var(--muted); font-size: 17px; }

section.wrap.last { margin-bottom: 80px; }

@media (max-width: 900px) {
  .cards, .videos, .figs { grid-template-columns: minmax(0, 1fr); }
}
@media (max-width: 560px) {
  :root { font-size: 17px; }
  .wrap { padding: 0 16px; }
  .hero { padding: 12px 0 36px; }
  .theme.menu { display: inline-flex; }
  .wrap.bar { position: relative; }
  /* the links drop down under the bar */
  .links {
    display: none; position: absolute; top: 64px; left: 0; right: 0; flex-direction: column;
    background: var(--bg); border-bottom: 1px solid var(--line); padding: 4px 16px 10px;
  }
  .topbar.open .links { display: flex; }
  .links a + a { margin-left: 0; }
  .links a { padding: 10px 0; font-size: 18px; border-top: 1px solid var(--line); }
  .links a:first-child { border-top: 0; }
  .topbar.open { border-bottom-color: var(--line); }
  .nav .brand { font-size: 18px; }
  .to-top { right: 16px; bottom: 16px; }
  .hero h1 { font-size: clamp(40px, 13vw, 52px); }
  .hero .lead { font-size: 25px; }
  h2 { font-size: 28px; }
  table.results td:last-child { white-space: normal; }
  .table-wrap { overflow-x: auto; }
}