diff --git a/content/blog/adventures-in-rust-webassembly.md b/content/blog/adventures-in-rust-webassembly.md index e8c0cc3..e95d0b1 100644 --- a/content/blog/adventures-in-rust-webassembly.md +++ b/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: - - WebAssembly - - Rust +tags: ["Rust", "Web"] math: false medium_enabled: false --- diff --git a/content/blog/anti-scraper-techniques.md b/content/blog/anti-scraper-techniques.md index df96b49..47aeb0a 100644 --- a/content/blog/anti-scraper-techniques.md +++ b/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: - - web scraping - - CAPTCHA - - rate limiting - - robots.txt - - proof of work +tags: [] math: false medium_enabled: false --- diff --git a/content/blog/blog-question-challenge-jan2025.md b/content/blog/blog-question-challenge-jan2025.md index 41c0610..b52e4ca 100644 --- a/content/blog/blog-question-challenge-jan2025.md +++ b/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: - - blogging +tags: [] math: false medium_enabled: false --- diff --git a/content/blog/cursed-knowledge-javascript-arrays-are-objects.md b/content/blog/cursed-knowledge-javascript-arrays-are-objects.md index beb3199..19a1934 100644 --- a/content/blog/cursed-knowledge-javascript-arrays-are-objects.md +++ b/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: - - JavaScript +tags: [] math: true medium_enabled: false --- diff --git a/content/blog/deterministic-set-iteration-dafny.md b/content/blog/deterministic-set-iteration-dafny.md index 43f818a..93b5d44 100644 --- a/content/blog/deterministic-set-iteration-dafny.md +++ b/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: - - Dafny - - Formal methods - - Deterministic algorithm - - Total order +tags: ["Formal Methods"] math: false medium_enabled: false --- diff --git a/content/blog/exploring-via-public-transit.md b/content/blog/exploring-via-public-transit.md index 6db0a58..19630d2 100644 --- a/content/blog/exploring-via-public-transit.md +++ b/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: - - public transport +tags: [] math: false medium_enabled: false --- diff --git a/content/blog/filesystem-as-persistent-kvs-python.md b/content/blog/filesystem-as-persistent-kvs-python.md index afcad1c..8bda61f 100644 --- a/content/blog/filesystem-as-persistent-kvs-python.md +++ b/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: - - key-value database - - file system - - Python +tags: [] math: false medium_enabled: false --- diff --git a/content/blog/flattening-cases-avoid-nesting-lean-4.md b/content/blog/flattening-cases-avoid-nesting-lean-4.md index 90f8ef5..3884611 100644 --- a/content/blog/flattening-cases-avoid-nesting-lean-4.md +++ b/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: - - Lean - - Proof assistant - - Formal Proof +tags: [] math: true medium_enabled: false --- diff --git a/content/blog/ollama-cuda-podman-quadlets.md b/content/blog/ollama-cuda-podman-quadlets.md index 742eb47..cce15c7 100644 --- a/content/blog/ollama-cuda-podman-quadlets.md +++ b/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: - - Ollama - - Podman - - CUDA +tags: [] math: false medium_enabled: false --- diff --git a/content/blog/program-safety-type-theory.md b/content/blog/program-safety-type-theory.md index 5be16e8..2655c1b 100644 --- a/content/blog/program-safety-type-theory.md +++ b/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: - - type theory - - type inference +tags: [] math: true medium_enabled: false --- diff --git a/content/blog/quick-lean-if-then-else-in-hypothesis.md b/content/blog/quick-lean-if-then-else-in-hypothesis.md index a282925..e9e4107 100644 --- a/content/blog/quick-lean-if-then-else-in-hypothesis.md +++ b/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: - - Lean - - Proof assistant +tags: ["Formal Methods"] math: false medium_enabled: false --- diff --git a/content/blog/recently-2504-april-showers.md b/content/blog/recently-2504-april-showers.md index 1b91bee..50ff039 100644 --- a/content/blog/recently-2504-april-showers.md +++ b/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: - - homelab +tags: [] math: false medium_enabled: false --- diff --git a/content/blog/verifying-proofs-type-checkers.md b/content/blog/verifying-proofs-type-checkers.md index fa05174..ef01423 100644 --- a/content/blog/verifying-proofs-type-checkers.md +++ b/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: - - Formal methods - - proof assistant - - Curry-Howard correspondence - - lambda cube - - calculus of constructions - - dependent type - - type theory +tags: ["Formal Methods"] math: true medium_enabled: false --- diff --git a/content/blog/weather-forcecasts-cli-nws.md b/content/blog/weather-forcecasts-cli-nws.md index 7925e89..11efecc 100644 --- a/content/blog/weather-forcecasts-cli-nws.md +++ b/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: - - Command-line interface - - National Weather Service - - Bash - - jq +tags: [] math: false medium_enabled: false --- diff --git a/data/wikidata_mappings.json b/data/wikidata_mappings.json deleted file mode 100644 index d2e9211..0000000 --- a/data/wikidata_mappings.json +++ /dev/null @@ -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" - } - ] - } -} diff --git a/themes/pulp b/themes/pulp index ded609d..fd4db04 160000 --- a/themes/pulp +++ b/themes/pulp @@ -1 +1 @@ -Subproject commit ded609da7dfd3eec8f1002560bfb00bc66db2c0b +Subproject commit fd4db04d3a6676f0db6dad6d65705b96cdf4b52a