content/blog/adventures-in-rust-webassembly.md

@@ -2,9 +2,7 @@
 title: "Adventures in Rust WebAssembly"
 date: 2025-02-21T10:13:17-05:00
 draft: false
-tags:
+tags: ["Rust", "Web"]
-    - WebAssembly
-    - Rust
 math: false
 medium_enabled: false
 ---

content/blog/anti-scraper-techniques.md

@@ -2,12 +2,7 @@
 title: "Dealing with Web Scrapers"
 date: 2025-07-02T09:10:23-04:00
 draft: false
-tags:
+tags: []
-  - web scraping
-  - CAPTCHA
-  - rate limiting
-  - robots.txt
-  - proof of work
 math: false
 medium_enabled: false
 ---

content/blog/blog-question-challenge-jan2025.md

@@ -2,8 +2,7 @@
 title: "Blog Question Challenge (Jan 2025)"
 date: 2025-01-29T21:18:03-05:00
 draft: false
-tags:
+tags: []
-  - blogging
 math: false
 medium_enabled: false
 ---

content/blog/cursed-knowledge-javascript-arrays-are-objects.md

@@ -2,8 +2,7 @@
 title: "Cursed Knowledge: Javascript Arrays Are Objects"
 date: 2025-09-01T09:47:01-04:00
 draft: false
-tags:
+tags: []
-    - JavaScript
 math: true
 medium_enabled: false
 ---

content/blog/deterministic-set-iteration-dafny.md

@@ -2,11 +2,7 @@
 title: "Deterministically Iterating over a set within Dafny functions"
 date: 2025-07-06T12:27:01-04:00
 draft: false
-tags:
+tags: ["Formal Methods"]
-    - Dafny
-    - Formal methods
-    - Deterministic algorithm
-    - Total order
 math: false
 medium_enabled: false
 ---

content/blog/exploring-via-public-transit.md

@@ -2,8 +2,7 @@
 title: "Exploring via Public Transit"
 date: 2025-06-15T21:38:02-04:00
 draft: false
-tags:
+tags: []
-  - public transport
 math: false
 medium_enabled: false
 ---

content/blog/filesystem-as-persistent-kvs-python.md

@@ -2,10 +2,7 @@
 title: "Filesystem as a persistent key-value store in Python"
 date: 2025-04-27T13:39:49-04:00
 draft: false
-tags:
+tags: []
-  - key-value database
-  - file system
-  - Python
 math: false
 medium_enabled: false
 ---

content/blog/flattening-cases-avoid-nesting-lean-4.md

@@ -2,10 +2,7 @@
 title: "Flattening Cases to Avoid Nesting in Lean 4"
 date: 2025-10-05T19:38:20-04:00
 draft: false
-tags:
+tags: []
-  - Lean
-  - Proof assistant
-  - Formal Proof
 math: true
 medium_enabled: false
 ---

content/blog/ollama-cuda-podman-quadlets.md

@@ -2,10 +2,7 @@
 title: "Setting up Ollama with CUDA on Podman Quadlets"
 date: 2025-03-29T09:59:55-04:00
 draft: false
-tags:
+tags: []
-  - Ollama
-  - Podman
-  - CUDA
 math: false
 medium_enabled: false
 ---

content/blog/program-safety-type-theory.md

@@ -2,9 +2,7 @@
 title: "Is this program safe? Lessons from Type Theory"
 date: 2025-05-10T09:28:07-04:00
 draft: false 
-tags:
+tags: []
-  - type theory
-  - type inference
 math: true
 medium_enabled: false
 ---

content/blog/quick-lean-if-then-else-in-hypothesis.md

@@ -2,9 +2,7 @@
 title: "Quick Lean: if-then-else statement in hypothesis"
 date: 2025-04-26T10:58:42-04:00
 draft: false
-tags:
+tags: ["Formal Methods"]
-  - Lean
-  - Proof assistant
 math: false
 medium_enabled: false
 ---

content/blog/recently-2504-april-showers.md

@@ -2,8 +2,7 @@
 title: "Recently: April Showers Bring..."
 date: 2025-04-12T10:38:45-04:00
 draft: false
-tags:
+tags: []
-  - homelab
 math: false
 medium_enabled: false
 ---

content/blog/verifying-proofs-type-checkers.md

@@ -2,14 +2,7 @@
 title: "Verifying Proofs with Type Checkers"
 date: 2025-05-27T09:27:59-04:00
 draft: false
-tags:
+tags: ["Formal Methods"]
-  - Formal methods
-  - proof assistant
-  - Curry-Howard correspondence
-  - lambda cube
-  - calculus of constructions
-  - dependent type
-  - type theory
 math: true
 medium_enabled: false
 ---

content/blog/weather-forcecasts-cli-nws.md

@@ -2,11 +2,7 @@
 title: "Weather Forcecasts on the Command-Line with the National Weather Service API"
 date: 2025-03-16T15:33:49-04:00
 draft: false 
-tags:
+tags: []
-  - Command-line interface
-  - National Weather Service
-  - Bash
-  - jq
 math: false
 medium_enabled: false
 ---

data/wikidata_mappings.json

@@ -1,344 +0,0 @@
-{
-  "fedora-coreos": {
-    "entities": [
-      {
-        "id": "Q98405060",
-        "url": "https://www.wikidata.org/wiki/Q98405060",
-        "description": "Linux distribution"
-      }
-    ]
-  },
-  "podman": {
-    "entities": [
-      {
-        "id": "Q70876440",
-        "url": "https://www.wikidata.org/wiki/Q70876440",
-        "description": "daemonless OCI-compliant container runtime"
-      }
-    ]
-  },
-  "selinux": {
-    "entities": [
-      {
-        "id": "Q116038",
-        "url": "https://www.wikidata.org/wiki/Q116038",
-        "description": "Linux kernel security module"
-      }
-    ]
-  },
-  "nftables": {
-    "entities": [
-      {
-        "id": "Q7021717",
-        "url": "https://www.wikidata.org/wiki/Q7021717",
-        "description": "userspace utility for Linux packet filtering"
-      }
-    ]
-  },
-  "lean": {
-    "entities": [
-      {
-        "id": "Q6509476",
-        "url": "https://www.wikidata.org/wiki/Q6509476",
-        "description": "software for interactive and automated theorem proving"
-      }
-    ]
-  },
-  "proof-assistant": {
-    "entities": [
-      {
-        "id": "Q11387554",
-        "url": "https://www.wikidata.org/wiki/Q11387554",
-        "description": "software tool to assist with the development of formal proofs by human-machine collaboration"
-      }
-    ]
-  },
-  "formal-proof": {
-    "entities": [
-      {
-        "id": "Q2762418",
-        "url": "https://www.wikidata.org/wiki/Q2762418",
-        "description": "establishment of a theorem using inference from the axioms"
-      }
-    ]
-  },
-  "javascript": {
-    "entities": [
-      {
-        "id": "Q2005",
-        "url": "https://www.wikidata.org/wiki/Q2005",
-        "description": "high-level programming language"
-      }
-    ]
-  },
-  "dafny": {
-    "entities": [
-      {
-        "id": "Q48989398",
-        "url": "https://www.wikidata.org/wiki/Q48989398",
-        "description": "programming language"
-      }
-    ]
-  },
-  "formal-methods": {
-    "entities": [
-      {
-        "id": "Q1049183",
-        "url": "https://www.wikidata.org/wiki/Q1049183",
-        "description": "mathematical program specification intended to allow correctness proofs, including algorithmically"
-      }
-    ]
-  },
-  "deterministic-algorithm": {
-    "entities": [
-      {
-        "id": "Q1064349",
-        "url": "https://www.wikidata.org/wiki/Q1064349",
-        "description": "algorithm which, given a particular input, will always produce the same output"
-      }
-    ]
-  },
-  "total-order": {
-    "entities": [
-      {
-        "id": "Q369377",
-        "url": "https://www.wikidata.org/wiki/Q369377",
-        "description": "ordering relation where all elements can be compared; binary relation on some set, which is antisymmetric, transitive, and total"
-      }
-    ]
-  },
-  "web-scraping": {
-    "entities": [
-      {
-        "id": "Q665452",
-        "url": "https://www.wikidata.org/wiki/Q665452",
-        "description": "data scraping used for extracting data from websites"
-      }
-    ]
-  },
-  "captcha": {
-    "entities": [
-      {
-        "id": "Q484598",
-        "url": "https://www.wikidata.org/wiki/Q484598",
-        "description": "computer test to discriminate human users from spambots"
-      }
-    ]
-  },
-  "rate-limiting": {
-    "entities": [
-      {
-        "id": "Q3420050",
-        "url": "https://www.wikidata.org/wiki/Q3420050",
-        "description": "Limiting the data rate on network controllers."
-      }
-    ]
-  },
-  "robots.txt": {
-    "entities": [
-      {
-        "id": "Q80776",
-        "url": "https://www.wikidata.org/wiki/Q80776",
-        "description": "standard used to advise web crawlers and scrapers not to index a web page or site"
-      }
-    ]
-  },
-  "proof-of-work": {
-    "entities": [
-      {
-        "id": "Q7249984",
-        "url": "https://www.wikidata.org/wiki/Q7249984",
-        "description": "a system that regulates the formation of blocks on a blockchain"
-      }
-    ]
-  },
-  "user-agent-http-header": {
-    "entities": [
-      {
-        "id": "Q115124801",
-        "url": "https://www.wikidata.org/wiki/Q115124801",
-        "description": "HTTP request header indicating the initiating software (e.g. browser)"
-      }
-    ]
-  },
-  "public-transport": {
-    "entities": [
-      {
-        "id": "Q178512",
-        "url": "https://www.wikidata.org/wiki/Q178512",
-        "description": "shared transportation service for use by the general public"
-      }
-    ]
-  },
-  "curry-howard-correspondence": {
-    "entities": [
-      {
-        "id": "Q975734",
-        "url": "https://www.wikidata.org/wiki/Q975734",
-        "description": "the direct relationship between computer programs and mathematical proofs"
-      }
-    ]
-  },
-  "lambda-cube": {
-    "entities": [
-      {
-        "id": "Q2036661",
-        "url": "https://www.wikidata.org/wiki/Q2036661",
-        "description": "a framework"
-      }
-    ]
-  },
-  "calculus-of-constructions": {
-    "entities": [
-      {
-        "id": "Q858320",
-        "url": "https://www.wikidata.org/wiki/Q858320",
-        "description": "formal system"
-      }
-    ]
-  },
-  "dependent-type": {
-    "entities": [
-      {
-        "id": "Q997433",
-        "url": "https://www.wikidata.org/wiki/Q997433",
-        "description": "data type whose definition depends on a value"
-      }
-    ]
-  },
-  "type-theory": {
-    "entities": [
-      {
-        "id": "Q1056428",
-        "url": "https://www.wikidata.org/wiki/Q1056428",
-        "description": "concept in mathematical logic and computer science"
-      }
-    ]
-  },
-  "type-inference": {
-    "entities": [
-      {
-        "id": "Q586459",
-        "url": "https://www.wikidata.org/wiki/Q586459",
-        "description": "automatic detection of the data type of an expression in a programming language"
-      }
-    ]
-  },
-  "key-value-database": {
-    "entities": [
-      {
-        "id": "Q20706915",
-        "url": "https://www.wikidata.org/wiki/Q20706915",
-        "description": "data storage paradigm designed for storing, retrieving, and managing associative arrays"
-      }
-    ]
-  },
-  "file-system": {
-    "entities": [
-      {
-        "id": "Q174989",
-        "url": "https://www.wikidata.org/wiki/Q174989",
-        "description": "concrete format or program for storing files and directories on a data storage device"
-      }
-    ]
-  },
-  "python": {
-    "entities": [
-      {
-        "id": "Q28865",
-        "url": "https://www.wikidata.org/wiki/Q28865",
-        "description": "general-purpose programming language"
-      }
-    ]
-  },
-  "homelab": {
-    "entities": [
-      {
-        "id": "Q750110",
-        "url": "https://www.wikidata.org/wiki/Q750110",
-        "description": "computing server located in a private residence providing services to other devices inside or outside the household through a home network or the Internet"
-      }
-    ]
-  },
-  "ollama": {
-    "entities": [
-      {
-        "id": "Q124636097",
-        "url": "https://www.wikidata.org/wiki/Q124636097",
-        "description": "large-language-model open-source software library"
-      }
-    ]
-  },
-  "cuda": {
-    "entities": [
-      {
-        "id": "Q477690",
-        "url": "https://www.wikidata.org/wiki/Q477690",
-        "description": "parallel computing platform and programming model"
-      }
-    ]
-  },
-  "command-line-interface": {
-    "entities": [
-      {
-        "id": "Q189053",
-        "url": "https://www.wikidata.org/wiki/Q189053",
-        "description": "type of computer interface based on entering text commands and viewing text output"
-      }
-    ]
-  },
-  "national-weather-service": {
-    "entities": [
-      {
-        "id": "Q1066823",
-        "url": "https://www.wikidata.org/wiki/Q1066823",
-        "description": "U.S. forecasting agency of the National Oceanic and Atmospheric Administration"
-      }
-    ]
-  },
-  "bash": {
-    "entities": [
-      {
-        "id": "Q189248",
-        "url": "https://www.wikidata.org/wiki/Q189248",
-        "description": "GNU Project implementation of the standard Unix shell"
-      }
-    ]
-  },
-  "jq": {
-    "entities": [
-      {
-        "id": "Q28801607",
-        "url": "https://www.wikidata.org/wiki/Q28801607",
-        "description": "command-line JSON processor"
-      }
-    ]
-  },
-  "webassembly": {
-    "entities": [
-      {
-        "id": "Q20155677",
-        "url": "https://www.wikidata.org/wiki/Q20155677",
-        "description": "portable, efficient virtual machine and bytecode format for compiled code on the Web"
-      }
-    ]
-  },
-  "rust": {
-    "entities": [
-      {
-        "id": "Q575650",
-        "url": "https://www.wikidata.org/wiki/Q575650",
-        "description": "memory-safe programming language without garbage collection"
-      }
-    ]
-  },
-  "blogging": {
-    "entities": [
-      {
-        "id": "Q21124681",
-        "url": "https://www.wikidata.org/wiki/Q21124681",
-        "description": "action of writing articles or maintaining a weblog"
-      }
-    ]
-  }
-}

themes/pulp

@@ -1 +1 @@
-Subproject commit ded609da7dfd3eec8f1002560bfb00bc66db2c0b
+Subproject commit fd4db04d3a6676f0db6dad6d65705b96cdf4b52a