From 7e6a7c32856cfd22c76e27853705613e75912ac1 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Sun, 30 Nov 2025 12:10:33 -0500 Subject: [PATCH 1/2] Retagged posts from 2025 --- content/blog/adventures-in-rust-webassembly.md | 4 +++- content/blog/anti-scraper-techniques.md | 7 ++++++- content/blog/blog-question-challenge-jan2025.md | 3 ++- .../cursed-knowledge-javascript-arrays-are-objects.md | 3 ++- content/blog/deterministic-set-iteration-dafny.md | 6 +++++- content/blog/exploring-via-public-transit.md | 3 ++- content/blog/filesystem-as-persistent-kvs-python.md | 5 ++++- content/blog/flattening-cases-avoid-nesting-lean-4.md | 5 ++++- content/blog/ollama-cuda-podman-quadlets.md | 5 ++++- content/blog/program-safety-type-theory.md | 4 +++- content/blog/quick-lean-if-then-else-in-hypothesis.md | 4 +++- content/blog/recently-2504-april-showers.md | 3 ++- content/blog/verifying-proofs-type-checkers.md | 9 ++++++++- content/blog/weather-forcecasts-cli-nws.md | 6 +++++- themes/pulp | 2 +- 15 files changed, 54 insertions(+), 15 deletions(-) diff --git a/content/blog/adventures-in-rust-webassembly.md b/content/blog/adventures-in-rust-webassembly.md index e95d0b1..e8c0cc3 100644 --- a/content/blog/adventures-in-rust-webassembly.md +++ b/content/blog/adventures-in-rust-webassembly.md @@ -2,7 +2,9 @@ title: "Adventures in Rust WebAssembly" date: 2025-02-21T10:13:17-05:00 draft: false -tags: ["Rust", "Web"] +tags: + - WebAssembly + - Rust math: false medium_enabled: false --- diff --git a/content/blog/anti-scraper-techniques.md b/content/blog/anti-scraper-techniques.md index 47aeb0a..df96b49 100644 --- a/content/blog/anti-scraper-techniques.md +++ b/content/blog/anti-scraper-techniques.md @@ -2,7 +2,12 @@ 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 --- diff --git a/content/blog/blog-question-challenge-jan2025.md b/content/blog/blog-question-challenge-jan2025.md index b52e4ca..41c0610 100644 --- a/content/blog/blog-question-challenge-jan2025.md +++ b/content/blog/blog-question-challenge-jan2025.md @@ -2,7 +2,8 @@ title: "Blog Question Challenge (Jan 2025)" date: 2025-01-29T21:18:03-05:00 draft: false -tags: [] +tags: + - blogging 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 19a1934..beb3199 100644 --- a/content/blog/cursed-knowledge-javascript-arrays-are-objects.md +++ b/content/blog/cursed-knowledge-javascript-arrays-are-objects.md @@ -2,7 +2,8 @@ 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 --- diff --git a/content/blog/deterministic-set-iteration-dafny.md b/content/blog/deterministic-set-iteration-dafny.md index 93b5d44..43f818a 100644 --- a/content/blog/deterministic-set-iteration-dafny.md +++ b/content/blog/deterministic-set-iteration-dafny.md @@ -2,7 +2,11 @@ title: "Deterministically Iterating over a set within Dafny functions" date: 2025-07-06T12:27:01-04:00 draft: false -tags: ["Formal Methods"] +tags: + - Dafny + - Formal methods + - Deterministic algorithm + - Total order math: false medium_enabled: false --- diff --git a/content/blog/exploring-via-public-transit.md b/content/blog/exploring-via-public-transit.md index 19630d2..6db0a58 100644 --- a/content/blog/exploring-via-public-transit.md +++ b/content/blog/exploring-via-public-transit.md @@ -2,7 +2,8 @@ title: "Exploring via Public Transit" date: 2025-06-15T21:38:02-04:00 draft: false -tags: [] +tags: + - public transport 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 8bda61f..afcad1c 100644 --- a/content/blog/filesystem-as-persistent-kvs-python.md +++ b/content/blog/filesystem-as-persistent-kvs-python.md @@ -2,7 +2,10 @@ 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 --- diff --git a/content/blog/flattening-cases-avoid-nesting-lean-4.md b/content/blog/flattening-cases-avoid-nesting-lean-4.md index 3884611..90f8ef5 100644 --- a/content/blog/flattening-cases-avoid-nesting-lean-4.md +++ b/content/blog/flattening-cases-avoid-nesting-lean-4.md @@ -2,7 +2,10 @@ 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 --- diff --git a/content/blog/ollama-cuda-podman-quadlets.md b/content/blog/ollama-cuda-podman-quadlets.md index cce15c7..742eb47 100644 --- a/content/blog/ollama-cuda-podman-quadlets.md +++ b/content/blog/ollama-cuda-podman-quadlets.md @@ -2,7 +2,10 @@ 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 --- diff --git a/content/blog/program-safety-type-theory.md b/content/blog/program-safety-type-theory.md index 2655c1b..5be16e8 100644 --- a/content/blog/program-safety-type-theory.md +++ b/content/blog/program-safety-type-theory.md @@ -2,7 +2,9 @@ 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 --- 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 e9e4107..a282925 100644 --- a/content/blog/quick-lean-if-then-else-in-hypothesis.md +++ b/content/blog/quick-lean-if-then-else-in-hypothesis.md @@ -2,7 +2,9 @@ title: "Quick Lean: if-then-else statement in hypothesis" date: 2025-04-26T10:58:42-04:00 draft: false -tags: ["Formal Methods"] +tags: + - Lean + - Proof assistant math: false medium_enabled: false --- diff --git a/content/blog/recently-2504-april-showers.md b/content/blog/recently-2504-april-showers.md index 50ff039..1b91bee 100644 --- a/content/blog/recently-2504-april-showers.md +++ b/content/blog/recently-2504-april-showers.md @@ -2,7 +2,8 @@ title: "Recently: April Showers Bring..." date: 2025-04-12T10:38:45-04:00 draft: false -tags: [] +tags: + - homelab math: false medium_enabled: false --- diff --git a/content/blog/verifying-proofs-type-checkers.md b/content/blog/verifying-proofs-type-checkers.md index ef01423..fa05174 100644 --- a/content/blog/verifying-proofs-type-checkers.md +++ b/content/blog/verifying-proofs-type-checkers.md @@ -2,7 +2,14 @@ title: "Verifying Proofs with Type Checkers" date: 2025-05-27T09:27:59-04:00 draft: false -tags: ["Formal Methods"] +tags: + - Formal methods + - proof assistant + - Curry-Howard correspondence + - lambda cube + - calculus of constructions + - dependent type + - type theory math: true medium_enabled: false --- diff --git a/content/blog/weather-forcecasts-cli-nws.md b/content/blog/weather-forcecasts-cli-nws.md index 11efecc..7925e89 100644 --- a/content/blog/weather-forcecasts-cli-nws.md +++ b/content/blog/weather-forcecasts-cli-nws.md @@ -2,7 +2,11 @@ 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 --- diff --git a/themes/pulp b/themes/pulp index fd4db04..56de4ba 160000 --- a/themes/pulp +++ b/themes/pulp @@ -1 +1 @@ -Subproject commit fd4db04d3a6676f0db6dad6d65705b96cdf4b52a +Subproject commit 56de4bacdb0e56462b6643bb831c61afc85a61e3 From af8795dcc55cfdaf5656ab3a6af12003882bccf4 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Sun, 30 Nov 2025 14:38:15 -0500 Subject: [PATCH 2/2] Added tags->entities data --- data/wikidata_mappings.json | 344 ++++++++++++++++++++++++++++++++++++ themes/pulp | 2 +- 2 files changed, 345 insertions(+), 1 deletion(-) create mode 100644 data/wikidata_mappings.json diff --git a/data/wikidata_mappings.json b/data/wikidata_mappings.json new file mode 100644 index 0000000..d2e9211 --- /dev/null +++ b/data/wikidata_mappings.json @@ -0,0 +1,344 @@ +{ + "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 56de4ba..ded609d 160000 --- a/themes/pulp +++ b/themes/pulp @@ -1 +1 @@ -Subproject commit 56de4bacdb0e56462b6643bb831c61afc85a61e3 +Subproject commit ded609da7dfd3eec8f1002560bfb00bc66db2c0b