Mdbook tweaks

.gitignore

@@ -4,3 +4,5 @@ inputs/
 support/*.o
 support/advent-support
 tmp/
+book/
+index.html

README.md

@@ -6,6 +6,9 @@ Idris files.
 
 ## Authors Note
 
+This entire book is a single literate code base, the source code is available at
+<https://git.stranger.systems/Idris/advent>.
+
 The solutions contained in this project are intended to be read in sequential
 order, though can reasonably be read in any order if you have a good level of
 familiarity with more advanced functional programming topics.
@@ -22,7 +25,7 @@ mailing list on source hut.
 While this project is intended to read more like a book, while it is still a
 work in progress, you can follow its development as a psuedo-blog by subscribing
 to the rss feed for the repository in your feed reader:
-https://git.stranger.systems/Idris/advent.rss
+<https://git.stranger.systems/Idris/advent.rss>.
 
 ## Index of non-day modules
 

book.toml

@@ -0,0 +1,13 @@
+[book]
+authors = ["Nathan McCarty"]
+language = "en"
+multilingual = false
+src = "src"
+title = "Idris 2 by Highly Contrived Example"
+
+[build]
+create-missing = false
+use-default-preprocessors = false
+
+[output.html]
+preferred-dark-theme = "ayu"

scripts/build-book

@@ -0,0 +1,101 @@
+#!/usr/bin/env raku
+
+use File::Temp;
+use Shell::Command;
+use paths;
+
+unit sub MAIN(Bool :$upload);
+
+my $tempdir = tempdir.IO;
+my $ttc-number = dir('build/ttc').first.basename;
+my $ttc = "build/ttc/$ttc-number".IO;
+
+# Filenames to ignore while processing source files
+my Str:D @ignored = ["README.md", "SUMMARY.md"];
+# Check to see if a filename is ignored
+sub not-ignored($path) {
+    for @ignored -> $ignored {
+        return False if $path.ends-with: $ignored;
+    }
+    return True;
+}
+
+# Copy a file from the current directory to the temporary directory, preserving
+# realtive path. Resolves symlinks in source, but does not reflect symlink
+# resoultion in the output path
+sub cp-temp($src) {
+   my $src-path = do given $src {
+       when Str {
+           $src.IO
+       }
+       when IO::Path {
+           $src
+       }
+       default {
+           die "Invalid source $src, {$src.WHAT}"
+       }
+   }
+   my $output-path = $tempdir.add($src-path.relative).IO;
+   # Create the parent directory if needed
+   if !$output-path.parent.d {
+       $output-path.parent.mkdir;
+
+   }
+   # Copy the file
+   $src-path.resolve.copy: $output-path;
+}
+
+# Invoke katla on a source file, streaming its output to the temporary directory
+sub katla($src, $ttc-src) {
+    # Run katla and collect the output
+    my $katla = run 'katla', 'markdown', $src, $ttc-src, :out;
+    my $output = $katla.out.slurp(:close);
+    # TODO: Post process them to set themeing correctly
+    $output ~~ s:g/'<style>' .* '</style>'//;
+    $output ~~ s:g/'<br />'//;
+    $output ~~ s:g/'<code'/<pre><code/;
+    $output ~~ s:g/'</code>'/<\/code><\/pre>/;
+    $output ~~ s:g/'class="IdrisKeyword"'/class="hljs-keyword"/;
+    $output ~~ s:g/'class="IdrisModule"'/class="hljs-symbol hljs-emphasis"/;
+    $output ~~ s:g/'class="IdrisComment"'/class="hljs-comment"/;
+    $output ~~ s:g/'class="IdrisFunction"'/class="hljs-symbol"/;
+    $output ~~ s:g/'class="IdrisBound"'/class="hljs-name"/;
+    $output ~~ s:g/'class="IdrisData"'/class="hljs-title"/;
+    $output ~~ s:g/'class="IdrisType"'/class="hljs-type"/;
+    $output ~~ s:g/'class="IdrisNamespace"'/class="hljs-symbol hljs-emphasis"/;
+
+    # Spurt the output to the temporary directory
+    my $output-path = $tempdir.add: $src;
+    if !$output-path.parent.d {
+        $output-path.parent.mkdir;
+    }
+    $output-path.spurt($output);
+}
+
+# Copy our metadata files
+cp-temp "book.toml";
+cp-temp "src/README.md";
+cp-temp "src/SUMMARY.md";
+
+# Katla over the source files
+for paths("src", :file(*.&not-ignored)) -> $path {
+    my $ttc-path = $ttc.add($path.IO.relative: "src").extension: "ttm";
+    katla $path.IO.relative, $ttc-path.relative;
+}
+
+# Build the book
+
+indir $tempdir, {
+    my $mdbook = run <mdbook build>;
+    die "Ooops" unless $mdbook;
+}
+
+# Copy it over
+rm_rf "book";
+cp $tempdir.add("book"), "book", :r;
+
+if $upload {
+   my $rsync = run 'rsync', '-avzh', $tempdir.add("book").Str,
+       'ubuntu@static.stranger.systems:/var/www/static.stranger.systems/idris-by-contrived-example';
+   die "rsync went bad" unless $rsync;
+}

src/Array.md

@@ -12,9 +12,9 @@ import Decidable.Equality
 import Control.WellFounded
 ```
 
-<!-- idris
+```idris hide
 import System
--->
+```
 
 ```idris
 %default total
@@ -89,9 +89,9 @@ Iterable (LazyList a) a where
 
 ## Immutable arrays
 
-<!-- idris
+```idris hide
 namespace Immutable
--->
+```
 
 Immutable arrays created from vectors that provide constant time indexing and
 slicing operations.

src/Main.md

@@ -76,7 +76,7 @@ data Error : Type where
 A `Show` implementation for `Error` is provided, hidden in this document for
 brevity.
 
-<!-- idris
+```idris hide
 Show Error where
   show (OptionsError errs) =
     let errs = unlines . map ("  " ++) . lines . joinBy "\n" $ errs
@@ -98,7 +98,7 @@ Show Error where
   show (SolveError year day part err) =
     let err = unlines . map ("  " ++) . lines . show $ err
     in "Error solving day \{show day} part \{show part} of year \{show year}: \n" ++ err
--->
+```
 
 ## Extract the year and day
 

src/Parser/Interface.md

@@ -27,7 +27,7 @@ data ParseError : Type where
     -> (rest : List ParseError) -> ParseError
 ```
 
-<!-- idris
+```idris hide
 export
 Show ParseError where
   show (MkParseError state message) = 
@@ -44,7 +44,7 @@ Show ParseError where
         position = show state.position.index
         first = "Error at line \{line}, column \{col} (\{position}): \{message}"
     in "\{first}\n\{rest}"
--->
+```
 
 ## Type Alias
 
@@ -219,23 +219,23 @@ Lift a parser producing a `List` or `List1` of `Char` into a parser producing a
 ```idris
 -- TODO: Rename these
 export
-parseString : Parser (List Char) -> Parser String
+liftString : Parser (List Char) -> Parser String
-parseString x = do
+liftString x = do
   xs <- x
   pure $ pack xs
 
 export
-parseString' : Parser (List1 Char) -> Parser String
+liftString' : Parser (List1 Char) -> Parser String
-parseString' x = parseString $ map forget x
+liftString' x = liftString $ map forget x
 ```
 
 Attempt to parse a specified character
 
 ```idris
 export
-parseExactChar : Char -> Parser Char
+charExact : Char -> Parser Char
-parseExactChar c = do
+charExact c = do
-  result <- parseExactChar' c
+  result <- charExact' c
   case result of
     GotChar char => pure char
     GotError err => throwParseError "Got \{show err} Expected \{show c}"
@@ -246,10 +246,10 @@ Attempt to parse one of a list of chars
 
 ```idris
 export
-parseTheseChars : List Char -> Parser Char
+theseChars : List Char -> Parser Char
-parseTheseChars cs = do
+theseChars cs = do
   pnote "Parsing one of: \{show cs}"
-  result <- parseChar (\x => any (== x) cs)
+  result <- charPredicate (\x => any (== x) cs)
   case result of
     GotChar char => pure char
     GotError err => throwParseError "Got \{show err} Expected one of \{show cs}"
@@ -267,7 +267,7 @@ exactString str with (asList str)
     pure ""
   exactString input@(strCons c str) | (c :: x) = do
     pnote "Parsing exact string \{show input}"
-    GotChar next <- parseChar (== c)
+    GotChar next <- charPredicate (== c)
       | GotError err => throwParseError "Got \{show err} expected \{show c}"
       | EndOfInput => throwParseError "End of input"
     rest <- exactString str | x
@@ -282,12 +282,12 @@ delimited : (before, after : Char) -> Parser a -> Parser a
 delimited before after x = do
   pnote "Parsing delimited by \{show before} \{show after}"
   starting_state <- save
-  _ <- parseExactChar before
+  _ <- charExact before
   Right val <- tryEither x
     | Left err => do
       load starting_state
       throw err
-  Just _ <- tryMaybe $ parseExactChar after
+  Just _ <- tryMaybe $ charExact after
     | _ => do
       load starting_state
       throw $ MkParseError starting_state "Unmatched delimiter \{show before}"

src/Parser/JSON.md

@@ -9,7 +9,7 @@ import public Parser.Numbers
 import Structures.Dependent.DList
 ```
 
-<!-- idris
+```idris hide
 import System
 import Derive.Prelude
 import Generics.Derive
@@ -19,7 +19,7 @@ import Generics.Derive
 %hide Generics.Derive.Show
 
 %language ElabReflection
--->
+```
 
 ## JSON components
 
@@ -54,7 +54,7 @@ data JSONValue : JSONType -> Type where
 %name JSONValue value, value2, value3
 ```
 
-<!-- idris
+```idris hide
 Show (JSONValue t) where
   show (VObject xs) = 
     let xs = dMap (\_,(key, value) => "\"\{key}\":\{show value}") xs
@@ -80,7 +80,7 @@ Eq (JSONValue t) where
   VNull == VNull = True
 
 %hide Language.Reflection.TT.WithFC.value
--->
+```
 
 ## Parsers
 
@@ -109,12 +109,7 @@ Define a `whitespace` character class based on the json specifications
 whitespace : Parser Char
 whitespace = do
   pnote "Whitespace character"
-  result <- 
+  theseChars [' ', '\n', '\r', '\t']
-    parseChar (\x => any (== x) $ the (List _) [' ', '\n', '\r', '\t'])
-  case result of
-    GotChar char => pure char
-    GotError err => throwParseError "Expected whitespace, got: \{show err}"
-    EndOfInput => throwParseError "End of Input"
 ```
 
 Convenience function
@@ -162,12 +157,12 @@ object = do
     keyValue : Parser (t : JSONType ** (String, JSONValue t))
     keyValue = do
       VString key <- surround whitespace string
-      _ <- parseExactChar ':'
+      _ <- charExact ':'
       (typ ** val) <- value
       pure (typ ** (key, val))
     restKeyValue : Parser (t : JSONType ** (String, JSONValue t))
     restKeyValue = do
-      _ <- parseExactChar ','
+      _ <- charExact ','
       keyValue
     pairs : Parser (List1 (t : JSONType ** (String, JSONValue t)))
     pairs = do
@@ -194,7 +189,7 @@ array = do
       pure $ VArray Nil
     restValue : Parser (t : JSONType ** JSONValue t)
     restValue = do
-      _ <- parseExactChar ','
+      _ <- charExact ','
       value
     values : Parser (List1 (t : JSONType ** JSONValue t))
     values = do
@@ -211,13 +206,13 @@ array = do
 ```idris
 string = do
   pnote "JSON String"
-  str <- parseString $ delimited '"' '"' (many stringCharacter)
+  str <- liftString $ delimited '"' '"' (many stringCharacter)
   pure $ VString str
   where
     -- TODO: Handle control characters properly
     stringCharacter : Parser Char
     stringCharacter = do
-      result <- parseChar (not . (== '"'))
+      result <- charPredicate (not . (== '"'))
       case result of
         GotChar char => pure char
         GotError err =>

src/Parser/Numbers.md

@@ -9,9 +9,9 @@ import Data.Vect
 import Control.Eff
 ```
 
-<!-- idris
+```idris hide
 import System
--->
+```
 
 ## Base Abstraction
 
@@ -63,7 +63,7 @@ nat b = do
   where
     parseDigit : Parser Nat
     parseDigit = do
-      GotChar char <- parseChar (hasDigit b)
+      GotChar char <- charPredicate (hasDigit b)
         | GotError e => throwParseError "\{show e} is not a digit"
         | EndOfInput => throwParseError "End Of Input"
       case digitValue b char of
@@ -82,7 +82,7 @@ natBase10 = nat base10
 export
 integer : Base -> Parser Integer
 integer b = do
-  negative <- map isJust . tryMaybe $ parseExactChar '-'
+  negative <- map isJust . tryMaybe $ charExact '-'
   value <- map natToInteger $ nat b
   if negative
     then pure $ negate value
@@ -120,13 +120,13 @@ double = do
   where
     parseDigit : Parser Char
     parseDigit = do
-      GotChar char <- parseChar (hasDigit base10)
+      GotChar char <- charPredicate (hasDigit base10)
         | GotError e => throwParseError "\{show e} is not a digit"
         | EndOfInput => throwParseError "End Of Input"
       pure char
     integer : Parser String
     integer = do
-      sign <- tryMaybe $ parseExactChar '-'
+      sign <- tryMaybe $ charExact '-'
       error <- replaceError "Expected digit"
       digits <- map forget $ atLeastOne error parseDigit
       case sign of
@@ -134,14 +134,14 @@ double = do
         Just x => pure $ pack (x :: digits)
     fraction : Parser String
     fraction = do
-      decimal <- parseExactChar '.'
+      decimal <- charExact '.'
       error <- replaceError "Expected digit"
       digits <- map forget $ atLeastOne error parseDigit
       pure $ pack digits
     exponent : Parser String
     exponent = do
-      e <- parseTheseChars ['e', 'E']
+      e <- theseChars ['e', 'E']
-      sign <- parseTheseChars ['+', '-']
+      sign <- theseChars ['+', '-']
       error <- replaceError "Expected digit"
       digits <- map forget $ atLeastOne error parseDigit
       pure . pack $ sign :: digits

src/Parser/ParserState.md

@@ -51,7 +51,7 @@ record Index (length : Int64) where
   {auto 0 prf : IsIndex length index}
 ```
 
-<!-- idris
+```idris hide
 export
 Eq (Index i) where
   x == y = x.index == y.index
@@ -63,7 +63,7 @@ Ord (Index i) where
 export
 Show (Index i) where
   show (MkIndex index) = show index
--->
+```
 
 Stores the location we are currently at in the string, and metadata about it for
 providing good error messages. Parsing an empty input isn't very interesting, so
@@ -156,7 +156,7 @@ positionPair pi =
           in (linum, col)
 ```
 
-<!-- idris
+```idris hide
 export
 Show (ParserInternal Id) where
   show pi = 
@@ -165,7 +165,7 @@ Show (ParserInternal Id) where
         pos = pi.position.index
         eof = show pi.end_of_input
     in "Position: \{pos}(\{line}, \{col}}) Value: \{show current} EoF: \{eof}"
--->
+```
 
 ### More Barbie Functionality
 
@@ -216,7 +216,7 @@ data ParserState : Type -> Type where
   Note : Lazy String -> ParserState ()
 ```
 
-<!-- idris
+```idris hide
 Show (ParserState t) where
   show Save = "Saving state"
   show (Load pi) = "Loading state \{show pi}"
@@ -224,7 +224,7 @@ Show (ParserState t) where
   show (ParseExactChar char) = "Parsing char \{show char}"
   show ParseEoF = "Parsing EoF"
   show (Note _) = "Note"
--->
+```
 
 ### Actions
 
@@ -243,14 +243,14 @@ load pi = send $ Load pi
 ||| predicate, updates the state if parsing succeeds, does not alter it in an 
 ||| error condition.
 export 
-parseChar : Has ParserState fs => (predicate : Char -> Bool)
+charPredicate : Has ParserState fs => (predicate : Char -> Bool)
   -> Eff fs ParseCharResult
-parseChar predicate = send $ ParseChar predicate 
+charPredicate predicate = send $ ParseChar predicate 
 
 ||| Parse a char by exact value
 export 
-parseExactChar' : Has ParserState fs => (chr : Char) -> Eff fs ParseCharResult
+charExact' : Has ParserState fs => (chr : Char) -> Eff fs ParseCharResult
-parseExactChar' chr = send $ ParseExactChar chr
+charExact' chr = send $ ParseExactChar chr
 
 ||| "Parse" the end of input, returning `True` if the parser state is currently
 ||| at the end of the input
@@ -366,4 +366,4 @@ runParserState s =
 
 ## Footnotes
 
-[^1]: https://github.com/stefan-hoeck/idris2-barbies
+[^1]: <https://github.com/stefan-hoeck/idris2-barbies>

src/README.md

@@ -0,0 +1 @@
+../README.md

src/SUMMARY.md

@@ -0,0 +1,35 @@
+# Summary
+
+[README](README.md)
+
+# Running the code
+
+- [Runner - Divide Code Into Years and Days](Runner.md)
+- [Main - Select a Day and Year to Run](Main.md)
+
+# Utility Mini-Library
+
+- [Util - Extend Standard Types](Util.md)
+  - [Util.Eff - Effects and Effect Accessories](Util/Eff.md)
+  - [Util.Digits - Pattern Matching Integers as Lists of Digits](Util/Eff.md)
+- [Array - Arrays With Constant Time Indexing and Slicing](Array.md)
+- [Parser - Recursive Descent Parsing, With Effects](Parser.md)
+  - [Interface - Core Parsing Functionality](Parser/Interface.md)
+  - [ParserState - Custom Effect for Parser Internal State](Parser/ParserState.md)
+  - [Numbers - Parsers for Numerical Values](Parser/Numbers.md)
+  - [JSON - A JSON Parser](Parser/JSON.md)
+
+# Problems
+
+- [2015](Years/Y2015.md)
+  - [Day 1 - Warmup](Years/Y2015/Day1.md)
+  - [Day 2 - Early Effectful Parsing](Years/Y2015/Day2.md)
+  - [Day 3 - Mutually Recursive Functions](Years/Y2015/Day3.md)
+  - [Day 4 - Basic FFI](Years/Y2015/Day4.md)
+  - [Day 5 - Views and Dependent Pattern Matching](Years/Y2015/Day5.md)
+  - [Day 6 - Naive 2D Grid](Years/Y2015/Day6.md)
+  - [Day 7 - Dependent Maps and Indexed Type Familes](Years/Y2015/Day7.md)
+  - [Day 8 - Proper Effectful Parsers](Years/Y2015/Day8.md)
+  - [Day 9 - Naive Graph Traversal](Years/Y2015/Day9.md)
+  - [Day 10 - Digits View](Years/Y2015/Day10.md)
+  - [Day 11 - Refinement Types](Years/Y2015/Day11.md)

src/Util.md

@@ -29,9 +29,9 @@ repeatN (S times') f seed = repeatN times' f (f seed)
 
 ## Either
 
-<!-- idris
+```idris hide
 namespace Either
--->
+```
 
 ### mapLeft
 
@@ -47,9 +47,9 @@ Applies a function to the contents of a `Left` if the value of the given
 
 ## List
 
-<!-- idris 
+```idris hide
 namespace List
--->
+```
 
 ### contains
 
@@ -94,12 +94,12 @@ Define some operations for pairs of numbers, treating them roughly like vectors
 
 ### Addition and Subtraction
 
-<!-- idris
+```idris hide
 export infixl 8 >+<
 export infixl 8 >-<
 
 namespace Pair
--->
+```
 
 ```idris
   public export
@@ -115,9 +115,9 @@ namespace Pair
 
 Extend `Data.SortedSet`
 
-<!-- idris
+```idris hide
 namespace Set
--->
+```
 
 ### length
 
@@ -133,9 +133,9 @@ Count the number of elements in a sorted set
 
 Extend `Data.String`
 
-<!-- idris
+```idris hide
 namespace String
--->
+```
 
 ### isSubstr
 

src/Util/Digits.md

@@ -6,11 +6,11 @@ module Util.Digits
 import Data.Monoid.Exponentiation
 ```
 
-<!-- idris
+```idris hide
 import System
 
 %default total
--->
+```
 
 This module provides views and associated functionality for treating `Integers`
 as if they were lists of numbers.
@@ -22,10 +22,10 @@ teaching purposes, we'll do it here, but please consider a library like
 [prim](https://github.com/stefan-hoeck/idris2-prim) if you find yourself needing
 to prove properties about primitive types.
 
-<!-- idris
+```idris hide
 -- This mutual block isn't strictly required, but is useful for literate purposes
 mutual
--->
+```
 
 ## Primitive functionality
 
@@ -50,14 +50,14 @@ most significant digit.
 
 For a clarifying example:
 
-<!-- idris
+```idris hide
   -- @@test Ascending Digits Example
   ascendingExample : IO Bool
   ascendingExample = do
     putStrLn "Expecting: \{show [5, 4, 3, 2, 1]}"
     putStrLn "Got: \{show . ascList $ ascending 12345}"
     pure $
--->
+```
 
 ```idris
     ascList (ascending 12345) == [5, 4, 3, 2, 1]
@@ -121,14 +121,14 @@ least significant digit.
 
 For a clarifying example:
 
-<!-- idris
+```idris hide
   -- @@test Descending Digits Example
   descendingExample : IO Bool
   descendingExample = do
     putStrLn "Expecting: \{show [1, 2, 3, 4, 5]}"
     putStrLn "Got: \{show . decList $ descending 12345}"
     pure $
--->
+```
 
 ```idris
     decList (descending 12345) == [1, 2, 3, 4, 5]

src/Util/Eff.md

@@ -36,7 +36,7 @@ data Level : Type where
   Other : (n : Nat) -> {auto _ : n `GT` 4} -> Level
 ```
 
-<!-- idris
+```idris hide
 export
 levelToNat : Level -> Nat
 levelToNat Err = 0
@@ -67,7 +67,7 @@ export infixl 8 >+
 export
 (>+) : Level -> Nat -> Level
 (>+) x k = natToLevel (k + levelToNat x)
--->
+```
 
 Convert a `Level` into a colorized tag
 

src/Years/Y2015.md

@@ -6,7 +6,7 @@ import Structures.Dependent.FreshList
 import Runner
 ```
 
-<!-- idris
+```idris hide
 import Years.Y2015.Day1
 import Years.Y2015.Day2
 import Years.Y2015.Day3
@@ -18,7 +18,7 @@ import Years.Y2015.Day8
 import Years.Y2015.Day9
 import Years.Y2015.Day10
 import Years.Y2015.Day11
--->
+```
 
 # Days
 

src/Years/Y2015/Day1.md

@@ -3,7 +3,7 @@
 Pretty simple, basic warmup problem, nothing really novel is on display here
 except the effectful part computations.
 
-<!-- idris
+```idris hide
 module Years.Y2015.Day1
 
 import Control.Eff
@@ -11,7 +11,7 @@ import Control.Eff
 import Runner
 
 %default total
--->
+```
 
 ## Solver Functions
 
@@ -76,8 +76,8 @@ part2 x = do
   pure $ findBasement 1 0 input
 ```
 
-<!-- idris
+```idris hide
 public export
 day1 : Day
 day1 = Both 1 part1 part2
--->
+```

src/Years/Y2015/Day10.md

@@ -3,13 +3,13 @@
 This day doesn't really add anything new, but we will show off our new views for
 viewing integers as lists of digits.
 
-<!-- idris
+```idris hide
 module Years.Y2015.Day10
 
 import Control.Eff
 
 import Runner
--->
+```
 
 ```idris
 import Data.String
@@ -22,9 +22,9 @@ import Util
 import Util.Digits
 ```
 
-<!-- idris
+```idris hide
 %default total
--->
+```
 
 # Solver Functions
 
@@ -118,8 +118,8 @@ part2 digits = do
   pure $ count (const True) output
 ```
 
-<!-- idris
+```idris hide
 public export
 day10 : Day
 day10 = Both 10 part1 part2
--->
+```

src/Years/Y2015/Day11.md

@@ -10,13 +10,13 @@ implement the one we need for today's task as a throw away data structure just
 for this module, we will be using the `refined`[^1] library's implementation for
 the sake of getting on with it.
 
-<!-- idris 
+```idris hide
 module Years.Y2015.Day11
 
 import Control.Eff
 
 import Runner
--->
+```
 
 ```idris
 import Data.Vect
@@ -55,13 +55,13 @@ record PasswordChar where
 %name PasswordChar pc
 ```
 
-<!-- idris
+```idris hide
 Show PasswordChar where
   show (MkPC char) = singleton char
 
 Eq PasswordChar where
   x == y = x.char == y.char
--->
+```
 
 A function to fallible convert `Char`s into refined `PasswordChar`s, this will
 return `Just` if the `Char` satisfies the predicate, and `Nothing` otherwise,
@@ -227,12 +227,12 @@ part2 password = do
   pure $ passwordToString next_password
 ```
 
-<!-- idris
+```idris hide
 public export
 day11 : Day
 day11 = Both 11 part1 part2
--->
+```
 
 ## References
 
-[^1]: https://github.com/stefan-hoeck/idris2-refined/
+[^1]: <https://github.com/stefan-hoeck/idris2-refined/>

src/Years/Y2015/Day2.md

@@ -2,13 +2,13 @@
 
 This day provides us our first little taste of effectful parsing
 
-<!-- idris
+```idris hide
 module Years.Y2015.Day2
 
 import Control.Eff
 
 import Runner
--->
+```
 
 ```idris
 import Data.List
@@ -16,9 +16,9 @@ import Data.List1
 import Data.String
 ```
 
-<!-- idris 
+```idris hide
 %default total
--->
+```
 
 ## Box structure
 
@@ -130,8 +130,8 @@ part2 : (boxes : List Box) -> Eff (PartEff String) Integer
 part2 boxes = pure . sum . map totalRibbon $ boxes
 ```
 
-<!-- idris
+```idris hide
 public export
 day2 : Day
 day2 = Both 2 part1 part2
--->
+```

src/Years/Y2015/Day3.md

@@ -3,13 +3,13 @@
 This day provides a gentle introduction to `mutual` blocks and mutually
 recursive functions.
 
-<!-- idris
+```idris hide
 module Years.Y2015.Day3
 
 import Control.Eff
 
 import Runner
--->
+```
 
 ```idris
 import Data.SortedSet
@@ -18,9 +18,9 @@ import Data.String
 import Util
 ```
 
-<!-- idris
+```idris hide
 %default total
--->
+```
 
 ## Parsing and data structures
 
@@ -152,8 +152,8 @@ part2 movements = do
   pure . length $ locations
 ```
 
-<!-- idris
+```idris hide
 public export
 day3 : Day
 day3 = Both 3 part1 part2
--->
+```

src/Years/Y2015/Day4.md

@@ -3,13 +3,13 @@
 This day introduces us to a little bit of FFI, linking to openssl to use it's
 `MD5` functionality.
 
-<!-- idris
+```idris hide
 module Years.Y2015.Day4
 
 import Control.Eff
 
 import Runner
--->
+```
 
 ```idris
 import Data.String
@@ -196,8 +196,8 @@ part2 seed = do
   pure number
 ```
 
-<!-- idris
+```idris hide
 public export
 day4 : Day
 day4 = Both 4 part1 part2
--->
+```

src/Years/Y2015/Day5.md

@@ -6,13 +6,13 @@ specifically `String`'s
 [`AsList`](https://www.idris-lang.org/docs/idris2/current/base_docs/docs/Data.String.html#Data.String.AsList)
 view, which lets us treat `String`s as if they were lazy lists or iterators.
 
-<!-- idris
+```idris hide
 module Years.Y2015.Day5
 
 import Control.Eff
 
 import Runner
--->
+```
 
 ```idris
 import Data.String
@@ -20,9 +20,9 @@ import Data.String
 import Util
 ```
 
-<!-- idris
+```idris hide
 %default total
--->
+```
 
 ## Nice Strings
 
@@ -213,8 +213,8 @@ part2 _ = do
   pure x
 ```
 
-<!-- idris
+```idris hide
 public export
 day5 : Day
 day5 = Both 5 part1 part2
--->
+```

src/Years/Y2015/Day6.md

@@ -1,16 +1,14 @@
-# \[Year 2015 Day 6\](https://adventofcode.com/2015/day/
+# [Year 2015 Day 6](https://adventofcode.com/2015/day/6)
-
-6.
 
 Introduction to the advent of code classic 2d grid problem.
 
-<!-- idris
+```idris hide
 module Years.Y2015.Day6
 
 import Control.Eff
 
 import Runner
--->
+```
 
 ```idris
 import Util
@@ -23,9 +21,9 @@ import Data.String
 import Data.IORef
 ```
 
-<!-- idris
+```idris hide
 %default total
--->
+```
 
 ## Parsing and data structures
 
@@ -77,12 +75,12 @@ The three types of action that can be performed on a light.
 data Action = On | Off | Toggle
 ```
 
-<!-- idris
+```idris hide
 Show Action where
   show On = "on"
   show Off = "off"
   show Toggle = "toggle"
--->
+```
 
 The range of coordinates that a command affects
 
@@ -92,11 +90,11 @@ record Range (rows, cols : Nat) where
   top_left, bottom_right : Coord rows cols
 ```
 
-<!-- idris
+```idris hide
 Show (Range rows cols) where
   show (MkRange top_left bottom_right) = 
     "\{show top_left} -> \{show bottom_right}"
--->
+```
 
 Helper function to extract a range of values from our Grid.
 
@@ -121,11 +119,11 @@ record Command (rows, cols : Nat) where
   range : Range rows cols
 ```
 
-<!-- idris
+```idris hide
 Show (Command rows cols) where
   show (MkCmd action range) = 
     "{\{show action}: \{show range}}"
--->
+```
 
 ### Parsing
 
@@ -336,8 +334,8 @@ part2 commands = do
   pure brightness
 ```
 
-<!-- idris
+```idris hide
 public export
 day6 : Day
 day6 = Both 6 part1 part2
--->
+```

src/Years/Y2015/Day7.md

@@ -1,6 +1,4 @@
-# \[Year 2015 Day 7\](https://adventofcode.com/2015/day/
+# [Year 2015 Day 7](https://adventofcode.com/2015/day/7)
-
-7.
 
 This day provides us a gentle introduction to dependent maps.
 
@@ -15,13 +13,13 @@ Ensuring that the input contains only one gate outputting for each wire is done
 through throwing a runtime error in the parsing function if a second gate
 outputting to a given wire is found in the input.
 
-<!-- idris
+```idris hide
 module Years.Y2015.Day7
 
 import Control.Eff
 
 import Runner
--->
+```
 
 ```idris
 import Data.Bits
@@ -33,9 +31,9 @@ import Data.SortedMap.Dependent
 import Decidable.Equality
 ```
 
-<!-- idris
+```idris hide
 %default total
--->
+```
 
 ## Parsing and data structures
 
@@ -254,8 +252,8 @@ part2 (circut, value) = do
   pure value
 ```
 
-<!-- idris
+```idris hide
 public export covering
 day7 : Day
 day7 = Both 7 part1 part2
--->
+```

src/Years/Y2015/Day8.md

@@ -3,7 +3,7 @@
 This day provides a more in depth introduction to writing effectful parsers,
 making use of state and non-determinism in our parsers.
 
-<!-- idris
+```idris hide
 module Years.Y2015.Day8
 
 import Control.Eff
@@ -11,7 +11,7 @@ import Control.Eff
 import Data.Primitives.Interpolation
 
 import Runner
--->
+```
 
 ```idris
 import Data.String
@@ -344,8 +344,8 @@ part2 inputs = do
   pure difference
 ```
 
-<!-- idris
+```idris hide
 public export
 day8 : Day
 day8 = Both 8 part1 part2
--->
+```

src/Years/Y2015/Day9.md

@@ -6,13 +6,13 @@ meeting the problem criteria, and then figure out the length in a separate step.
 This isn't a particularly efficient solution, but its good enough for this small
 problem size.
 
-<!-- idris
+```idris hide
 module Years.Y2015.Day9
 
 import Control.Eff
 
 import Runner
--->
+```
 
 ```idris
 import Data.String
@@ -70,10 +70,10 @@ DistanceMap : Type
 DistanceMap = SortedMap Location (List LP)
 ```
 
-<!-- idris
+```idris hide
 Show l => Show (LocationPair l) where
   show (MkLP [x, y] distance) = "\{show x} <-> \{show y}: \{show distance}"
--->
+```
 
 Perform simple, pattern matching based parsing of a location pair.
 
@@ -287,8 +287,8 @@ part2 (distance_map, pairs) = do
   pure len
 ```
 
-<!-- idris
+```idris hide
 public export
 day9 : Day
 day9 = Both 9 part1 part2
--->
+```