Merge remote-tracking branch 'origin/master'

6 files changed, 54 insertions, 48 deletions

diff --git a/config.toml b/config.toml
index ec96fb9..6a987fa 100644
--- a/config.toml
+++ b/config.toml
@@ -8,7 +8,7 @@ theme = "ymherklotz"
   katex = true
 
 [permalinks]
-  blog = '/:year/:month/:title/'
+  blog = '/:filename/'
 
 [markup.goldmark.renderer]
   unsafe = true
diff --git a/content.org b/content.org
index bbc3d27..f99374f 100644
--- a/content.org
+++ b/content.org
@@ -12,8 +12,8 @@
 
 #+html: <img src="/images/portrait.jpg" alt="Profile picture" class="profile-picture" />
 
-@@hugo:<span class="first-letter">H</span>@@@@latex:H@@i! I'm currently a PhD student in the
-Circuits and Systems group at Imperial College London, supervised by [[https://johnwickerson.github.io][John Wickerson]].
+Hi! I'm currently a PhD student in the Circuits and Systems group at Imperial College London,
+supervised by [[https://johnwickerson.github.io][John Wickerson]].
 
 My research focuses on formalising the process of converting high-level programming language
 descriptions to correct hardware that is functionally equivalent to the input. This process is
@@ -35,6 +35,11 @@ is located.
 
 Here you can find all my previous posts:
 
+** TODO About the Promise of Performance from Formal Verification
+
+When one thinks about formal verification, one normally associates this with sacrificing performance
+for an improvement in reliability.  However, this does not necessarily have to be the case.  In this
+post I'll try and argue for why
 ** TODO Reasoning about :logic:
 :PROPERTIES:
 :EXPORT_DATE: 2022-02-22
@@ -66,10 +71,10 @@ as reason about complex code using modern SMT solvers.
 ** Introduction to Luhmann's Zettelkasten :writing:emacs:
 :PROPERTIES:
 :EXPORT_DATE: 2020-12-21
-:EXPORT_FILE_NAME: introduction-to-luhmanns-zettelkasten
+:EXPORT_FILE_NAME: zettelkasten
 :EXPORT_HUGO_SECTION: blog
-:EXPORT_HUGO_CUSTOM_FRONT_MATTER: :summary "Niklas Luhmann's Zettelkasten is becoming increasingly popular for being a great note taking technique.  However, it is often misunderstood as taking notes without any structure, whereas Luhmann actually structured his notes hierarchically, but also allowed for arbitrary links between notes." :aliases '("/blog/2020-12-21-introduction-to-luhmanns-zettelkasten.html")
-:CUSTOM_ID: introduction-to-luhmanns-zettelkasten
+:EXPORT_HUGO_CUSTOM_FRONT_MATTER: :summary "Niklas Luhmann's Zettelkasten is becoming increasingly popular for being a great note taking technique.  However, it is often misunderstood as taking notes without any structure, whereas Luhmann actually structured his notes hierarchically, but also allowed for arbitrary links between notes." :aliases '("/blog/2020-12-21-introduction-to-luhmanns-zettelkasten.html" "/2020/12/introduction-to-luhmanns-zettelkasten/")
+:CUSTOM_ID: zettelkasten
 :END:
 
 Niklas Luhmann's [[https://niklas-luhmann-archiv.de/bestand/zettelkasten/suche][Zettelkasten]] is becoming increasingly popular for being a great note taking
@@ -362,10 +367,10 @@ these notes.
 ** Nix for Coq Development :nix:coq:
 :PROPERTIES:
 :EXPORT_DATE: 2020-02-15
-:EXPORT_FILE_NAME: nix-for-coq-development
+:EXPORT_FILE_NAME: nix-for-coq
 :EXPORT_HUGO_SECTION: blog
-:EXPORT_HUGO_CUSTOM_FRONT_MATTER: :summary "Nix is a great package manager that can be used to control various complex environments easily, such as Coq development with ocaml extraction with various dependencies." :aliases '("/blog/2020-02-15-nix-for-coq-development.html")
-:CUSTOM_ID: nix-for-coq-development
+:EXPORT_HUGO_CUSTOM_FRONT_MATTER: :summary "Nix is a great package manager that can be used to control various complex environments easily, such as Coq development with ocaml extraction with various dependencies." :aliases '("/blog/2020-02-15-nix-for-coq-development.html" "/2020/02/nix-for-coq-development/")
+:CUSTOM_ID: nix-for-coq
 :END:
 
 I first learnt about [[https://nixos.org/nix/][Nix]] because of Haskell, eventually running into cabal hell while working on
@@ -615,10 +620,10 @@ Coq.
 ** MSR PhD Workshop on Next-Generation Cloud Infrastructure :workshop:FPGA:
 :PROPERTIES:
 :EXPORT_DATE: 2019-11-26
-:EXPORT_FILE_NAME: msr-phd-workshop-next-generation-cloud-infrastructure
+:EXPORT_FILE_NAME: msr-phd-workshop
 :EXPORT_HUGO_SECTION: blog
-:EXPORT_HUGO_CUSTOM_FRONT_MATTER: :summary "Summary of the microsoft talks and posters presented at the MSR PhD Workshop on Next-Generation Cloud Infrastructure." :aliases '("/blog/2019-11-26-msr-phd-workshop-next-generation-cloud-infrastructure.html")
-:CUSTOM_ID: msr-phd-workshop-on-next-generation-cloud-infrastructure
+:EXPORT_HUGO_CUSTOM_FRONT_MATTER: :summary "Summary of the microsoft talks and posters presented at the MSR PhD Workshop on Next-Generation Cloud Infrastructure." :aliases '("/blog/2019-11-26-msr-phd-workshop-next-generation-cloud-infrastructure.html" "/2019/11/msr-phd-workshop-next-generation-cloud-infrastructure/")
+:CUSTOM_ID: msr-phd-workshop
 :END:
 
 Microsoft Research held their first PhD Workshop which focused on new technologies for the
@@ -745,7 +750,7 @@ straightforward as they are thinking.
 :EXPORT_DATE: 2019-06-19
 :EXPORT_FILE_NAME: verismith
 :EXPORT_HUGO_SECTION: blog
-:EXPORT_HUGO_CUSTOM_FRONT_MATTER: :summary "Verilog Fuzzer to test the major verilog compilers by generating random, valid Verilog." :aliases '("/blog/2019-06-19-verismith.html")
+:EXPORT_HUGO_CUSTOM_FRONT_MATTER: :summary "Verilog Fuzzer to test the major verilog compilers by generating random, valid Verilog." :aliases '("/blog/2019-06-19-verismith.html" "/2019/06/verismith/")
 :CUSTOM_ID: verismith
 :END:
 
@@ -833,7 +838,7 @@ The following resources provide more context about Verismith:
 :EXPORT_DATE: 2019-02-24
 :EXPORT_FILE_NAME: realistic-graphics
 :EXPORT_HUGO_SECTION: blog
-:EXPORT_HUGO_CUSTOM_FRONT_MATTER: :summary "Environment maps can be used to render objects with realistic lighting by indexing into the map." :aliases '("/blog/2019-02-24-realistic-graphics.html")
+:EXPORT_HUGO_CUSTOM_FRONT_MATTER: :summary "Environment maps can be used to render objects with realistic lighting by indexing into the map." :aliases '("/blog/2019-02-24-realistic-graphics.html" "/2019/02/realistic-graphics/")
 :CUSTOM_ID: realistic-graphics
 :END:
 
@@ -904,10 +909,10 @@ sample a few lights.
 ** Jekyll to create a portfolio website :web:
 :PROPERTIES:
 :EXPORT_DATE: 2018-07-08
-:EXPORT_FILE_NAME: jekyll-for-portfolio-website
+:EXPORT_FILE_NAME: jekyll
 :EXPORT_HUGO_SECTION: blog
-:EXPORT_HUGO_CUSTOM_FRONT_MATTER: :summary "Jekyll can be effectively used to publish a static website, even containing multiple pages such as a portfolio." :aliases '("/blog/2018-07-08-jekyll-for-portfolio-website.html")
-:CUSTOM_ID: jekyll-to-create-a-portfolio-website
+:EXPORT_HUGO_CUSTOM_FRONT_MATTER: :summary "Jekyll can be effectively used to publish a static website, even containing multiple pages such as a portfolio." :aliases '("/blog/2018-07-08-jekyll-for-portfolio-website.html" "/2018/07/jekyll-to-create-a-portfolio-website/")
+:CUSTOM_ID: jekyll
 :END:
 
 [[https://jekyllrb.com/][Jekyll]] is a static site generator written in ruby that can be used in conjunction with Github Pages
@@ -1020,7 +1025,7 @@ the descriptions and blogs using markdown.
 :EXPORT_DATE: 2018-03-23
 :EXPORT_FILE_NAME: noise-silencer
 :EXPORT_HUGO_SECTION: blog
-:EXPORT_HUGO_CUSTOM_FRONT_MATTER: :summary "A real-time noise cancelling processor that reduces noise from audio." :aliases '("/blog/2018-03-23-noise-silencer.html")
+:EXPORT_HUGO_CUSTOM_FRONT_MATTER: :summary "A real-time noise cancelling processor that reduces noise from audio." :aliases '("/blog/2018-03-23-noise-silencer.html" "/2018/03/noise-silencer/")
 :CUSTOM_ID: noise-silencer
 :END:
 
@@ -1035,7 +1040,7 @@ original spectrum of the signal.
 :EXPORT_DATE: 2018-03-23
 :EXPORT_FILE_NAME: fmark
 :EXPORT_HUGO_SECTION: blog
-:EXPORT_HUGO_CUSTOM_FRONT_MATTER: :summary "FMark is a markdown engine in F#, supporting various extensions such as latex rendered math and macros." :aliases '("/blog/2018-03-23-fmark.html")
+:EXPORT_HUGO_CUSTOM_FRONT_MATTER: :summary "FMark is a markdown engine in F#, supporting various extensions such as latex rendered math and macros." :aliases '("/blog/2018-03-23-fmark.html" "/2018/03/fmark/")
 :CUSTOM_ID: fmark
 :END:
 
@@ -1102,8 +1107,8 @@ over once something changes.
 :EXPORT_DATE: 2018-02-23
 :EXPORT_FILE_NAME: emotion-classification
 :EXPORT_HUGO_SECTION: blog
-:EXPORT_HUGO_CUSTOM_FRONT_MATTER: :summary "A convolutional neural network was trained to classify images based on 6 emotions, achieving an accuracy of about 60%." :aliases '("/blog/2018-02-23-emotion-classification.html")
-:CUSTOM_ID: emotion-classification-using-images
+:EXPORT_HUGO_CUSTOM_FRONT_MATTER: :summary "A convolutional neural network was trained to classify images based on 6 emotions, achieving an accuracy of about 60%." :aliases '("/blog/2018-02-23-emotion-classification.html" "/2018/02/emotion-classification/")
+:CUSTOM_ID: emotion-classification
 :END:
 
 We wrote a Convolutional Neural Network that would classify images into the 6 base emotions. We used
@@ -1114,7 +1119,7 @@ tensorflow and python to design the network and train it.
 :EXPORT_DATE: 2018-01-20
 :EXPORT_FILE_NAME: yage
 :EXPORT_HUGO_SECTION: blog
-:EXPORT_HUGO_CUSTOM_FRONT_MATTER: :summary "YAGE is a game engine that was built in C++ using OpenGL as a back end." :aliases '("/blog/2018-01-20-yage.html")
+:EXPORT_HUGO_CUSTOM_FRONT_MATTER: :summary "YAGE is a game engine that was built in C++ using OpenGL as a back end." :aliases '("/blog/2018-01-20-yage.html" "/2018/01/yage/")
 :CUSTOM_ID: yage
 :END:
 
@@ -1140,8 +1145,8 @@ that can be drawn high.
 :EXPORT_DATE: 2018-01-14
 :EXPORT_FILE_NAME: emacs-email-client
 :EXPORT_HUGO_SECTION: blog
-:EXPORT_HUGO_CUSTOM_FRONT_MATTER: :summary "Emacs can be used effectively as an email client to quickly write emails using familiar keybindings, as well as easily linking emails to org files for reminders." :aliases '("/blog/2018-01-14-emacs-email-client.html")
-:CUSTOM_ID: emacs-as-an-email-client
+:EXPORT_HUGO_CUSTOM_FRONT_MATTER: :summary "Emacs can be used effectively as an email client to quickly write emails using familiar keybindings, as well as easily linking emails to org files for reminders." :aliases '("/blog/2018-01-14-emacs-email-client.html" "/2018/01/emacs-email-client/")
+:CUSTOM_ID: emacs-email-client
 :END:
 
 Emacs is a very powerful editor, therefore there are many benefits from using it as an email client,
@@ -1267,9 +1272,9 @@ Emacs is now ready to be used as a full featured email client.
 ** CPU Introduction :hardware:
 :PROPERTIES:
 :EXPORT_DATE: 2016-12-14
-:EXPORT_FILE_NAME: CPU-introduction
+:EXPORT_FILE_NAME: cpu-introduction
 :EXPORT_HUGO_SECTION: blog
-:EXPORT_HUGO_CUSTOM_FRONT_MATTER: :summary "Introduction to how a CPU works, following the MIPS I architecture and explaining properties such as pipelining." :aliases '(/blog/2016-12-14-CPU-introduction.html)
+:EXPORT_HUGO_CUSTOM_FRONT_MATTER: :summary "Introduction to how a CPU works, following the MIPS I architecture and explaining properties such as pipelining." :aliases '("/blog/2016-12-14-CPU-introduction.html" "/2016/12/cpu-introduction/")
 :CUSTOM_ID: cpu-introduction
 :END:
 
@@ -1326,7 +1331,7 @@ however, it means that the complexity of the hardware increases by a lot.
 :EXPORT_DATE: 2017-02-20
 :EXPORT_FILE_NAME: compiler
 :EXPORT_HUGO_SECTION: blog
-:EXPORT_HUGO_CUSTOM_FRONT_MATTER: :summary "Implemented a C compiler to MIPS assembly code using flex and bison as the frontend. An abstract syntax tree is built from the parser and code generation is implemented as part of the AST." :aliases '(/blog/2017-02-20-compiler.html)
+:EXPORT_HUGO_CUSTOM_FRONT_MATTER: :summary "Implemented a C compiler to MIPS assembly code using flex and bison as the frontend. An abstract syntax tree is built from the parser and code generation is implemented as part of the AST." :aliases '("/blog/2017-02-20-compiler.html" "/2017/02/compiler/")
 :CUSTOM_ID: compiler
 :END:
 
@@ -1380,7 +1385,7 @@ TODO Part about compiler
 :EXPORT_DATE: 2016-10-03
 :EXPORT_FILE_NAME: mips-processor
 :EXPORT_HUGO_SECTION: blog
-:EXPORT_HUGO_CUSTOM_FRONT_MATTER: :summary "Implemented a MIPS I CPU simulator in C++ which can execute assembly code." :aliases '("/blog/2016-10-03-mips-processor.html")
+:EXPORT_HUGO_CUSTOM_FRONT_MATTER: :summary "Implemented a MIPS I CPU simulator in C++ which can execute assembly code." :aliases '("/blog/2016-10-03-mips-processor.html" "/2016/10/mips-processor/")
 :CUSTOM_ID: mips-processor
 :END:
 
@@ -1397,8 +1402,8 @@ instructions.
 :EXPORT_DATE: 2016-03-24
 :EXPORT_FILE_NAME: note-reader
 :EXPORT_HUGO_SECTION: blog
-:EXPORT_HUGO_CUSTOM_FRONT_MATTER: :summary "We built a real-time music note reader using an FPGA and a camera. It can read custom sheet music and play it back in real-time. The pitch is also adjustable using a blue marker placed anywhere in front of the camera." :aliases '("/blog/2016-03-24-note-reader.html")
-:CUSTOM_ID: fpga-note-reader
+:EXPORT_HUGO_CUSTOM_FRONT_MATTER: :summary "We built a real-time music note reader using an FPGA and a camera. It can read custom sheet music and play it back in real-time. The pitch is also adjustable using a blue marker placed anywhere in front of the camera." :aliases '("/blog/2016-03-24-note-reader.html" "/2016/03/note-reader/")
+:CUSTOM_ID: note-reader
 :END:
 
 In our first year of uni, we built a real-time music note reader using an FPGA and a camera. It can
diff --git a/themes/ymherklotz/layouts/partials/head.html b/themes/ymherklotz/layouts/partials/head.html
index 8d6b33a..e1a9962 100644
--- a/themes/ymherklotz/layouts/partials/head.html
+++ b/themes/ymherklotz/layouts/partials/head.html
@@ -26,6 +26,7 @@
   <link rel="stylesheet" href="{{ .Site.BaseURL }}/css/syntax_dark.css" />
   <link rel="stylesheet" href="{{ .Site.BaseURL }}/css/colours.css" />
   <link rel="stylesheet" href="{{ .Site.BaseURL }}/css/default.css" />
+  {{ if .IsPage }}<link rel="stylesheet" href="{{ .Site.BaseURL }}/css/blog.css" />{{ end }}
 
   <link rel="preload" href="{{ .Site.BaseURL }}/fonts/woff2/iosevka-extrabold.woff2">
 </head>
diff --git a/themes/ymherklotz/static/css/blog.css b/themes/ymherklotz/static/css/blog.css
index d09b02f..5d44281 100644
--- a/themes/ymherklotz/static/css/blog.css
+++ b/themes/ymherklotz/static/css/blog.css
@@ -1,7 +1,8 @@
-article > p:first-of-type::first-letter {
+article > p:first-of-type:first-letter {
   float: left;
-  line-height: 0.8;
-  margin-right: 10px;
-  font-weight: bold;
-  font-size: 6rem;
+  line-height: 1;
+  padding-right: 5px;
+  margin: 0 auto;
+  font-family: 'EBGaramond-Init', 'EBGaramond', serif;
+  font-size: 75px;
 }
diff --git a/themes/ymherklotz/static/css/colours.css b/themes/ymherklotz/static/css/colours.css
index 12f6529..4e64bb0 100644
--- a/themes/ymherklotz/static/css/colours.css
+++ b/themes/ymherklotz/static/css/colours.css
@@ -8,7 +8,7 @@ body {
 }
 
 a {
-  color: #00c266;
+  color: #00A659;
 }
 
 a:hover {
diff --git a/themes/ymherklotz/static/css/default.css b/themes/ymherklotz/static/css/default.css
index 09d8232..25cdd00 100644
--- a/themes/ymherklotz/static/css/default.css
+++ b/themes/ymherklotz/static/css/default.css
@@ -128,23 +128,22 @@ th, td {
 }
 
 .social {
-  font-size: 2rem;
   line-height: 0;
   text-align: center;
 }
 
-article > p:first-of-type:first-letter {
-  float: left;
-  line-height: 1;
-  padding-right: 5px;
-  margin: 0 auto;
-  font-family: 'EBGaramond-Init', 'EBGaramond', serif;
-  font-size: 5.15em;
-}
+/* article > p:first-of-type:first-letter { */
+/*   float: left; */
+/*   line-height: 1; */
+/*   padding-right: 5px; */
+/*   margin: 0 auto; */
+/*   font-family: 'EBGaramond-Init', 'EBGaramond', serif; */
+/*   font-size: 75px; */
+/* } */
 
-article > p:first-of-type:first-line {
-  font-family: 'EBGaramond-SC', 'EBGaramond', serif;
-}
+/* article > p:first-of-type:first-line { */
+/*   font-family: 'EBGaramond-SC', 'EBGaramond', serif; */
+/* } */
 
 .heading-anchor1 {
   text-decoration: none;