2 Commits

Author SHA1 Message Date
  Amélia Liao 3a29725003 dump 9 months ago
  Amélia Liao 8ba6920ff4 parsing layout 1 year ago
129 changed files with 3005 additions and 795 deletions
Split View
  1. +98
    -0
      css/agda.scss
  2. +0
    -45
      css/code.css
  3. +0
    -31
      css/colors.scss
  4. +0
    -13
      css/computermodern.css
  5. +372
    -444
      css/default.scss
  6. +419
    -0
      css/fonts.scss
  7. +62
    -0
      css/vars.scss
  8. +2
    -2
      package.json
  9. +15
    -8
      pages/contact.md
  10. +70
    -4
      pages/index.html
  11. +2
    -3
      pages/oss.md
  12. +1
    -0
      pages/posts/2016-08-17-parsec.md
  13. +1
    -0
      pages/posts/2016-08-23-hasochism.lhs
  14. +1
    -0
      pages/posts/2016-08-26-parsec2.lhs
  15. +1
    -0
      pages/posts/2018-02-18-amulet-tc2.md
  16. +1
    -1
      pages/posts/2018-03-14-amulet-safety.md
  17. +1
    -1
      pages/posts/2018-03-27-amulet-gadts.md
  18. +0
    -4
      pages/posts/2020-01-31-lazy-eval.lhs
  19. +3
    -3
      pages/posts/2020-10-30-reflecting-equality.md
  20. +7
    -7
      pages/posts/2021-03-07-cubical.md
  21. +1
    -1
      pages/posts/2021-06-07-ax-j.md
  22. +5
    -9
      pages/posts/2021-06-21-cubical-sets.md
  23. +884
    -0
      pages/posts/2021-09-03-parsing-layout.md
  24. +420
    -0
      pages/posts/2021-09-05-outsidein-x.md
  25. BIN
      site
  26. +133
    -52
      site.hs
  27. +2
    -3
      stack.yaml
  28. +11
    -18
      stack.yaml.lock
  29. +0
    -10
      static/default.css
  30. BIN
      static/icon/android-chrome-192x192.png
  31. BIN
      static/icon/android-chrome-512x512.png
  32. BIN
      static/icon/apple-touch-icon.png
  33. BIN
      static/icon/cube-128x.png
  34. BIN
      static/icon/favicon-16x16.png
  35. BIN
      static/icon/favicon-32x32.png
  36. BIN
      static/icon/favicon.ico
  37. BIN
      static/icon/pfp.jpg
  38. BIN
      static/icon/pfp.png
  39. BIN
      static/icon/[email protected]
  40. BIN
      static/icon/[email protected]
  41. BIN
      static/icon/[email protected]
  42. BIN
      static/icon/[email protected]
  43. +0
    -93
      static/licenses/LICENSE.FantasqueSansMono
  44. +110
    -0
      static/licenses/LICENSE.Iosevka
  45. +200
    -0
      static/licenses/LICENSE.Noto
  46. +31
    -0
      static/not-doom.svg
  47. +10
    -0
      static/svg/amulet.svg
  48. +31
    -0
      static/svg/gitea.svg
  49. +3
    -0
      static/svg/github.svg
  50. +46
    -0
      static/svg/kofi.svg
  51. +3
    -0
      static/svg/twitter.svg
  52. BIN
      static/ttf/iosevk-abbie-bold.ttf
  53. BIN
      static/ttf/iosevk-abbie-bolditalic.ttf
  54. BIN
      static/ttf/iosevk-abbie-boldoblique.ttf
  55. BIN
      static/ttf/iosevk-abbie-extended.ttf
  56. BIN
      static/ttf/iosevk-abbie-extendedbold.ttf
  57. BIN
      static/ttf/iosevk-abbie-extendedbolditalic.ttf
  58. BIN
      static/ttf/iosevk-abbie-extendedboldoblique.ttf
  59. BIN
      static/ttf/iosevk-abbie-extendedextrabold.ttf
  60. BIN
      static/ttf/iosevk-abbie-extendedextrabolditalic.ttf
  61. BIN
      static/ttf/iosevk-abbie-extendedextraboldoblique.ttf
  62. BIN
      static/ttf/iosevk-abbie-extendedheavy.ttf
  63. BIN
      static/ttf/iosevk-abbie-extendedheavyitalic.ttf
  64. BIN
      static/ttf/iosevk-abbie-extendedheavyoblique.ttf
  65. BIN
      static/ttf/iosevk-abbie-extendeditalic.ttf
  66. BIN
      static/ttf/iosevk-abbie-extendedmedium.ttf
  67. BIN
      static/ttf/iosevk-abbie-extendedmediumitalic.ttf
  68. BIN
      static/ttf/iosevk-abbie-extendedmediumoblique.ttf
  69. BIN
      static/ttf/iosevk-abbie-extendedoblique.ttf
  70. BIN
      static/ttf/iosevk-abbie-extendedsemibold.ttf
  71. BIN
      static/ttf/iosevk-abbie-extendedsemibolditalic.ttf
  72. BIN
      static/ttf/iosevk-abbie-extendedsemiboldoblique.ttf
  73. BIN
      static/ttf/iosevk-abbie-extrabold.ttf
  74. BIN
      static/ttf/iosevk-abbie-extrabolditalic.ttf
  75. BIN
      static/ttf/iosevk-abbie-extraboldoblique.ttf
  76. BIN
      static/ttf/iosevk-abbie-heavy.ttf
  77. BIN
      static/ttf/iosevk-abbie-heavyitalic.ttf
  78. BIN
      static/ttf/iosevk-abbie-heavyoblique.ttf
  79. BIN
      static/ttf/iosevk-abbie-italic.ttf
  80. BIN
      static/ttf/iosevk-abbie-medium.ttf
  81. BIN
      static/ttf/iosevk-abbie-mediumitalic.ttf
  82. BIN
      static/ttf/iosevk-abbie-mediumoblique.ttf
  83. BIN
      static/ttf/iosevk-abbie-oblique.ttf
  84. BIN
      static/ttf/iosevk-abbie-regular.ttf
  85. BIN
      static/ttf/iosevk-abbie-semibold.ttf
  86. BIN
      static/ttf/iosevk-abbie-semibolditalic.ttf
  87. BIN
      static/ttf/iosevk-abbie-semiboldoblique.ttf
  88. BIN
      static/woff2/iosevk-abbie-bold.woff2
  89. BIN
      static/woff2/iosevk-abbie-bolditalic.woff2
  90. BIN
      static/woff2/iosevk-abbie-boldoblique.woff2
  91. BIN
      static/woff2/iosevk-abbie-extended.woff2
  92. BIN
      static/woff2/iosevk-abbie-extendedbold.woff2
  93. BIN
      static/woff2/iosevk-abbie-extendedbolditalic.woff2
  94. BIN
      static/woff2/iosevk-abbie-extendedboldoblique.woff2
  95. BIN
      static/woff2/iosevk-abbie-extendedextrabold.woff2
  96. BIN
      static/woff2/iosevk-abbie-extendedextrabolditalic.woff2
  97. BIN
      static/woff2/iosevk-abbie-extendedextraboldoblique.woff2
  98. BIN
      static/woff2/iosevk-abbie-extendedheavy.woff2
  99. BIN
      static/woff2/iosevk-abbie-extendedheavyitalic.woff2
  100. BIN
      static/woff2/iosevk-abbie-extendedheavyoblique.woff2

+ 98
- 0
css/agda.scss View File

@ -0,0 +1,98 @@
$code-bg: hsl(230,1%,98%);
$code-fg: #ABB2BF;
$code-red: #D65122;
$code-red-br: #AE3B36;
$code-green: #88B966;
$code-yellow: #DEB468;
$code-orange: #C58853;
$code-blue: #519DEB;
$code-pink: #C678DD;
$code-cyan: #48A8B5;
$code-white: #ABB2BF;
$code-grey: #7F848E;
@font-face {
font-family: 'Iosevka';
font-display: swap;
font-weight: 400;
font-stretch: normal;
font-style: normal;
src: url('/static/woff2/iosevk-abbie-regular.woff2') format('woff2'), url('/static/ttf/iosevk-abbie-regular.ttf') format('truetype');
}
body {
margin: 0;
background-color:$code-bg;
color:#ABB2BF;
}
html {
background-color: $code-bg;
color:#ABB2BF;
}
pre.Agda {
margin: 0;
padding: 1em;
background-color: $code-bg;
color: $code-fg;
}
@keyframes highlight {
0% {
background-color: #F5DEB3;
}
100% {
background-color: $code-bg;
}
}
/* Aspects. */
.Agda {
.Comment { color: $code-grey; }
.Background { background-color: $code-bg; }
.Markup { color: $code-fg; }
.Keyword { color: $code-orange; }
.String { color: $code-red; }
.Number { color: $code-pink; }
.Symbol { color: $code-fg; }
.PrimitiveType { color: $code-blue; }
.Pragma { color: $code-fg; }
/* NameKinds. */
.Bound { color: $code-fg; }
.Generalizable { color: $code-fg; }
.InductiveConstructor { color: $code-green; }
.CoinductiveConstructor { color: $code-green; }
.Datatype { color: $code-blue; }
.Field { color: #F570B7; }
.Function { color: $code-blue; }
.Module { color: $code-pink; }
.Postulate { color: $code-blue; }
.Primitive { color: $code-blue; }
.Record { color: $code-blue; }
/* OtherAspects. */
.UnsolvedMeta { color: $code-fg; background: yellow }
.UnsolvedConstraint { color: $code-fg; background: yellow }
.TerminationProblem { color: $code-fg; background: #FFA07A }
.IncompletePattern { color: $code-fg; background: #F5DEB3 }
.Error { color: red; text-decoration: underline }
.TypeChecks { color: $code-fg; background: #ADD8E6 }
.Deadcode { color: $code-fg; background: #808080 }
.ShadowingInTelescope { color: $code-fg; background: #808080 }
/* Standard attributes. */
a { text-decoration: none }
a[href]:hover {
text-decoration: 2px #B4EEB4 underline dotted;
}
a[href]:target {
animation: highlight 2.5s;
}
background-color: #282C34;
font-family: 'Iosevka', 'Fantasque Sans Mono', 'Roboto Mono', monospace;
font-weight: 400;
font-size: 16pt;
}

+ 0
- 45
css/code.css View File

@ -1,45 +0,0 @@
code, div.sourceCode {
font-family: Fantasque Sans Mono, Fira Mono, monospace;
font-size: 15pt;
}
code.inline {
background-color: rgb(250,250,250);
/* border: 1px solid rgb(200,200,200); */
}
table.sourceCode, tr.sourceCode, td.lineNumbers, td.sourceCode {
margin: 0; padding: 0; vertical-align: baseline; border: none;
}
table.sourceCode {
width: 100%; line-height: 100%;
}
td.lineNumbers { text-align: right; padding-right: 4px; padding-left: 4px; color: #aaaaaa; border-right: 1px solid #aaaaaa; }
td.sourceCode { padding-left: 5px; }
code.kw, span.kw { color: #af005f; } /* Keyword */
code.dt, span.dt { color: #5f5faf; } /* DataType */
code.dv, span.dv { color: #268bd2; } /* DecVal */
code.bn, span.bn { color: #268bd2; } /* BaseN */
code.fl, span.fl { color: #268bd2; } /* Float */
code.ch, span.ch { color: #cb4b16; } /* Char */
code.st, span.st { color: #cb4b16; } /* String */
code.co, span.co { color: #8a8a8a; } /* Comment */
code.ot, span.ot { color: #007020; } /* Other */
code.al, span.al { color: #ff0000; } /* Alert */
code.fu, span.fu { color: #666666; } /* Function */
code.er, span.er { color: #ff0000; } /* Error */
code.wa, span.wa { color: #60a0b0; } /* Warning */
code.cn, span.cn { color: #880000; } /* Constant */
code.sc, span.sc { color: #4070a0; } /* SpecialChar */
code.vs, span.vs { color: #4070a0; } /* VerbatimString */
code.ss, span.ss { color: #2aa198; } /* SpecialString */
code.va, span.va { color: #073642; } /* Variable */
code.cf, span.cf { color: #007020; } /* ControlFlow */
code.op, span.op { color: #d33682; } /* Operator */
code.pp, span.pp { color: #bc7a00; } /* Preprocessor */
code.at, span.at { color: #7d9029; } /* Attribute */
code.do, span.do { color: #ba2121; } /* Documentation */
code.an, span.an { color: #60a0b0; } /* Annotation */
code.cv, span.cv { color: #60a0b0; } /* CommentVar */

+ 0
- 31
css/colors.scss View File

@ -1,31 +0,0 @@
$black: #282c34;
$white: #abb2bf;
$light_red: #e06c75;
$dark_red: #be5046;
$green: #98c379;
$light_yellow: #e5c07b;
$dark_yellow: #d19a66;
$blue: #61afef;
$magenta: #c678dd;
$cyan: #56b6c2;
$gutter_grey: #4b5263;
$comment_grey: #5c6370;
$orange: #ffac5f;
$blonde: #f5ddbc;
$light-purple: #f2f1f8;
$purple: #7060eb;
$yugo: #ea8472;
$code-background: $black;
$code-language-background: lighten($black, 5%);
$code-language-color: $white;
$code-fg: $white;
$code-kw: $light_red;
$code-dt: $dark_yellow;
$code-ot: $code-fg;
$code-co: $comment_grey;
// comment

+ 0
- 13
css/computermodern.css View File

@ -1,13 +0,0 @@
@font-face {
font-family: "Computer Modern";
src: url('/static/cmunorm.woff');
}
.math {
font-family: Computer Modern, serif;
}
.math .display {
font-size: 18px;
text-align: center;
}

+ 372
- 444
css/default.scss View File

@ -1,596 +1,524 @@
$purple: #4834d4;
$orange: #ffbe76;
$blonde: #f5ddbc;
$light-purple: #faf0fa;
$yugo: #ea8472;
$pink_glamour: #ff7979;
$carmine_pink: #eb4d4b;
@import "vars.scss";
$header: $orange;
$header-height: 50px;
$max-width: 80ch;
.mathpar, .math-paragraph {
@mixin center-that-bitch {
display: flex;
flex-direction: row;
flex-wrap: wrap;
justify-content: space-around;
flex-direction: column;
align-items: center;
> figure {
width: auto;
}
}
a#mastodon {
display: none;
}
html, body {
html {
min-height: 100%;
height: 100%;
margin: 0;
max-width: 100%;
margin: 0;
background-color: white;
font-family: -apple-system,BlinkMacSystemFont,"Segoe UI",Roboto,Oxygen-Sans,Ubuntu,Cantarell,"Helvetica Neue",sans-serif;
overflow-x: clip;
}
body {
display: flex;
flex-direction: column;
font-family: -apple-system, BlinkMacSystemFont, 'Segoe UI', Roboto, Oxygen, Ubuntu, Cantarell, 'Open Sans', 'Helvetica Neue', sans-serif;
counter-reset: theorem figure;
}
width: 100%;
div#header {
background-color: $header;
height: $header-height;
@include center-that-bitch;
margin: 0;
color: $bluegray-900;
font-size: $font-size;
overflow-x: clip;
}
body > header {
background-color: $purple-600;
display: flex;
flex-direction: row;
align-items: stretch;
height: $nav-height;
width: 100%;
z-index: 999;
position: fixed;
justify-content: space-between;
flex-wrap: nowrap;
overflow-x: auto;
align-items: center;
div#logo {
margin-left: .5em;
line-height: $header-height;
padding-left: 1em;
padding-right: 1em;
padding-left: .5em;
padding-right: .5em;
font-size: 18pt;
border-bottom: 3px solid $purple-700;
box-sizing: border-box;
a {
color: black;
text-decoration: none;
}
div, nav > a {
height: $nav-height;
padding-left: 0.3em;
padding-right: 0.3em;
transition: background-color .2s ease-in-out;
display: flex;
align-items: center;
}
div#logo:hover {
background-color: darken($header, 10%);
div:hover, nav > a:hover {
background-color: $purple-500;
transition: background-color 0.3s ease-in-out;
}
div#navigation {
margin-right: .5em;
a {
color: white;
font-size: $font-size * 1.2;
text-decoration: none;
}
nav {
display: flex;
flex-direction: row;
align-items: stretch;
align-self: flex-end;
justify-content: flex-end;
align-items: center;
gap: 0.5em;
}
}
line-height: $header-height;
@mixin left-bordered-block($color) {
padding-left: 1em;
padding-top: 0.2em;
padding-bottom: 0.2em;
a {
color: black;
text-decoration: none;
border-left: 5px dashed $color;
}
margin-left: .5em;
margin-right: .5em;
}
@mixin material {
padding: 1em;
div.nav-button {
height: 100%;
transition: background-color .2s ease-in-out;
}
margin-top: 1em;
margin-bottom: 1em;
div.nav-button:hover {
background-color: darken($header, 10%);
}
}
box-shadow: 2px 2px 6px black;
border-radius: 10px;
}
div#content, div.post-list-synopsys {
max-width: $max-width + 4ch;
main {
max-width: 100ch;
width: 100%;
margin: 0px auto 0px auto;
flex: 1 0 auto;
padding: 2ch;
padding-top: $nav-height;
span.katex, span.together {
display: inline-block;
}
box-sizing: border-box;
span.together {
white-space: nowrap;
div#title h2 {
display: none;
}
p {
code {
display: inline-block;
}
span.qed {
float: right;
}
span.theorem ::after {
counter-increment: theorem;
content: " " counter(theorem);
}
span.theorem, span.paragraph-marker {
font-style: italic;
div#post-toc-container {
aside#toc {
display: none;
}
span.word {
display: inline-block;
article {
grid-column: 2;
width: 100%;
line-height: 1.5;
}
}
p.image {
text-align: center !important;
}
h1 {
max-width: 120ch;
}
> article {
> blockquote {
width: 85%;
margin: auto;
border-left: 12px solid $purple;
border-right: 3px dashed $purple;
border-top: 3px dashed $purple;
border-bottom: 3px dashed $purple;
padding: 2ch;
}
> div.code-container {
// width: 80%;
// margin: auto;
pre {
padding: 0px 1em;
width: 80%;
margin: auto;
}
div#post-info {
font-style: italic;
line-height: 1.2;
> span {
display: inline;
}
}
@include left-bordered-block($bluegray-500);
}
}
div.code-container {
padding-top: 5px;
background-color: $light-purple;
border-radius: 5px;
border: 1px solid darken($light-purple, 10%);
overflow-x: auto;
> div.code-tag {
background-color: darken($light-purple, 10%);
overflow: hidden;
line-height: 80%;
font-size: 12pt;
margin-top: 5px;
width: 100%;
span {
padding: 0.5em 1em 0.25em 1em;
border-top-left-radius: 10px;
div.warning {
@include material;
background-color: $red-200;
}
box-shadow: 1px 1px darken($light-purple, 20%);
// display: none;
figure.wraparound {
float: right;
width: auto;
float: right;
}
}
margin-left: 2em;
}
pre {
overflow-x: auto;
}
figure {
overflow-x: auto;
overflow-y: clip;
width: 100%;
margin: auto;
div.sourceCode {
padding: 0px .5em;
}
@include center-that-bitch;
figcaption {
margin-top: 0.3em;
display: inline-block;
text-align: center;
}
div.code-container.custom-tag {
> span::after {
display: none;
}
p {
margin: 0;
}
}
div.code-container.continues {
> span {
display: none;
ol, ul {
padding-left: 1.2em;
li {
margin-top: 5px;
margin-bottom: 5px;
p {
margin-top: 5px;
margin-bottom: 5px;
}
}
}
div.warning {
&:before {
content: "Heads up!";
display: block;
font-size: 16pt;
}
margin: 16px auto;
width: 85%;
border-left: 12px solid $carmine_pink;
border-right: 3px dashed $carmine_pink;
border-top: 3px dashed $carmine_pink;
border-bottom: 3px dashed $carmine_pink;
padding: 2ch;
&>:first-child {
margin-top: 0.5em;
}
&>:last-child {
margin-bottom: 0px;
}
.katex-display {
> span.katex {
white-space: normal;
}
}
div.text-image {
display: flex;
margin-bottom: -18px;
div.mathpar {
display: flex;
flex-flow: row wrap;
justify-content: center;
align-items: center;
> figure {
min-width: 25px;
padding-left: 2em;
}
}
gap: 1em;
* {
max-width: 100%;
> figure {
width: auto;
max-width: 33%;
}
}
details {
summary {
margin-left: 1em;
font-size: 14pt;
padding: .2em 1em;
}
border-radius: 5px;
border: 1px solid $purple;
padding: .2em 1em;
background-color: white;
margin-top: 0.5em;
margin-bottom: 0.5em;
transition: font-size 0.3s ease-in-out, background-color 0.3s ease-in-out;
transform: rotate3d(0, 0, 0, 0);
}
div.columns {
blockquote, details.blockquote {
padding-right: 1em;
padding-left: 1em;
padding-top: 0.2em;
padding-bottom: 0.2em;
details[open] {
font-size: 14pt;
border: 0;
}
}
.special-thanks {
display: flex;
flex-direction: column;
align-items: center;
justify-content: space-around;
p {
font-size: 21pt;
margin-top: .5em;
margin-bottom: 0px;
}
code, pre, .sourceCode {
font-size: $font-size * 1.2;
font-family: 'Iosevka', 'Fantasque Sans Mono', Consolas, "Andale Mono WT", "Andale Mono", "Lucida Console", "Lucida Sans Typewriter", "DejaVu Sans Mono", "Bitstream Vera Sans Mono", "Liberation Mono", "Nimbus Mono L", Monaco, "Courier New", Courier, monospace;
font-weight: 500;
}
ul {
list-style: none;
li {
margin: .5em 0px;
border-radius: 10px;
border: 1px solid $purple;
background-color: $light-purple;
padding: 1em;
a {
text-decoration: underline;
}
div.sourceCode, pre {
background-color: $code-bg;
color: $code-fg;
flex-grow: 0;
transition: all 0.2s ease-in-out;
}
@include material;
li:hover {
border-radius: 5px;
transform: scale(1.01);
background-color: lighten($light-purple, 5%);
}
}
overflow-x: auto;
line-height: 1.2;
code {
display: block;
}
.eqn-list {
list-style: none;
direction: rtl;
counter-reset: equation;
li {
counter-increment: equation;
> pre {
padding: unset;
margin-top: unset;
margin-bottom: unset;
box-shadow: unset;
span.katex-display {
margin: 2px;
}
* {
direction: ltr;
}
}
margin: 0;
li::marker {
content: "(" counter(equation) ")";
font-family: KaTeX_Main, Times New Roman, serif;
}
}
font-size: 14pt;
line-height: 1.4;
span.katex-display {
overflow-x: auto;
overflow-y: clip;
}
}
.footnote-back {
margin-left: 0.5em;
p > code {
white-space: nowrap;
}
div.info, span#reading-length {
padding-left: 1em;
font-style: italic;
}
blockquote, details.blockquote {
@include material;
span#reading-length::before {
content: "Word count: "
}
background-color: $purple-100;
div#footer {
display: flex;
align-items: center;
justify-content: space-between;
margin-left: 0;
margin-right: 0;
padding-left: 1em;
padding-right: 1em;
background-color: $light-purple;
height: 50px;
h2 {
margin-top: 0;
}
}
.definition {
text-decoration: dotted underline;
table {
width: 70%;
margin: auto;
border-collapse: collapse;
td, th {
text-align: center;
padding: 0px 1em 0px 1em;
border: 2px solid $purple-400;
}
}
.post-list {
list-style: none;
padding: 0px;
ul#post-list {
list-style-type: none;
display: flex;
flex-direction: column;
width: 90%;
margin: auto;
.post-list-item {
@include left-bordered-block($yellow-500);
@include material;
div.post-list-item {
margin-top: .2em;
margin-bottom: .2em;
margin: 0;
padding: 1em;
background-color: $yellow-50;
border-radius: 10px;
background-color: $light-purple;
.post-list-header {
margin-top: 0.2em;
div.post-list-header {
display: flex;
justify-content: space-between;
flex-wrap: wrap;
align-items: flex-end;
line-height: 14pt;
font-style: italic;
font-size: 10pt;
a {
font-size: 14pt;
padding-right: 2em;
font-style: normal;
color: $bluegray-800;
}
}
font-size: 11pt;
}
}
table {
margin: auto;
border-collapse: collapse;
div.contact-list {
display: flex;
justify-content: space-evenly;
align-items: stretch;
gap: 3em;
td, th {
border: 1px solid $purple;
text-align: center;
padding: 0px 1em 0px 1em;
div.contact-card {
background-color: $purple-200;
@include material;
width: 33%;
max-width: 33%;
flex-grow: 1;
> * {
vertical-align: middle;
p {
margin: 0;
}
}
td.image {
padding: 0px;
img {
margin-top: auto;
div.contact-header {
// I really hate Pandoc sometimes
display: flex;
align-items: center;
gap: 1em;
margin-bottom: 10px;
img {
height: 48px;
clip-path: url(#squircle);
}
span.username {
font-size: 16pt;
}
}
}
}
figure {
width: 100%;
margin: auto;
display: flex;
flex-direction: column;
align-items: center;
justify-content: space-around;
div {
width: 100%;
overflow-x: auto;
@media only screen and (max-width: 450px) {
body > header {
div#logo {
width: 100%;
display: flex;
flex-direction: row;
justify-content: center;
}
nav {
display: none;
}
}
}
> p {
margin-bottom: 0px;
@media only screen and (min-width: 1500px) {
.narrow-only {
display: none !important;
}
figcaption {
font-size: 14pt;
display: inline-block;
main {
max-width: 100%;
> div#title {
font-size: 15pt;
h1, h2 {
margin: 0;
}
h2 {
font-style: italic;
font-weight: normal;
display: block;
z-index: 1;
}
> p {
margin-top: 0px;
margin-bottom: 0px;
margin-top: 0.5em;
margin-bottom: 1em;
@include center-that-bitch;
}
}
// figcaption::before {
// counter-increment: figure;
// content: "Figure " counter(figure) ". ";
// display: inline;
// }
}
div#post-toc-container {
display: grid;
grid-template-columns: 0.5fr 2fr 0.5fr;
gap: 1em;
@media only screen and (max-width: $max-width) {
div#content {
margin-left: 1px;
margin-right: 1px;
aside#toc {
display: block !important;
padding: 1ch;
h3 { @include center-that-bitch; }
div.text-image {
display: block;
> figure {
padding-left: 0px;
}
}
div#toc-container {
overflow-x: hidden;
width: 100%;
position: sticky;
top: 2em;
figure figcaption {
max-width: 85%;
margin: auto;
overflow-y: auto;
max-height: 90vh;
bottom: 2em;
ul {
border-left: 2px solid $bluegray-400;
list-style-type: none;
padding-left: 1em;
a {
text-decoration: none;
}
a:hover {
text-decoration: underline;
}
}
}
p {
font-style: italic;
}
}
ul {
padding-left: 20px;
article {
max-width: 100ch;
margin-top: -100px;
margin: auto;
}
}
p {
hyphens: auto;
div.columns {
display: grid;
grid-template-columns: 1fr 1fr;
gap: 1em;
span.katex {
display: inline;
}
}
}
}
.mathpar {
overflow-x: auto;
justify-content: space-evenly;
#index {
padding-top: 4em;
> * {
margin-left: .2em;
margin-right: .2em;
flex-shrink: 0;
flex-grow: 0;
a.ico-left {
img {
clip-path: url(#squircle);
width: 96px;
height: 96px;
}
float: left;
margin-right: 1em;
width: 96px;
height: 96px;
}
header {
nav div {
&>:nth-child(3) {
display: none;
}
a.ico-right {
img {
clip-path: url(#squircle);
width: 96px;
height: 96px;
}
float: right;
margin-left: 1em;
width: 96px;
height: 96px;
}
}
// Contact page
.contact-list {
display: flex;
flex-direction: row;
flex-wrap: wrap;
justify-content: space-around;
align-items: center;
.contact-card {
margin: 0px .5em;
border: 1px solid $purple;
border-radius: 10px;
background-color: $blonde;
padding: 0px 1em;
div#social {
display: flex;
flex-direction: row;
justify-content: center;
width: 100%;
gap: 8px;
.username, .username * {
font-size: 21pt;
color: $purple;
img {
width: 48px;
height: 48px;
clip-path: url(#squircle);
transition: width 0.25s, height 0.25s;
&:hover {
width: 54px;
height: 54px;
}
}
p {
display: flex;
align-items: center;
justify-content: space-evenly;
max-width: 40ch !important;
a {
filter: drop-shadow(2px 2px 3px rgba(50, 50, 0, 0.5));
height: 54px;
}
transition: all 0.2s ease-in-out;
}
}
.contact-card:hover {
margin: 0px .55em;
background-color: darken($blonde, 10%);
border-radius: 5px;
transform: scale(1.01);
@media only screen and (min-width: 1500px) {
#index {
display: grid;
grid-template-columns: 0.20fr 0.75fr 0.20fr 1fr 0.20fr;
}
}
span.math.inline {
display: inline-block;
}
@font-face {
font-family: 'Fantasque Sans Mono';
src: url('fonts/FantasqueSansMono-Regular.woff2') format('woff2');
font-weight: 400;
font-style: normal;
details {
margin-top: 1em;
margin-bottom: 1em;
}
// Styles for code
code.kw, span.kw { color: $code-pink; } /* Keyword */
code.dt, span.dt { color: $code-blue; } /* DataType */
code.dv, span.dv { color: $code-orange; } /* DecVal */
code.bn, span.bn { color: $code-orange; } /* BaseN */
code.fl, span.fl { color: $code-orange; } /* Float */
code.ch, span.ch { color: $code-green; } /* Char */
code.st, span.st { color: $code-green; } /* String */
code.co, span.co { color: $code-grey; } /* Comment */
code.ot, span.ot { color: $code-green; } /* Other */
code.al, span.al { color: #ff0000; } /* Alert */
code.fu, span.fu { color: $code-fg; } /* Function */
code.er, span.er { color: #ff0000; } /* Error */
code.wa, span.wa { color: #60a0b0; } /* Warning */
code.cn, span.cn { color: $code-orange; } /* Constant */
code.sc, span.sc { color: $code-yellow; } /* SpecialChar */
code.vs, span.vs { color: $code-blue; } /* VerbatimString */
code.ss, span.ss { color: $code-green; } /* SpecialString */
code.va, span.va { color: $code-fg; } /* Variable */
code.cf, span.cf { color: $code-pink; } /* ControlFlow */
code.op, span.op { color: $code-green; } /* Operator */
code.pp, span.pp { color: $code-orange; } /* Preprocessor */
code.at, span.at { color: $code-green; } /* Attribute */
code.do, span.do { color: $code-red; } /* Documentation */
code.an, span.an { color: $code-red; } /* Annotation */
code.cv, span.cv { color: $code-red; } /* CommentVar */

+ 419
- 0
css/fonts.scss View File

@ -0,0 +1,419 @@
@font-face {
font-family: 'Iosevka';
font-display: swap;
font-weight: 400;
font-stretch: normal;
font-style: normal;
src: url('/static/woff2/iosevk-abbie-regular.woff2') format('woff2'), url('/static/ttf/iosevk-abbie-regular.ttf') format('truetype');
}
@font-face {
font-family: 'Iosevka';
font-display: swap;
font-weight: 400;
font-stretch: expanded;
font-style: normal;
src: url('/static/woff2/iosevk-abbie-extended.woff2') format('woff2'), url('/static/ttf/iosevk-abbie-extended.ttf') format('truetype');
}
@font-face {
font-family: 'Iosevka';
font-display: swap;
font-weight: 400;
font-stretch: normal;
font-style: oblique;
src: url('/static/woff2/iosevk-abbie-oblique.woff2') format('woff2'), url('/static/ttf/iosevk-abbie-oblique.ttf') format('truetype');
}
@font-face {
font-family: 'Iosevka Oblique';
font-display: swap;
font-weight: 400;
font-stretch: normal;
src: url('/static/woff2/iosevk-abbie-oblique.woff2') format('woff2'), url('/static/ttf/iosevk-abbie-oblique.ttf') format('truetype');
}
@font-face {
font-family: 'Iosevka';
font-display: swap;
font-weight: 400;
font-stretch: expanded;
font-style: oblique;
src: url('/static/woff2/iosevk-abbie-extendedoblique.woff2') format('woff2'), url('/static/ttf/iosevk-abbie-extendedoblique.ttf') format('truetype');
}
@font-face {
font-family: 'Iosevka Oblique';
font-display: swap;
font-weight: 400;
font-stretch: expanded;
src: url('/static/woff2/iosevk-abbie-extendedoblique.woff2') format('woff2'), url('/static/ttf/iosevk-abbie-extendedoblique.ttf') format('truetype');
}
@font-face {
font-family: 'Iosevka';
font-display: swap;
font-weight: 400;
font-stretch: normal;
font-style: italic;
src: url('/static/woff2/iosevk-abbie-italic.woff2') format('woff2'), url('/static/ttf/iosevk-abbie-italic.ttf') format('truetype');
}
@font-face {
font-family: 'Iosevka';
font-display: swap;
font-weight: 400;
font-stretch: expanded;
font-style: italic;
src: url('/static/woff2/iosevk-abbie-extendeditalic.woff2') format('woff2'), url('/static/ttf/iosevk-abbie-extendeditalic.ttf') format('truetype');
}
@font-face {
font-family: 'Iosevka';
font-display: swap;
font-weight: 500;
font-stretch: normal;
font-style: normal;
src: url('/static/woff2/iosevk-abbie-medium.woff2') format('woff2'), url('/static/ttf/iosevk-abbie-medium.ttf') format('truetype');
}
@font-face {
font-family: 'Iosevka';
font-display: swap;
font-weight: 500;
font-stretch: expanded;
font-style: normal;
src: url('/static/woff2/iosevk-abbie-extendedmedium.woff2') format('woff2'), url('/static/ttf/iosevk-abbie-extendedmedium.ttf') format('truetype');
}
@font-face {
font-family: 'Iosevka';
font-display: swap;
font-weight: 500;
font-stretch: normal;
font-style: oblique;
src: url('/static/woff2/iosevk-abbie-mediumoblique.woff2') format('woff2'), url('/static/ttf/iosevk-abbie-mediumoblique.ttf') format('truetype');
}
@font-face {
font-family: 'Iosevka Oblique';
font-display: swap;
font-weight: 500;
font-stretch: normal;
src: url('/static/woff2/iosevk-abbie-mediumoblique.woff2') format('woff2'), url('/static/ttf/iosevk-abbie-mediumoblique.ttf') format('truetype');
}
@font-face {
font-family: 'Iosevka';
font-display: swap;
font-weight: 500;
font-stretch: expanded;
font-style: oblique;
src: url('/static/woff2/iosevk-abbie-extendedmediumoblique.woff2') format('woff2'), url('/static/ttf/iosevk-abbie-extendedmediumoblique.ttf') format('truetype');
}
@font-face {
font-family: 'Iosevka Oblique';
font-display: swap;
font-weight: 500;
font-stretch: expanded;
src: url('/static/woff2/iosevk-abbie-extendedmediumoblique.woff2') format('woff2'), url('/static/ttf/iosevk-abbie-extendedmediumoblique.ttf') format('truetype');
}
@font-face {
font-family: 'Iosevka';
font-display: swap;
font-weight: 500;
font-stretch: normal;
font-style: italic;
src: url('/static/woff2/iosevk-abbie-mediumitalic.woff2') format('woff2'), url('/static/ttf/iosevk-abbie-mediumitalic.ttf') format('truetype');
}
@font-face {
font-family: 'Iosevka';
font-display: swap;
font-weight: 500;
font-stretch: expanded;
font-style: italic;
src: url('/static/woff2/iosevk-abbie-extendedmediumitalic.woff2') format('woff2'), url('/static/ttf/iosevk-abbie-extendedmediumitalic.ttf') format('truetype');
}
@font-face {
font-family: 'Iosevka';
font-display: swap;
font-weight: 600;
font-stretch: normal;
font-style: normal;
src: url('/static/woff2/iosevk-abbie-semibold.woff2') format('woff2'), url('/static/ttf/iosevk-abbie-semibold.ttf') format('truetype');
}
@font-face {
font-family: 'Iosevka';
font-display: swap;
font-weight: 600;
font-stretch: expanded;
font-style: normal;
src: url('/static/woff2/iosevk-abbie-extendedsemibold.woff2') format('woff2'), url('/static/ttf/iosevk-abbie-extendedsemibold.ttf') format('truetype');
}
@font-face {
font-family: 'Iosevka';
font-display: swap;
font-weight: 600;
font-stretch: normal;
font-style: oblique;
src: url('/static/woff2/iosevk-abbie-semiboldoblique.woff2') format('woff2'), url('/static/ttf/iosevk-abbie-semiboldoblique.ttf') format('truetype');
}
@font-face {
font-family: 'Iosevka Oblique';
font-display: swap;
font-weight: 600;
font-stretch: normal;
src: url('/static/woff2/iosevk-abbie-semiboldoblique.woff2') format('woff2'), url('/static/ttf/iosevk-abbie-semiboldoblique.ttf') format('truetype');
}
@font-face {
font-family: 'Iosevka';
font-display: swap;
font-weight: 600;
font-stretch: expanded;
font-style: oblique;
src: url('/static/woff2/iosevk-abbie-extendedsemiboldoblique.woff2') format('woff2'), url('/static/ttf/iosevk-abbie-extendedsemiboldoblique.ttf') format('truetype');
}
@font-face {
font-family: 'Iosevka Oblique';
font-display: swap;
font-weight: 600;
font-stretch: expanded;
src: url('/static/woff2/iosevk-abbie-extendedsemiboldoblique.woff2') format('woff2'), url('/static/ttf/iosevk-abbie-extendedsemiboldoblique.ttf') format('truetype');
}
@font-face {
font-family: 'Iosevka';
font-display: swap;
font-weight: 600;
font-stretch: normal;
font-style: italic;
src: url('/static/woff2/iosevk-abbie-semibolditalic.woff2') format('woff2'), url('/static/ttf/iosevk-abbie-semibolditalic.ttf') format('truetype');
}
@font-face {
font-family: 'Iosevka';
font-display: swap;
font-weight: 600;
font-stretch: expanded;
font-style: italic;
src: url('/static/woff2/iosevk-abbie-extendedsemibolditalic.woff2') format('woff2'), url('/static/ttf/iosevk-abbie-extendedsemibolditalic.ttf') format('truetype');
}
@font-face {
font-family: 'Iosevka';
font-display: swap;
font-weight: 700;
font-stretch: normal;
font-style: normal;
src: url('/static/woff2/iosevk-abbie-bold.woff2') format('woff2'), url('/static/ttf/iosevk-abbie-bold.ttf') format('truetype');
}
@font-face {
font-family: 'Iosevka';
font-display: swap;
font-weight: 700;
font-stretch: expanded;
font-style: normal;
src: url('/static/woff2/iosevk-abbie-extendedbold.woff2') format('woff2'), url('/static/ttf/iosevk-abbie-extendedbold.ttf') format('truetype');
}
@font-face {
font-family: 'Iosevka';
font-display: swap;
font-weight: 700;
font-stretch: normal;
font-style: oblique;
src: url('/static/woff2/iosevk-abbie-boldoblique.woff2') format('woff2'), url('/static/ttf/iosevk-abbie-boldoblique.ttf') format('truetype');
}
@font-face {
font-family: 'Iosevka Oblique';
font-display: swap;
font-weight: 700;
font-stretch: normal;
src: url('/static/woff2/iosevk-abbie-boldoblique.woff2') format('woff2'), url('/static/ttf/iosevk-abbie-boldoblique.ttf') format('truetype');
}
@font-face {
font-family: 'Iosevka';
font-display: swap;
font-weight: 700;
font-stretch: expanded;
font-style: oblique;
src: url('/static/woff2/iosevk-abbie-extendedboldoblique.woff2') format('woff2'), url('/static/ttf/iosevk-abbie-extendedboldoblique.ttf') format('truetype');
}
@font-face {
font-family: 'Iosevka Oblique';
font-display: swap;
font-weight: 700;
font-stretch: expanded;
src: url('/static/woff2/iosevk-abbie-extendedboldoblique.woff2') format('woff2'), url('/static/ttf/iosevk-abbie-extendedboldoblique.ttf') format('truetype');
}
@font-face {
font-family: 'Iosevka';
font-display: swap;
font-weight: 700;
font-stretch: normal;
font-style: italic;
src: url('/static/woff2/iosevk-abbie-bolditalic.woff2') format('woff2'), url('/static/ttf/iosevk-abbie-bolditalic.ttf') format('truetype');
}
@font-face {
font-family: 'Iosevka';
font-display: swap;
font-weight: 700;
font-stretch: expanded;
font-style: italic;
src: url('/static/woff2/iosevk-abbie-extendedbolditalic.woff2') format('woff2'), url('/static/ttf/iosevk-abbie-extendedbolditalic.ttf') format('truetype');
}
@font-face {
font-family: 'Iosevka';
font-display: swap;
font-weight: 800;
font-stretch: normal;
font-style: normal;
src: url('/static/woff2/iosevk-abbie-extrabold.woff2') format('woff2'), url('/static/ttf/iosevk-abbie-extrabold.ttf') format('truetype');
}
@font-face {
font-family: 'Iosevka';
font-display: swap;
font-weight: 800;
font-stretch: expanded;
font-style: normal;
src: url('/static/woff2/iosevk-abbie-extendedextrabold.woff2') format('woff2'), url('/static/ttf/iosevk-abbie-extendedextrabold.ttf') format('truetype');
}
@font-face {
font-family: 'Iosevka';
font-display: swap;
font-weight: 800;
font-stretch: normal;
font-style: oblique;
src: url('/static/woff2/iosevk-abbie-extraboldoblique.woff2') format('woff2'), url('/static/ttf/iosevk-abbie-extraboldoblique.ttf') format('truetype');
}
@font-face {
font-family: 'Iosevka Oblique';
font-display: swap;
font-weight: 800;
font-stretch: normal;
src: url('/static/woff2/iosevk-abbie-extraboldoblique.woff2') format('woff2'), url('/static/ttf/iosevk-abbie-extraboldoblique.ttf') format('truetype');
}
@font-face {
font-family: 'Iosevka';
font-display: swap;
font-weight: 800;
font-stretch: expanded;
font-style: oblique;
src: url('/static/woff2/iosevk-abbie-extendedextraboldoblique.woff2') format('woff2'), url('/static/ttf/iosevk-abbie-extendedextraboldoblique.ttf') format('truetype');
}
@font-face {
font-family: 'Iosevka Oblique';
font-display: swap;
font-weight: 800;
font-stretch: expanded;
src: url('/static/woff2/iosevk-abbie-extendedextraboldoblique.woff2') format('woff2'), url('/static/ttf/iosevk-abbie-extendedextraboldoblique.ttf') format('truetype');
}
@font-face {
font-family: 'Iosevka';
font-display: swap;
font-weight: 800;
font-stretch: normal;
font-style: italic;
src: url('/static/woff2/iosevk-abbie-extrabolditalic.woff2') format('woff2'), url('/static/ttf/iosevk-abbie-extrabolditalic.ttf') format('truetype');
}
@font-face {
font-family: 'Iosevka';
font-display: swap;
font-weight: 800;
font-stretch: expanded;
font-style: italic;
src: url('/static/woff2/iosevk-abbie-extendedextrabolditalic.woff2') format('woff2'), url('/static/ttf/iosevk-abbie-extendedextrabolditalic.ttf') format('truetype');
}
@font-face {
font-family: 'Iosevka';
font-display: swap;
font-weight: 900;
font-stretch: normal;
font-style: normal;
src: url('/static/woff2/iosevk-abbie-heavy.woff2') format('woff2'), url('/static/ttf/iosevk-abbie-heavy.ttf') format('truetype');
}
@font-face {
font-family: 'Iosevka';
font-display: swap;
font-weight: 900;
font-stretch: expanded;
font-style: normal;
src: url('/static/woff2/iosevk-abbie-extendedheavy.woff2') format('woff2'), url('/static/ttf/iosevk-abbie-extendedheavy.ttf') format('truetype');
}
@font-face {
font-family: 'Iosevka';
font-display: swap;
font-weight: 900;
font-stretch: normal;
font-style: oblique;
src: url('/static/woff2/iosevk-abbie-heavyoblique.woff2') format('woff2'), url('/static/ttf/iosevk-abbie-heavyoblique.ttf') format('truetype');
}
@font-face {
font-family: 'Iosevka Oblique';
font-display: swap;
font-weight: 900;
font-stretch: normal;
src: url('/static/woff2/iosevk-abbie-heavyoblique.woff2') format('woff2'), url('/static/ttf/iosevk-abbie-heavyoblique.ttf') format('truetype');
}
@font-face {
font-family: 'Iosevka';
font-display: swap;
font-weight: 900;
font-stretch: expanded;
font-style: oblique;
src: url('/static/woff2/iosevk-abbie-extendedheavyoblique.woff2') format('woff2'), url('/static/ttf/iosevk-abbie-extendedheavyoblique.ttf') format('truetype');
}
@font-face {
font-family: 'Iosevka Oblique';
font-display: swap;
font-weight: 900;
font-stretch: expanded;
src: url('/static/woff2/iosevk-abbie-extendedheavyoblique.woff2') format('woff2'), url('/static/ttf/iosevk-abbie-extendedheavyoblique.ttf') format('truetype');
}
@font-face {
font-family: 'Iosevka';
font-display: swap;
font-weight: 900;
font-stretch: normal;
font-style: italic;
src: url('/static/woff2/iosevk-abbie-heavyitalic.woff2') format('woff2'), url('/static/ttf/iosevk-abbie-heavyitalic.ttf') format('truetype');
}
@font-face {
font-family: 'Iosevka';
font-display: swap;
font-weight: 900;
font-stretch: expanded;
font-style: italic;
src: url('/static/woff2/iosevk-abbie-extendedheavyitalic.woff2') format('woff2'), url('/static/ttf/iosevk-abbie-extendedheavyitalic.ttf') format('truetype');
}

+ 62
- 0
css/vars.scss View File

@ -0,0 +1,62 @@
$purple-50: #faf5ff;
$purple-100: #f3e8ff;
$purple-200: #e9d5ff;
$purple-300: #d8b4fe;
$purple-400: #c084fc;
$purple-500: #a855f7;
$purple-600: #9333ea;
$purple-700: #7e22ce;
$purple-800: #6b21a8;
$purple-900: #581c87;
$yellow-50: #fefce8;
$yellow-100: #fef9c3;
$yellow-200: #fef08a;
$yellow-300: #fde047;
$yellow-400: #facc15;
$yellow-500: #eab308;
$yellow-600: #ca8a04;
$yellow-700: #a16207;
$yellow-800: #854d0e;
$yellow-900: #713f12;
$bluegray-50: #f8fafc;
$bluegray-100: #f1f5f9;
$bluegray-200: #e2e8f0;
$bluegray-300: #cbd5e1;
$bluegray-400: #94a3b8;
$bluegray-500: #64748b;
$bluegray-600: #475569;
$bluegray-700: #334155;
$bluegray-800: #1e293b;
$bluegray-900: #0f172a;
$red-50: #fef2f2;
$red-100: #fee2e2;
$red-200: #fecaca;
$red-300: #fca5a5;
$red-400: #f87171;
$red-500: #ef4444;
$red-600: #dc2626;
$red-700: #b91c1c;
$red-800: #991b1b;
$red-900: #7f1d1d;
$nav-height: 48px;
$font-size: 14pt;
$code-bg: #282C34;
$code-fg: #ABB2BF;
$code-red: #D65122;
$code-red-br: #AE3B36;
$code-green: #88B966;
$code-yellow: #DEB468;
$code-orange: #C58853;
$code-blue: #519DEB;
$code-pink: #C678DD;
$code-cyan: #48A8B5;
$code-white: #ABB2BF;
$code-grey: #7F848E;
// foo

+ 2
- 2
package.json View File

@ -1,7 +1,7 @@
{
"name": "blag",
"version": "1.0.0",
"description": "[Go here instead](https://abby.how)",
"description": "[Go here instead](https://amelia.how)",
"main": "index.js",
"dependencies": {
"katex": "^0.13.11",
@ -14,7 +14,7 @@
},
"repository": {
"type": "git",
"url": "https://git.abby.how/abby/blag.git"
"url": "https://git.amelia.how/amelia/blag.git"
},
"author": "",
"license": "ISC"


+ 15
- 8
pages/contact.md View File

@ -8,27 +8,34 @@ span#reading-length { display: none; }
</style>
<div class="contact-list">
<div class="contact-card">
<span class="username">Abbie#4600</span>
<div class="contact-header">
<span class="username">@plt_amy</span>
</div>
My Discord friend requests are always open. Feel free to add me for questions or comments!
<span>
I am unhealthily active on the bird website, so follow me on Twitter to stay up to date with what I think about.. everything!
</span>
</div>
<div class="contact-card">
<span class="username">{abby}</span>
<div class="contact-header">
<span class="username">{ames}</span>
</div>
<span>
Message me directly on <a href="https://libera.chat">Libera</a> IRC, or join `##dependent` to talk about types!
</span>
<span>
I'm active in `##dependent` on [libera.chat](https://libera.chat) to talk about types!
</span>
</div>
</div>
If you like what I do, here are some ways you can support this blog:
<div class="contact-list">
<div class="contact-card">
<span class="username"><a href="https://ko-fi.com/pltabby">Ko-fi</a></span>
<span class="username"><a href="https://ko-fi.com/plt_amy">Ko-fi</a></span>
You can send me a one-time donation on Ko-Fi. Just remember not to read the name on the receipt!
(Paypal sucks)
</div>


+ 70
- 4
pages/index.html View File

@ -2,12 +2,78 @@
title: Home
---
<p>
You've reached Abigail's blog, a place where I exposit and reflect on programming languages and type theory.
Here's the posts I've written recently:
<div id=index>
<div style="grid-column: 2;">
<h2 id=hi>Hi!</h2>
<p style="height: 98px">
<a class=ico-left href="/">
<img alt="profile picture" decoding=async src="/static/icon/[email protected]" />
</a>
I'm Amélia, a non-binary (they/them) mathematician & programmer. This
blog is where I write about programming languages: their implementation,
their semantics, etc.
</p>
<hr />
<div id=social>
<a href="https://twitter.com/plt_amy">
<img class=social decoding=async title="My Twitter profile" src="/static/svg/twitter.svg" style="background-color: #1DA1F2;" />
</a>
<a href="https://github.com/plt-amy">
<img class=social decoding=async title="My GitHub profile" src="/static/svg/github.svg" style="background-color: black;" />
</a>
<a href="https://git.amelia.how">
<img class=social decoding=async title="My personal Gitea" src="/static/svg/gitea.svg" style="background-color: #609926;" />
</a>
<a href="https://ko-fi.com/plt_amy">
<img class=social decoding=async title="Buy me a coffee on Ko-Fi" src="/static/svg/kofi.svg" style="background-color: #434B57;" />
</a>
</div>
<hr />
<p style="height: 98px">
<a class=ico-right href="https://cubical.1lab.dev">
<img class=ico-right alt="cube" decoding=async src="/static/icon/cube-128x.png" />
</a>
In addition to this blog, I maintain <a
href="https://cubical.1lab.dev">the 1Lab</a>, a formalised, cross-linked
reference resource for Homotopy Type Theory, done in Cubical Agda.
</p>
<hr />
<p style="height: 98px">
<a class=ico-left href="https://amulet.works">
<img alt="amulet" decoding=async src="/static/svg/amulet.svg" />
</a>
My most significant project other than this blog and the 1lab is <a
href="https://amulet.works">Amulet</a>, a functional programming
language in the ML tradition with support for advanced type-level
programming.
</p>
</div>
<div style="grid-column: 4;">
<h2>Posts</h2>
<p>
Here are the lastest 5 posts from the blog:
</p>
$partial("templates/post-list.html")$
<p>…or you can find more in the <a href="/archive.html">archives</a>.</p>
<p>…or you can find more in the <a href="/archive.html">archives</a>.</p>
</div>
</div>
<style>
main > div#title {
display: none;
}
</style>

+ 2
- 3
pages/oss.md View File

@ -8,7 +8,6 @@ span#reading-length { display: none; }
This blog redistributes (parts of) the following free software projects:
* **KaTeX** is a fast JavaScript library for rendering LaTeX on the client. I use it to pre-generate amazing looking mathematics at compile time. **KaTeX is licensed under the terms of the MIT license, with a copy available [here](/static/licenses/LICENSE.KaTeX)**.
* **KaTeX** is a fast JavaScript library for rendering LaTeX on the client. I use it to pre-generate amazing looking mathematics at compile time. **KaTeX is licensed under the terms of the MIT license; A copy is available [here](/static/licenses/LICENSE.KaTeX)**.
* **Fantasque Sans Mono** is the programming font I've used for the past 3 years, including on this website. **Fantasque Sans Mono is distributed under the terms of the Open Font License (OFL), with a copy available [here](/static/licenses/LICENSE.FantasqueSansMono)**.
* **Iosevka** is a customizable monospace font designed for programmers. It's used in this website for code blocks, and also for any Agda developments I've shared under the amelia.how domain. **Iosevka is distributed under the terms of the SIL Open Font License; A copy is available [here](/static/licenses/LICENSE.Iosevka).**

+ 1
- 0
pages/posts/2016-08-17-parsec.md View File

@ -1,6 +1,7 @@
---
title: You could have invented Parsec
date: August 17, 2016 01:29 AM
synopsys: 2
---
As most of us should know, [Parsec](https://hackage.haskell.org/package/parsec)


+ 1
- 0
pages/posts/2016-08-23-hasochism.lhs View File