/* Metamath Zero — homepage. Theme-aware base16, the same palette the explorer and editor speak, so the site is made of the same material as the tools it points at. `light-dark()` keeps each colour's two values together; `color-scheme` decides which applies, and the toggle pins it by stamping `data-theme` on . The accents are not decoration. Each already means something in the ecosystem and means the same here: term = blue, axiom = orange, theorem = purple, sort/hypothesis = green. */ /* The wordmark's face, subset to what a heading can hold. EB Garamond is cut at two optical sizes and this is the one for small text: beside the text cut it carries a x-height .71 of its cap against .62, and a stem 22% heavier, so it holds up at the sizes this page sets and the text cut reads thin. It is held here rather than fetched, so the page makes no third party request. site/README.md has the command that builds it, and its licence sits beside it. */ @font-face { font-family: "EB Garamond 08"; src: url("fonts/EBGaramond08.woff2") format("woff2"); font-weight: 400; font-style: normal; font-display: swap; } :root { color-scheme: light dark; --bg: light-dark(#fbfbfb, #181818); --panel: light-dark(#f2f2f2, #1f1f1f); --raised: light-dark(#ffffff, #202124); --fg: light-dark(#2b2b2b, #d8d8d8); --dim: light-dark(#5b5b5b, #9a9a9a); --faint: light-dark(#9b9b9b, #5a5a5a); --border: light-dark(#e0e0e0, #333333); --hair: light-dark(#ececec, #262626); --term: light-dark(#26647e, #7cafc2); --axiom: light-dark(#9c520f, #dc9656); --thm: light-dark(#834876, #ba8baf); --sort: light-dark(#4c6a12, #a1b56c); --link: light-dark(#26647e, #8fbccc); --shadow: light-dark(0 1px 2px rgba(20,30,40,.06), 0 1px 2px rgba(0,0,0,.4)); --mono: ui-monospace, "SF Mono", SFMono-Regular, "JetBrains Mono", Menlo, Consolas, "Liberation Mono", monospace; --sans: system-ui, -apple-system, "Segoe UI", Roboto, Helvetica, Arial, sans-serif; /* The headings, and the name in the nav: the readme's wordmark is EB Garamond, and this is that face where it is installed, an old style serif of the same build where it is not. */ --serif: "EB Garamond 08", "EB Garamond", Garamond, "Adobe Garamond Pro", "Iowan Old Style", "Palatino Linotype", Palatino, Georgia, serif; --edge: clamp(1.1rem, 5vw, 4rem); /* page side padding */ --wide: 1080px; /* content column */ } :root[data-theme="light"] { color-scheme: light; } :root[data-theme="dark"] { color-scheme: dark; } * { box-sizing: border-box; } html { scroll-behavior: smooth; } @media (prefers-reduced-motion: reduce) { html { scroll-behavior: auto; } } body { margin: 0; background: var(--bg); color: var(--fg); font-family: var(--sans); font-size: 16px; line-height: 1.6; -webkit-font-smoothing: antialiased; text-rendering: optimizeLegibility; } a { color: var(--link); text-decoration: none; } a:hover { text-decoration: underline; text-underline-offset: 3px; } code { font-family: var(--mono); font-size: .92em; } :focus-visible { outline: 2px solid var(--term); outline-offset: 3px; border-radius: 2px; } .skip { position: absolute; left: -999px; top: 0; background: var(--term); color: var(--bg); padding: .5rem .9rem; z-index: 20; } .skip:focus { left: .5rem; top: .5rem; } /* The mark, defined once in the page and instanced with . It is stroked in currentColor, so it follows the theme and whatever colour it sits in. 1.205 : 1 is its own aspect; `height` is the only size to set. */ .sprite { position: absolute; width: 0; height: 0; overflow: hidden; } .mark { flex: none; width: 1.205em; height: 1em; } /* Semantic accent helpers. */ .c-term { color: var(--term); } .c-axiom { color: var(--axiom); } .c-thm { color: var(--thm); } .c-sort { color: var(--sort); } .dim { color: var(--dim); } /* ---------------------------------------------------------------- nav */ .nav { position: sticky; top: 0; z-index: 10; display: flex; align-items: center; gap: 1rem; padding: .6rem var(--edge); background: color-mix(in srgb, var(--bg) 88%, transparent); backdrop-filter: blur(8px); border-bottom: 1px solid var(--hair); } /* The bar's height is set by the theme switch, 34px, so the lockup has room to be read rather than merely present: at 1.7rem with the line box closed up to the type, it stands 27.9px in a bar that does not move. */ .wordmark { display: block; white-space: nowrap; color: var(--fg); font-family: var(--serif); font-size: 1.7rem; line-height: 1; } .wordmark:hover { text-decoration: none; } /* The readme's lockup, in miniature: the mark stands 1.55 cap heights tall and .85 of one clear of the word, and its middle sits on the middle of the M. EB Garamond 08's cap height is .596em, which is where these numbers come from; the mark's own baseline is its bottom edge, so centring it means lowering that by half its height less half the cap height. vertical-align rather than a flex baseline, which chromium and firefox synthesize differently for an inline svg. */ .wordmark .mark { width: 1.113em; height: 0.924em; vertical-align: -0.164em; margin-right: 0.507em; } .nav .links { margin-left: auto; display: flex; gap: clamp(.8rem, 3vw, 1.7rem); } .nav .links a { color: var(--dim); font-family: var(--sans); font-size: .92rem; letter-spacing: .01em; } .nav .links a:hover { color: var(--fg); text-decoration: none; } .theme { flex: none; display: grid; place-items: center; width: 34px; height: 34px; padding: 0; background: none; border: 1px solid var(--border); border-radius: 7px; color: var(--dim); cursor: pointer; } .theme:hover { color: var(--fg); border-color: var(--dim); } .theme svg { width: 17px; height: 17px; fill: none; stroke: currentColor; stroke-width: 1.6; } /* section rhythm */ main { display: block; } section { padding-left: var(--edge); padding-right: var(--edge); } .eyebrow { margin: 0 0 1rem; font-family: var(--mono); font-size: .74rem; letter-spacing: .16em; text-transform: uppercase; color: var(--faint); } .section-head { max-width: 46rem; margin: 0 auto; } .section-head.center { text-align: center; } .section-head h2 { margin: 0 0 .6rem; } .section-head p { margin: 0; } h1, h2, h3 { font-family: var(--serif); font-weight: 400; line-height: 1.2; } /* ---------------------------------------------------------------- hero */ .hero { max-width: var(--wide); margin: 0 auto; padding-top: clamp(2.4rem, 7vw, 4.5rem); padding-bottom: clamp(1.2rem, 3vw, 1.8rem); } .hero h1 { margin: 0 0 1rem; font-size: clamp(1.75rem, 3.7vw, 2.55rem); } .hero .lede { max-width: 42rem; margin: 0 0 1.6rem; font-size: clamp(1.02rem, 2vw, 1.2rem); color: var(--dim); } .hero .lede em { font-style: normal; color: var(--fg); } .cta { display: flex; flex-wrap: wrap; gap: .8rem; } .btn { display: inline-flex; align-items: center; gap: .45rem; padding: .62rem 1.15rem; border-radius: 8px; font-family: var(--sans); font-size: .95rem; font-weight: 500; border: 1px solid var(--border); color: var(--fg); } .btn:hover { text-decoration: none; border-color: var(--dim); } .btn.primary { background: var(--term); border-color: var(--term); color: var(--bg); } .btn.primary:hover { filter: brightness(1.08); } /* SIGNATURE — the verification pipeline with its trust boundary. */ .pipe { margin: 0; padding: clamp(1.1rem, 3vw, 1.8rem); display: flex; flex-wrap: wrap; align-items: stretch; gap: clamp(.7rem, 2.5vw, 1.5rem); border: 1px solid var(--border); border-radius: 14px; background: var(--panel); } .pipe-untrusted { position: relative; flex: 1 1 auto; display: flex; align-items: center; flex-wrap: wrap; gap: clamp(.6rem, 2vw, 1.1rem); padding: 1.5rem 1.1rem .95rem; border: 1px dashed var(--border); border-radius: 11px; } .pipe-band { display: none; } .pipe-label { position: absolute; top: -.72rem; left: 1rem; padding: 0 .5rem; background: var(--panel); font-family: var(--mono); font-size: .68rem; letter-spacing: .06em; text-transform: uppercase; color: var(--faint); } .pipe-trusted { position: relative; flex: 0 0 auto; display: flex; align-items: center; padding: 1.5rem 1.1rem .95rem; border: 1px solid var(--term); border-radius: 11px; background: color-mix(in srgb, var(--term) 9%, transparent); } .pipe-trusted .pipe-label { background: var(--bg); color: var(--term); } .node-pair { display: flex; gap: .6rem; } .node { display: flex; flex-direction: column; gap: .15rem; padding: .5rem .8rem; min-width: 5.4rem; background: var(--raised); border: 1px solid var(--border); border-radius: 9px; box-shadow: var(--shadow); color: var(--fg); } .node:hover { text-decoration: none; border-color: var(--dim); transform: translateY(-1px); } @media (prefers-reduced-motion: reduce) { .node:hover { transform: none; } } .node-kind { font-family: var(--mono); font-weight: 600; font-size: 1rem; } .node-role { font-family: var(--sans); font-size: .74rem; color: var(--dim); } .node.check { border-color: var(--term); background: var(--raised); } .node.check .node-kind { color: var(--term); } .arrow { color: var(--faint); font-family: var(--mono); align-self: center; } .arrow.big { font-size: 1.4rem; align-self: center; } /* ---------------------------------------------------------------- pillars */ .pillars { max-width: var(--wide); margin: 0 auto; padding-top: clamp(2.5rem, 6vw, 4rem); padding-bottom: clamp(2.5rem, 6vw, 4rem); display: grid; grid-template-columns: repeat(2, 1fr); gap: 1px; background: var(--hair); border: 1px solid var(--hair); border-radius: 12px; overflow: hidden; } .pillars article { background: var(--bg); padding: clamp(1.3rem, 3vw, 2rem); } .pillars h2 { margin: 0 0 .55rem; font-size: 1.26rem; } .pillars p { margin: 0; color: var(--dim); font-size: .96rem; } .pillars code { color: var(--fg); } /* ---------------------------------------------------------------- code sample */ .sample { max-width: var(--wide); margin: 0 auto; padding-top: 0; padding-bottom: clamp(2.5rem, 6vw, 4rem); } /* How it works — the pipeline band, now its own section under the code. */ .how { max-width: var(--wide); margin: 0 auto; padding-top: clamp(2rem, 5vw, 3.2rem); padding-bottom: clamp(2.5rem, 6vw, 4rem); } .how .section-head { text-align: center; margin: 0 auto clamp(1.4rem, 3vw, 2rem); } .sample-head { max-width: 44rem; margin: 0 0 1.6rem; } .sample-head h2 { margin: 0 0 .5rem; font-size: clamp(1.58rem, 3.3vw, 2.15rem); } .sample-head p { margin: 0; } .code { border: 1px solid var(--border); border-radius: 12px; overflow: hidden; background: var(--raised); } .tabs { display: flex; align-items: center; gap: .25rem; padding: .4rem .5rem; background: var(--panel); border-bottom: 1px solid var(--border); } .tabs [role="tab"] { padding: .35rem .7rem; border: 0; border-radius: 7px; cursor: pointer; background: none; color: var(--dim); font-family: var(--mono); font-size: .82rem; font-weight: 600; } .tabs [role="tab"]:hover { color: var(--fg); } .tabs [role="tab"][aria-selected="true"] { background: var(--raised); color: var(--fg); box-shadow: var(--shadow); } .tab-sub { font-weight: 400; color: var(--faint); font-size: .74rem; } .tabs [role="tab"][aria-selected="true"] .tab-sub { color: var(--dim); } .verified { margin-left: auto; padding: .2rem .6rem; border-radius: 20px; font-family: var(--mono); font-size: .72rem; letter-spacing: .03em; color: var(--sort); border: 1px solid color-mix(in srgb, var(--sort) 45%, transparent); background: color-mix(in srgb, var(--sort) 9%, transparent); } .code pre { margin: 0; padding: clamp(1rem, 2.5vw, 1.5rem); overflow-x: auto; } .code code { font-family: var(--mono); font-size: clamp(.78rem, 1.7vw, .9rem); line-height: 1.7; color: var(--fg); } .code .kw { color: var(--dim); } .code .cm { color: var(--faint); font-style: italic; } .sample-foot { margin: 1rem 0 0; font-size: .85rem; } /* ---------------------------------------------------------------- explore */ .explore { padding-top: clamp(2.5rem, 6vw, 4rem); padding-bottom: clamp(2.5rem, 6vw, 4rem); } .explore .section-head { text-align: center; margin-bottom: clamp(1.6rem, 4vw, 2.5rem); } .explore .section-head h2 { font-size: clamp(1.7rem, 3.9vw, 2.38rem); } .cards { max-width: var(--wide); margin: 0 auto; display: grid; grid-template-columns: repeat(3, 1fr); gap: 1rem; } .card { display: flex; flex-direction: column; gap: .55rem; padding: clamp(1.2rem, 2.5vw, 1.6rem); background: var(--raised); border: 1px solid var(--border); border-radius: 12px; color: var(--fg); box-shadow: var(--shadow); } .card:hover { text-decoration: none; border-color: var(--dim); transform: translateY(-2px); } @media (prefers-reduced-motion: reduce) { .card:hover { transform: none; } } .card-mark { font-family: var(--mono); font-weight: 600; font-size: .78rem; letter-spacing: .08em; } .card h3 { margin: 0; font-size: 1.3rem; } .card p { margin: 0; flex: 1; color: var(--dim); font-size: .92rem; } .card code { color: var(--fg); } .card-go { font-family: var(--sans); font-size: .9rem; color: var(--link); font-weight: 500; } /* ---------------------------------------------------------------- learn + install */ .learn { max-width: var(--wide); margin: 0 auto; padding-top: clamp(2rem, 5vw, 3rem); padding-bottom: clamp(2.5rem, 6vw, 4rem); display: grid; grid-template-columns: 1fr 1fr; gap: clamp(1.5rem, 4vw, 3rem); align-items: start; } .learn .section-head { margin: 0 0 1.2rem; } .learn .section-head h2 { font-size: 1.7rem; } .doclist { list-style: none; margin: 0; padding: 0; display: flex; flex-direction: column; gap: .5rem; } .doclist a { display: block; padding: .85rem 1rem; border: 1px solid var(--border); border-radius: 10px; background: var(--raised); color: var(--fg); } .doclist a:hover { text-decoration: none; border-color: var(--dim); } .doc-name { display: block; font-family: var(--sans); font-weight: 600; font-size: 1rem; } .doc-tag { margin-left: .45rem; padding: .05rem .4rem; vertical-align: .08em; font-size: .64rem; letter-spacing: .06em; font-weight: 600; color: var(--axiom); border: 1px solid color-mix(in srgb, var(--axiom) 45%, transparent); border-radius: 4px; } .doc-desc { display: block; margin-top: .2rem; color: var(--dim); font-size: .86rem; } .steps { margin: 0; padding: 0; list-style: none; counter-reset: step; display: flex; flex-direction: column; gap: 1rem; } .steps li { counter-increment: step; } .step-note { display: block; margin-bottom: .5rem; color: var(--dim); font-size: .9rem; } .step-note::before { content: counter(step); margin-right: .55rem; display: inline-grid; place-items: center; width: 1.4rem; height: 1.4rem; vertical-align: -.35rem; font-family: var(--mono); font-size: .78rem; color: var(--term); border: 1px solid var(--term); border-radius: 50%; } .steps pre { margin: 0; padding: .9rem 1rem; overflow-x: auto; background: var(--panel); border: 1px solid var(--border); border-radius: 9px; } .steps code { font-family: var(--mono); font-size: .82rem; line-height: 1.7; color: var(--fg); } .steps .cm { color: var(--faint); } /* ---------------------------------------------------------------- trust */ .trust { background: var(--panel); border-top: 1px solid var(--hair); border-bottom: 1px solid var(--hair); padding-top: clamp(2.5rem, 6vw, 4rem); padding-bottom: clamp(2.5rem, 6vw, 4rem); } .trust .section-head { margin-bottom: clamp(1.8rem, 4vw, 2.6rem); } .trust .section-head h2 { font-size: clamp(1.7rem, 3.9vw, 2.38rem); } .trust-grid { max-width: var(--wide); margin: 0 auto; display: grid; grid-template-columns: 1fr 1fr; gap: clamp(1.2rem, 3vw, 2.4rem); } .trust-grid h3 { margin: 0 0 .8rem; font-size: 1.18rem; color: var(--dim); } .trust-grid ul { margin: 0; padding: 0; list-style: none; display: flex; flex-direction: column; gap: .55rem; } .verifiers li { font-family: var(--mono); font-size: .9rem; } .verifiers .dim { font-family: var(--sans); font-size: .82rem; } .landmarks li { font-size: .95rem; } .endgoal { margin: 1rem 0 0; font-size: .88rem; } .endgoal code { color: var(--fg); } /* ---------------------------------------------------------------- footer */ .foot { padding: clamp(2rem, 5vw, 3rem) var(--edge); display: flex; flex-wrap: wrap; align-items: center; gap: 1rem 1.5rem; max-width: var(--wide); margin: 0 auto; } .foot-mark { display: block; white-space: nowrap; font-family: var(--serif); font-size: 1.18rem; } .foot-mark .mark { width: 1.113em; height: 0.924em; vertical-align: -0.164em; margin-right: 0.507em; } .foot-links { display: flex; flex-wrap: wrap; gap: 1rem; } .foot-links a { color: var(--dim); font-family: var(--sans); font-size: .88rem; } .foot-links a:hover { color: var(--fg); text-decoration: none; } .foot-note { flex-basis: 100%; margin: 0; color: var(--faint); font-size: .82rem; } /* ---------------------------------------------------------------- responsive */ @media (max-width: 860px) { /* minmax(0, 1fr), not 1fr: a grid track is at least as wide as the widest thing in it unless told otherwise, and one column of these holds a command line that does not wrap. The `pre` scrolls; the page should not. */ .learn, .trust-grid { grid-template-columns: minmax(0, 1fr); } .cards { grid-template-columns: minmax(0, 1fr); } } @media (max-width: 620px) { .pillars { grid-template-columns: 1fr; } /* The name, four links and the switch do not fit on one line at this width: the links take a row of their own rather than pushing the page sideways. */ .nav { flex-wrap: wrap; row-gap: .45rem; } .nav .links { order: 3; width: 100%; margin-left: 0; gap: .8rem; justify-content: space-between; } .arrow.big { width: 100%; text-align: center; transform: rotate(90deg); } .pipe { flex-direction: column; align-items: stretch; } .node { min-width: 0; } }