Add donations

.gitmodules

@@ -1,3 +1,9 @@
 [submodule "code/aoc-2020"]
 	path = code/aoc-2020
 	url = https://dev.danilafe.com/Advent-of-Code/AdventOfCode-2020.git
+[submodule "code/libabacus"]
+	path = code/libabacus
+	url = https://dev.danilafe.com/Experiments/libabacus
+[submodule "themes/vanilla"]
+	path = themes/vanilla
+	url = https://dev.danilafe.com/Web-Projects/vanilla-hugo.git

assets/scss/donate.scss

@@ -0,0 +1,36 @@
+@import "../../themes/vanilla/assets/scss/mixins.scss";
+
+.donation-methods {
+    padding: 0;
+    border: none;
+    border-spacing: 0 0.5rem;
+
+    td {
+        padding: 0;
+        overflow: hidden;
+
+        &:first-child {
+            @include bordered-block;
+            text-align: right;
+            border-right: none;
+            border-top-right-radius: 0;
+            border-bottom-right-radius: 0;
+            padding-left: 0.5em;
+            padding-right: 0.5rem;
+        }
+
+        &:last-child {
+            @include bordered-block;
+            border-top-left-radius: 0;
+            border-bottom-left-radius: 0;
+        }
+    }
+
+    code {
+        width: 100%;
+        box-sizing: border-box;
+        border: none;
+        display: inline-block;
+        padding: 0.25rem;
+    }
+}

code/aoc-coq/day1.v

@@ -1,102 +0,0 @@
-Require Import Coq.Lists.List.
-Require Import Omega.
-
-Definition has_pair (t : nat) (is : list nat) : Prop :=
-  exists n1 n2 : nat, n1 <> n2 /\ In n1 is /\ In n2 is /\ n1 + n2 = t.
-
-Fixpoint find_matching (is : list nat) (total : nat) (x : nat) : option nat :=
-  match is with
-  | nil => None
-  | cons y ys =>
-      if Nat.eqb (x + y) total
-      then Some y
-      else find_matching ys total x 
-  end.
-
-Fixpoint find_sum (is : list nat) (total : nat) : option (nat * nat) :=
-  match is with
-  | nil => None
-  | cons x xs =>
-      match find_matching xs total x with
-      | None => find_sum xs total (* Was buggy! *)
-      | Some y => Some (x, y)
-      end
-  end.
-
-Lemma find_matching_correct : forall is k x y,
-  find_matching is k x = Some y -> x + y = k.
-Proof.
-  intros is. induction is;
-  intros k x y Hev.
-  - simpl in Hev. inversion Hev.
-  - simpl in Hev. destruct (Nat.eqb (x+a) k) eqn:Heq.
-    + injection Hev as H; subst.
-      apply EqNat.beq_nat_eq. auto.
-    + apply IHis. assumption.
-Qed.
-
-Lemma find_matching_skip : forall k x y i is,
-  find_matching is k x = Some y -> find_matching (cons i is) k x = Some y.
-Proof.
-  intros k x y i is Hsmall.
-  simpl. destruct (Nat.eqb (x+i) k) eqn:Heq.
-  - apply find_matching_correct in Hsmall.
-    symmetry in Heq. apply EqNat.beq_nat_eq in Heq.
-    assert (i = y). { omega. } rewrite H. reflexivity.
-  - assumption.
-Qed.
-
-Lemma find_matching_works : forall is k x y, In y is /\ x + y = k ->
-  find_matching is k x = Some y.
-Proof.
-  intros is. induction is;
-  intros k x y [Hin Heq].
-  - inversion Hin.
-  - inversion Hin.
-    + subst a. simpl. Search Nat.eqb.
-      destruct (Nat.eqb_spec (x+y) k).
-      * reflexivity.
-      * exfalso. apply n. assumption.
-    + apply find_matching_skip. apply IHis.
-      split; assumption.
-Qed.
-
-Theorem find_sum_works :
-  forall k is, has_pair k is ->
-  exists x y, (find_sum is k = Some (x, y) /\ x + y = k).
-Proof.
-  intros k is. generalize dependent k.
-  induction is; intros k [x' [y' [Hneq [Hinx [Hiny Hsum]]]]].
-  - (* is is empty. But x is in is! *)
-    inversion Hinx.
-  - (* is is not empty. *)
-    inversion Hinx. 
-    + (* x is the first element. *)
-      subst a. inversion Hiny.
-      * (* y is also the first element; but this is impossible! *)
-        exfalso. apply Hneq. apply H.
-      * (* y is somewhere in the rest of the list.
-           We've proven that we will find it! *)
-        exists x'. simpl.
-        erewrite find_matching_works.
-        { exists y'. split. reflexivity. assumption. }
-        { split; assumption. }
-    + (* x is not the first element. *)
-      inversion Hiny.
-      * (* y is the first element,
-           so x is somewhere in the rest of the list.
-           Again, we've proven that we can find it. *)
-        subst a. exists y'. simpl.
-        erewrite find_matching_works.
-        { exists x'. split. reflexivity. rewrite plus_comm. assumption. }
-        { split. assumption. rewrite plus_comm. assumption. }
-      * (* y is not the first element, either.
-           Of course, there could be another matching pair
-           starting with a. Otherwise, the inductive hypothesis applies. *)
-        simpl. destruct (find_matching is k a) eqn:Hf.
-        { exists a. exists n. split.
-          reflexivity. 
-          apply find_matching_correct with is. assumption. }
-        { apply IHis. unfold has_pair. exists x'. exists y'.
-          repeat split; assumption. }
-Qed.

config-gen.toml

@@ -0,0 +1,5 @@
+[params]
+  [params.submoduleLinks]
+    [params.submoduleLinks.aoc2020]
+      url = "https://dev.danilafe.com/Advent-of-Code/AdventOfCode-2020/src/commit/7a8503c3fe1aa7e624e4d8672aa9b56d24b4ba82"
+      path = "aoc-2020"

content/about.md

@@ -1,6 +1,8 @@
 ---
 title: About
 ---
+{{< donate_css >}}
+
 I'm Daniel, a Computer Science student currently working towards my Master's Degree at Oregon State University.
 Due to my initial interest in calculators and compilers, I got involved in the Programming Language Theory research
 group, gaining same experience in formal verification, domain specific language, and explainable computing.
@@ -8,3 +10,34 @@ group, gaining same experience in formal verification, domain specific language,
 For work, school, and hobby projects, I use a variety of programming languages, most commonly C/C++,
 Haskell, [Crystal](https://crystal-lang.org/), and [Elm](https://elm-lang.org/). I also have experience
 with Java, Python, Haxe, and JavaScript.
+
+A few notes about me or this site:
+* __Correctness__: I mostly write technical content. Even though I proofread my articles, there's
+always a fairly good chance that I'm wrong. You should always use your best judgement when reading
+anything on this site -- if something seems wrong, it may very well be. I'm far from an expert.
+* __Schedule__: I do not have a set post schedule. There are many reasons for this:
+schoolwork, personal life, lack of inspiration. It also takes a _very_ long time for
+me to write a single article. My article on [polymorphic type checking]({{< relref "/blog/10_compiler_polymorphism.md" >}})
+is around 8,000 words long; besides writing it, I have to edit it, link up all the code
+references, and proofread the final result. And of course, I need to write the code and
+occasionally do some research.
+* __Design__: I am doing my best to keep this website accessible and easy on the eyes.
+I'm also doing my best to avoid any and all uses of JavaScript. I used to use a lot of
+uMatrix, and most of the websites I browsed during this time were broken. Similarly,
+a lot of websites were unusable on my weaker machines. So, I'm doing my part and
+making this site usable without any JavaScript, and, as it seems to me, even
+without any CSS.
+* __Source code__: This blog is open source, but not on GitHub. Instead,
+you can find the code on my [Gitea instance](https://dev.danilafe.com/Web-Projects/blog-static).
+If you use this code for your own site, I would prefer that you don't copy the theme.
+
+### Donate
+I don't run ads, nor do I profit from writing anything on here. I have no trouble paying for hosting,
+and I write my articles voluntarily, for my own enjoyment. However, if you found something particularly
+helpful on here, and would like to buy me a cup of coffee or help host the site, you can donate using
+the method(s) below.
+
+{{< donation_methods >}}
+{{< donation_method "Bitcoin" "1BbXPZhdzv4xHq5LYhme3xBiUsHw5fmafd" >}}
+{{< donation_method "Ethereum" "0xd111E49344bEC80570e68EE0A00b87B1EFcb5D56" >}}
+{{< /donation_methods >}}

content/blog/01_aoc_coq.md

@@ -1,8 +1,7 @@
 ---
 title: "Advent of Code in Coq - Day 8"
-date: 2020-12-31T17:55:25-08:00
+date: 2021-01-10T22:48:39-08:00
 tags: ["Advent of Code", "Coq"]
-draft: true
 ---
 
 Huh? We're on day 8? What happened to days 2 through 7?
@@ -39,7 +38,7 @@ we go about using _inference rules_. Let's talk about those next.
 
 #### Inference Rules
 Inference rules are a very general notion. The describe how we can determine (infer) a conclusion
-from a set of assumption. It helps to look at an example. Here's a silly little inference rule:
+from a set of assumptions. It helps to look at an example. Here's a silly little inference rule:
 
 {{< latex >}}
 \frac
@@ -181,7 +180,7 @@ it will add 0 to the accumulator (keeping it the same),
 do nothing, and finally jump back to the beginning. At this point, it will try to run the addition instruction again,
 which is not allowed; thus, the program will terminate.
 
-Did you catch that? The semantics of this language will require more information than just our program itself (which we'll denote \\(p\\)).
+Did you catch that? The semantics of this language will require more information than just our program itself (which we'll denote by \\(p\\)).
 * First, to evaluate the program we will need a program counter, \\(\\textit{c}\\). This program counter
 will tell us the position of the instruction to be executed next. It can also point past the last instruction,
 which means our program terminated successfully. 
@@ -242,16 +241,30 @@ is done evaluating, and is in a "failed" state.
 
 We use \\(\\text{length}(p)\\) to represent the number of instructions in \\(p\\). Note the second premise:
 even if our program counter \\(c\\) is not included in the valid set, if it's "past the end of the program",
-the program terminates in an "ok" state. Here's a rule for terminating in the "ok" state:
+the program terminates in an "ok" state.
+{{< sidenote "left" "avoid-c-note" "Here's a rule for terminating in the \"ok\" state:" >}}
+In the presented rule, we don't use the variable <code>c</code> all that much, and we know its concrete
+value (from the equality premise). We could thus avoid introducing the name \(c\) by
+replacing it with said known value:
+
+{{< latex >}}
+\frac{}
+{(\text{length}(p), a, v) \Rightarrow_{p} (\text{length}(p), a, v)}
+{{< /latex >}}
+
+This introduces some duplication, but that is really because all "base case" evaluation rules
+start and stop in the same state. To work around this, we could define a separate proposition
+to mean "program \(p\) is done in state \(s\)", then \(s\) will really only need to occur once,
+and so will \(\text{length}(p)\). This is, in fact, what we will do later on,
+since being able to talk abut "programs being done" will help us with
+components of our proof.
+{{< /sidenote >}}
 
 {{< latex >}}
 \frac{c = \text{length}(p)}
 {(c, a, v) \Rightarrow_{p} (c, a, v)}
 {{< /latex >}}
 
-{{< todo >}}
-We can make this closer to the Coq version.
-{{< /todo >}}
 When our program counter reaches the end of the program, we are also done evaluating it. Even though
 both rules {{< sidenote "right" "redundant-note" "lead to the same conclusion," >}}
 In fact, if the end of the program is never included in the valid set, the second rule is completely redundant.
@@ -350,8 +363,8 @@ Inductive t A : nat -> Type :=
 ```
 
 The `nil` constructor represents the empty list \\([]\\), and `cons` represents
-the operation of prepending an element (called `h` in the code in \\(x\\) in our inference rules)
+the operation of prepending an element (called `h` in the code and \\(x\\) in our inference rules)
-to another vector of length \\(n\\), which is remains unnamed in the code but is called \\(\\textit{xs}\\) in our rules.
+to another vector of length \\(n\\), which remains unnamed in the code but is called \\(\\textit{xs}\\) in our rules.
 
 These two definitions work together quite well. For instance, suppose we have a vector of length \\(n\\).
 If we were to access its elements by indices starting at 0, we'd be allowed to access indices 0 through \\(n-1\\).
@@ -369,8 +382,6 @@ and convert that index into a \\(\\text{Fin} \\; n\\). We formalize it in a lemm
 
 {{< codelines "Coq" "aoc-2020/day8.v" 80 82 >}}
 
-{{< todo >}}Prove this (at least informally) {{< /todo >}}
-
 There's a little bit of a gotcha here. Instead of translating our above statement literally,
 and returning a value that's the result of "tightening" our input `f`, we return a value
 `f'` that can be "weakened" to `f`. This is because "tightening" is not a total function - 
@@ -378,6 +389,29 @@ it's not always possible to convert a \\(\\text{Fin} \\; (n+1)\\) into a \\(\\te
 However, "weakening" \\(\\text{Fin} \\; n\\) _is_ a total function, since a number less than \\(n\\)
 is, by the transitive property of a total order, also less than \\(n+1\\).
 
+The Coq proof for this claim is as follows:
+
+{{< codelines "Coq" "aoc-2020/day8.v" 88 97 >}}
+
+The `Fin.rectS` function is a convenient way to perform inductive proofs over
+our finite natural numbers. Informally, our proof proceeds as follows:
+
+* If the current finite natural number is zero, take a look at the "bound" (which
+we assume is nonzero, since there isn't a natural number less than zero).
+    * If this "bounding number" is one, our `f` can't be tightened any further,
+    since doing so would create a number less than zero. Fortunately, in this case,
+    `n` must be `0`, so `f` is the finite representation of `n`.
+    * Otherwise, `f` is most definitely a weakened version of another `f'`,
+    since the tightest possible type for zero has a "bounding number" of one, and
+    our "bounding number" is greater than that. We return a tighter version of our finite zero.
+* If our number is a successor of another finite number, we check if that other number
+can itself be tightened.
+    * If it can't be tightened, then our smaller number is a finite representation of
+    `n-1`. This, in turn, means that adding one to it will be the finite representation
+    of `n` (if \\(x\\) is equal to \\(n-1\\), then \\(x+1\\) is equal to \\(n\\)).
+    * If it _can_ be tightened, then so can the successor (if \\(x\\) is less
+    than \\(n-1\\), then \\(x+1\\) is less than \\(n\\)).
+
 Next, let's talk about addition, specifically the kind of addition done by the \\(\\texttt{jmp}\\) instruction.
 We can always add an integer to a natural number, but we can at best guarantee that the result
 will be an integer. For instance, we can add `-1000` to `1`, and get `-999`, which is _not_ a natural
@@ -393,14 +427,11 @@ that Coq provides facilities for working with arbitrary implementations of integ
 without relying on how they are implemented under the hood. This can be seen in its
 [`Coq.ZArith.Int`](https://coq.inria.fr/library/Coq.ZArith.Int.html) module,
 which describes what functions and types an implementation of integers should provide.
-Among those is `t`, the type an integer in such an arbitrary implementation. We too
+Among those is `t`, the type of an integer in such an arbitrary implementation. We too
 will not make an assumption about how the integers are implemented, and simply
 use this generic `t` from now on.
 
-#### Semantics in Coq
+Now, suppose we wanted to write a function that _does_ return a valid program
-
-Now that we've seen finite sets and vectors, it's time to use them to
-encode our semantics in Coq. Let's start with jumps. Suppose we wanted to write a function that _does_ return a valid program
 counter after adding the offset to it. Since it's possible for this function to fail
 (for instance, if the offset is very negative), it has to return `option (fin (S n))`.
 That is, this function may either fail (returning `None`) or succeed, returning
@@ -409,11 +440,93 @@ the function in Coq (again, don't worry too much about the definition):
 
 {{< codelines "Coq" "aoc-2020/day8.v" 61 61 >}}
 
-But earlier, didn't we say:
+We will make use of this function when we define and verify our semantics.
+Let's take a look at that next.
+
+#### Semantics in Coq
+
+Now that we've seen finite sets and vectors, it's time to use them to
+encode our semantics in Coq. Before we do anything else, we need
+to provide Coq definitions for the various components of our
+language, much like what we did with `tinylang`. We can start with opcodes:
+
+{{< codelines "Coq" "aoc-2020/day8.v" 20 23 >}}
+
+Now we can define a few other parts of our language and semantics, namely
+states, instructions and programs (which I called "inputs" since, we'll, they're
+our puzzle input). A state is simply the 3-tuple of the program counter, the set
+of valid program counters, and the accumulator. We write it as follows:
+
+{{< codelines "Coq" "aoc-2020/day8.v" 33 33 >}}
+
+The star `*` is used here to represent a [product type](https://en.wikipedia.org/wiki/Product_type)
+rather than arithmetic multiplication. Our state type accepts an argument,
+`n`, much like a finite natural number or a vector. In fact, this `n` is passed on
+to the state's program counter and set types. Rightly, a state for a program
+of length \\(n\\) will not be of the same type as a state for a program of length \\(n+1\\).
+
+An instruction is also a tuple, but this time containing only two elements: the opcode and
+the number. We write this as follows:
+
+{{< codelines "Coq" "aoc-2020/day8.v" 36 36 >}}
+
+Finally, we have to define the type of a program. This type will also be
+indexed by `n`, the program's length. A program of length `n` is simply a
+vector of instructions `inst` of length `n`. This leads to the following
+definition:
+
+{{< codelines "Coq" "aoc-2020/day8.v" 38 38 >}}
+
+So far, so good! Finally, it's time to get started on the semantics themselves.
+We begin with the inductive definition of \\((\\rightarrow_i)\\).
+I think this is fairly straightforward. However, we do use
+`t` instead of \\(n\\) from the rules, and we use `FS`
+instead of \\(+1\\). Also, we make the formerly implicit
+assumption that \\(c+n\\) is valid explicit, by
+providing a proof that `valid_jump_t pc t = Some pc'`.
+
+{{< codelines "Coq" "aoc-2020/day8.v" 103 110 >}}
+
+Next, it will help us to combine the premises for
+"failed" and "ok" terminations into Coq data types.
+This will make it easier for us to formulate a lemma later on.
+Here are the definitions:
+
+{{< codelines "Coq" "aoc-2020/day8.v" 112 117 >}}
+
+Since all of out "termination" rules start and
+end in the same state, there's no reason to
+write that state twice. Thus, both `done`
+and `stuck` only take the input `inp`,
+and the state, which includes the accumulator
+`acc`, the set of allowed program counters `v`, and
+the program counter at which the program came to an end.
+When the program terminates successfully, this program
+counter will be equal to the length of the program `n`,
+so we use `nat_to_fin n`. On the other hand, if the program
+terminates in as stuck state, it must be that it terminated
+at a program counter that points to an instruction. Thus, this
+program counter is actually a \\(\\text{Fin} \\; n\\), and not
+a \\(\\text{Fin} \\ (n+1)\\), and is not in the set of allowed program counters.
+We use the same "weakening" trick we saw earlier to represent
+this.
+
+Finally, we encode the three inference rules we came up with:
+
+{{< codelines "Coq" "aoc-2020/day8.v" 119 126 >}}
+
+Notice that we fused two of the premises in the last rule.
+Instead of naming the instruction at the current program
+counter (by writing \\(p[c] = i\\)) and using it in another premise, we simply use
+`nth inp pc`, which corresponds to \\(p[c]\\) in our
+"paper" semantics.
+
+Before we go on writing some actual proofs, we have
+one more thing we have to address. Earlier, we said:
 
 > All jumps will lead either to an instruction, or right to the end of a program.
 
-To make Coq aware of this constraint, we'll have to formalize this notion. To
+To make Coq aware of this constraint, we'll have to formalize it. To
 start off, we'll define the notion of a "valid instruction", which is guaranteed
 to keep the program counter in the correct range.
 There are a couple of ways to do this, but we'll use yet another definition based
@@ -423,20 +536,20 @@ is perfectly valid for a program with thousands of instructions, but if it occur
 in a program with only 3 instructions, it will certainly lead to disaster. Specifically,
 the validity of an instruction depends on the length of the program in which it resides,
 and the program counter at which it's encountered.
-Thus, we refine our idea of validity to "being valid for a program of length n at program counter f".
+Thus, we refine our idea of validity to "being valid for a program of length \\(n\\) at program counter \\(f\\)".
 For this, we can use the following two inference rules:
 
 {{< latex >}}
 \frac
 {c : \text{Fin} \; n}
-{\texttt{acc} \; t \; \text{valid for} \; n, c }
+{\texttt{add} \; t \; \text{valid for} \; n, c }
 \quad
 \frac
 {c : \text{Fin} \; n \quad o \in \{\texttt{nop}, \texttt{jmp}\} \quad J_v(c, t) = \text{Some} \; c' }
 {o \; t \; \text{valid for} \; n, c }
 {{< /latex >}}
 
-The first rule states that if a program has length \\(n\\), then it's valid
+The first rule states that if a program has length \\(n\\), then \\(\\texttt{add}\\) is valid
 at any program counter whose value is less than \\(n\\). This is because running
 \\(\\texttt{add}\\) will increment the program counter \\(c\\) by 1,
 and thus, create a new program counter that's less than \\(n+1\\),
@@ -444,11 +557,12 @@ which, as we discussed above, is perfectly valid.
 
 The second rule works for the other two instructions. It has an extra premise:
 the result of `jump_valid_t` (written as \\(J_v\\)) has to be \\(\\text{Some} \\; c'\\),
-that is, `jump_valid_t` must succeed. Now, if an instruction satisfies these validity
+that is, `jump_valid_t` must succeed. Note that we require this even for no-ops,
-rules for a given program at a given program counter, evaluating it will always
+since it later turns out that one of the them may be a jump after all.
-result in a program counter that has a proper value.
 
-We encode this in Coq as follows:
+We now have our validity rules. If an instruction satisfies them for a given program
+and at a given program counter, evaluating it will always result in a program counter that has a proper value.
+We encode the rules in Coq as follows:
 
 {{< codelines "Coq" "aoc-2020/day8.v" 152 157 >}}
 
@@ -470,44 +584,357 @@ encode this in Coq, too:
 
 {{< codelines "Coq" "aoc-2020/day8.v" 160 161 >}}
 
-In the above, we use `input n` to mean "a program of length `n`".
+In the above, `n` is made implicit where possible.
-This is just an alias for `vect inst n`, a vector of instructions
-of length `n`. In the above, `n` is made implicit where possible.
 Since \\(c\\) (called `pc` in the code) is of type \\(\\text{Fin} \\; n\\), there's no
-need to write \\(n\\) _again_.
+need to write \\(n\\) _again_. The curly braces tell Coq to infer that
+argument where possible.
 
-Finally, it's time to get started on the semantics themselves.
+### Proving Termination
-We start with the inductive definition of \\((\\rightarrow_i)\\).
+Here we go! It's finally time to make some claims about our
-I think this is fairly straightforward. We use
+definitions. Who knows - maybe we wrote down total garbage!
-`t` instead of \\(n\\) from the rules, and we use `FS`
+We will be creating several related lemmas and theorems.
-instead of \\(+1\\). Also, we make the formerly implicit
+All of them share two common assumptions:
-assumption that \\(c+n\\) is valid explicit, by
-providing a proof that `valid_jump_t pc t = Some pc'`.
 
-{{< codelines "Coq" "aoc-2020/day8.v" 103 110 >}}
+* We have some valid program `inp` of length `n`.
+* This program is a valid input, that is, `valid_input` holds for it.
+There's no sense in arguing based on an invalid input program.
 
-Next, it will help us to combine the premises for a
+We represent these grouped assumptions by opening a Coq
-"failed" and "ok" terminations into Coq data types.
+`Section`, which we call `ValidInput`, and listing our assumptions:
-This will help us formulate a lemma later on. Here they are:
 
-{{< codelines "Coq" "aoc-2020/day8.v" 112 117 >}}
+{{< codelines "Coq" "aoc-2020/day8.v" 163 166 >}}
 
-Since all of out "termination" rules start and
+We had to also explicitly mention the length `n` of our program.
-end in the same state, there's no reason to
+From now on, the variables `n`, `inp`, and `Hv` will be
-write that state twice. Thus, both `done`
+available to all of the proofs we write in this section.
-and `stuck` only take the input `inp`,
+The first proof is rather simple. The claim is:
-and the state, which includes the accumulator
-`acc`, set of allowed program counters `v`, and
-the program counter at which the program came to an end.
-When the program terminates successfully, this program
-counter will be equal to the length of the program `n`,
-so we use `nat_to_fin n`. On the other hand, if the program
-terminates in as stuck state, it must be that it terminated
-at a program counter that points to an instruction. Thus, this
-program counter is actually a \\(\\text{Fin} \\; n\\), and not
-a \\(\\text{Fin} \\ (n+1)\\) (we use the same "weakening" trick
-we saw earlier), and is not in the set of allowed program counters.
 
-Finally, we encode the three inference rules we came up with:
+> For our valid program, at any program counter `pc`
+and accumulator `acc`, there must exist another program
+counter `pc'` and accumulator `acc'` such that the
+instruction evaluation relation \\((\rightarrow_i)\\)
+connects the two. That is, valid addresses aside,
+we can always make a step.
 
-{{< codelines "Coq" "aoc-2020/day8.v" 119 126 >}}
+Here is this claim encoded in Coq:
+
+{{< codelines "Coq" "aoc-2020/day8.v" 168 169 >}}
+
+We start our proof by introducing all the relevant variables into
+the global context. I've mentioned this when I wrote about
+day 1, but here's the gist: the `intros` keyword takes
+variables from a `forall`, and makes them concrete.
+In short, `intros x` is very much like saying "suppose
+we have an `x`", and going on with the proof.
+
+{{< codelines "Coq" "aoc-2020/day8.v" 170 171 >}}
+
+Here, we said "take any program counter `pc` and any
+accumulator `acc`". Now what? Well, first of all,
+we want to take a look at the instruction at the current
+`pc`. We know that this instruction is a combination
+of an opcode and a number, so we use `destruct` to get
+access to both of these parts:
+
+{{< codelines "Coq" "aoc-2020/day8.v" 172 172 >}}
+
+Now, Coq reports the following proof state:
+
+```
+1 subgoal
+
+n : nat
+inp : input n
+Hv : valid_input inp
+pc : Fin.t n
+acc : t
+o : opcode
+t0 : t
+Hop : nth inp pc = (o, t0)
+
+========================= (1 / 1)
+
+exists (pc' : fin (S n)) (acc' : t),
+  step_noswap (o, t0) (pc, acc) (pc', acc')
+```
+
+We have some opcode `o`, and some associated number
+`t0`, and we must show that there exist a `pc'`
+and `acc'` to which we can move on. To prove
+that something exists in Coq, we must provide
+an instance of that "something". If we claim
+that there exists a dog that's not a good boy,
+we better have this elusive creature in hand.
+In other words, proofs in Coq are [constructive](https://en.wikipedia.org/wiki/Constructive_proof).
+Without knowing the kind of operation we're dealing with, we can't
+say for sure how the step will proceed. Thus, we proceed by
+case analysis on `o`.
+
+{{< codelines "Coq" "aoc-2020/day8.v" 173 173 >}}
+
+There are three possible cases we have to consider,
+one for each type of instruction.
+
+* If the instruction is \\(\\texttt{add}\\), we know
+that `pc' = pc + 1` and `acc' = acc + t0`. That is,
+the program counter is simply incremented, and the accumulator
+is modified with the number part of the instruction.
+* If the instruction is \\(\\texttt{nop}\\), the program
+coutner will again be incremented (`pc' = pc + 1`),
+but the accumulator will stay the same, so `acc' = acc`.
+* If the instruction is \\(\\texttt{jmp}\\), things are
+more complicated. We must rely on the assumption
+that our input is valid, which tells us that adding
+`t0` to our `pc` will result in `Some f`, and not `None`.
+Given this, we have `pc' = f`, and `acc' = acc`.
+
+This is how these three cases are translated to Coq:
+
+{{< codelines "Coq" "aoc-2020/day8.v" 174 177 >}}
+
+For the first two cases, we simply provide the
+values we expect for `pc'` and `acc'`, and
+apply the corresponding inference rule that
+is satisfied by these values. For the third case, we have
+to invoke `Hv`, the hypothesis that our input is valid.
+In particular, we care about the instruction at `pc`,
+so we use `specialize` to plug `pc` into the more general
+hypothesis. We then replace `nth inp pc` with its known
+value, `(jmp, t0)`. This tells us the following, in Coq's words:
+
+```
+Hv : valid_inst (jmp, t0) pc
+```
+
+That is, `(jmp, t0)` is a valid instruction at `pc`. Then, using
+Coq's `inversion` tactic, we ask: how is this possible? There is
+only one inference rule that gives us such a conclusion, and it is named `valid_inst_jmp`
+in our Coq code. Since we have a proof that our `jmp` is valid,
+it must mean that this rule was used. Furthermore, since this
+rule requires that `valid_jump_t` evaluates to `Some f'`, we know
+that this must be the case here! Coq now has adds the following
+two lines to our proof state:
+
+```
+f' : fin (S n)
+H0 : valid_jump_t pc t0 = Some f'
+```
+
+Finally, we specify, as mentioned earlier, that `pc' = f'` and `acc' = acc`.
+As before, we apply the corresponding step rule for `jmp`. When it asks
+for a proof that `valid_jump_t` produces a valid program counter,
+we hand it `H0` using `apply H0`. And with that, Coq is happy!
+
+Next, we prove a claim that a valid program can always do _something_,
+and that something is one of three things:
+
+* It can terminate in the "ok" state if the program counter
+reaches the programs' end.
+* It can terminate with an error if it's currently at a program
+counter that is not included in the valid set.
+* Otherwise, it can run the current instruction and advance
+to a "next" state.
+
+Alternatively, we could say that one of the inference rules
+for \\((\\Rightarrow_p)\\) must apply. This is not the case if the input
+is not valid, since, as I said
+before, an arbitrary input program can lead us to jump
+to a negative address (or to an address _way_ past the end of the program).
+Here's the claim, translated to Coq:
+
+{{< codelines "Coq" "aoc-2020/day8.v" 181 186 >}}
+
+Informally, we can prove this as follows:
+
+* If the current program counter is equal to the length
+of the program, we've reached the end. Thus, the program
+can terminate in the "ok" state.
+* Otherwise, the current program counter must be
+less than the length of the program.
+    * If we've already encountered this program counter (that is,
+    if it's gone from the set of valid program counters),
+    then the program will terminate in the "error" state.
+    * Otherwise, the program counter is in the set of
+    valid instructions. By our earlier theorem, in a valid
+    program, the instruction at any program counter can be correctly
+    executed, taking us to the next state. Now too
+    our program can move to this next state.
+
+Below is the Coq translation of the above.
+
+{{< codelines "Coq" "aoc-2020/day8.v" 187 203 >}}
+
+It doesn't seem like we're that far from being done now.
+A program can always take a step, and each time it does,
+the set of valid program counters decreases in size. Eventually,
+this set will become empty, so if nothing else, our program will
+eventually terminate in an "error" state. Thus, it will stop
+running no matter what. 
+
+This seems like a task for induction, in this case on the size
+of the valid set. In particular, strong mathematical induction
+{{< sidenote "right" "strong-induction-note" "seem to work best." >}}
+Why strong induction? If we remove a single element from a set,
+its size should decrease strictly by 1. Thus, why would we need
+to care about sets of <em>all</em> sizes less than the current
+set's size?<br>
+<br>
+Unfortunately, we're not working with purely mathematical sets.
+Coq's default facility for sets is simply a layer on top
+of good old lists, and makes no effort to be "correct by construction".
+It is thus perfectly possible to have a "set" which inlcudes an element
+twice. Depending on the implementation of <code>set_remove</code>,
+we may end up removing the repeated element multiple times, thereby
+shrinking the length of our list by more than 1. I'd rather
+not worry about implementation details like that.
+{{< /sidenote >}}
+Someone on StackOverflow [implemented this](https://stackoverflow.com/questions/45872719/how-to-do-induction-on-the-length-of-a-list-in-coq),
+so I'll just use it. The Coq theorem corresonding to strong induction
+on the length of a list is as follows:
+
+{{< codelines "Coq" "aoc-2020/day8.v" 205 207 >}}
+
+It reads,
+
+> If for some list `l`, the property `P` holding for all lists
+shorter than `l` means that it also holds for `l` itself, then
+`P` holds for all lists.
+
+This is perhaps not particularly elucidating. We can alternatively
+think of this as trying to prove some property for all lists `l`.
+We start with all empty lists. Here, we have nothing else to rely
+on; there are no lists shorter than the empty list, and our property
+must hold for all empty lists. Then, we move on to proving
+the property for all lists of length 1, already knowing that it holds
+for all empty lists. Once we're done there, we move on to proving
+that `P` holds for all lists of length 2, now knowing that it holds
+for all empty lists _and_ all lists of length 1. We continue
+doing this, eventually covering lists of any length.
+
+Before proving termination, there's one last thing we have to
+take care off. Coq's standard library does not come with
+a proof that removing an element from a set makes it smaller;
+we have to provide it ourselves. Here's the claim encoded
+in Coq:
+
+{{< codelines "Coq" "aoc-2020/day8.v" 217 219 >}}
+
+This reads, "if a set `s` contains a finite natural
+number `f`, removing `f` from `s` reduces the set's size".
+The details of the proof are not particularly interesting,
+and I hope that you understand intuitively why this is true.
+Finally, we make our termination claim.
+
+{{< codelines "Coq" "aoc-2020/day8.v" 230 231 >}}
+
+It's quite a strong claim - given _any_ program counter,
+set of valid addresses, and accumulator, a valid input program
+will terminate. Let's take a look at the proof.
+
+{{< codelines "Coq" "aoc-2020/day8.v" 232 234 >}}
+
+We use `intros` again. However, it brings in variables
+in order, and we really only care about the _second_ variable.
+We thus `intros` the first two, and then "put back" the first
+one using `generalize dependent`. Then, we proceed by
+induction on length, as seen above.
+
+{{< codelines "Coq" "aoc-2020/day8.v" 235 236>}}
+
+Now we're in the "inductive step". Our inductive hypothesis
+is that any set of valid addresses smaller than the current one will
+guarantee that the program will terminate. We must show
+that using our set, too, will guarantee termination. We already
+know that a valid input, given a state, can have one of three
+possible outcomes: "ok" termination, "failed" termination,
+or a "step". We use `destruct` to take a look at each of these
+in turn. The first two cases ("ok" termination and "failed" termination)
+are fairly trivial:
+
+{{< codelines "Coq" "aoc-2020/day8.v" 237 240 >}}
+
+We basically connect the dots between the premises (in a form like `done`)
+and the corresponding inference rule (`run_noswap_ok`). The more
+interesting case is when we can take a step.
+
+{{< codelines "Coq" "aoc-2020/day8.v" 241 253 >}}
+
+Since we know we can take a step, we know that we'll be removing
+the current program counter from the set of valid addresses. This
+set must currently contain the present program counter (since otherwise
+we'd have "failed"), and thus will shrink when we remove it. This,
+in turn, lets us use the inductive hypothesis: it tells us that no matter the
+program counter or accumulator, if we start with this new "shrunk"
+set, we will terminate in some state. Coq's constructive
+nature helps us here: it doesn't just tells us that there is some state
+in which we terminate - it gives us that state! We use `edestruct` to get
+a handle on this final state, which Coq automatically names `x`. At this
+time Coq still isn't convinced that our new set is smaller, so we invoke
+our earlier `set_remove_length` theorem to placate it.
+
+We now have all the pieces: we know that we can take a step, removing
+the current program counter from our current set. We also know that
+with that newly shrunken set, we'll terminate in some final state `x`.
+Thus, all that's left to say is to apply our "step" rule. It asks
+us for three things:
+
+1. That the current program counter is in the set. We've long since
+established this, and `auto` takes care of that.
+2. That a step is possible. We've already established this, too,
+since we're in the "can take a step" case. We apply `Hst`,
+the hypothesis that confirms that we can, indeed, step.
+3. That we terminate after this. The `x` we got
+from our induction hypothesis came with a proof that
+running with the "next" program counter and accumulator
+will result in termination. We apply this proof, automatically
+named `H0` by Coq.
+
+And that's it! We've proved that a program terminates no matter what.
+This has also (almost!) given us a solution to part 1. Consider the case
+in which we start with program counter 0, accumulator 0, and the "full"
+set of allowed program counters. Since our proof works for _all_ configurations,
+it will also work for this one. Furthermore, since Coq proofs are constructive,
+this proof will __return to us the final program counter and accumulator!__
+This is precisely what we'd need to solve part 1.
+
+But wait, almost? What's missing? We're missing a few implementation details:
+* We've not provided a concrete impelmentation of integers. The simplest
+thing to do here would be to use [`Coq.ZArith.BinInt`](https://coq.inria.fr/library/Coq.ZArith.BinInt.html),
+for which there is a module [`Z_as_Int`](https://coq.inria.fr/library/Coq.ZArith.Int.html#Z_as_Int)
+that provides `t` and friends.
+* We assumed (reasonably, I would say) that it's possible to convert a natural
+number to an integer. If we're using the aforementioned `BinInt` module,
+we can use [`Z.of_nat`](https://coq.inria.fr/library/Coq.ZArith.BinIntDef.html#Z.of_nat).
+* We also assumed (still reasonably) that we can try convert an integer
+back to a finite natural number, failing if it's too small or too large.
+There's no built-in function for this, but `Z`, for one, distinguishes
+between the "positive", "zero", and "negative" cases, and we have
+`Pos.to_nat` for the positive case.
+
+Well, I seem to have covered all the implementation details. Why not just
+go ahead and solve the problem? I tried, and ran into two issues:
+
+* Although this is "given", we assumed that our input program will be
+valid. For us to use the result of our Coq proof, we need to provide it
+a constructive proof that our program is valid. Creating this proof is tedious
+in theory, and quite difficult in practice: I've run into a
+strange issue trying to pattern match on finite naturals.
+* Even supposing we _do_ have a proof of validity, I'm not certain
+if it's possible to actually extract an answer from it. It seems
+that Coq distinguishes between proofs (things of type `Prop`) and
+values (things of type `Set`). things of types `Prop` are supposed
+to be _erased_. This means that when you convert Coq code,
+to, say, Haskell, you will see no trace of any `Prop`s in that generated
+code. Unfortunately, this also means we
+[can't use our proofs to construct values](https://stackoverflow.com/questions/27322979/why-coq-doesnt-allow-inversion-destruct-etc-when-the-goal-is-a-type),
+even though our proof objects do indeed contain them.
+
+So, we "theoretically" have a solution to part 1, down to the algorithm
+used to compute it and a proof that our algorithm works. In "reality", though, we
+can't actually use this solution to procure an answer. Like we did with day 1, we'll have
+to settle for only a proof.
+
+Let's wrap up for this post. It would be more interesting to devise and
+formally verify an algorithm for part 2, but this post has already gotten
+quite long and contains a lot of information. Perhaps I will revisit this
+at a later time. Thanks for reading!

content/blog/codelines/index.md

@@ -0,0 +1,268 @@
+---
+title: "Pleasant Code Includes with Hugo"
+date: 2021-01-13T21:31:29-08:00
+tags: ["Hugo"]
+---
+
+Ever since I started [the compiler series]({{< relref "00_compiler_intro.md" >}}),
+I began to include more and more fragments of code into my blog.
+I didn't want to be copy-pasting my code between my project
+and my Markdown files, so I quickly wrote up a Hugo [shortcode](https://gohugo.io/content-management/shortcodes/)
+to pull in other files in the local directory. I've since improved on this
+some more, so I thought I'd share what I created with others.
+
+### Including Entire Files and Lines
+My needs for snippets were modest at first. For the most part,
+I had a single code file that I wanted to present, so it was
+acceptable to plop it in the middle of my post in one piece.
+The shortcode for that was quite simple:
+
+```
+{{ highlight (readFile (printf "code/%s" (.Get 1))) (.Get 0) "" }}
+```
+
+This leverages Hugo's built-in [`highlight`](https://gohugo.io/functions/highlight/)
+function to provide syntax highlighting to the included snippet. Hugo
+doesn't guess at the language of the code, so you have to manually provide
+it. Calling this shortcode looks as follows:
+
+```
+{{</* codeblock "C++" "compiler/03/type.hpp" */>}}
+```
+
+Note that this implicitly adds the `code/` prefix to all
+the files I include. This is a personal convention: I want
+all my code to be inside a dedicated directory.
+
+Of course, including entire files only takes you so far.
+What if you only need to discuss a small part of your code?
+Alternaitvely, what if you want to present code piece-by-piece,
+in the style of literate programming? I quickly ran into the
+need to do this, for which I wrote another shortcode:
+
+```
+{{ $s := (readFile (printf "code/%s" (.Get 1))) }}
+{{ $t := split $s "\n" }}
+{{ if not (eq (int (.Get 2)) 1) }}
+{{ .Scratch.Set "u" (after (sub (int (.Get 2)) 1) $t) }}
+{{ else }}
+{{ .Scratch.Set "u" $t }}
+{{ end }}
+{{ $v := first (add (sub (int (.Get 3)) (int (.Get 2))) 1) (.Scratch.Get "u") }}
+{{ if (.Get 4) }}
+{{ .Scratch.Set "opts" (printf ",%s" (.Get 4)) }}
+{{ else }}
+{{ .Scratch.Set "opts" "" }}
+{{ end }}
+{{ highlight (delimit $v "\n") (.Get 0) (printf "linenos=table,linenostart=%d%s" (.Get 2) (.Scratch.Get "opts")) }}
+```
+
+This shortcode takes a language and a filename as before, but it also takes
+the numbers of the first and last lines indicating the part of the code that should be included. After
+splitting the contents of the file into lines, it throws away all lines before and
+after the window of code that you want to include. It seems to me (from my commit history)
+that Hugo's [`after`](https://gohugo.io/functions/after/) function (which should behave
+similarly to Haskell's `drop`) doesn't like to be given an argument of `0`.
+I had to add a special case for when this would occur, where I simply do not invoke `after` at all.
+The shortcode can be used as follows:
+
+```
+{{</* codelines "C++" "compiler/04/ast.cpp" 19 22 */>}}
+```
+
+To support a fuller range of Hugo's functionality, I also added an optional argument that
+accepts Hugo's Chroma settings. This way, I can do things like highlight certain
+lines in my code snippet, which is done as follows:
+
+```
+{{</* codelines "Idris" "typesafe-interpreter/TypesafeIntrV3.idr" 31 39 "hl_lines=7 8 9" */>}}
+```
+
+Note that the `hl_lines` field doesn't seem to work properly with `linenostart`, which means
+that the highlighted lines are counted from 1 no matter what. This is why in the above snippet,
+although I include lines 31 through 39, I feed lines 7, 8, and 9 to `hl_lines`. It's unusual,
+but hey, it works!
+
+### Linking to Referenced Code
+Some time after implementing my initial system for including lines of code,
+I got an email from a reader who pointed out that it was hard for them to find
+the exact file I was referencing, and to view the surrounding context of the
+presented lines. To address this, I decided that I'd include the link
+to the file in question. After all, my website and all the associated
+code is on a [Git server I host](https://dev.danilafe.com/Web-Projects/blog-static),
+so any local file I'm referencing should -- assuming it was properly committed --
+show up there, too. I hardcoded the URL of the `code` directory on the web interface,
+and appended the relative path of each included file to it. The shortcode came out as follows:
+
+```
+{{ $s := (readFile (printf "code/%s" (.Get 1))) }}
+{{ $t := split $s "\n" }}
+{{ if not (eq (int (.Get 2)) 1) }}
+{{ .Scratch.Set "u" (after (sub (int (.Get 2)) 1) $t) }}
+{{ else }}
+{{ .Scratch.Set "u" $t }}
+{{ end }}
+{{ $v := first (add (sub (int (.Get 3)) (int (.Get 2))) 1) (.Scratch.Get "u") }}
+{{ if (.Get 4) }}
+{{ .Scratch.Set "opts" (printf ",%s" (.Get 4)) }}
+{{ else }}
+{{ .Scratch.Set "opts" "" }}
+{{ end }}
+<div class="highlight-group">
+    <div class="highlight-label">From <a href="https://dev.danilafe.com/Web-Projects/blog-static/src/branch/master/code/{{ .Get 1 }}">{{ path.Base (.Get 1) }}</a>,
+        {{ if eq (.Get 2) (.Get 3) }}line {{ .Get 2 }}{{ else }} lines {{ .Get 2 }} through {{ .Get 3 }}{{ end }}</div>
+    {{ highlight (delimit $v "\n") (.Get 0) (printf "linenos=table,linenostart=%d%s" (.Get 2) (.Scratch.Get "opts")) }}
+</div>
+```
+
+This results in code blocks like the one in the image below. The image
+is the result of the `codelines` call for the Idris language, presented above.
+
+{{< figure src="example.png" caption="An example of how the code looks." class="medium" >}}
+
+I got a lot of mileage out of this setup . . . until I wanted to include code from _other_ git repositories.
+For instance, I wanted to talk about my [Advent of Code](https://adventofcode.com/) submissions,
+without having to copy-paste the code into my blog repository!
+
+### Code from Submodules
+My first thought when including code from other repositories was to use submodules.
+This has the added advantage of "pinning" the version of the code I'm talking about,
+which means that even if I push significant changes to the other repository, the code
+in my blog will remain the same. This, in turn, means that all of my `codelines`
+shortcodes will work as intended.
+
+The problem is, most Git web interfaces (my own included) don't display paths corresponding
+to submodules. Thus, even if all my code is checked out and Hugo correctly
+pulls the selected lines into its HTML output, the _links to the file_ remain
+broken!
+
+There's no easy way to address this, particularly because _different submodules
+can be located on different hosts_! The Git URL used for a submodule is
+not known to Hugo (since, to the best of my knowledge, it can't run
+shell commands), and it could reside on `dev.danilafe.com`, or `github.com`,
+or elsewhere. Fortunately, it's fairly easy to tell when a file is part
+of a submodule, and which submodule that is. It's sufficient to find
+the longest submodule path that matches the selected file. If no
+submodule path matches, then the file is part of the blog repository,
+and no special action is needed.
+
+Of course, this means that Hugo needs to be made aware of the various
+submodules in my repository. It also needs to be aware of the submodules
+_inside_ those submodules, and so on: it needs to be recursive. Git
+has a command to list all submodules recursively:
+
+```Bash
+git submodule status --recursive
+```
+
+However, this only prints the commit, submodule path, and the upstream branch.
+I don't think there's a way to list the remotes' URLs with this command; however,
+we do _need_ the URLs, since that's how we create links to the Git web interfaces.
+
+There's another issue: how do we let Hugo know about the various submodules,
+even if we can find them? Hugo can read files, but doing any serious
+text processing is downright impractical. However, Hugo
+itself is not able to run commands, so it needs to be able to read in
+the output of another command that _can_ find submodules.
+
+I settled on using Hugo's `params` configuration option. This
+allows users to communicate arbitrary properties to Hugo themes
+and templates. In my case, I want to communicate a collection
+of submodules. I didn't know about TOML's inline tables, so
+I decided to represent this collection as a map of (meaningless)
+submodule names to tables:
+
+```TOML
+[params]
+  [params.submoduleLinks]
+    [params.submoduleLinks.aoc2020]
+      url = "https://dev.danilafe.com/Advent-of-Code/AdventOfCode-2020/src/commit/7a8503c3fe1aa7e624e4d8672aa9b56d24b4ba82"
+      path = "aoc-2020"
+```
+
+Since it was seemingly impossible to wrangle Git into outputting
+all of this information using one command, I decided
+to write a quick Ruby script to generate a list of submodules
+as follows. I had to use `cd` in one of my calls to Git
+because Git's `--git-dir` option doesn't seem to work
+with submodules, treating them like a "bare" checkout.
+I also chose to use an allowlist of remote URLs,
+since the URL format for linking to files in a
+particular repository differs from service to service.
+For now, I only use my own Git server, so only `dev.danilafe.com`
+is allowed; however, just by adding `elsif`s to my code,
+I can add other services in the future.
+
+```Ruby
+puts "[params]"
+puts "  [params.submoduleLinks]"
+
+def each_submodule(base_path)
+  `cd #{base_path} && git submodule status`.lines do |line|
+    hash, path = line[1..].split " "
+    full_path = "#{base_path}/#{path}"
+    url = `git config --file #{base_path}/.gitmodules --get 'submodule.#{path}.url'`.chomp.delete_suffix(".git")
+    safe_name = full_path.gsub(/\/|-|_\./, "")
+
+    if url =~ /dev.danilafe.com/
+      file_url = "#{url}/src/commit/#{hash}"
+    else
+      raise "Submodule URL #{url.dump} not in a known format!"
+    end
+
+    yield ({ :path => full_path, :url => file_url, :name => safe_name })
+    each_submodule(full_path) { |m| yield m }
+  end
+end
+
+each_submodule(".") do |m|
+  next unless m[:path].start_with? "./code/"
+  puts "    [params.submoduleLinks.#{m[:name].delete_prefix(".code")}]"
+  puts "      url = #{m[:url].dump}"
+  puts "      path = #{m[:path].delete_prefix("./code/").dump}"
+end
+```
+
+I pipe the output of this script into a separate configuration file
+called `config-gen.toml`, and then run Hugo as follows:
+
+```
+hugo --config config.toml,config-gen.toml
+```
+
+Finally, I had to modify my shortcode to find and handle the longest submodule prefix.
+Here's the relevant portion, and you can
+[view the entire file here](https://dev.danilafe.com/Web-Projects/blog-static/src/commit/bfeae89ab52d1696c4a56768b7f0c6682efaff82/themes/vanilla/layouts/shortcodes/codelines.html).
+
+```
+{{ .Scratch.Set "bestLength" -1 }}
+{{ .Scratch.Set "bestUrl" (printf "https://dev.danilafe.com/Web-Projects/blog-static/src/branch/master/code/%s" (.Get 1)) }}
+{{ $filePath := (.Get 1) }}
+{{ $scratch := .Scratch }}
+{{ range $module, $props := .Site.Params.submoduleLinks }}
+{{ $path := index $props "path" }}
+{{ $bestLength := $scratch.Get "bestLength" }}
+{{ if and (le $bestLength (len $path)) (hasPrefix $filePath $path) }}
+{{ $scratch.Set "bestLength" (len $path) }}
+{{ $scratch.Set "bestUrl" (printf "%s%s" (index $props "url") (strings.TrimPrefix $path $filePath)) }}
+{{ end }}
+{{ end }}
+```
+
+And that's what I'm using at the time of writing!
+
+### Conclusion
+My current system for code includes allows me to do the following
+things:
+
+* Include entire files or sections of files into the page. This
+saves me from having to copy and paste code manually, which
+is error prone and can cause inconsistencies.
+* Provide links to the files I reference on my Git interface.
+This allows users to easily view the entire file that I'm talking about.
+* Correctly link to files in repositories other than my blog
+repository, when they are included using submodules. This means
+I don't need to manually copy and update code from other projects.
+
+I hope some of these shortcodes and script come in handy for someone else.
+Thank you for reading!

content/blog/hugo_functions.md

@@ -0,0 +1,79 @@
+---
+title: "Approximating Custom Functions in Hugo"
+date: 2021-01-17T18:44:53-08:00
+tags: ["Hugo"]
+---
+
+This will be an uncharacteristically short post. Recently,
+I wrote about my experience with [including code from local files]({{< relref "codelines" >}}).
+After I wrote that post, I decided to expand upon my setup. In particular,
+I wanted to display links to the files I'm referring to, in three
+different cases: when I'm referring to an entire code file, to an entire raw (non-highlighted)
+file, or to a portion of a code file.
+
+The problem was that in all three cases, I needed to determine the
+correct file URL to link to. The process for doing so is identical: it
+really only depends on the path to the file I'm including. However,
+many other aspects of each case are different. In the "entire code file"
+case, I simply need to read in a file. In the "portion of a code file"
+case, I have to perform some processing to extract the specific lines I want to include.
+Whenever I include a code file -- entirely or partially -- I need to invoke the `highlight`
+function to perform syntax highlighting; however, I don't want to do that when including a raw file.
+It would be difficult to write a single shortcode or partial to handle all of these different cases.
+
+However, computing the target URL is a simple transformation
+of a path and a list of submodules into a link. More plainly,
+it is a function. Hugo doesn't really have support for
+custom functions, at least according to this [Discourse post](https://discourse.gohugo.io/t/adding-custom-functions/14164). The only approach to add a _real_ function to Hugo is to edit the Go-based
+source code, and recompile the thing. However, your own custom functions
+would then not be included in normal Hugo distributions, and any websites
+using these functions would not be portable. _Really_ adding your own functions
+is not viable.
+
+However, we can approximate functions using Hugo's
+[scratchpad feature](https://gohugo.io/functions/scratch/)
+By feeding a 
+{{< sidenote "right" "mutable-note" "scratchpad" >}}
+In reality, any mutable container will work. The scratchpad
+just seems like the perfect tool for this purpose.
+{{< /sidenote >}}
+to a partial, and expecting the partial to modify the
+scratchpad in some way, we can effectively recover data.
+For instance, in my `geturl` partial, I have something like
+the following:
+
+```
+{{ .scratch.Set "bestUrl" theUrl }}
+```
+
+Once this partial executes, and the rendering engine is back to its call site,
+the scratchpad will contain `bestUrl`. To call this partial while providing inputs
+(like the file path, for example), we can use Hugo's `dict` function. An (abridged)
+example:
+
+```
+{{ partial "geturl.html" (dict "scratch" .Scratch "path" filePath) }}
+```
+
+Now, from inside the partial, we'll be able to access the two variable using `.scratch` and `.path`.
+Once we've called our partial, we simply extract the returned data from the scratchpad and use it:
+
+```
+{{ partial "geturl.html" (dict "scratch" .Scratch "path" filePath) }}
+{{ $bestUrl := .Scratch.Get "bestUrl" }}
+{{ ... do stuff with $bestUrl ... }}
+```
+
+Thus, although it's a little bit tedious, we're able to use `geturl` like a function,
+thereby refraining from duplicating its definition everywhere the same logic is needed. A few
+closing thoughts:
+
+* __Why not just use a real language?__ It's true that I wrote a Ruby script to
+do some of the work involved with linking submodules. However, generating the same
+information for all calls to `codelines` would complicate the process of rendering
+the blog, and make live preview impossible. In general, by limiting the use of external
+scripts, it's easier to make `hugo` the only "build tool" for the site.
+* __Is there an easier way?__ I _think_ that calls to `partial` return a string. If you
+simply wanted to return a string, you could probably do without using a scratchpad.
+However, if you wanted to do something more complicated (say, return a map or list),
+you'd probably want the scratchpad method after all.

content/search.md

@@ -0,0 +1,14 @@
+---
+title: Search
+type: "search"
+description: Interactive search for posts on Daniel's personal site.
+---
+
+Here's a [Stork](https://github.com/jameslittle230/stork)-powered search for all articles on
+this site. Stork takes some time to load on slower devices, which is why this isn't on
+every page (or even on the index page). Because the LaTeX rendering occurs _after_
+the search indexing, you may see raw LaTeX code in the content of the presented
+articles, like `\beta`. This does, however, also mean that you can search for mathematical
+symbols using only the English alphabet!
+
+If you're just browsing, you could alternatively check out [all posts](/blog), or perhaps my [favorite articles](/favorites) from this blog.

layouts/shortcodes/donate_css.html

@@ -0,0 +1,2 @@
+{{ $style := resources.Get "scss/donate.scss" | resources.ToCSS | resources.Minify }}
+<link rel="stylesheet" href="{{ $style.Permalink }}">

layouts/shortcodes/donation_method.html

@@ -0,0 +1,4 @@
+<tr>
+    <td>{{ .Get 0 }}</td>
+    <td><code>{{ .Get 1 }}</code></td>
+</tr>

layouts/shortcodes/donation_methods.html

@@ -0,0 +1,3 @@
+<table class="donation-methods">
+    {{ .Inner }}
+</table>

submodule-links.rb

@@ -0,0 +1,27 @@
+puts "[params]"
+puts "  [params.submoduleLinks]"
+
+def each_submodule(base_path)
+  `cd #{base_path} && git submodule status`.lines do |line|
+    hash, path = line[1..].split " "
+    full_path = "#{base_path}/#{path}"
+    url = `git config --file #{base_path}/.gitmodules --get 'submodule.#{path}.url'`.chomp.delete_suffix(".git")
+    safe_name = full_path.gsub(/\/|-|_\./, "")
+
+    if url =~ /dev.danilafe.com/
+      file_url = "#{url}/src/commit/#{hash}"
+    else
+      raise "Submodule URL #{url.dump} not in a known format!"
+    end
+
+    yield ({ :path => full_path, :url => file_url, :name => safe_name })
+    each_submodule(full_path) { |m| yield m }
+  end
+end
+
+each_submodule(".") do |m|
+  next unless m[:path].start_with? "./code/"
+  puts "    [params.submoduleLinks.#{m[:name].delete_prefix(".code")}]"
+  puts "      url = #{m[:url].dump}"
+  puts "      path = #{m[:path].delete_prefix("./code/").dump}"
+end

themes/vanilla/LICENSE

@@ -1,20 +0,0 @@
-The MIT License (MIT)
-
-Copyright (c) 2019 YOUR_NAME_HERE
-
-Permission is hereby granted, free of charge, to any person obtaining a copy of
-this software and associated documentation files (the "Software"), to deal in
-the Software without restriction, including without limitation the rights to
-use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
-the Software, and to permit persons to whom the Software is furnished to do so,
-subject to the following conditions:
-
-The above copyright notice and this permission notice shall be included in all
-copies or substantial portions of the Software.
-
-THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
-IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
-FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
-COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
-IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
-CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.

themes/vanilla/archetypes/default.md

@@ -1,2 +0,0 @@
-+++
-+++

themes/vanilla/assets/scss/code.scss

@@ -1,93 +0,0 @@
-@import "variables.scss";
-
-$code-color-lineno: grey;
-$code-color-keyword: black;
-$code-color-type: black;
-$code-color-comment: grey;
-
-.highlight-label {
-    padding: 0.25rem 0.5rem 0.25rem 0.5rem;
-    border: $code-border;
-    border-bottom: none;
-
-    a {
-        font-family: $font-code;
-    }
-}
-
-code {
-  font-family: $font-code;
-  background-color: $code-color;
-  border: $code-border;
-  padding: 0 0.25rem 0 0.25rem;
-}
-
-pre code {
-    display: block;
-    box-sizing: border-box;
-    padding: 0.5rem;
-    overflow: auto;
-}
-
-.chroma {
-    .lntable {
-        border-spacing: 0;
-        padding: 0.5rem 0 0.5rem 0;
-        background-color: $code-color;
-        border-radius: 0;
-        border: $code-border;
-        display: block;
-        overflow: auto;
-        margin-bottom: 1rem;
-
-        td {
-            padding: 0;
-        }
-
-        code {
-            border: none;
-            padding: 0;
-        }
-
-        pre {
-            margin: 0;
-        }
-
-        .lntd:last-child {
-            width: 100%;
-        }
-    }
-
-    .lntr {
-        display: table-row;
-    }
-
-    .lnt {
-        display: block;
-        padding: 0 1rem 0 1rem;
-        color: $code-color-lineno;
-    }
-
-    .hl {
-        display: block;
-        background-color: #fffd99; 
-
-        .lnt::before {
-            content: "*";
-        }
-    }
-}
-
-.kr, .k {
-    font-weight: bold;
-    color: $code-color-keyword;
-}
-
-.kt {
-    font-weight: bold;
-    color: $code-color-type;
-}
-
-.c, .c1 {
-    color: $code-color-comment;   
-}

themes/vanilla/assets/scss/margin.scss

@@ -1,47 +0,0 @@
-@import "variables.scss";
-@import "mixins.scss";
-
-$margin-width: 30rem;
-$margin-inner-offset: 0.5rem;
-$margin-outer-offset: 1rem;
-
-@mixin below-two-margins {
-    @media screen and
-        (max-width: $container-width-threshold +
-            2 * ($margin-width + $margin-inner-offset + $margin-outer-offset)) {
-        @content;
-    }
-}
-
-@mixin below-one-margin {
-    @media screen and
-        (max-width: $container-width-threshold +
-            ($margin-width + $margin-inner-offset + $margin-outer-offset)) {
-        @content;
-    }
-}
-
-@mixin margin-content {
-    display: block;
-    position: absolute;
-    width: $margin-width;
-    box-sizing: border-box;
-}
-
-@mixin margin-content-left {
-    left: 0;
-    margin-left: -($margin-width + $container-min-padding + $margin-inner-offset);
-
-    @include below-two-margins {
-        display: none;
-    }
-}
-
-@mixin margin-content-right {
-    right: 0;
-    margin-right: -($margin-width + $container-min-padding + $margin-inner-offset);
-
-    @include below-one-margin {
-        display: none;
-    }
-}

themes/vanilla/assets/scss/mixins.scss

@@ -1,13 +0,0 @@
-@import "variables.scss";
-
-@mixin bordered-block {
-    border: $standard-border;
-    border-radius: .2rem;
-}
-
-@mixin below-container-width {
-    @media screen and (max-width: $container-width-threshold){
-        @content;
-    }
-}
-

themes/vanilla/assets/scss/search.scss

@@ -1,99 +0,0 @@
-@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-wrapper {
-    margin-top: 0.5rem;
-    margin-bottom: 0.5rem;
-}
-
-.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/assets/scss/sidenotes.scss

@@ -1,75 +0,0 @@
-@import "variables.scss";
-@import "mixins.scss";
-@import "margin.scss";
-
-$sidenote-padding: 1rem;
-$sidenote-highlight-border-width: .2rem;
-
-.sidenote {
-    &:hover {
-        .sidenote-label {
-            background-color: $primary-color;
-            color: white;
-        }
-
-        .sidenote-content {
-            border: $sidenote-highlight-border-width dashed;
-            padding: $sidenote-padding -
-                ($sidenote-highlight-border-width - $standard-border-width);
-            border-color: $primary-color;
-        }
-    }
-}
-
-.sidenote-label {
-    border-bottom: .2rem dashed $primary-color;
-}
-
-.sidenote-checkbox {
-    display: none;
-}
-
-.sidenote-content {
-    @include margin-content;
-    @include bordered-block;
-    margin-top: -1.5rem;
-    padding: $sidenote-padding;
-    text-align: left;
-
-    &.sidenote-right {
-        @include margin-content-right;
-    }
-
-    &.sidenote-left {
-        @include margin-content-left;
-    }
-}
-
-.sidenote-delimiter {
-    display: none;
-}
-
-@mixin hidden-sidenote {
-    position: static;
-    margin-top: 1rem;
-    margin-bottom: 1rem;
-    width: 100%;
-
-    .sidenote-checkbox:checked ~ & {
-        display: block;
-    }
-}
-
-@include below-two-margins {
-    .sidenote-content.sidenote-left {
-        @include hidden-sidenote;
-        margin-left: 0rem;
-    }
-}
-
-@include below-one-margin {
-    .sidenote-content.sidenote-right {
-        @include hidden-sidenote;
-        margin-right: 0rem;
-    }
-}

themes/vanilla/assets/scss/style.scss

@@ -1,265 +0,0 @@
-@import "variables.scss";
-@import "mixins.scss";
-@import "margin.scss";
-@import "toc.scss";
-
-body {
-  font-family: $font-body;
-  font-size: 1.0rem;
-  line-height: 1.5;
-  margin-bottom: 1rem;
-  text-align: justify;
-
-  @include below-container-width {
-    text-align: left;
-  }
-}
-
-h1, h2, h3, h4, h5, h6 {
-  margin-bottom: .1rem;
-  margin-top: .5rem;
-  font-family: $font-heading;
-  font-weight: normal;
-  text-align: center;
-
-  a {
-    border-bottom: none;
-
-    &:hover {
-      color: $primary-color;
-    }
-  }
-}
-
-.container {
-  position: relative;
-  margin: auto;
-  width: 100%;
-  max-width: $container-width;
-  box-sizing: border-box;
-
-  @include below-container-width {
-      padding: 0 $container-min-padding 0 $container-min-padding;
-      margin: 0;
-      max-width: $container-width + 2 * $container-min-padding;
-  }
-
-  @include below-two-margins {
-      left: -($margin-width + $margin-inner-offset + $margin-outer-offset)/2;
-  }
-
-  @include below-one-margin {
-      left: 0;
-  }
-}
-
-.button, input[type="submit"] {
-  padding: 0.5rem;
-  background-color: $primary-color;
-  border: none;
-  color: white;
-  transition: color 0.25s, background-color 0.25s;
-  text-align: left;
-
-  &:focus {
-    outline: none;
-  }
-
-  &:hover, &:focus {
-    background-color: white;
-    color: $primary-color;
-  }
-}
-
-nav {
-  width: 100%;
-  margin: 0rem 0rem 1rem 0rem;
-
-  .container {
-    display: flex;
-    justify-content: center;
-    flex-wrap: wrap;
-  }
-
-  a {
-    padding: 0.25rem 0.75rem 0.25rem .75rem;
-    text-decoration: none;
-    color: black;
-    display: inline-block;
-    border-bottom: none;
-    white-space: nowrap;
-  }
-}
-
-.post-subscript {
-  color: #8f8f8f;
-  text-align: center;
-}
-
-.post-content {
-  margin-top: .5rem;
-}
-
-h1 {
-  font-size: 3.0rem;
-}
-
-h2 {
-  font-size: 2.6rem;
-}
-
-h3 {
-  font-size: 2.2rem;
-}
-
-h4 {
-  font-size: 1.8rem;
-}
-
-h5 {
-  font-size: 1.4rem;
-}
-
-h6 {
-  font-size: 1.0rem;
-}
-
-a {
-  color: black;
-  text-decoration: none;
-  border-bottom: .2rem solid $primary-color;
-  transition: color 0.25s;
-
-  &:hover {
-    color: $primary-color;
-  }
-}
-
-img {
-  max-width: 100%
-}
-
-table {
-    @include bordered-block;
-    margin: auto;
-    padding: 0.5rem;
-}
-
-tr {
-    @include below-container-width {
-        display: flex;
-        flex-direction: column;
-    }
-}
-
-td {
-    @include below-container-width {
-        overflow-x: auto;
-    }
-    padding: 0.5rem;
-}
-
-div.highlight tr {
-    display: table-row;
-}
-
-hr.header-divider {
-    background-color: $primary-color;
-    height: 0.3rem;
-    border: none;
-    border-radius: 0.15rem;
-}
-
-hr.footer-divider {
-    margin: auto;
-    margin-top: 1.5rem;
-    margin-bottom: 1.5rem;
-    border: none;
-    border-bottom: $standard-border;
-    max-width: $container-width;
-
-    @include below-container-width {
-        max-width: 80%;
-    }
-}
-
-ul.post-list {
-    list-style: none;
-    padding: 0;
-
-    li {
-        @include bordered-block;
-        margin-bottom: 1rem;
-        padding: 1rem;
-    }
-
-    p {
-        margin: 0;
-    }
-
-    a.post-title {
-        border-bottom: none;
-        font-size: 1.4rem;
-        font-family: $font-heading;
-        text-align: center;
-        display: block;
-    }
-
-    p.post-wordcount {
-        text-align: center;
-        margin-bottom: 0.6rem;
-    }
-}
-
-.katex-html {
-    white-space: nowrap;
-}
-
-figure {
-    img {
-        max-width: 70%;
-        display: block;
-        margin: auto;
-
-        @include below-container-width {
-            max-width: 100%;
-        }
-    }
-
-    figcaption {
-        text-align: center;
-    }
-
-    &.tiny img {
-        max-height: 15rem;
-    }
-
-    &.small img {
-        max-height: 20rem;
-    }
-
-    &.medium img {
-        max-height: 30rem;
-    }
-}
-
-.twitter-tweet {
-    margin: auto;
-}
-
-.draft-warning {
-    @include bordered-block;
-    padding: 0.5rem;
-    background-color: #ffee99;
-    border-color: #f5c827;
-}
-
-.feather {
-  width: 1rem;
-  height: 1rem;
-  stroke: currentColor;
-  stroke-width: 2;
-  stroke-linecap: round;
-  stroke-linejoin: round;
-  fill: currentColor;
-}

themes/vanilla/assets/scss/toc.scss

@@ -1,49 +0,0 @@
-@import "variables.scss";
-@import "mixins.scss";
-
-$toc-color: $code-color;
-$toc-border-color: $code-border-color;
-
-.table-of-contents {
-    @include margin-content;
-    @include margin-content-left;
-    display: flex;
-    flex-direction: column;
-    align-items: flex-end;
-    margin-bottom: 1rem;
-
-    em {
-        font-style: normal;
-        font-weight: bold;
-        font-size: 1.2em;
-        display: block;
-        margin-bottom: 0.5rem;
-    }
-
-    #TableOfContents > ul {
-        padding-left: 0;
-    }
-
-    nav {
-        margin: 0px;
-    }
-
-    ul {
-        list-style: none;
-        padding-left: 2rem;
-        margin: 0px;
-    }
-
-    a {
-        padding: 0;
-    }
-
-    div.wrapper {
-        @include bordered-block;
-        padding: 1rem;
-        background-color: $toc-color;
-        border-color: $toc-border-color;
-        box-sizing: border-box;
-        max-width: 100%;
-    }
-}

themes/vanilla/assets/scss/variables.scss

@@ -1,16 +0,0 @@
-$container-width: 45rem;
-$container-min-padding: 1rem;
-$container-width-threshold: $container-width + 2 * $container-min-padding;
-$standard-border-width: .075rem;
-
-$primary-color: #36e281;
-$border-color: #bfbfbf;
-$code-color: #f0f0f0;
-$code-border-color: darken($code-color, 10%);
-
-$font-heading: "Lora", serif;
-$font-body: "Raleway", serif;
-$font-code: "Inconsolata", monospace;
-
-$standard-border: $standard-border-width solid $border-color;
-$code-border: $standard-border-width solid $code-border-color;

themes/vanilla/layouts/_default/baseof.html

@@ -1,12 +0,0 @@
-<!DOCTYPE html>
-<html lang="{{ .Site.Language.Lang }}">
-    {{- partial "head.html" . -}}
-    <body>
-        {{- partial "header.html" . -}}
-        <div class="container"><hr class="header-divider"></div>
-        <main class="container">
-        {{- block "main" . }}{{- end }}
-        </main>
-        {{- block "after" . }}{{- end }}
-    </body>
-</html>

themes/vanilla/layouts/_default/baseof.toml

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

themes/vanilla/layouts/_default/list.html

@@ -1,9 +0,0 @@
-{{ define "main" }}
-<h2>{{ .Title }}</h2>
-
-<ul class="post-list">
-    {{ range .Pages.ByDate.Reverse }}
-    {{ partial "post.html" . }}
-    {{ end }}
-</ul>
-{{ end }}

themes/vanilla/layouts/_default/list.toml

@@ -1,12 +0,0 @@
-[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.html

@@ -1,4 +0,0 @@
-{{ define "main" }}
-<h2>{{ .Title }}</h2>
-{{ .Content }}
-{{ end }}

themes/vanilla/layouts/_default/single.toml

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

themes/vanilla/layouts/blog/single.html

@@ -1,42 +0,0 @@
-{{ define "main" }}
-<h2>{{ .Title }}</h2>
-<div class="post-subscript">
-    <p>
-        {{ range .Params.tags }}
-        <a class="button" href="{{ $.Site.BaseURL }}/tags/{{ . | urlize }}">{{ . }}</a>
-        {{ end }}
-    </p>
-    <p>Posted on {{ .Date.Format "January 2, 2006" }}.</p>
-</div>
-
-<div class="post-content">
-    {{ if not (eq .TableOfContents "<nav id=\"TableOfContents\"></nav>") }}
-    <div class="table-of-contents">
-        <div class="wrapper">
-            <em>Table of Contents</em>
-            {{ .TableOfContents }}
-        </div>
-    </div>
-    {{ end }}
-
-    {{ if .Draft }}
-    <div class="draft-warning">
-        <em>Warning!</em> This post is a draft. At best, it may contain grammar mistakes;
-        at worst, it can include significant errors and bugs. Please
-        use your best judgement!
-    </div>
-    {{ end }}
-
-    {{ .Content }}
-</div>
-{{ end }}
-{{ define "after" }}
-<hr class="container footer-divider">
-<footer class="container">
-    Liked this article? I'm currently looking for Computer Science internships for the summer
-    of 2021. Take a look at my <a href="/Resume-Danila-Fedorin.pdf">resume</a>, 
-    <a href="https://github.com/DanilaFe">GitHub profile</a>,
-    and <a href="/favorites">my favorite articles from this blog</a>
-    to learn more about me!
-</footer>
-{{ end }}

themes/vanilla/layouts/favorites/single.html

@@ -1,10 +0,0 @@
-{{ define "main" }}
-<h2>{{ .Title }} </h2>
-{{ .Content }}
-
-<ul class="post-list">
-    {{ range (where (where .Site.Pages.ByDate.Reverse "Section" "blog") ".Kind" "!=" "section") }}
-    {{ if .Params.favorite }}{{ partial "post.html" . }}{{ end }}
-    {{ end }}
-</ul>
-{{ end }}

themes/vanilla/layouts/index.html

@@ -1,11 +0,0 @@
-{{ define "main" }}
-{{ .Content }}
-
-Recent posts:
-<ul class="post-list">
-    {{ range first 10 (where (where .Site.Pages.ByDate.Reverse "Section" "blog") ".Kind" "!=" "section") }}
-    {{ partial "post.html" . }}
-    {{ end }}
-</ul>
-
-{{ end }}

themes/vanilla/layouts/partials/head.html

@@ -1,23 +0,0 @@
-<head>
-    <meta charset="utf-8">
-    <meta name="viewport" content="width=device-width, initial-scale=1">
-    <meta name="theme-color" content="#1dc868">
-    {{ if .Description }}
-    <meta name="description" content="{{ .Description }}">
-    {{ end }}
-
-    <link rel="stylesheet" href="https://fonts.googleapis.com/css2?family=Inconsolata:wght@400;700&family=Raleway&family=Lora&display=block" media="screen"> 
-    <link rel="stylesheet" href="//cdnjs.cloudflare.com/ajax/libs/normalize/5.0.0/normalize.min.css" media="screen">
-    {{ $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 }}
-    {{ $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="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 }}">
-
-    <title>{{ .Title }}</title>
-</head>

themes/vanilla/layouts/partials/header.html

@@ -1,13 +0,0 @@
-<div class="container">
-    <h1>Daniel's Blog</h1>
-</div>
-<nav>
-    <div class="container">
-        <a href="/">Home</a>
-        <a href="/about">About</a>
-        <a href="https://github.com/DanilaFe">GitHub</a>
-        <a href="/Resume-Danila-Fedorin.pdf">Resume</a>
-        <a href="/tags">Tags</a>
-        <a href="/blog">All Posts</a>
-    </div>
-</nav>

themes/vanilla/layouts/partials/icon.html

@@ -1,3 +0,0 @@
-<svg class="feather">
-    <use xlink:href="/feather-sprite.svg#{{ . }}"/>
-</svg>

themes/vanilla/layouts/partials/post.html

@@ -1,5 +0,0 @@
-<li>
-    <a href="{{ .Permalink }}" class="post-title">{{ if .Params.favorite }}{{ partial "icon.html" "star" }}{{ end }} {{ .Title }}</a>
-    <p class="post-wordcount">{{ .WordCount }} words, about {{ .ReadingTime }} minutes to read.</p>
-    <p class="post-preview">{{ .Summary }} . . .</p>
-</li>

themes/vanilla/layouts/partials/sidenotes.html

@@ -1,5 +0,0 @@
-<style>
-.sidenote-checkbox {
-    display: none;
-}
-</style>

themes/vanilla/layouts/rss.xml

@@ -1,39 +0,0 @@
-{{- $pctx := . -}}
-{{- if .IsHome -}}{{ $pctx = .Site }}{{- end -}}
-{{- $pages := slice -}}
-{{- if or $.IsHome $.IsSection -}}
-{{- $pages = $pctx.RegularPages -}}
-{{- else -}}
-{{- $pages = $pctx.Pages -}}
-{{- end -}}
-{{- $limit := .Site.Config.Services.RSS.Limit -}}
-{{- if ge $limit 1 -}}
-{{- $pages = $pages | first $limit -}}
-{{- end -}}
-{{- printf "<?xml version=\"1.0\" encoding=\"utf-8\" standalone=\"yes\"?>" | safeHTML }}
-<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom">
-  <channel>
-    <title>{{ if eq  .Title  .Site.Title }}{{ .Site.Title }}{{ else }}{{ with .Title }}{{.}} on {{ end }}{{ .Site.Title }}{{ end }}</title>
-    <link>{{ .Permalink }}</link>
-    <description>Recent content {{ if ne  .Title  .Site.Title }}{{ with .Title }}in {{.}} {{ end }}{{ end }}on {{ .Site.Title }}</description>
-    <generator>Hugo -- gohugo.io</generator>{{ with .Site.LanguageCode }}
-    <language>{{.}}</language>{{end}}{{ with .Site.Author.email }}
-    <managingEditor>{{.}}{{ with $.Site.Author.name }} ({{.}}){{end}}</managingEditor>{{end}}{{ with .Site.Author.email }}
-    <webMaster>{{.}}{{ with $.Site.Author.name }} ({{.}}){{end}}</webMaster>{{end}}{{ with .Site.Copyright }}
-    <copyright>{{.}}</copyright>{{end}}{{ if not .Date.IsZero }}
-    <lastBuildDate>{{ .Date.Format "Mon, 02 Jan 2006 15:04:05 -0700" | safeHTML }}</lastBuildDate>{{ end }}
-    {{ with .OutputFormats.Get "RSS" }}
-	{{ printf "<atom:link href=%q rel=\"self\" type=%q />" .Permalink .MediaType | safeHTML }}
-    {{ end }}
-    {{ range $pages }}
-    <item>
-      <title>{{ .Title }}</title>
-      <link>{{ .Permalink }}</link>
-      <pubDate>{{ .Date.Format "Mon, 02 Jan 2006 15:04:05 -0700" | safeHTML }}</pubDate>
-      {{ with .Site.Author.email }}<author>{{.}}{{ with $.Site.Author.name }} ({{.}}){{end}}</author>{{end}}
-      <guid>{{ .Permalink }}</guid>
-      <description>{{ .Content | html }}</description>
-    </item>
-    {{ end }}
-  </channel>
-</rss>

themes/vanilla/layouts/shortcodes/codeblock.html

@@ -1 +0,0 @@
-{{ highlight (readFile (printf "code/%s" (.Get 1))) (.Get 0) "" }}

themes/vanilla/layouts/shortcodes/codelines.html

@@ -1,18 +0,0 @@
-{{ $s := (readFile (printf "code/%s" (.Get 1))) }}
-{{ $t := split $s "\n" }}
-{{ if not (eq (int (.Get 2)) 1) }}
-{{ .Scratch.Set "u" (after (sub (int (.Get 2)) 1) $t) }}
-{{ else }}
-{{ .Scratch.Set "u" $t }}
-{{ end }}
-{{ $v := first (add (sub (int (.Get 3)) (int (.Get 2))) 1) (.Scratch.Get "u") }}
-{{ if (.Get 4) }}
-{{ .Scratch.Set "opts" (printf ",%s" (.Get 4)) }}
-{{ else }}
-{{ .Scratch.Set "opts" "" }}
-{{ end }}
-<div class="highlight-group">
-    <div class="highlight-label">From <a href="https://dev.danilafe.com/Web-Projects/blog-static/src/branch/master/code/{{ .Get 1 }}">{{ path.Base (.Get 1) }}</a>,
-        {{ if eq (.Get 2) (.Get 3) }}line {{ .Get 2 }}{{ else }} lines {{ .Get 2 }} through {{ .Get 3 }}{{ end }}</div>
-    {{ highlight (delimit $v "\n") (.Get 0) (printf "linenos=table,linenostart=%d%s" (.Get 2) (.Scratch.Get "opts")) }}
-</div>

themes/vanilla/layouts/shortcodes/latex.html

@@ -1,3 +0,0 @@
-$$
-{{ .Inner }}
-$$

themes/vanilla/layouts/shortcodes/numberedsidenote.html

@@ -1,11 +0,0 @@
-{{ .Page.Scratch.Add "numbernote-id" 1 }}
-{{ $id := .Page.Scratch.Get "numbernote-id" }}
-<span class="sidenote">
-<label class="sidenote-label" for="numbernote-{{ $id }}">({{ $id }})</label>
-<input class="sidenote-checkbox" type="checkbox" id="numbernote-{{ $id }}"></input>
-<span class="sidenote-content sidenote-{{ .Get 0 }}">
-<span class="sidenote-delimiter">[note:</span>
-{{ .Inner }}
-<span class="sidenote-delimiter">]</span>
-</span>
-</span>

themes/vanilla/layouts/shortcodes/rawblock.html

@@ -1 +0,0 @@
-<pre><code>{{ readFile (printf "code/%s" (.Get 0)) }}</code></pre>

themes/vanilla/layouts/shortcodes/sidenote.html

@@ -1,9 +0,0 @@
-<span class="sidenote">
-<label class="sidenote-label" for="{{ .Get 1 }}">{{ .Get 2 }}</label>
-<input class="sidenote-checkbox" type="checkbox" id="{{ .Get 1 }}"></input>
-<span class="sidenote-content sidenote-{{ .Get 0 }}">
-<span class="sidenote-delimiter">[note:</span>
-{{ .Inner }}
-<span class="sidenote-delimiter">]</span>
-</span>
-</span>

themes/vanilla/layouts/shortcodes/todo.html

@@ -1,3 +0,0 @@
-<div style="background-color: tomato; color: white; padding: 10px;">
-    <em>TODO: </em>{{ .Inner }}
-</div>

themes/vanilla/layouts/tags/list.html

@@ -1,9 +0,0 @@
-{{ define "main" }}
-<h2>Tagged "{{ .Title }}"</h2>
-
-<ul class="post-list">
-    {{ range .Pages.ByDate.Reverse }}
-    {{ partial "post.html" . }}
-    {{ end }}
-</ul>
-{{ end }}

themes/vanilla/layouts/tags/terms.html

@@ -1,10 +0,0 @@
-{{ define "main" }}
-<h2>{{ .Title }}</h2>
-Below is a list of all the tags ever used on this site.
-
-<ul>
-    {{ range sort .Pages "Title" }}
-    <li><a href="{{ .Permalink }}">{{ .Title }}</a></li>
-    {{ end }}
-</ul>
-{{ end }}

themes/vanilla/theme.toml

@@ -1,21 +0,0 @@
-# theme.toml template for a Hugo theme
-# See https://github.com/gohugoio/hugoThemes#themetoml for an example
-
-name = "Vanilla"
-license = "MIT"
-# licenselink = "https://github.com/yourname/yourtheme/blob/master/LICENSE"
-# description = ""
-# homepage = "http://example.com/"
-# tags = []
-# features = []
-min_version = "0.41"
-
-[author]
-  name = "Danila Fedorin"
-  homepage = "https://danilafe.com"
-
-# If porting an existing theme
-# [original]
-#   name = ""
-#   homepage = ""
-#   repo = ""