michael
/
blog
1
0
Fork 0
Code Issues 1 Pull Requests Releases Wiki Activity

Ye

This commit is contained in:
Michael Zhang 2022-02-08 16:51:36 -06:00 committed by Michael Zhang
parent fe2c3f2524
commit baa186ea5a
5 changed files with 207 additions and 76 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
assets/sass/_content.scss
View File

@ -138,6 +138,14 @@ pre > code {
font-size: 0.9em; font-size: 0.9em;
} }
details {
font-size: 0.95rem;
summary {
cursor: pointer;
}
}
table.table { table.table {
border: 1px solid $faded; border: 1px solid $faded;
border-collapse: collapse; border-collapse: collapse;

248
assets/sass/_syntax.scss
View File

@ -1,70 +1,178 @@
pre.highlight { background-color: #444444; color: #cccccc } .highlight .chroma {
.highlight .hll { background-color: #444444; color: #cccccc } margin: 0;
.highlight .c { color: #608b4e } /* Comment */
.highlight .err { color: #cccccc; border: 1px solid #f44747 } /* Error */ .lntable td.lntd:last-child {
.highlight .g { color: #cccccc } /* Generic */ background-color: $faded-background-color;
.highlight .k { color: #569cd6 } /* Keyword */ padding-right: 12px;
.highlight .l { color: #cccccc } /* Literal */ }
.highlight .n { color: #cccccc } /* Name */ }
.highlight .o { color: #d4d4d4 } /* Operator */
.highlight .x { color: #cccccc } /* Other */ @media (prefers-color-scheme: light) {
.highlight .p { color: #cccccc } /* Punctuation */ /* Background */ .highlight { background-color: #ffffff }
.highlight .cm { color: #608b4e } /* Comment.Multiline */ /* Other */ .highlight .x { }
.highlight .cp { color: #569cd6 } /* Comment.Preproc */ /* Error */ .highlight .err { color: #a61717; background-color: #e3d2d2 }
.highlight .c1 { color: #608b4e } /* Comment.Single */ /* LineTableTD */ .highlight .lntd { vertical-align: top; padding: 0; margin: 0; border: 0; }
.highlight .cs { color: #cd0000; font-weight: bold } /* Comment.Special */ /* LineTable */ .highlight .lntable { border-spacing: 0; padding: 0; margin: 0; border: 0; width: auto; overflow: auto; display: block; }
.highlight .gd { color: #cd0000 } /* Generic.Deleted */ /* LineHighlight */ .highlight .hl { display: block; width: 100%;background-color: #ffffcc }
.highlight .ge { color: #cccccc; font-style: italic } /* Generic.Emph */ /* LineNumbersTable */ .highlight .lnt { margin-right: 0.4em; padding: 0 0.4em 0 0.4em;color: #7f7f7f }
.highlight .gr { color: #FF0000 } /* Generic.Error */ /* LineNumbers */ .highlight .ln { margin-right: 0.4em; padding: 0 0.4em 0 0.4em;color: #7f7f7f }
.highlight .gh { color: #000080; font-weight: bold } /* Generic.Heading */ /* Keyword */ .highlight .k { color: #000000; font-weight: bold }
.highlight .gi { color: #00cd00 } /* Generic.Inserted */ /* KeywordConstant */ .highlight .kc { color: #000000; font-weight: bold }
.highlight .go { color: #808080 } /* Generic.Output */ /* KeywordDeclaration */ .highlight .kd { color: #000000; font-weight: bold }
.highlight .gp { color: #000080; font-weight: bold } /* Generic.Prompt */ /* KeywordNamespace */ .highlight .kn { color: #000000; font-weight: bold }
.highlight .gs { color: #cccccc; font-weight: bold } /* Generic.Strong */ /* KeywordPseudo */ .highlight .kp { color: #000000; font-weight: bold }
.highlight .gu { color: #800080; font-weight: bold } /* Generic.Subheading */ /* KeywordReserved */ .highlight .kr { color: #000000; font-weight: bold }
.highlight .gt { color: #0040D0 } /* Generic.Traceback */ /* KeywordType */ .highlight .kt { color: #445588; font-weight: bold }
.highlight .kc { color: #569cd6 } /* Keyword.Constant */ /* Name */ .highlight .n { }
.highlight .kd { color: #00cd00 } /* Keyword.Declaration */ /* NameAttribute */ .highlight .na { color: #008080 }
.highlight .kn { color: #cd00cd } /* Keyword.Namespace */ /* NameBuiltin */ .highlight .nb { color: #0086b3 }
.highlight .kp { color: #569cd6 } /* Keyword.Pseudo */ /* NameBuiltinPseudo */ .highlight .bp { color: #999999 }
.highlight .kr { color: #569cd6 } /* Keyword.Reserved */ /* NameClass */ .highlight .nc { color: #445588; font-weight: bold }
.highlight .kt { color: #4EC9B0 } /* Keyword.Type */ /* NameConstant */ .highlight .no { color: #008080 }
.highlight .ld { color: #cccccc } /* Literal.Date */ /* NameDecorator */ .highlight .nd { color: #3c5d5d; font-weight: bold }
.highlight .m { color: #b5cea8 } /* Literal.Number */ /* NameEntity */ .highlight .ni { color: #800080 }
.highlight .s { color: #ce9178 } /* Literal.String */ /* NameException */ .highlight .ne { color: #990000; font-weight: bold }
.highlight .na { color: #cccccc } /* Name.Attribute */ /* NameFunction */ .highlight .nf { color: #990000; font-weight: bold }
.highlight .nb { color: #b5cea8 } /* Name.Builtin */ /* NameFunctionMagic */ .highlight .fm { }
.highlight .nc { color: #00cdcd } /* Name.Class */ /* NameLabel */ .highlight .nl { color: #990000; font-weight: bold }
.highlight .no { color: #cccccc } /* Name.Constant */ /* NameNamespace */ .highlight .nn { color: #555555 }
.highlight .nd { color: #cccccc } /* Name.Decorator */ /* NameOther */ .highlight .nx { }
.highlight .ni { color: #cccccc } /* Name.Entity */ /* NameProperty */ .highlight .py { }
.highlight .ne { color: #666699; font-weight: bold } /* Name.Exception */ /* NameTag */ .highlight .nt { color: #000080 }
.highlight .nf { color: #cccccc } /* Name.Function */ /* NameVariable */ .highlight .nv { color: #008080 }
.highlight .nl { color: #cccccc } /* Name.Label */ /* NameVariableClass */ .highlight .vc { color: #008080 }
.highlight .nn { color: #cccccc } /* Name.Namespace */ /* NameVariableGlobal */ .highlight .vg { color: #008080 }
.highlight .nx { color: #cccccc } /* Name.Other */ /* NameVariableInstance */ .highlight .vi { color: #008080 }
.highlight .py { color: #cccccc } /* Name.Property */ /* NameVariableMagic */ .highlight .vm { }
.highlight .nt { color: #cccccc } /* Name.Tag */ /* Literal */ .highlight .l { }
.highlight .nv { color: #00cdcd } /* Name.Variable */ /* LiteralDate */ .highlight .ld { }
.highlight .ow { color: #cdcd00 } /* Operator.Word */ /* LiteralString */ .highlight .s { color: #dd1144 }
.highlight .w { color: #cccccc } /* Text.Whitespace */ /* LiteralStringAffix */ .highlight .sa { color: #dd1144 }
.highlight .mf { color: #b5cea8 } /* Literal.Number.Float */ /* LiteralStringBacktick */ .highlight .sb { color: #dd1144 }
.highlight .mh { color: #b5cea8 } /* Literal.Number.Hex */ /* LiteralStringChar */ .highlight .sc { color: #dd1144 }
.highlight .mi { color: #b5cea8 } /* Literal.Number.Integer */ /* LiteralStringDelimiter */ .highlight .dl { color: #dd1144 }
.highlight .mo { color: #b5cea8 } /* Literal.Number.Oct */ /* LiteralStringDoc */ .highlight .sd { color: #dd1144 }
.highlight .sb { color: #ce9178 } /* Literal.String.Backtick */ /* LiteralStringDouble */ .highlight .s2 { color: #dd1144 }
.highlight .sc { color: #ce9178 } /* Literal.String.Char */ /* LiteralStringEscape */ .highlight .se { color: #dd1144 }
.highlight .sd { color: #ce9178 } /* Literal.String.Doc */ /* LiteralStringHeredoc */ .highlight .sh { color: #dd1144 }
.highlight .s2 { color: #ce9178 } /* Literal.String.Double */ /* LiteralStringInterpol */ .highlight .si { color: #dd1144 }
.highlight .se { color: #ce9178 } /* Literal.String.Escape */ /* LiteralStringOther */ .highlight .sx { color: #dd1144 }
.highlight .sh { color: #ce9178 } /* Literal.String.Heredoc */ /* LiteralStringRegex */ .highlight .sr { color: #009926 }
.highlight .si { color: #ce9178 } /* Literal.String.Interpol */ /* LiteralStringSingle */ .highlight .s1 { color: #dd1144 }
.highlight .sx { color: #ce9178 } /* Literal.String.Other */ /* LiteralStringSymbol */ .highlight .ss { color: #990073 }
.highlight .sr { color: #ce9178 } /* Literal.String.Regex */ /* LiteralNumber */ .highlight .m { color: #009999 }
.highlight .s1 { color: #ce9178 } /* Literal.String.Single */ /* LiteralNumberBin */ .highlight .mb { color: #009999 }
.highlight .ss { color: #ce9178 } /* Literal.String.Symbol */ /* LiteralNumberFloat */ .highlight .mf { color: #009999 }
.highlight .bp { color: #b5cea8 } /* Name.Builtin.Pseudo */ /* LiteralNumberHex */ .highlight .mh { color: #009999 }
.highlight .vc { color: #569cd6 } /* Name.Variable.Class */ /* LiteralNumberInteger */ .highlight .mi { color: #009999 }
.highlight .vg { color: #00cdcd } /* Name.Variable.Global */ /* LiteralNumberIntegerLong */ .highlight .il { color: #009999 }
.highlight .vi { color: #00cdcd } /* Name.Variable.Instance */ /* LiteralNumberOct */ .highlight .mo { color: #009999 }
.highlight .il { color: #b5cea8 } /* Literal.Number.Integer.Long */ /* Operator */ .highlight .o { color: #000000; font-weight: bold }
/* OperatorWord */ .highlight .ow { color: #000000; font-weight: bold }
/* Punctuation */ .highlight .p { }
/* Comment */ .highlight .c { color: #999988; font-style: italic }
/* CommentHashbang */ .highlight .ch { color: #999988; font-style: italic }
/* CommentMultiline */ .highlight .cm { color: #999988; font-style: italic }
/* CommentSingle */ .highlight .c1 { color: #999988; font-style: italic }
/* CommentSpecial */ .highlight .cs { color: #999999; font-weight: bold; font-style: italic }
/* CommentPreproc */ .highlight .cp { color: #999999; font-weight: bold; font-style: italic }
/* CommentPreprocFile */ .highlight .cpf { color: #999999; font-weight: bold; font-style: italic }
/* Generic */ .highlight .g { }
/* GenericDeleted */ .highlight .gd { color: #000000; background-color: #ffdddd }
/* GenericEmph */ .highlight .ge { color: #000000; font-style: italic }
/* GenericError */ .highlight .gr { color: #aa0000 }
/* GenericHeading */ .highlight .gh { color: #999999 }
/* GenericInserted */ .highlight .gi { color: #000000; background-color: #ddffdd }
/* GenericOutput */ .highlight .go { color: #888888 }
/* GenericPrompt */ .highlight .gp { color: #555555 }
/* GenericStrong */ .highlight .gs { font-weight: bold }
/* GenericSubheading */ .highlight .gu { color: #aaaaaa }
/* GenericTraceback */ .highlight .gt { color: #aa0000 }
/* GenericUnderline */ .highlight .gl { text-decoration: underline }
/* TextWhitespace */ .highlight .w { color: #bbbbbb }
}
@media (prefers-color-scheme: dark) {
/* Background */ .highlight { color: #e5e5e5; background-color: #000000 }
/* Other */ .highlight .x { }
/* Error */ .highlight .err { color: #ff0000 }
/* LineTableTD */ .highlight .lntd { vertical-align: top; padding: 0; margin: 0; border: 0; }
/* LineTable */ .highlight .lntable { border-spacing: 0; padding: 0; margin: 0; border: 0; width: auto; overflow: auto; display: block; }
/* LineHighlight */ .highlight .hl { display: block; width: 100%;background-color: #ffffcc }
/* LineNumbersTable */ .highlight .lnt { margin-right: 0.4em; padding: 0 0.4em 0 0.4em;color: #727272 }
/* LineNumbers */ .highlight .ln { margin-right: 0.4em; padding: 0 0.4em 0 0.4em;color: #727272 }
/* Keyword */ .highlight .k { color: #ffffff; font-weight: bold }
/* KeywordConstant */ .highlight .kc { color: #ffffff; font-weight: bold }
/* KeywordDeclaration */ .highlight .kd { color: #ffffff; font-weight: bold }
/* KeywordNamespace */ .highlight .kn { color: #ffffff; font-weight: bold }
/* KeywordPseudo */ .highlight .kp { color: #ffffff; font-weight: bold }
/* KeywordReserved */ .highlight .kr { color: #ffffff; font-weight: bold }
/* KeywordType */ .highlight .kt { color: #ffffff; font-weight: bold }
/* Name */ .highlight .n { }
/* NameAttribute */ .highlight .na { color: #007f7f }
/* NameBuiltin */ .highlight .nb { color: #ffffff; font-weight: bold }
/* NameBuiltinPseudo */ .highlight .bp { }
/* NameClass */ .highlight .nc { }
/* NameConstant */ .highlight .no { }
/* NameDecorator */ .highlight .nd { }
/* NameEntity */ .highlight .ni { }
/* NameException */ .highlight .ne { }
/* NameFunction */ .highlight .nf { }
/* NameFunctionMagic */ .highlight .fm { }
/* NameLabel */ .highlight .nl { }
/* NameNamespace */ .highlight .nn { }
/* NameOther */ .highlight .nx { }
/* NameProperty */ .highlight .py { }
/* NameTag */ .highlight .nt { font-weight: bold }
/* NameVariable */ .highlight .nv { }
/* NameVariableClass */ .highlight .vc { }
/* NameVariableGlobal */ .highlight .vg { }
/* NameVariableInstance */ .highlight .vi { }
/* NameVariableMagic */ .highlight .vm { }
/* Literal */ .highlight .l { }
/* LiteralDate */ .highlight .ld { color: #ffff00; font-weight: bold }
/* LiteralString */ .highlight .s { color: #00ffff; font-weight: bold }
/* LiteralStringAffix */ .highlight .sa { color: #00ffff; font-weight: bold }
/* LiteralStringBacktick */ .highlight .sb { color: #00ffff; font-weight: bold }
/* LiteralStringChar */ .highlight .sc { color: #00ffff; font-weight: bold }
/* LiteralStringDelimiter */ .highlight .dl { color: #00ffff; font-weight: bold }
/* LiteralStringDoc */ .highlight .sd { color: #00ffff; font-weight: bold }
/* LiteralStringDouble */ .highlight .s2 { color: #00ffff; font-weight: bold }
/* LiteralStringEscape */ .highlight .se { color: #00ffff; font-weight: bold }
/* LiteralStringHeredoc */ .highlight .sh { color: #00ffff; font-weight: bold }
/* LiteralStringInterpol */ .highlight .si { color: #00ffff; font-weight: bold }
/* LiteralStringOther */ .highlight .sx { color: #00ffff; font-weight: bold }
/* LiteralStringRegex */ .highlight .sr { color: #00ffff; font-weight: bold }
/* LiteralStringSingle */ .highlight .s1 { color: #00ffff; font-weight: bold }
/* LiteralStringSymbol */ .highlight .ss { color: #00ffff; font-weight: bold }
/* LiteralNumber */ .highlight .m { color: #ffff00; font-weight: bold }
/* LiteralNumberBin */ .highlight .mb { color: #ffff00; font-weight: bold }
/* LiteralNumberFloat */ .highlight .mf { color: #ffff00; font-weight: bold }
/* LiteralNumberHex */ .highlight .mh { color: #ffff00; font-weight: bold }
/* LiteralNumberInteger */ .highlight .mi { color: #ffff00; font-weight: bold }
/* LiteralNumberIntegerLong */ .highlight .il { color: #ffff00; font-weight: bold }
/* LiteralNumberOct */ .highlight .mo { color: #ffff00; font-weight: bold }
/* Operator */ .highlight .o { }
/* OperatorWord */ .highlight .ow { }
/* Punctuation */ .highlight .p { }
/* Comment */ .highlight .c { color: #007f7f }
/* CommentHashbang */ .highlight .ch { color: #007f7f }
/* CommentMultiline */ .highlight .cm { color: #007f7f }
/* CommentSingle */ .highlight .c1 { color: #007f7f }
/* CommentSpecial */ .highlight .cs { color: #007f7f }
/* CommentPreproc */ .highlight .cp { color: #00ff00; font-weight: bold }
/* CommentPreprocFile */ .highlight .cpf { color: #00ff00; font-weight: bold }
/* Generic */ .highlight .g { }
/* GenericDeleted */ .highlight .gd { }
/* GenericEmph */ .highlight .ge { }
/* GenericError */ .highlight .gr { }
/* GenericHeading */ .highlight .gh { font-weight: bold }
/* GenericInserted */ .highlight .gi { }
/* GenericOutput */ .highlight .go { }
/* GenericPrompt */ .highlight .gp { }
/* GenericStrong */ .highlight .gs { font-weight: bold }
/* GenericSubheading */ .highlight .gu { font-weight: bold }
/* GenericTraceback */ .highlight .gt { }
/* GenericUnderline */ .highlight .gl { text-decoration: underline }
/* TextWhitespace */ .highlight .w { }
}

3
assets/sass/main.scss
View File

@ -1,6 +1,5 @@
@import "agda"; @import "agda";
@import "mixins"; @import "mixins";
@import "syntax";
@import "fonts"; @import "fonts";
$sansfont: "Poppins", "Helvetica", "Arial", "Liberation Sans", sans-serif; $sansfont: "Poppins", "Helvetica", "Arial", "Liberation Sans", sans-serif;
@ -19,6 +18,7 @@ $monofont: "PragmataPro Mono Liga", "Roboto Mono", "Roboto Mono for Powerline",
$link-color: royalblue; $link-color: royalblue;
$code-color: firebrick; $code-color: firebrick;
$tag-color: lighten($link-color, 35%); $tag-color: lighten($link-color, 35%);
@import "syntax";
@import "content"; @import "content";
} }
@ -33,5 +33,6 @@ $monofont: "PragmataPro Mono Liga", "Roboto Mono", "Roboto Mono for Powerline",
$link-color: lightskyblue; $link-color: lightskyblue;
$code-color: lighten(firebrick, 25%); $code-color: lighten(firebrick, 25%);
$tag-color: darken($link-color, 55%); $tag-color: darken($link-color, 55%);
@import "syntax";
@import "content"; @import "content";
} }

14
config.toml
View File

@ -14,3 +14,17 @@ startLevel = 2
[markup.goldmark.renderer] [markup.goldmark.renderer]
unsafe = true unsafe = true
[markup.highlight]
anchorLineNos = true
codeFences = true
guessSyntax = false
hl_Lines = ''
lineAnchors = ''
lineNoStart = 1
lineNos = true
lineNumbersInTable = true
noClasses = false
style = 'monokai'
tabWidth = 4

10
content/posts/2022-02-02-formal-cek-machine-in-agda/_index.md
View File

@ -30,11 +30,11 @@ My lambda calculus implemented `call/cc` on top of a CEK machine.
output. If this were a library function I'd like to tell people who write code output. If this were a library function I'd like to tell people who write code
that uses this function "don't give me an empty list!" that uses this function "don't give me an empty list!"
Unfortunately, just writing this in documentation isn't enough. What we'd But just writing this in documentation isn't enough. What we'd really like is
really like is for a tool (like a compiler) to tell any developer who is for a tool (like a compiler) to tell any developer who is trying to pass an
trying to pass an empty list into our maximum function "You can't do that." empty list into our maximum function "You can't do that." Unfortunately, most
Unfortunately, most of the popular languages being used today have no way of of the popular languages being used today have no way of describing "a list
describing "a list that's not empty." that's not empty."
We still have a way to prevent people from running into this problem, though We still have a way to prevent people from running into this problem, though
it involves pushing the problem to runtime rather than compile time. The it involves pushing the problem to runtime rather than compile time. The