Update index.

config.toml

@@ -6,6 +6,15 @@ pygmentsCodeFences = true
 pygmentsUseClasses = true
 summaryLength = 20
 
+[outputFormats]
+  [outputFormats.Toml]
+    name = "toml"
+    mediaType = "application/toml"
+    isHTML = false
+
+[outputs]
+  home = ["html","rss","toml"]
+
 [markup]
   [markup.tableOfContents]
     endLevel = 4

content/blog/00_aoc_coq.md

@@ -1,8 +1,7 @@
 ---
 title: "Advent of Code in Coq - Day 1"
-date: 2020-12-01T21:50:28-08:00
+date: 2020-12-02T18:44:56-08:00
 tags: ["Advent of Code", "Coq"]
-draft: true
 ---
 
 The first puzzle of this year's [Advent of Code](https://adventofcode.com) was quite
@@ -21,19 +20,19 @@ problem statement:
 With this in mind, we can move on to writing some Coq!
 
 ### Defining the Functions
-The first step to proving our code correct is to actually write the code! As a first
-step, let's write a helper function that, given a number `x`, tries to find another number
-`y` such that `x + y = 2020`. The code is quite simple:
+The first step to proving our code correct is to actually write the code! To start with,
+let's write a helper function that, given a number `x`, tries to find another number
+`y` such that `x + y = 2020`. In fact, rather than hardcoding the desired
+sum to `2020`, let's just use another argument called `total`. The code is quite simple:
 
 {{< codelines "Coq" "aoc-coq/day1.v" 7 14 >}}
 
-Here, `is` is the list of numbers that we want to search, and `total` is the number
-we want to add up to (`2020` in our particular case), and `x` is the same as it was in
-the previous paragraph. We proceed by case analysis: if the list is empty, we can't
+Here, `is` is the list of numbers that we want to search.
+We proceed by case analysis: if the list is empty, we can't
 find a match, so we return `None` (the Coq equivalent of Haskell's `Nothing`).
-On the other hand, if the list has at least one element, `y`, we see if it adds
-up to `total`, and return `y` if it does. If it doesn't, we continue our search
-into the rest of the list.
+On the other hand, if the list has at least one element `y`, we see if it adds
+up to `total`, and return `Some y` (equivalent to `Just y` in Haskell) if it does.
+If it doesn't, we continue our search into the rest of the list.
 
 It's somewhat unusual, in my experience, to put the list argument first when writing
 functions in a language with [currying](https://wiki.haskell.org/Currying). However,
@@ -92,7 +91,7 @@ hold for the empty list, which is the simplest possible list.
 In our case, this means `find_matching` searching an empty list.
 * The __inductive case__. Assuming that a property holds for any list
 `[b, c, ...]`, we want to show that the property also holds for 
-the list `[a, b, ...]`. That is, the property must remain true if we
+the list `[a, b, c, ...]`. That is, the property must remain true if we
 prepend an element to a list for which this property holds.
 
 These two things combined give us a proof for _all_ lists, which is exactly
@@ -105,7 +104,8 @@ an element to the list, this time a `3`, and conclude that `P [3,4]`.
 Repeating this twice more, we arrive at our desired fact: `P [1,2,3,4]`.
 
 When we write `induction is`, Coq will generate two proof goals for us,
-one for the base case, and one for the inductive case. Since we have
+one for the base case, and one for the inductive case. We will have to prove
+each of them separately. Since we have
 not yet introduced the variables `k`, `x`, and `y`, they remain
 inside a `forall` quantifier at that time. To be able to refer
 to them, we want to use `intros`. We want to do this in both the
@@ -147,14 +147,14 @@ Hev : None = Some y
 ```
 
 Well, this doesn't make any sense. How can something be equal to nothing?
-We ask Coq this question using `inversion Hev`. Effectively, `inversion` asks
-the question: what are the possible ways we could have acquired `Hev`?
+We ask Coq this question using `inversion Hev`. Effectively, the question
+that `inversion` asks is: what are the possible ways we could have acquired `Hev`?
 Coq generates a proof goal for each of these possible ways. Alas, there are
 no ways to arrive at this contradictory assumption: the number of proof sub-goals
 is zero. This means we're done with the base case!
 
 The inductive case is the meat of this proof. Here's the corresponding part
-of the proof:
+of the Coq source file:
 
 {{< codelines "Coq" "aoc-coq/day1.v" 32 36 >}}
 
@@ -175,7 +175,7 @@ x + y = k
 Following the footsteps of our informal description of the inductive case,
 Coq has us prove our property for `(a :: is)`, or the list `is` to which
 `a` is being prepended. Like before, we assume that our property holds for `is`.
-This is represented in the __induction hypothesis__ `IHis`. It states that if we
+This is represented in the __induction hypothesis__ `IHis`. It states that if
 `find_matching` finds a `y` in `is`, it must add up to `k`. However, `IHis`
 doesn't tell us anything about `a :: is`: that's our job. We also still have
 `Hev`, which is our assumption that `find_matching` finds a `y` in `(a :: is)`.
@@ -186,13 +186,16 @@ Hev : (if x + a =? k then Some a else find_matching is k x) = Some y
 ```
 
 The result of `find_matching` now depends on whether or not the new element `a`
-adds up to `k`. We're not sure if this is the case. Fortunately, we don't need to be!
+adds up to `k`. If it does, then `find_matching` will return `a`, which means
+that `y` is the same as `a`. If not, it must be that `find_matching` finds
+the `y` in the rest of the list, `is`. We're not sure which of the possibilities
+is the case. Fortunately, we don't need to be!
 If we can prove that the `y` that `find_matching` finds is correct regardless
 of whether `a` adds up to `k` or not, we're good to go! To do this,
 we perform case analysis using `destruct`.
 
-Our particular use of `destruct` says: check any possible value for `Nat.eqb (x+a) k`,
-and create an equation `Heq` that tells us what that value is. `Nat.eqb` returns a boolean
+Our particular use of `destruct` says: check any possible value for `x + a ?= k`,
+and create an equation `Heq` that tells us what that value is. `?=` returns a boolean
 value, and so `destruct` generates two new goals: one where the function returns `true`,
 and one where it returns `false`. We start with the former. Here's the proof state:
 
@@ -210,11 +213,11 @@ x + y = k
 ```
 
 There is a new hypothesis: `Heq`. It tells us that we're currently
-considering the case where `Nat.eqb` evaluates to `true`. Also,
+considering the case where `?=` evaluates to `true`. Also,
 `Hev` has been considerably simplified: now that we know the condition
 of the `if` expression, we can just replace it with the `then` branch.
 
-Looking at `Hev`, we can see that `a` is equal to `y`. After all,
+Looking at `Hev`, we can see that our prediction was right: `a` is equal to `y`. After all,
 if they weren't, `Some a` wouldn't equal to `Some y`. To make Coq
 take this information into account, we use `injection`. This will create
 a new hypothesis, `a = y`. But if one is equal to the other, why don't we
@@ -236,11 +239,11 @@ x + y = k
 
 We're close, but there's one more detail to keep in mind. Our goal, `x + y = k`,
 is the __proposition__ that `x + y` is equal to `k`. However, `Heq` tells us
-that the __function__ `eqb` evaluates to `true`. These are fundamentally different.
-One talks about mathematical equality, while the other about some function `eqb`
+that the __function__ `?=` evaluates to `true`. These are fundamentally different.
+One talks about mathematical equality, while the other about some function `?=`
 defined somewhere in Coq's standard library. Who knows - maybe there's a bug in
-Coq's implementation! Fortunately, Coq comes with a proof that if two things
-are equal according to `eqb`, they are mathematically equal. This proof is
+Coq's implementation! Fortunately, Coq comes with a proof that if two numbers
+are equal according to `?=`, they are mathematically equal. This proof is
 called `eqb_nat_eq`. We tell Coq to use this with `apply`. Our proof goal changes to:
 
 ```
@@ -248,9 +251,9 @@ true = (x + y =? k)
 ```
 
 This is _almost_ like `Heq`, but flipped. Instead of manually flipping it and using `apply`
-with `Heq`, I let Coq figure the rest of the work out using `auto`.
+with `Heq`, I let Coq do the rest of the work using `auto`.
 
-Phew! All this for the `true` case of `eqb`. Next, what happens if `x + a` does not equal `k`?
+Phew! All this for the `true` case of `?=`. Next, what happens if `x + a` does not equal `k`?
 Here's the proof state at this time:
 
 ```
@@ -294,12 +297,12 @@ This reads, if there _is_ an element `y` in `is` that adds up to `k` with `x`, t
 hold, it would mean that `find_matching` would occasionally fail to find a matching
 number, even though it's there! We can't have that.
 
-Finally, we want to specify what it means for `find_sum`, or solution function, to actually
+Finally, we want to specify what it means for `find_sum`, our solution function, to actually
 work. The naive definition would be:
 
 > Given a list of integers, `find_sum` always finds a pair of numbers that add up to `k`.
 
-Unfortunately, this is not true. What if, for instance, we have `find_sum` an empty list?
+Unfortunately, this is not true. What if, for instance, we give `find_sum` an empty list?
 There are no numbers from that list to find and add together. Even a non-empty list
 may not include such a pair! We need a way to characterize valid input lists. I claim
 that all lists from this Advent of Code puzzle are guaranteed to have two numbers that
@@ -311,11 +314,10 @@ we state this as follows:
 This defines a new property, `has_pair t is` (read "`is` has a pair of numbers that add to `t`"),
 which means:
 
-* There are two numbers `n1` and `n2` such that,
-* They are not equal to each other (`n1 <> n2`) and (`/\`),
-* The number `n1` is an element of `is` (`In n1 is`) and,
-* The number `n2` is an element of `is` (`In n2 is`) and,
-* The two numbers add up to `t` (`n1 + n2 = t`).
+> There are two numbers `n1` and `n2` such that, they are not equal to each other (`n1<>n2`) __and__
+> the number `n1` is an element of `is` (`In n1 is`) __and__
+> the number `n2` is an element of `is` (`In n2 is`) __and__
+> the two numbers add up to `t` (`n1 + n2 = t`).
 
 When making claims about the correctness of our algorithm, we will assume that this
 property holds. Finally, here's the theorem we want to prove:

themes/vanilla/assets/scss/search.scss

@@ -0,0 +1,94 @@
+@import "variables.scss";
+@import "mixins.scss";
+
+$search-input-padding: 0.5rem;
+$search-element-padding: 0.5rem 1rem 0.5rem 1rem;
+
+@mixin green-shadow {
+    box-shadow: 0px 0px 5px rgba($primary-color, 0.7);
+}
+
+.stork-input-wrapper {
+    display: flex;
+    flex-direction: row;
+    flex-wrap: wrap;
+}
+
+input.stork-input {
+    @include bordered-block;
+    font-family: $font-body;
+    padding: $search-input-padding;
+
+    &:active, &:focus {
+        @include green-shadow;
+        border-color: $primary-color;
+    }
+
+    flex-grow: 1;
+}
+
+.stork-close-button {
+    @include bordered-block;
+    font-family: $font-body;
+    padding: $search-input-padding;
+
+    background-color: $code-color;
+    padding-left: 1.5rem;
+    padding-right: 1.5rem;
+
+    border-left: none;
+    border-top-left-radius: 0;
+    border-bottom-left-radius: 0;
+}
+
+.stork-output-visible {
+    @include bordered-block;
+
+    border-top: none;
+}
+
+.stork-result, .stork-message, .stork-attribution {
+    padding: $search-element-padding;
+}
+
+.stork-message:not(:last-child), .stork-result  {
+    border-bottom: $standard-border;
+}
+
+.stork-results {
+    margin: 0;
+    padding: 0;
+}
+
+.stork-result {
+    list-style: none;
+
+    &.selected {
+        background-color: $code-color;
+    }
+
+    a:hover {
+        color: black;
+    }
+}
+
+.stork-title, .stork-excerpt {
+    margin: 0;
+}
+
+.stork-excerpt {
+    white-space: nowrap;
+    overflow: hidden;
+    text-overflow: ellipsis;
+}
+
+.stork-title {
+    font-family: $font-heading;
+    font-size: 1.4rem;
+    text-align: left;
+    width: 100%;
+}
+
+.stork-highlight {
+    background-color: lighten($primary-color, 30%);
+}

themes/vanilla/layouts/_default/baseof.toml

@@ -0,0 +1 @@
+{{- block "main" . }}{{- end }}

themes/vanilla/layouts/_default/list.toml.toml

@@ -0,0 +1,12 @@
+[input]
+base_directory = "content/"
+title_boost = "Large"
+files = [
+    {{ range $index , $e := .Site.RegularPages }}{{ if $index }}, {{end}}{ filetype = "PlainText", contents = {{ $e.Plain | jsonify }}, title = {{ $e.Title | jsonify }}, url = {{ $e.Permalink | jsonify }} }
+    {{ end }}
+]
+
+[output]
+filename = "index.st"
+excerpts_per_result = 2
+displayed_results_count = 5

themes/vanilla/layouts/_default/single.toml

@@ -0,0 +1,3 @@
+{{ define "main" }}
+{{ .Content }}
+{{ end }}

themes/vanilla/layouts/index.html

@@ -1,10 +1,22 @@
 {{ define "main" }}
 {{ .Content }}
 
+<p>
+    <div class="stork-wrapper">
+        <div class="stork-input-wrapper">
+            <input class="stork-input" data-stork="blog" placeholder="Search (requires JavaScript)"/>
+        </div>
+        <div class="stork-output" data-stork="blog-output"></div>
+    </div>
+</p>
+
 Recent posts:
 <ul class="post-list">
     {{ range first 10 (where (where .Site.Pages.ByDate.Reverse "Section" "blog") ".Kind" "!=" "section") }}
     {{ partial "post.html" . }}
     {{ end }}
 </ul>
+
+<script src="https://files.stork-search.net/stork.js"></script>
+<script>stork.register("blog", "/index.st");</script>
 {{ end }}

themes/vanilla/layouts/partials/head.html

@@ -11,11 +11,13 @@
     {{ $style := resources.Get "scss/style.scss" | resources.ToCSS | resources.Minify }}
     {{ $sidenotes := resources.Get "scss/sidenotes.scss" | resources.ToCSS | resources.Minify }}
     {{ $code := resources.Get "scss/code.scss" | resources.ToCSS | resources.Minify }}
+    {{ $search := resources.Get "scss/search.scss" | resources.ToCSS | resources.Minify }}
     {{ $icon := resources.Get "img/favicon.png" }}
     {{- partial "sidenotes.html" . -}}
     <link rel="stylesheet" href="{{ $style.Permalink }}" media="screen">
     <link rel="stylesheet" href="{{ $sidenotes.Permalink }}" media="screen">
     <link rel="stylesheet" href="{{ $code.Permalink }}" media="screen">
+    <link rel="stylesheet" href="{{ $search.Permalink }}" media="screen">
     <link rel="stylesheet" href="https://cdn.jsdelivr.net/npm/katex@0.11.1/dist/katex.min.css" integrity="sha384-zB1R0rpPzHqg7Kpt0Aljp8JPLqbXI3bhnPWROx27a9N0Ll6ZP/+DiW/UqRcLbRjq" crossorigin="anonymous" media="screen">
     <link rel="icon" type="image/png" href="{{ $icon.Permalink }}">