mirror of
https://github.com/Smaug123/static-site-pipeline
synced 2025-10-05 16:28:41 +00:00
Compare commits
49 Commits
bootstrap
...
cd3e6426a1
Author | SHA1 | Date | |
---|---|---|---|
|
cd3e6426a1 | ||
|
23ba49ce71 | ||
|
023d31419a | ||
|
1ac4d77cc9 | ||
|
3d0b74d125 | ||
|
12db6adbb5 | ||
|
5523bb7957 | ||
|
975a37a108 | ||
|
bff167f362 | ||
|
22b80e1fc3 | ||
|
8256606ca0 | ||
|
45f1d56d53 | ||
|
8aac808eac | ||
|
98efc23981 | ||
|
c9d197ebb5 | ||
|
f6e28b0b30 | ||
|
4caf4ee1e6 | ||
|
2ce132a914 | ||
|
8a73e10de3 | ||
|
56669036f0 | ||
|
1cd47be72c | ||
|
aba1f13646 | ||
|
eb2780622d | ||
|
4205c95fa0 | ||
|
151b69aeab | ||
|
d4f0837fb9 | ||
|
ac6e52f16d | ||
|
a19aa1c2e3 | ||
|
97ed4d00f3 | ||
|
2fd36b7437 | ||
|
06c71b0da2 | ||
|
95e110408b | ||
|
b76d192516 | ||
|
fa05c57c35 | ||
|
570afed012 | ||
|
a99747fe39 | ||
|
860640283f | ||
|
fc9bcfb85a | ||
|
2517e03143 | ||
|
ce38f6ba39 | ||
|
a680d7badf | ||
|
18314d94f6 | ||
|
da3a4d2e53 | ||
|
11853da860 | ||
|
8b2bab9baa | ||
|
c211ad7df3 | ||
|
fe90bc0405 | ||
|
b35c219d0e | ||
|
5076d02c81 |
1
.gitignore
vendored
1
.gitignore
vendored
@@ -29,3 +29,4 @@ hugo/static/misc/TokyoEntrance2016/
|
||||
|
||||
.idea/
|
||||
.profile*
|
||||
.direnv/
|
||||
|
78
flake.lock
generated
78
flake.lock
generated
@@ -79,6 +79,24 @@
|
||||
"inputs": {
|
||||
"systems": "systems_2"
|
||||
},
|
||||
"locked": {
|
||||
"lastModified": 1710146030,
|
||||
"narHash": "sha256-SZ5L6eA7HJ/nmkzGG7/ISclqe6oZdOZTNoesiInkXPQ=",
|
||||
"owner": "numtide",
|
||||
"repo": "flake-utils",
|
||||
"rev": "b1d9ab70662946ef0850d488da1c9019f3a9752a",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"owner": "numtide",
|
||||
"repo": "flake-utils",
|
||||
"type": "github"
|
||||
}
|
||||
},
|
||||
"flake-utils_3": {
|
||||
"inputs": {
|
||||
"systems": "systems_3"
|
||||
},
|
||||
"locked": {
|
||||
"lastModified": 1694529238,
|
||||
"narHash": "sha256-zsNZZGTGnMOf9YpHKJqMSsa0dXbfmxeoJ7xHlrt+xmY=",
|
||||
@@ -104,11 +122,11 @@
|
||||
"scripts": "scripts_2"
|
||||
},
|
||||
"locked": {
|
||||
"lastModified": 1696175612,
|
||||
"narHash": "sha256-8V8klzc7T3EdAdS4r8RRjNvTTytQOsvfi7DfK6NFK6M=",
|
||||
"lastModified": 1721842442,
|
||||
"narHash": "sha256-bjvLR/KwHToz0/kRcZ8/MHXs3y4YCTtz3UUQ/D/AliA=",
|
||||
"ref": "refs/heads/main",
|
||||
"rev": "ac0b0180304bce7683dc8b4466a6e92b339c0b7e",
|
||||
"revCount": 15,
|
||||
"rev": "cab3ccc58ec12af893c9ea6b87aac0dfeefa3752",
|
||||
"revCount": 24,
|
||||
"type": "git",
|
||||
"url": "file:/Users/patrick/Desktop/website/static-site-images"
|
||||
},
|
||||
@@ -119,19 +137,15 @@
|
||||
},
|
||||
"katex": {
|
||||
"inputs": {
|
||||
"flake-utils": [
|
||||
"flake-utils"
|
||||
],
|
||||
"nixpkgs": [
|
||||
"nixpkgs"
|
||||
]
|
||||
"flake-utils": "flake-utils_3",
|
||||
"nixpkgs": "nixpkgs_2"
|
||||
},
|
||||
"locked": {
|
||||
"lastModified": 1696151934,
|
||||
"narHash": "sha256-8kihcqdgYjoVuGozfgfcWh81yqMUvns4+C/fgkn+RNQ=",
|
||||
"lastModified": 1704150937,
|
||||
"narHash": "sha256-G6uJKkY5VErgobe51IIbp/ugHDIhVx5e0xNjJ90JEOk=",
|
||||
"owner": "Smaug123",
|
||||
"repo": "KaTeX",
|
||||
"rev": "ac1f9b30441f63ea20216a36ffa7148dc0e9a9b3",
|
||||
"rev": "b74ed701beec2bebd161a0b5ea30c496c5206b96",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
@@ -172,6 +186,21 @@
|
||||
"type": "github"
|
||||
}
|
||||
},
|
||||
"nixpkgs_3": {
|
||||
"locked": {
|
||||
"lastModified": 1725713604,
|
||||
"narHash": "sha256-hkFQdL1jDji7JGas0AZosDI+QPPIl0T1Be05yXOFjwA=",
|
||||
"owner": "NixOS",
|
||||
"repo": "nixpkgs",
|
||||
"rev": "b8f54737435ff536bb3bff595bbe22614c112d65",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"owner": "NixOS",
|
||||
"repo": "nixpkgs",
|
||||
"type": "github"
|
||||
}
|
||||
},
|
||||
"pdfs": {
|
||||
"inputs": {
|
||||
"flake-utils": [
|
||||
@@ -183,11 +212,11 @@
|
||||
"scripts": "scripts_3"
|
||||
},
|
||||
"locked": {
|
||||
"lastModified": 1696190787,
|
||||
"narHash": "sha256-bO/NInpwVefs5Iey8WVwPFnXPt/3WN7WvYXTxzLKmGQ=",
|
||||
"lastModified": 1725713640,
|
||||
"narHash": "sha256-JBTpmQn3Gg3scVUUyLuks1gX+EzkctD+ZN3CBsxXuwQ=",
|
||||
"owner": "Smaug123",
|
||||
"repo": "static-site-pdfs",
|
||||
"rev": "a36d3025b9625cc50fc5bd2eca867eacd8a5bcb9",
|
||||
"rev": "e7133d72e6fab800aa3fd91cab47b6bc6824a0ca",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
@@ -203,7 +232,7 @@
|
||||
"flake-utils": "flake-utils_2",
|
||||
"images": "images",
|
||||
"katex": "katex",
|
||||
"nixpkgs": "nixpkgs_2",
|
||||
"nixpkgs": "nixpkgs_3",
|
||||
"pdfs": "pdfs",
|
||||
"scripts": "scripts_4"
|
||||
}
|
||||
@@ -297,6 +326,21 @@
|
||||
"repo": "default",
|
||||
"type": "github"
|
||||
}
|
||||
},
|
||||
"systems_3": {
|
||||
"locked": {
|
||||
"lastModified": 1681028828,
|
||||
"narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
|
||||
"owner": "nix-systems",
|
||||
"repo": "default",
|
||||
"rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"owner": "nix-systems",
|
||||
"repo": "default",
|
||||
"type": "github"
|
||||
}
|
||||
}
|
||||
},
|
||||
"root": "root",
|
||||
|
@@ -2,17 +2,16 @@
|
||||
description = "Static site builder for patrickstevens.co.uk";
|
||||
|
||||
inputs = {
|
||||
flake-utils.url = github:numtide/flake-utils;
|
||||
flake-utils.url = "github:numtide/flake-utils";
|
||||
scripts.url = "github:Smaug123/flake-shell-script";
|
||||
nixpkgs.url = "github:NixOS/nixpkgs/nixos-22.11";
|
||||
nixpkgs.url = "github:NixOS/nixpkgs";
|
||||
extra-content = {
|
||||
url = "path:/Users/patrick/Desktop/website/extra-site-content";
|
||||
flake = false;
|
||||
};
|
||||
katex = {
|
||||
url = "github:Smaug123/KaTeX/nix";
|
||||
inputs.nixpkgs.follows = "nixpkgs";
|
||||
inputs.flake-utils.follows = "flake-utils";
|
||||
# inputs.nixpkgs.follows = "nixpkgs";
|
||||
};
|
||||
images = {
|
||||
url = "git+file:/Users/patrick/Desktop/website/static-site-images";
|
||||
@@ -85,7 +84,7 @@
|
||||
mv output $out
|
||||
'';
|
||||
};
|
||||
in rec {
|
||||
in {
|
||||
packages = flake-utils.lib.flattenTree {
|
||||
gitAndTools = pkgs.gitAndTools;
|
||||
default = website;
|
||||
|
@@ -80,6 +80,10 @@ pygmentsCodefences = true
|
||||
name = "Film List"
|
||||
identifier = "films"
|
||||
url = "/films"
|
||||
[[menu.main]]
|
||||
name = "Games"
|
||||
identifier = "games"
|
||||
url = "/games"
|
||||
[[menu.main]]
|
||||
name = "Lifehacks"
|
||||
identifier = "lifehacks"
|
||||
|
@@ -6,6 +6,11 @@ layout: page
|
||||
sidenotes: true
|
||||
---
|
||||
I am Patrick Stevens, a software engineer based in London, England.
|
||||
|
||||
{{< rawhtml >}}
|
||||
<img src="/images/AboutMe/northern-lights.png" alt="Photo of me under the Northern Lights" style="max-width: 500px;">
|
||||
{{< /rawhtml >}}
|
||||
|
||||
I completed my BA+MMath at the University of Cambridge.
|
||||
|
||||
Social media accounts:
|
||||
|
@@ -7,6 +7,10 @@ layout: page
|
||||
|
||||
This page holds a list of films I have watched, spoiler-free, starting from 9th January 2015.
|
||||
|
||||
* [The Grand Budapest Hotel](https://www.imdb.com/title/tt2278388/): This is one of my favourite films. In general I find Wes Anderson a bit hit-or-miss, but this film is sublime. Excellent characterisation, quick deadpan wit. Ralph Fiennes is just glorious here.
|
||||
|
||||
* [Argylle](https://www.imdb.com/title/tt15009428/): Sadly disappointing. This film was at least twice as long as it should have been. A good version would have been a short funny pastiche; what we actually got was a long boring film punctuated by moments of glorious whimsy.
|
||||
|
||||
* [A Haunting in Venice](https://www.imdb.com/title/tt22687790/): Well, I really enjoyed this, and I think I was surrounded by heathens in the cinema. I successfully called precisely none of the plot, and it all tied up so neatly. Ariadne Oliver will always be Zoë Wanamaker to me, but I believed Kenneth Branagh. Top-tier Poirot.
|
||||
|
||||
* [Oppenheimer](https://en.wikipedia.org/wiki/Oppenheimer_(film)): Brilliant. It was a little too long, but I couldn't pick out anything to take away. Great acting, great filming, a bit harrowing.
|
||||
|
58
hugo/content/games/index.md
Normal file
58
hugo/content/games/index.md
Normal file
@@ -0,0 +1,58 @@
|
||||
---
|
||||
lastmod: "2024-04-28T20:51:00.0000000+01:00"
|
||||
title: Games
|
||||
author: patrick
|
||||
layout: page
|
||||
---
|
||||
|
||||
This page holds an incomplete list of games I have played.
|
||||
|
||||
# Video games
|
||||
|
||||
## In progress
|
||||
|
||||
* Chants of Sennaar. An extremely impressive 81% of players have the Steam achievement for leaving the first game area, which I think tells you how gripping this game is. It's basically a particular kind of IQ test, but it's really fun. Reminiscent of _Return of the Obra Dinn_.
|
||||
|
||||
## Not in progress
|
||||
|
||||
* Baldur's Gate 3 (hundreds of hours). Glorious game, aesthetically beautiful, absolutely gigantic amount of content, and sometimes succeeds at making you empathise with the characters. Having played this, I wouldn't really want to go back to playing a DnD-style RPG any other way: all the bookkeeping happens in the background.
|
||||
* Factorio, and Dyson Sphere Program (both hundreds of hours). Grouped together because they are basically the same game. I have banned myself from playing this genre of game (I gave myself RSI from it for a while). Between the two, DSP is much prettier and somewhat more forgiving, but also it has the annoying mechanic of laying your factory out on spheres. "Cannot place blueprint across tropic lines" just feels bad; you really want your factory layout not to depend on where it is situated.
|
||||
* Outer Wilds (about half an hour). Everyone raves about this game, but it makes me travel-sick very fast. No further comment.
|
||||
* Human Resource Corporation, and 7 Billion Humans (25 hours total). As I've got older, games which are purely programming have become less appealing (that is, after all, my day job). These ones are visually pretty, but I have no idea how they'll play for someone who is not a programmer.
|
||||
* Among Us (70 hours). I love this game (multiplayer social deduction), and am quite sad that everyone stopped playing it after the pandemic. Your first few games will be extremely hard if you're an impostor, because your plausibility relies on being able to make up what you were doing where (which means you need to know the maps), but once you've got over that it's just really fun.
|
||||
* Antichamber (2 hours). This makes me motion-sick really quickly, and I have only played it in ten-minute bursts. I imagine this would be very interesting if I could play it.
|
||||
* Baba Is You (68 hours). Cute puzzle game, with some extremely difficult puzzles. Mind-blowingly beautiful mechanics as you get towards the end. Tier 1. I played this with my housemates on a big screen and it was a great way to play!
|
||||
* Braid (9 hours). Lovely puzzle game, innovative, coherent; a classic Jonathan Blow game. See [qntm's write-up](https://qntm.org/braid).
|
||||
* Classic Sudoku (135 hours) and Killer Sudoku (107 hours), by the Cracking the Cryptic team. A bunch of these puzzles are just really neat! A few are slogs, but many of them are cute, and I got the impression at the time that it might be quite a good introduction to advanced Sudoku techniques. The over-100-hours is because I have done each puzzle twice.
|
||||
* Death and Taxes (2 hours). Meh. Three years after playing it I can't really remember it at all.
|
||||
* Disco Elysium (17 hours). Some of this game is pretty funny. I haven't completed it, because it was getting to be a bit of a slog.
|
||||
* Dota 2 (thousands of hours). Deeply addictive. You will spend the first thousand hours or so *completely sucking* at this game, and improvement comes from recognising that you suck (thanks Purge for the framing on this). I stopped playing this game many years ago when I discovered that I didn't actually enjoy it. My mechanical skill was pretty mediocre, so my specialist skill, inasmuch as I had one, was to bind together a team and keep morale up. A team of five coherent players will beat a team of five individuals any day of the week, and a team of five players will beat a team of four players plus a griefer, so an extremely valuable role is "keep your team feeling like a unit". But it grinds away at the soul, and eventually I realised it isn't fun.
|
||||
* Elsinore (7 hours). Intriguing and cute puzzle game: you're playing Ophelia, caught in a time loop for several critical days in the setting of Hamlet. You gradually learn what happens when, and how you can act to change what happens. I haven't finished this because it had a bit too much of the [Shlemiel the Painter](https://www.joelonsoftware.com/2001/12/11/back-to-basics/) about it: as you solve milestones, you keep revealing more, but have to keep retracing the same steps anyway.
|
||||
* The Zachtronics games (Exapunks, TIS-100, Shenzhen I/O, Opus Magnum, MOLEK-SYNTEZ; excluding Infinifactory; a couple of hours). Again, like Human Resource Corporation, these games are purely programming, and I'm getting too old for that sort of thing to be a fun way to relax.
|
||||
* The House of da Vinci (and 2 and 3; 20 hours). These are all a bit too point-and-click linear for my liking.
|
||||
* Inscryption (15 hours). Interesting card game mechanic; intriguing metagame.
|
||||
* Islands of Insight (55 hours). Loads and *loads* of small puzzles, many of them Nikoli-like. Some are just quite annoying ("go to this place and hunt around"). Some are deeply absorbing. Very pretty aesthetics.
|
||||
* The Witness (55 hours). Good lord is this game amazing. It's a superstimulus for the sense of discovering an insight. The game mechanics are all taught entirely without words, which is a brilliant trick if you can manage it.
|
||||
* The Looker (2 hours). Parody of The Witness. Some of it laugh-out-loud funny.
|
||||
* Loop Hero (25 hours, not all of which was me). Very playable roguelike.
|
||||
* Obduction (7 hours). I distinctly remember that when I was much younger I enjoyed Myst and friends. This was back in the days when I had the patience to read _The Lord of the Rings_, for example. Nowadays I suspect I just don't have the attention span and/or patience. Obduction in particular requires a *lot* of walking around.
|
||||
* Offworld Trading Company (30 hours). I am *terrible* at this game, and find it deeply stressful, but it's extremely compelling. The market mechanic is either very innovative or very innovatively phrased.
|
||||
* Oxygen Not Included (8 hours). I feel like I'm missing some fundamental part of this game. It feels like it should be some massive Factorio-like infinite world automation thing, but in practice I ended up doing an awful lot of micromanagement. Probably a skill issue.
|
||||
* Patrick's Parabox (10 hours). Cute puzzle game. Mind-bending, innovative. Really good.
|
||||
* Portal (and 2, and the Reloaded mod; 35 hours in total). Classics, of course.
|
||||
* Return of the Obra Dinn (12 hours). Aesthetically beautiful game. When the main mechanic was introduced, I sat back in awe. You gradually get to have quite a good mental map of what's going on here. Highly recommended.
|
||||
* Slay the Spire (hundreds of hours). Deep gameplay (_extremely_ deep - check out Jorbs's streams!). One of those games where it takes a while to realise just how bad at it you are; all your losses feel like luck, but actually this game is at least 80% skill.
|
||||
* Roguebook (23 hours). A variant of Slay the Spire. Aesthetically quite pleasing, but I didn't find it as gripping as StS.
|
||||
* Subnautica (26 hours). Personally I am a wimp and found quite a bit of this game primally terrifying; so much so that I ended up watching a stream of the game past a certain point. I don't much like the choice to phrase the story in terms of time pressure, when everything is actually triggered by reaching certain milestones. It's pretty, though, and if I weren't a wuss I'd definitely have played it to the end.
|
||||
* SUPERHOT (3 hours). This is the first-person shooter for the person like me who is terrible at first-person shooters! It's more like a puzzle game than a shooter, but for the first time it made me feel like I had a game in the shooter genre that I could play!
|
||||
* Taiji (12 hours). This is a puzzle game much like The Witness but a bit worse (but still a great game!).
|
||||
* The Talos Principle (and 2; 35 hours total). Puzzle games with a skin of basic philosophy. Aesthetically beautiful; some very hard puzzles.
|
||||
* Torment: Tides of Numenera (40 hours, because I've played it twice). If you're going to play an RPG, play Baldur's Gate 3 instead. Torment is much less pretty and considerably smaller, but I did have fun playing it.
|
||||
* Understand (3 hours). Tiny puzzle game. Almost precisely an IQ test. Great fun.
|
||||
* We Were Here (and Too, and Together; a few hours total). Two-player co-op games. The in-game chat is really janky, so we just used Discord. I feel like these were nearly great games, but something just felt missing. A Baldur's Gate 3 campaign completely supplanted this.
|
||||
|
||||
# Board games
|
||||
|
||||
(This section is basically a placeholder for now.)
|
||||
|
||||
* Agricola, one of my favourite games.
|
@@ -7,6 +7,7 @@ comments: true
|
||||
date: "2018-02-03T00:00:00Z"
|
||||
title: Infinitesimals as an idea that took a long time
|
||||
summary: Answering the question, "Which mathematical ideas took a long time to define rigorously?".
|
||||
math: true
|
||||
---
|
||||
|
||||
*This is my answer to the same [question posed on the Mathematics Stack Exchange](https://math.stackexchange.com/q/2633847/259262). It is therefore licenced under [CC-BY-SA 3.0](https://creativecommons.org/licenses/by-sa/3.0/).*
|
||||
|
@@ -8,6 +8,7 @@ comments: true
|
||||
date: "2021-03-17T00:00:00Z"
|
||||
title: Rewriting the Technical Interview, in Mathematica
|
||||
summary: "An exploration into reaching into the internals of Mathematica to natively evaluate C code."
|
||||
math: true
|
||||
---
|
||||
|
||||
*Cross-posted at the [G-Research official blog](https://www.gresearch.co.uk/article/rewriting-the-technical-interview-in-mathematica/).*
|
||||
|
53
hugo/content/posts/2023-10-18-squash-stacked-prs.md
Normal file
53
hugo/content/posts/2023-10-18-squash-stacked-prs.md
Normal file
@@ -0,0 +1,53 @@
|
||||
---
|
||||
lastmod: "2023-10-18T20:36:00.0000000+01:00"
|
||||
author: patrick
|
||||
categories:
|
||||
- programming
|
||||
date: "2023-10-18T20:36:00.0000000+01:00"
|
||||
title: Squashed stacked PRs workflow
|
||||
summary: "How to handle stacked pull requests in a repository which requires squashing all history on merge."
|
||||
---
|
||||
|
||||
Recall that the "stacked PRs" Git workflow deals with a set of changes (say `C` depends on `B`, which itself depends on `A`), each dependent on the last, and all going into some base branch which I'll call `main` for the sake of this note.
|
||||
The workflow represents this set of changes as a collection of pull requests: `A` into `main`, `B` into `A`, and `C` into `B`.
|
||||
|
||||
# Problem statement
|
||||
|
||||
The stacked PRs workflow is fine as long as we *merge* each pull request into its target, because then Git's standard merge algorithms are "sufficiently associative" that the sequence of merges tends to do the right thing.
|
||||
(Of course, Git's standard merge algorithms are not associative; see [the Pijul manual](https://pijul.org/manual/why_pijul.html) for concrete examples and discussion of why this is inherently true.)
|
||||
|
||||
But if we *squash* each pull request into its target, then the only way we can merge the entire stack is to merge `C` into `B`, then `B+C` into `A`, then `A+B+C` into `main`.
|
||||
Any other order, and the rewrite of history in the squash causes the computed merge base of our source and target to be very different from what we actually know it is, and this almost always causes the merge to become wildly conflicted.
|
||||
|
||||
For example, if we squash-merge `A` into `main` (which for the sake of argument should be a fast-forward merge, except that we've squashed), then we construct a new commit `squash(A)` whose tree is the same as `A` and which has the parent `main`; then we set `main` to point to `squash(A)`.
|
||||
The merge base of `B` with `squash(A)` would be simply `A` if we hadn't squashed, but `A` is no longer in the history of `squash(A)`, so the merge base is actually `main^` (i.e. `main` as it was before the squash-merge); and the merge of `squash(A)` and `B` with a base of `main^` is liable to be gruesome.
|
||||
So we can't cleanly merge `B` into `main = squash(A)`.
|
||||
|
||||
The clean problem statement, then, is:
|
||||
|
||||
> How do I squash-merge the stack in the order `A -> main`, `B -> main + A`, `C -> main + A + B`, without having to resolve conflicts at each step?
|
||||
|
||||
# Solution
|
||||
|
||||
Since we're squashing into `main` anyway, we should feel free to make a complete mess of history on our branches.
|
||||
|
||||
* Squash-merge `A` into `main`.
|
||||
* Merge into `B` the `A` commit that's immediately before the squash into `main`. (This should be clean unless you made changes to `A` which genuinely conflicted with `B`, so this is work you should really have done in preparation for the review of `B` anyway.)
|
||||
* Fetch `origin/main` locally, and merge into `B` the `main` commit that's immediately before the squash of `A`. (This should be clean if you've been hygienically keeping your branches up to date with `main` by merging `main -> A`, `A -> B`, `B -> C`. If it's not clean, again this is work that you would have to do anyway even in a non-squashing world.)
|
||||
|
||||
Now `B` is up to date both with `main` and `A` as of immediately before `A` was squashed into `main`, so it should be the case that merging `main + A` into `B` would be a no-op: it should not change the tree of `B`.
|
||||
However, we aren't merging `main + A`.
|
||||
We're instead merging the squashed `main + squash(A)` for some single commit `squash(A)` which Git thinks is completely unrelated to `A`, but which in fact has the same *tree* as `A`.
|
||||
|
||||
So the last step is:
|
||||
|
||||
* Merge the squashed `main + squash(A)` commit into `B` with the `ours` strategy: `git merge $COMMIT_HASH --strategy=ours`. That is: since we know `B`'s got the right *tree*, but its history is woefully incompatible with `main + squash(A)`'s history, we just do a dummy no-op merge to make their histories compatible again.
|
||||
|
||||
(Then merge this back up the stack, by merging the new `B` into `C`.)
|
||||
|
||||
## The state after performing this procedure
|
||||
|
||||
* `A` has been squashed into `main`.
|
||||
* `B`'s tree is as if `A` were merged into `main` and then the resulting `main + A` were merged into `B`.
|
||||
* `B`'s history contains the squashed `main + squash(A)`, so subsequent merges of `main` into `B` or `B` into `main` will be clean.
|
||||
* `B`'s history looks a bit mad, but we shrug and move on.
|
43
hugo/content/posts/2023-12-31-ios-interface.md
Normal file
43
hugo/content/posts/2023-12-31-ios-interface.md
Normal file
@@ -0,0 +1,43 @@
|
||||
---
|
||||
lastmod: "2023-12-31T12:49:00.0000000+00:00"
|
||||
author: patrick
|
||||
categories:
|
||||
- uncategorized
|
||||
date: "2023-12-31T12:49:00.0000000+00:00"
|
||||
title: iOS interface
|
||||
summary: "A bunch of ways the iOS user interface is bad, and some undiscoverable features."
|
||||
---
|
||||
|
||||
As I think is generally agreed, the iOS user interface is really very bad.
|
||||
I use iOS because it has fewer fundamental bugs than Android does, but I *much* prefer Android if only it worked.
|
||||
Here are some of my gripes, and some features it's completely impossible to discover but which are necessary to know.
|
||||
The list is incomplete: it's just what came to the top of my head over about half an hour.
|
||||
|
||||
* Keyboard layout, dead space: As far as I can tell, there is genuinely dead space on the outside of the A and L keys on the QWERTY layout. There is simply no need to demand this much accuracy from the typist.
|
||||
* Keyboard layout, symbols: every keyboard is nerfed compared to the corresponding Android keyboard. The idiom appears to be to hide symbols behind the "symbols" key, rather than being able to hold any key to reveal more symbols. Microsoft SwiftKey on Android was brilliant: you could access symbols either by clicking the "symbols" key, or by knowing its "hold a key and swipe" shortcut. On iOS, the best you can do is swipe from the "symbols" key, which means your thumb is traversing a lot of the screen a lot more frequently.
|
||||
* Keyboard layout, general paucity: I literally had to Google how to type one of the characters in one of my passwords.
|
||||
* Keyboard layout, numbers: it appears to be standard to omit a number row from the keyboard. SwiftKey at least lets you turn this on, but I believe the OS secure keyboard (for password entry) does not have a number row; certainly I have several times been in an interface where I wanted to type numbers but had to go through a menu to do so.
|
||||
* Filling in forms. The "Done" button is always at the top of the screen, which is at the opposite end of the screen from where you are entering data into the form.
|
||||
* Filling in forms. The "Done" button appears as flat blue text, with nothing to suggest that it is a button. (This is part of a more general problem that it's generally very unclear what you can interact with.)
|
||||
* The Home screen is almost completely non-customisable. On Android, you can move icons around however you like, and in particular you can put empty space between icons.
|
||||
* Calendar. The Calendar app is *weirdly* hard to use. It's miles worse than stock Android's. Why is there no week view that shows you, like, the events happening this week? The best they have is a complete chronological listing of all events in your calendar, which loses any spatial intuition of when events are throughout their days.
|
||||
* Login. The "OK" button is on the other side of the screen from the numpad: you can comfortably type the numbers with one or both thumbs, but then must stretch or reposition entirely to reach the OK button. (This is a common theme in iOS.)
|
||||
* Settings search. iOS is *much* worse at finding things in its own Settings app than Android is.
|
||||
* Search discoverability: a common iOS design idiom appears to be to hide search in a secret "scroll up to view the search box" mode. This is, of course, ridiculous.
|
||||
* General device search. It's frequently the case that appending to the search term will cause matching results to *vanish* from the list.
|
||||
* Waking the phone. Latency between "tilt to wake" and the phone actually waking is such that I very frequently press the power button to turn on the phone, then a visible delay occurs, then the phone wakes because I had tilted it, and then the phone sleeps again because I pressed the power button seconds ago.
|
||||
* The Tips app lets you "practise key gestures" (perfect! every OS should have this!), but… only once at a time? For example, the "Select and edit text" practice (which is absolutely necessary, because of how bad text selection is on iOS) lets you "Try it", but if you pause for too long while you're doing it, it decides you've finished and displays a checkmark, and freezes the interface. If you want to do it again, you have to click "Practise again". Why?!
|
||||
* The "silence" toggle on the side of the phone has turned into an Action Button on the latest iPhones. Sure, give me customisable buttons, but before that I would strongly prefer a physical toggle like I had on my OnePlus 8 Pro. You can't feel what state your phone is in if that functionality is a button.
|
||||
* The phone status screen you get by swiping down-left from the top-right is *much* worse than Android's. A bunch of key functionality is hidden behind "press and hold in this area". In a very unusual move for Apple, they have removed almost all the text from this screen, which is the opposite problem from everywhere else in iOS (namely "everything is unstyled text and you can't know it's a button"): everything is clearly a button, but you can't know what it does.
|
||||
* I have to Google "how to turn off an iPhone". [So does Patrick McKenzie](https://twitter.com/patio11/status/1740623388446769661).
|
||||
|
||||
## Necessary features you can't find out about
|
||||
|
||||
* You can scroll to arbitrary places in a document. Reveal the scroll bar by scrolling a little, then hold the scroll bar until it blips at you; then you can drag it up and down. (You will need to practise this, because it's extremely finnicky. For example, it appears that once you've quick-scrolled this way once, you cannot do so again until you've slow-scrolled once more.) Why this isn't the default mode I cannot fathom.
|
||||
* The Calendar is just bad, as I noted above. You can at least see the chronological list of all events in the calendar by double-clicking the "Today" text in the bottom left corner of the screen. This is impossible to discover except by accident.
|
||||
* You can turn off the phone (without invoking Siri): hold the power button and any volume button simultaneously for a while until it blips at you and gives you an interface you can use. Mnemonic: you can't turn off the phone unless you SHOUT AT IT by turning up the volume while you do it.
|
||||
|
||||
## Necessary features you can find out about but which aren't the default
|
||||
|
||||
* By default the phone shows notification content on the locked home screen. This is a *really* odd default and is trivially seriously vulnerable to attack. Go Settings -> Notifications, and set "Show Previews" to "When Unlocked".
|
||||
* You can set a black home-screen background to reduce the home-screen clutter. Go Settings -> Wallpaper, hit "Customise", and then select a "Colour".
|
20
hugo/content/posts/2023-12-31-woofware-myriad-plugins.md
Normal file
20
hugo/content/posts/2023-12-31-woofware-myriad-plugins.md
Normal file
@@ -0,0 +1,20 @@
|
||||
---
|
||||
lastmod: "2023-12-31T13:42:00.0000000+00:00"
|
||||
author: patrick
|
||||
categories:
|
||||
- uncategorized
|
||||
date: "2023-12-31T13:42:00.0000000+00:00"
|
||||
title: Announcing WoofWare.Myriad.Plugins
|
||||
summary: "Some F# source generators to solve common problems I have."
|
||||
---
|
||||
|
||||
This is a linkpost for [WoofWare.Myriad.Plugins](https://github.com/Smaug123/WoofWare.Myriad), a set of [F#](https://en.wikipedia.org/wiki/F_Sharp_(programming_language)) source generators ([see it on NuGet](https://www.nuget.org/packages/WoofWare.Myriad.Plugins)).
|
||||
Go and read [the README on GitHub](https://github.com/Smaug123/WoofWare.Myriad/blob/main/README.md) if you're interested.
|
||||
As of this writing, the following are implemented:
|
||||
|
||||
* `[<JsonParse>]` (to stamp out `jsonParse : JsonNode -> 'T` methods)
|
||||
* `[<RemoveOptions>]` (to strip `option` modifiers from a type)
|
||||
* `[<HttpClient>]` (to stamp out a [RestEase](https://github.com/canton7/RestEase)-style HTTP client)
|
||||
* `[<GenerateMock>]` (to stamp out a record type corresponding to an interface, for easy record-update syntax when [mocking](https://en.wikipedia.org/wiki/Mock_object)).
|
||||
|
||||
They are particularly intended for `PublishAot` [ahead-of-time compilation](https://learn.microsoft.com/en-us/dotnet/core/deploying/native-aot/) contexts, in which reflection is heavily restricted, but also for anyone who doesn't want reflection for whatever reason (e.g. "to obtain the ability to step through code in a debugger", or "for more predictable speed").
|
29
hugo/content/posts/2024-01-19-starting-suspended-process.md
Normal file
29
hugo/content/posts/2024-01-19-starting-suspended-process.md
Normal file
@@ -0,0 +1,29 @@
|
||||
---
|
||||
lastmod: "2024-01-19T18:51:00.0000000+00:00"
|
||||
author: patrick
|
||||
categories:
|
||||
- programming
|
||||
date: "2024-01-19T18:51:00.0000000+00:00"
|
||||
title: Starting a suspended process
|
||||
summary: "How to start a process into a suspended state on Linux"
|
||||
---
|
||||
|
||||
(This is not fancy and is probably common knowledge, but I only learned how to do it today.)
|
||||
|
||||
Say you want to start a process, then log its PID, then allow it to run (so that if it starts logging to the console, you're guaranteed to have done all your logging before it starts polluting stdout).
|
||||
|
||||
This is easy on Windows: [`CreateProcess` accepts `CREATE_SUSPENDED`](https://learn.microsoft.com/en-us/windows/win32/procthread/process-creation-flags).
|
||||
But on Linux, it's not obvious.
|
||||
|
||||
1. The parent sets up a signal handler for SIGUSR1 (say), so that it can know when the child is ready.
|
||||
1. The parent forks, then waits for SIGUSR1.
|
||||
1. The child sets up a signal handler for SIGUSR2, so that it can know when the parent is ready.
|
||||
1. The child sends SIGUSR1 to its parent to signal readiness, then waits for SIGUSR2.
|
||||
1. The parent does whatever it wants to do with the now-running child process (whose PID it now knows).
|
||||
1. The parent sends SIGUSR2 to the child.
|
||||
1. The child `exec`s into the process that it actually wanted to start all along.
|
||||
1. The parent unregisters the SIGUSR1 handler.
|
||||
|
||||
Note that [forked processes have the same signal handlers](https://man7.org/linux/man-pages/man7/signal.7.html) as the parent, but those signal handlers are blatted by an `exec`.
|
||||
|
||||
(Good lord is this not investment advice. It's hard to express just how much of a novice I am at signal handling.)
|
65
hugo/content/posts/2024-03-01-no-confusion.md
Normal file
65
hugo/content/posts/2024-03-01-no-confusion.md
Normal file
@@ -0,0 +1,65 @@
|
||||
---
|
||||
lastmod: "2024-03-01T13:51:00.0000000+00:00"
|
||||
author: patrick
|
||||
categories:
|
||||
- programming
|
||||
date: "2024-03-01T13:51:00.0000000+00:00"
|
||||
title: Why does no-confusion use equality rather than a recursive call?
|
||||
summary: "A question about the definition of a no-confusion type."
|
||||
---
|
||||
|
||||
## Question
|
||||
|
||||
Conor McBride defined the no-confusion property of `Nat` on page 11 of [A Polynomial Testing Principle](https://personal.cis.strath.ac.uk/conor.mcbride/PolyTest.pdf) as:
|
||||
|
||||
```agda
|
||||
NoConf : Nat → Nat → Set
|
||||
NoConf ze ze = 1
|
||||
NoConf ze (su y) = 0
|
||||
NoConf (su x ) ze = 0
|
||||
NoConf (su x ) (su y) = x ≡ y
|
||||
```
|
||||
|
||||
Why was this defined that way, rather than the following way which works without dependencies?
|
||||
|
||||
```agda
|
||||
NoConf : Nat → Nat → Set
|
||||
NoConf ze ze = 1
|
||||
NoConf ze (su y) = 0
|
||||
NoConf (su x) ze = 0
|
||||
NoConf (su x) (su y) = NoConf x y
|
||||
```
|
||||
|
||||
## Context
|
||||
|
||||
I still had this question quite near the end of my working through A Polynomial Testing Principle, and it didn't seem to have been answered: I managed to get through most of the paper without serious problems arising from my different definition.
|
||||
|
||||
## Answer
|
||||
|
||||
Conor immediately follows the definition of `NoConf` by defining a canonical way to construct a `NoConf`:
|
||||
|
||||
```agda
|
||||
noConf : {x y : Nat} -> x ≡ y → NoConf x y
|
||||
noConf {zero} refl = record {}
|
||||
noConf {suc n} {.(suc n)} refl = refl
|
||||
```
|
||||
|
||||
If you do it my way instead, you end up unable to use this canonical construction to do proofs by no-confusion.
|
||||
You probably find yourself proving that `succ` is injective manually, and then using that directly instead of via the `NoConf`; which defeats the entire purpose of packaging up the no-confusion property into a type.
|
||||
|
||||
For example:
|
||||
|
||||
```agda
|
||||
+cancel : (a b : Nat) {c d : Nat} -> a ≡ b -> (a + c) ≡ (b + d) -> c ≡ d
|
||||
+cancel zero .zero refl sums_equal = sums_equal
|
||||
+cancel (succ a) (succ .a) refl sums_equal = +cancel a a refl {!!}
|
||||
```
|
||||
|
||||
What should go here?
|
||||
We need something of type `a + c ≡ a + d`, but all we have in scope is the input `succ (a + c) ≡ succ (a + d)`.
|
||||
That is, we need the no-confusion property for `succ`; which suggests that `NoConf` should somehow contain an equality type, so that we can use it!
|
||||
|
||||
## Commentary
|
||||
|
||||
I think I only had this question because `Nat` is such a simple type.
|
||||
If there were more constructors and more cases in each pattern-match, it would have been obvious straight away that I had deleted the entire point of the `NoConf` construction.
|
80
hugo/content/posts/2024-03-13-northern-lights-trip.md
Normal file
80
hugo/content/posts/2024-03-13-northern-lights-trip.md
Normal file
@@ -0,0 +1,80 @@
|
||||
---
|
||||
lastmod: "2024-03-13T12:18:00.0000000+00:00"
|
||||
author: patrick
|
||||
date: "2024-03-13T12:18:00.0000000+00:00"
|
||||
title: Trip to Tromsø
|
||||
summary: "Travelogue of my trip to Norway."
|
||||
gallery: true
|
||||
---
|
||||
|
||||
# Friday (2024-03-08)
|
||||
|
||||
* Wagamama's at Gatwick
|
||||
* Toblerone
|
||||
* Plane to Tromsø!
|
||||
* Landed 2340 local time
|
||||
* About an hour between landing and getting a taxi
|
||||
* First sight of tunnel system under Tromsø mountains
|
||||
{{< foldergallery src="images/galleries/Tromso2024/1-AirportOutbound" >}}
|
||||
|
||||
Northern Lights visible from plane; they turned off the cabin lights so we could see.
|
||||
{{< foldergallery src="images/galleries/Tromso2024/2-NorthernLightsFromPlane" summary="Northern Lights viewed from the plane" >}}
|
||||
|
||||
# Saturday (2024-03-09)
|
||||
|
||||
* Breakfast (great smoked salmon and pickled herring, scrambled eggs, mushrooms, beans, bread, butter, apple jam)
|
||||
* Ran into some lost tourists, resulting in a rainy walk over [bridge to east](https://en.wikipedia.org/wiki/Troms%C3%B8_Bridge)
|
||||
{{< foldergallery src="images/galleries/Tromso2024/3-TromsoWalk" >}}
|
||||
* [Arctic cathedral](https://www.ishavskatedralen.no/en/the-arctic-cathedral/)
|
||||
{{< foldergallery src="images/galleries/Tromso2024/4-Cathedral" >}}
|
||||
* [Cable car](https://www.fjellheisen.no/engelsk/fjellheisen-home) up mountain, vue panoramique
|
||||
{{< foldergallery src="images/galleries/Tromso2024/5-Viewpoint" >}}
|
||||
* Back to hotel, sauna
|
||||
* Cinnamon bun and golden milk at [Pust Kafé](https://www.kafe.pust.io/) (maximum bougie London energy)
|
||||
* [Polar museum](https://en.uit.no/tmu/polarmuseet)
|
||||
{{< foldergallery src="images/galleries/Tromso2024/6-PolarMuseum" >}}
|
||||
* Carrot cake and Lady Grey tea at hotel
|
||||
{{< foldergallery src="images/galleries/Tromso2024/7-Cake" >}}
|
||||
* Tea at hotel, sauna again and jacuzzi outside
|
||||
{{< foldergallery src="images/galleries/Tromso2024/8-Jacuzzi" >}}
|
||||
|
||||
# Sunday (2024-03-10)
|
||||
|
||||
{{< foldergallery src="images/galleries/Tromso2024/9-BreakfastSunday" summary="Breakfast photos" >}}
|
||||
|
||||
* [Snowshoe walk](https://www.wanderingowl.com/tour/tromso/winter-walk-on-the-wild-side-troms%C3%B8/P7YEHB/) at Kattfjordeidet
|
||||
|
||||
{{< foldergallery src="images/galleries/Tromso2024/10-Snowshoes" summary="My photos" >}}
|
||||
{{< foldergallery src="images/galleries/Tromso2024/11-SnowshoesOfficial" summary="Photos from our guide Evgeni" >}}
|
||||
|
||||
* [Aurora tour](https://auroratour.no/about-us/), ending up around [Skibotn](https://en.wikipedia.org/wiki/Skibotn); back around 0230 local time
|
||||
|
||||
{{< foldergallery src="images/galleries/Tromso2024/12-NorthernLights" summary="My photos" >}}
|
||||
{{< foldergallery src="images/galleries/Tromso2024/13-NorthernLightsOfficial" summary="Photos from our guide Marcin" >}}
|
||||
|
||||
# Monday (2024-03-11)
|
||||
|
||||
* [Husky sledding](https://tromsodogsledding.com/)
|
||||
{{< foldergallery src="images/galleries/Tromso2024/14-Huskies" >}}
|
||||
* Jacuzzi again
|
||||
{{< foldergallery src="images/galleries/Tromso2024/15-JacuzziAgain" >}}
|
||||
|
||||
# Tuesday (2024-03-12)
|
||||
|
||||
* [Glass blowing workshop](https://www.blaast.no/)
|
||||
{{< foldergallery src="images/galleries/Tromso2024/18-GlassBlower" >}}
|
||||
* More buns at Pust
|
||||
{{< foldergallery src="images/galleries/Tromso2024/17-Cake" >}}
|
||||
* [Aquarium](https://polaria.no/en/) (featuring seals!)
|
||||
{{< foldergallery src="images/galleries/Tromso2024/16-Aquarium" >}}
|
||||
|
||||
* Plane to Luton
|
||||
* Arrived home 0120 GMT
|
||||
|
||||
# Stats
|
||||
|
||||
* Nikoli-style puzzles solved: 48
|
||||
* Saunas: 7
|
||||
* Jacuzzis: 2
|
||||
* Cardamom buns: 2
|
||||
* Items of clothing lost: 1
|
41
hugo/content/posts/2024-03-14-yaml-superset-json.md
Normal file
41
hugo/content/posts/2024-03-14-yaml-superset-json.md
Normal file
@@ -0,0 +1,41 @@
|
||||
---
|
||||
lastmod: "2024-04-14T00:12:00.0000000+00:00"
|
||||
author: patrick
|
||||
date: "2024-03-14T00:12:00.0000000+00:00"
|
||||
title: YAML is not a superset of JSON
|
||||
summary: "All the reasons I know for why YAML is not a superset of JSON."
|
||||
categories:
|
||||
- programming
|
||||
---
|
||||
|
||||
I keep forgetting, so here we go.
|
||||
Please let me know if you have any others!
|
||||
|
||||
## Treatment of e.g. `1e2`
|
||||
|
||||
JSON treats the value `1e2` a number, of course, because it's not in quote marks.
|
||||
YAML fails to parse it as a number so silently falls back to treating it as a string.
|
||||
|
||||
```python
|
||||
>>> import yaml
|
||||
>>> import json
|
||||
|
||||
>>> yaml.safe_load('{"a": 1e2}')
|
||||
{'a': '1e2'}
|
||||
|
||||
>>> json.loads('{"a": 1e2}')
|
||||
{'a': 100.0}
|
||||
```
|
||||
|
||||
## Tabs as indentation
|
||||
|
||||
YAML does not permit tabs to be used as indentation.
|
||||
|
||||
```python
|
||||
>>> yaml.load ('{\n "list": [\n {},\n\t{}\n ]\n}')
|
||||
# yaml.scanner.ScannerError: while scanning for the next token
|
||||
# found character '\t' that cannot start any token
|
||||
|
||||
>>> json.loads('{\n "list": [\n {},\n\t{}\n ]\n}')
|
||||
{'list': [{}, {}]}
|
||||
```
|
51
hugo/content/posts/2024-03-27-chatgpt-and-programming.md
Normal file
51
hugo/content/posts/2024-03-27-chatgpt-and-programming.md
Normal file
@@ -0,0 +1,51 @@
|
||||
---
|
||||
lastmod: "2024-03-27T12:01:00.0000000+00:00"
|
||||
author: patrick
|
||||
date: "2024-03-27T12:01:00.0000000+00:00"
|
||||
title: ChatGPT's effect on my programming
|
||||
summary: "After a decent while programming with ChatGPT, I'm not sure it's even a net positive on my ability."
|
||||
categories:
|
||||
- programming
|
||||
---
|
||||
|
||||
For almost a year now, I've had access to ChatGPT 4.
|
||||
In that time, I've used it pretty extensively, I have some large custom instructions to try and get it to be precise and accurate, and so forth.
|
||||
After a particularly gruelling weekend [getting my Neovim environment up to scratch](https://github.com/Smaug123/nix-dotfiles/pull/38/files), in which I used ChatGPT for approximately 70 distinct chats (some of which were quite long), I decided to put down some thoughts.
|
||||
|
||||
# Where is ChatGPT good?
|
||||
|
||||
* Language-to-language translation. Bog-standard line-for-line translation of Vimscript to Lua went pretty much perfectly each time. However, ChatGPT never flagged places where I was doing things that were simply unnecessary or wrong, and a human who understood Neovim would have done. (For example, there are Vim options which make no sense in Neovim and are silently ignored.)
|
||||
* Fixing syntax, if you don't have a decent language server doing that for you. It's worse than a proper language server, but better than nothing.
|
||||
* Explaining what code is doing, if you don't want to dig too deep but just want a general gist.
|
||||
|
||||
# On using ChatGPT to write code for me
|
||||
|
||||
This is where ChatGPT is really pernicious.
|
||||
It's *so* tempting to use its output without putting in the work of building a mental model, but this *never* works.
|
||||
|
||||
I think on balance the presence of ChatGPT might actually have slowed down my Neovim migration, because it allowed me to get 80% of the way there without learning the domain at all.
|
||||
To get the final 20%, you need to understand the domain, but it takes a great deal of discipline to do so when ChatGPT is ready to give you implementations that almost work without any thought at all.
|
||||
I don't really have that discipline, and I think I would have been better off simply with a search engine.
|
||||
|
||||
(The [Neovim API docs](https://neovim.io/doc/user/api.html) are generally awful.
|
||||
They'd be adequate if they were documenting an API in a language with a decent type system, but Lua is untyped so the amount of documentation required is at least 3x bigger.
|
||||
The poor quality of the documentation adds extra friction if you want to learn what you're doing: it's more attractive to just not learn, if learning involves reading large amounts of an unfamiliar language in the guts of the implementation of a system you don't know.
|
||||
[Looking](https://github.com/dotnet/dotnet-api-docs/pull/9753) [at](https://github.com/dotnet/dotnet-api-docs/pull/9595) [you](https://github.com/dotnet/runtime/pull/95956) [too](https://github.com/dotnet/docs/pull/35171), [.NET](https://github.com/dotnet/dotnet-api-docs/pull/9394).)
|
||||
|
||||
I can imagine that ChatGPT 5 would be adequate for writing code for me, but right now I think the time it saves on starting you up (and getting you 80% of the way) is more than eaten up by the amount of learning/fixing/debugging that it makes you do in the future.
|
||||
There's a really high cost to not having a good mental model of what you're doing, and ChatGPT makes it far too easy to put yourself in that debt.
|
||||
|
||||
# What about Opus?
|
||||
|
||||
Claude 3 Opus [has had a lot of hype](https://thezvi.substack.com/p/on-claude-30) for its coding abilities, but over the past few days I've been running side-by-side comparisons with ChatGPT and there's simply no contest.
|
||||
ChatGPT gives better answers: they're more likely to be correct, and they're almost always more useful even when wrong.
|
||||
I have not yet got a single correct code snippet out of Opus.
|
||||
|
||||
# What I actually want from such a system
|
||||
|
||||
A really really good search engine, which has consumed all the relevant documentation.
|
||||
Claude 3 Opus's chat interface won't take more than 16% of the [home-manager documentation](https://nix-community.github.io/home-manager/options.xhtml), and the [POSIX spec](https://pubs.opengroup.org/onlinepubs/9699919799.2018edition/) is orders of magnitude too big.
|
||||
(Perhaps I need to suck it up and start using the Claude API.)
|
||||
|
||||
What I need is to ask "Where precisely in the spec should I look to discover the behaviour in this particular case?", "Under what configuration option does one configure this thing?", "Can you show me some code in the wild where someone is successfully using this?".
|
||||
|
148
hugo/content/posts/2024-04-13-yoneda.md
Normal file
148
hugo/content/posts/2024-04-13-yoneda.md
Normal file
@@ -0,0 +1,148 @@
|
||||
---
|
||||
lastmod: "2024-04-13T16:58:00.0000000+01:00"
|
||||
author: patrick
|
||||
date: "2024-04-13T16:58:00.0000000+01:00"
|
||||
title: The Yoneda lemma
|
||||
summary: "Another attempt to explain that the Yoneda lemma is actually intuitive."
|
||||
math: true
|
||||
---
|
||||
|
||||
*Read this post with a pencil and paper! Draw pictures!*
|
||||
|
||||
# What is a diagram?
|
||||
|
||||
A functor \\(\mathcal{C} \to \mathcal{D}\\) is basically a way of identifying a copy of \\(\mathcal{C}\\) inside \\(\mathcal{D}\\).
|
||||
That is, it's a specification of an object of \\(\mathcal{D}\\) for every object of \\(\mathcal{C}\\), and corresponding morphisms inside \\(\mathcal{D}\\) which must go between the right objects for this to be a copy of \\(\mathcal{C}\\).
|
||||
|
||||
If we specialise to the category of sets, a functor \\(\mathcal{C} \to \mathrm{\mathbf{Set}}\\) is a set for every object of \\(\mathcal{C}\\), and functions between those objects.
|
||||
|
||||
Imagine \\(\mathcal{C}\\) as some kind of abstract template of a universe of types; then a functor \\(\mathcal{C} \to \mathrm{\mathbf{Set}}\\) is an *instantation* of that universe of types.
|
||||
For example, perhaps we decide that this particular object of \\(\mathcal{C}\\) will be instantiated to \\(\mathbb{N}\\), and that particular object will be instantiated to \\(\mathrm{Bool}\\), and this arrow between them will be instantiated to \\(n \mapsto \mathrm{isEven}(n)\\).
|
||||
|
||||
Recall what the functor laws in this context are:
|
||||
|
||||
* The functor respects endpoints of morphisms: if \\(f: A \to B\\) in \\(\mathcal{C}\\), then \\(Ff : FA \to FB\\) in \\(\mathrm{\mathbf{Set}}\\). That is, we really are identifying a copy of \\(\mathcal{C}\\) in \\(\mathrm{\mathbf{Set}}\\): we're not actively breaking the structure in translation. If the template \\(\mathcal{C}\\) tells us how to get from \\(A\\) to \\(B\\), then we can do that in our instantiation.
|
||||
* The identity morphism is always taken to the identity function. (This one's fairly self-explanatory.)
|
||||
* The functor respects compositions: \\(F(g \circ f) = F(g) \circ F(f)\\). That is, if the template tells us we can do \\(f\\) then \\(g\\), we can also do that in our instantiation; moreover, if our template tells us two paths are equal, then they're also equal in the instantiation.
|
||||
|
||||
Note what we're *not* requiring of our instantiations: that they're somehow "fully preserving all the structure".
|
||||
If \\(\mathcal{C}\\) has two objects \\(A\\) and \\(B\\), we're perfectly happy to instantiate both of them to the same type, as long as all the arrows keep composing correctly.
|
||||
In particular, for example, our instantiation might squash away arbitrarily much of the category's structure: every category has a trivial instantiation to the universe where there's only one set \\(\emptyset\\), and only one arrow \\(\mathrm{id} : \emptyset \to \emptyset\\).
|
||||
|
||||
# Homomorphisms between diagrams
|
||||
|
||||
Thinking of a diagram as some kind of instantiation of an abstract template, we can define homomorphisms (that is, structure-preserving maps) between them.
|
||||
The concrete example of the "trivial instantiation" in the previous section may help you imagine how these homomorphisms should work.
|
||||
|
||||
If we have two diagrams \\(F, G : \mathcal{C} \to \mathrm{\mathbf{Set}}\\), we can define some particular homomorphism \\(\alpha\\) from the \\(F\\)-instantiation to the \\(G\\)-instantiation by sending every concrete \\(F\\)-type to a corresponding concrete \\(G\\)-type.
|
||||
In order to deserve the name "homomorphism", it had better preserve the structure: that is, if \\(x : FA \to FB\\) is a function in our concrete instantiation of \\(\mathcal{C}\\), then it had better be the case that our homomorphism \\(\alpha\\) takes \\(x\\) to a suitable corresponding function \\(GA \to GB\\) in the \\(G\\)-instantiation.
|
||||
|
||||
In fact, every function in the \\(F\\)-instantiation is an image of a morphism from \\(\mathcal{C}\\) (that is, we defined our instantiations so that we weren't considering any extraneous functions there might be between the sets), so instead of considering the set of all general \\(x : FA \to FB\\), we only need to consider the set of all \\(Ff : FA \to FB\\).
|
||||
Similarly, the functions \\(GA \to GB\\) are all of the form \\(Gg : GA \to GB\\) for some morphism \\(g\\) of \\(\mathcal{C}\\).
|
||||
|
||||
That is, a homomorphism from diagram \\(F\\) to diagram \\(G\\) is:
|
||||
|
||||
* an assignment, for each \\(A : |\mathcal{C}|\\), of some \\(GX\\) corresponding to \\(FA\\) (but note that in fact this \\(GX\\) must be \\(GA\\) to meet the later requirements, so there was no choice of target here);
|
||||
* an assignment, for each \\(\mathcal{C}\\)-morphism \\(f : A \to B\\), of some \\(Gg\\) corresponding to \\(Ff\\) (but note that this must be \\(Gf\\) to meet the later requirements, so similarly there's no choice of target here);
|
||||
* proofs that the homomorphism respects the basic structure of the category: if \\(f : A \to B\\) in \\(\mathcal{C}\\), then the map \\(Ff : FA \to FB\\) gets taken to the map \\(Gf : GA \to GB\\);
|
||||
* proofs that the homomorphism "respects moving around within the diagram": "moving around in \\(F\\) and then taking the homomorphism over to \\(G\\)" should be the same as "taking the homomorphism to \\(G\\) and then making the same movement in \\(G\\)".
|
||||
|
||||
The homomorphism \\(\alpha\\) is pretty constrained: the only freedom is to decide exactly *how* \\(\alpha\\) sends \\(FA\\) to \\(GA\\) for each \\(A : |\mathcal{C}|\\).
|
||||
|
||||
We have a special name for these structure-preserving maps between diagrams: we call them *natural transformations*.
|
||||
They provide us with a way of mapping between instantiations of the abstract theory specified by \\(\mathcal{C}\\).
|
||||
|
||||
# There are some very special examples of diagrams
|
||||
|
||||
We saw already that there are some pretty degenerate diagrams: the one which has every object going to the empty set, for instance.
|
||||
That diagram has somehow "thrown away all the information" from the category.
|
||||
|
||||
Diagrams can also be pretty complex.
|
||||
For example, take the diagrams for the very simple category that contains just one object and one arrow.
|
||||
Literally every set in the universe (together with the corresponding identity function on that set) is a diagram for this category!
|
||||
Most of those diagrams involve us ignoring tons of structure.
|
||||
|
||||
For example, there are \\(\mathbb{R}\\)-many functions \\(\mathbb{N} \to \mathbb{N}\\), so we're having to ignore uncountably many functions in the category of sets if we take the diagram consisting of "\\(\mathbb{N}\\) and its sole identity function".
|
||||
This diagram wants to have way more structure than there was in \\(\mathcal{C}\\), and it's only by shutting our eyes and ignoring the set-structure we don't care about that we recover anything that looks remotely like \\(\mathcal{C}\\)!
|
||||
|
||||
It turns out there's a sweet spot of diagrams with "exactly the amount of structure \\(\mathcal{C}\\) specified, and no more".
|
||||
The construction is: start with only one element in \\(FA\\) (for some \\(A\\)), and then chase through everything else that \\(\mathcal{C}\\) says should exist (which may involve adding in more elements of \\(FA\\) if there are morphisms telling us there should be more).
|
||||
|
||||
What does \\(\mathcal{C}\\) say should exist?
|
||||
If \\(f : A \to B\\) is a morphism of \\(\mathcal{C}\\), and if \\(a \in FA\\) is an element of our concrete instantiation of the object \\(A\\), we really want there to be a distinct object \\((Ff)(a) \in FB\\) so that we've preserved the information "\\(f\\) was a morphism \\(A \to B\\)".
|
||||
(If there weren't any such member of \\(FB\\), then our diagram has lost information: we might not be able to distinguish any more whether there was a morphism \\(f\\) in \\(\mathcal{C}\\) or not, just by looking at our instantiation \\(F\\).)
|
||||
|
||||
So if we assume there's an element \\(a \in FA\\), then for every \\(B \in |\mathcal{C}|\\), we can deduce the existence of elements \\((Ff)(a) \in B\\) for every \\(f : A \to B\\) in \\(\mathcal{C}\\); and they'd better all be distinct if we couldn't prove them to be equal in \\(\mathcal{C}\\).
|
||||
|
||||
Formally: for each object \\(A\\) of \\(\mathcal{C}\\), we can define a diagram \\(\mathrm{Rep}_A : \mathcal{C} \to \mathrm{\mathbf{Set}}\\) given by sending each \\(B\\) to the set of all morphisms in \\(\mathcal{C}\\) which go from \\(A\\) to \\(B\\).
|
||||
This somehow "captures exactly all the structure that \\(\mathcal{C}\\) said \\(A\\) has".
|
||||
(I've used the symbol \\(\mathrm{Rep}\\) to denote these diagrams, because the category-theoretic term for a diagram isomorphic to one of these is "*representable functor*".)
|
||||
|
||||
Note that I haven't yet written down the functions in these concrete instantiations of \\(\mathcal{C}\\); there's only one thing it could plausibly be.
|
||||
Given \\(f : B \to C\\) a morphism of \\(\mathcal{C}\\), the corresponding function \\(\mathrm{Rep}_A(f) : \mathrm{Rep}_A(B) \to \mathrm{Rep}_A(C)\\) (that is, the function \\(\mathrm{Rep}_A(f) : \langle \text{morphisms $A \to B$ in $\mathcal{C}$} \rangle \to \langle\text{morphisms $A \to C$ in $\mathcal{C}$}\rangle\\)) is defined to be given by composing with \\(f\\): we send \\(g : A \to B\\) to \\(f \circ g : A \to C\\).
|
||||
|
||||
These particular diagrams, the *representable functors* (one for every object in \\(\mathcal{C}\\)), together tell you everything there is to know about the category.
|
||||
(That is kind of intuitive, by their definition as "the sets of morphisms": we can list out every morphism in the category, just by writing down every element of every object in each of these concrete instantiations.)
|
||||
What might be less intuitive and requires a bit more thinking is their characterisation as "define \\(F\\) by supposing there's some single member \\(a \in FA\\), and then seeing what else is forced to exist"; you might find it helps to write out a concrete example of performing this operation for some particular tiny categories.
|
||||
|
||||
# Homomorphisms of the representable functors
|
||||
|
||||
The representable functors contain so little structure that their homomorphisms are forced to be quite simple.
|
||||
|
||||
Given any diagram \\(G : \mathcal{C} \to \mathrm{\mathbf{Set}}\\), and given any \\(A \in |\mathcal{C}|\\), we can precisely characterise the homomorphisms \\(\mathrm{Rep}_A \to G\\).
|
||||
Remember, \\(\mathrm{Rep}_A\\) was defined by supposing there's just one "free generator" element \\(a \in \mathrm{Rep}_A(A)\\), and then throwing into every object all the other elements that are forced to exist by morphisms of \\(\mathcal{C}\\).
|
||||
So intuitively speaking it should be the case that a homomorphism \\(\mathrm{Rep}_A \to G\\) is precisely defined by where that one element \\(a\\) is sent; once we've defined that, *everything* else in our instantiation \\(\mathrm{Rep}_A\\) should be forced by the "preserves morphism structure" property of homomorphisms.
|
||||
|
||||
This reasoning is made formal in the *Yoneda lemma*:
|
||||
|
||||
> Pick an arbitrary diagram \\(G : \mathcal{C} \to \mathrm{\mathbf{Set}}\\). Then for every object \\(A : |\mathcal{C}|\\), the homomorphisms from the diagram \\(\mathrm{Rep}_A\\) to \\(G\\) are precisely in correspondence with the elements of \\(G(A)\\). Moreover, this correspondence is natural in both \\(A\\) and \\(G\\).
|
||||
|
||||
Intuition: the homomorphisms are precisely defined by what happens to the "free generator", and we can get such a homomorphism from any choice of where the "free generator" goes.
|
||||
Moreover,
|
||||
* this construction is respected by homomorphisms out of \\(G\\) (that's "naturality in \\(G\\)": if we have a homomorphism \\(h : G \to H\\), and we perform the construction on both \\(G\\) and \\(H\\), we find that every homomorphism \\(\mathrm{Rep}_A \xrightarrow{\text{Yoneda corresponding to $x \in GA$}} G \xrightarrow{h} H\\) is equal to \\(\mathrm{Rep}_A \xrightarrow{\text{Yoneda corresponding to $h(x) \in HA$}} H\\));
|
||||
* this construction is respected by morphisms \\(A \to B\\) (that's "naturality in \\(A\\)"): this is currently entirely an exercise because I've ground to a halt.
|
||||
|
||||
The precise construction is like so:
|
||||
|
||||
* Given an element \\(a \in G(A)\\), define a homomorphism \\(\mathrm{Rep}_A\\) to \\(G\\) by sending \\(f : A \to B\\) to \\((Gf)(a)\\).
|
||||
* Given a homomorphism \\(\alpha : \mathrm{Rep}_A\\) to \\(G\\), define an element of \\(G(A)\\) by \\(\alpha(\mathrm{id}_A : A \to A)\\).
|
||||
* Show that these are inverse to each other.
|
||||
* Prove the naturality conditions.
|
||||
|
||||
Exercise: do those formally, as follows!
|
||||
|
||||
1. Prove that the homomorphism \\((f : A \to B) \mapsto (Gf)(a)\\) is indeed a homomorphism (that is, a natural transformation), by writing out the necessary properties which define a natural transformation and showing that they each hold.
|
||||
1. Prove (by writing out the equations) that the two Yoneda maps are inverse to each other.
|
||||
1. Write out the equations for both naturality conditions (that is, in \\(A\\) and in \\(G\\)) in full, and prove them.
|
||||
|
||||
# The Yoneda embedding
|
||||
|
||||
Given any (locally-small) category \\(\mathcal{C}\\) and an object \\(A : |\mathcal{C}|\\), we've seen a way to construct an instantiation of \\(\mathcal{C}\\) in \\(\mathrm{\mathbf{Set}}\\) in a canonical way, representing exactly the structure of \\(\mathcal{C}\\) that was available at \\(A\\).
|
||||
|
||||
## Definition of "fully faithful"
|
||||
|
||||
Recall the definitions of "full" and "faithful" for a functor \\(F : \mathcal{C} \to \mathcal{D}\\):
|
||||
* The functor is *faithful* if it is injective on parallel arrows: for all \\(A, B : |\mathcal{C}|\\), no two morphisms \\(A \to B\\) get mapped to the same target arrow.
|
||||
* The functor is *full* if it is surjective on objects which came from the functor: for all \\(A, B : |\mathcal{C}|\\), and for all \\(g : FA \to FB\\), there is \\(f : A \to B\\) with \\(Ff = g\\).
|
||||
|
||||
A functor \\(\mathcal{C} \to \mathcal{D}\\) is *fully faithful* if it is both full and faithful.
|
||||
While it may collapse away some of \\(\mathcal{C}\\)'s structure, and while it might not hit all of \\(\mathcal{D}\\), it does "locally" preserve all of \\(\mathcal{C}\\)'s structure and introduces no new structure locally: if we fix two objects \\(A, B\\) in \\(\mathcal{C}\\) and restrict ourselves to only looking at \\(A, B\\) and \\(FA, FB\\), the restricted \\(F\\) is a bijection.
|
||||
|
||||
## The Yoneda embedding is fully faithful
|
||||
|
||||
Notice that the collection of representable functors (that is, the "sweet spot" instantiations of \\(\mathcal{C}\\)) has got the right number of objects to try and be a copy of \\(\mathcal{C}\\): there's a representable functor for each object of \\(\mathcal{C}\\) already (because that's how we defined the representable functors).
|
||||
So what happens if we try and complete this into a copy of \\(\mathcal{C}\\) with all its categorical structure, inside the much larger space of instantiations of \\(\mathcal{C}\\)?
|
||||
This would be a nice thing to have, because the space of instantiations of \\(\mathcal{C}\\) is very well-behaved (they're all just sets!).
|
||||
|
||||
So to view it as a copy of \\(\mathcal{C}\\), we need for any \\(A, B : |\mathcal{C}|\\) and any morphism \\(f : A \to B\\) to find a homomorphism from \\(\mathrm{Rep}_A\\) to \\(\mathrm{Rep}_B\\).
|
||||
Take the Yoneda lemma and specialise it by setting \\(G := \mathrm{Rep}_B\\); then we have that the homomorphisms \\(\mathrm{Rep}_A \to \mathrm{Rep}_B\\) are naturally in bijection with the elements of \\(\mathrm{Rep}\_B(A)\\), which is by definition \\(\mathrm{Hom}\_{\mathcal{C}}(B, A)\\).
|
||||
|
||||
That's… not actually what we wanted!
|
||||
It's very close, but the arrows are going the wrong way: we have homomorphisms \\(\mathrm{Rep}\_A \to \mathrm{Rep}\_B\\) corresponding naturally to \\(\mathrm{Hom}\_{\mathcal{C}}(B, A)\\).
|
||||
|
||||
What we've actually done is built a canonical copy of the *opposite* category of \\(\mathcal{C}\\) inside the space of instantiations of \\(\mathcal{C}\\).
|
||||
This canonical copy is called the *Yoneda embedding*, and you can prove that it is full and faithful.
|
||||
|
||||
That was the *contravariant Yoneda embedding*, which takes \\(\mathcal{C}^{\mathrm{op}}\\) and embeds it fully faithfully in \\(\mathrm{Nat}(\mathcal{C} \to \mathrm{\mathbf{Set}})\\), the space of all \\(\mathrm{\mathbf{Set}}\\)-instantiations of \\(\mathcal{C}\\).
|
||||
(That space is more precisely a category, with morphisms being precisely the instantiation homomorphisms, or natural transformations.)
|
||||
By flipping all the arrows around, we also get the *covariant Yoneda embedding*, which takes \\(\mathcal{C}\\) and embeds it fully faithfully in \\(\mathrm{Nat}(\mathcal{C}^{\mathrm{op}} \to \mathrm{\mathbf{Set}})\\), the space of all \\(\mathrm{\mathbf{Set}}\\)-instantiations of \\(\mathcal{C}^{\mathrm{op}}\\) (also known as the space of all *presheaves* over \\(\mathcal{C}\\)).
|
25
hugo/content/posts/2024-05-01-i-notice-that-i-am-confused.md
Normal file
25
hugo/content/posts/2024-05-01-i-notice-that-i-am-confused.md
Normal file
@@ -0,0 +1,25 @@
|
||||
---
|
||||
lastmod: "2024-05-01T11:38:00.0000000+01:00"
|
||||
author: patrick
|
||||
date: "2024-05-01T11:38:00.0000000+01:00"
|
||||
title: The phrase "I Notice That I Am Confused"
|
||||
summary: "To me it's got a specific meaning, but I've seen it used much more generally, and I think its meaning should not be polluted."
|
||||
---
|
||||
|
||||
In LessWrong-speak, "[I notice that I am confused](https://www.lesswrong.com/s/zpCiuR4T343j9WkcK)" is a pretty standard phrase.
|
||||
I've seen [Zvi](https://thezvi.wordpress.com/) in particular use that phrase in a great many contexts where my understanding of it doesn't match.
|
||||
So here's my understanding of it.
|
||||
|
||||
> "I Notice That I Am Confused" is the phrase that accompanies/triggers the motion "pause, attach the debugger to your world modelling system, and replay the last explanation you accepted".
|
||||
|
||||
Here are a couple of possible reasons I might want to attach the debugger:
|
||||
|
||||
* I can feel my world model contorting itself around something. (Maybe I can only feel the fact of a contortion and not the nature of it.)
|
||||
* Some part of my world modelling system appears to be actively working on something, but I can see no reason for it to do so. An idle process should not be consuming 20% CPU. Maybe it's still shaking out the implications of something (which means by definition I'm still confused).
|
||||
* Or maybe what it's working on is "make sure I never see this flaw in the model"! That actually happens! The modelling system wants to feel that its model is correct, and it's only of secondary importance that the model actually *be* correct. I am very familiar with the mental motion "there's no need to look over here, and there's *definitely* nothing over here that would invalidate the explanation".
|
||||
|
||||
Those all feel quite adversarial; here's one which is more of a cooperative process:
|
||||
|
||||
* Maybe there's just a nagging sense that not all the data is explained. An explanation feels complete, but the model is highlighting that some piece of data doesn't quite fit (possibly I haven't yet consciously identified what doesn't fit or why).
|
||||
|
||||
The point of the phrase "I notice that I am confused" is to indicate "this explanation feels compelling, but *something is off* and I need to promote this to consciousness to discover why".
|
21
hugo/content/posts/2024-07-24-philosophy-of-code.md
Normal file
21
hugo/content/posts/2024-07-24-philosophy-of-code.md
Normal file
@@ -0,0 +1,21 @@
|
||||
---
|
||||
lastmod: "2024-07-24T17:38:00.0000000+01:00"
|
||||
author: patrick
|
||||
date: "2024-07-24T17:38:00.0000000+01:00"
|
||||
title: Code having "the right philosophy"
|
||||
summary: "Those who would give up essential safety, to purchase a little temporary simplicity, deserve (and will get) neither safety nor simplicity."
|
||||
---
|
||||
|
||||
[Hacker News](https://news.ycombinator.com/item?id=41032806):
|
||||
|
||||
> Time library can be simple, it's just rust libraries tend to be philosophic for some reason, but it's only one of many design approaches.
|
||||
|
||||
Certainly a true statement.
|
||||
|
||||
I claim that the "some reason" here is that this "philosophic" design approach is correct, and the other ones aren't.
|
||||
Most standard libraries (.NET, Golang, Python) don't care about correctness enough that they'd actually *model the domains* in question, so they don't, so they make it trivial to write completely unnecessary bugs.
|
||||
|
||||
As evidence, I submit the fact that I have twice had to rewrite someone else's .NET code to fix time-related bugs in it, whose ultimate direct cause was "the .NET `DateTime` type is an extremely bad model for dates-and-times in the world".
|
||||
In one of those two cases, I ended up completely rewriting the entire application, using NodaTime to drive the date-time computations, because that's a library that actually attempts to model dates-and-times.
|
||||
|
||||
Those who would give up essential safety, to purchase a little temporary simplicity, deserve (and will get) neither safety nor simplicity.
|
28
hugo/content/posts/2024-07-25-lob-theorem.md
Normal file
28
hugo/content/posts/2024-07-25-lob-theorem.md
Normal file
@@ -0,0 +1,28 @@
|
||||
---
|
||||
lastmod: "2024-07-25T19:48:00.0000000+01:00"
|
||||
author: patrick
|
||||
date: "2024-07-25T19:48:00.0000000+01:00"
|
||||
title: Learning plan for "Program Equilibrium in the Prisoner's Dilemma"
|
||||
summary: The questions whose answers I don't know, and the things I intend to learn, on the way to understanding a paper.
|
||||
---
|
||||
|
||||
## Resources
|
||||
The paper is [Program Equilibrium in the Prisoner's Dilemma](https://intelligence.org/files/ProgramEquilibrium.pdf).
|
||||
|
||||
A prerequisite is [Löb's theorem](https://en.wikipedia.org/wiki/L%C3%B6b's_theorem), for which Yudkowsky has a [cartoon guide](https://www.lesswrong.com/posts/ALCnqX6Xx8bpFMZq3/the-cartoon-guide-to-loeb-s-theorem).
|
||||
|
||||
One of the foundational papers is by Smullyan: [Logicians who reason about themselves](https://dl.acm.org/doi/pdf/10.5555/1029786.1029818).
|
||||
|
||||
## Questions I intend to answer
|
||||
|
||||
* Why can't we similarly prove that we're going to defect? "If it's provable that we defect, then we defect"?
|
||||
* I had [an objection about "parametric bounded Löb"](/misc/ParametricBoundedLoeb2016/ParametricBoundedLoeb2016.pdf) ages and ages ago; do I still believe it?
|
||||
* The paper currently works relative to a provability oracle; is it possible in principle for us to precompute and hand over proofs along with our source code? What would such a proof look like?
|
||||
* Understand the [diagonal lemma](https://en.wikipedia.org/wiki/Diagonal_lemma).
|
||||
* Understand Löb's theorem.
|
||||
* Why does Wikipedia say that Smullyan refers to an agent as "modest" when 'such a reasoner can never believe "my belief in P would imply that P is true", without also believing that P is true'? Why that word?
|
||||
* Can I get an intuition for what it would actually feel like to be an ideal agent going through the thought process of FairBot? (Or what it would mean to *be* PA computing the truth of a statement via Löb?)
|
||||
* Fully and precisely write out the definition of FairBot and of PrudentBot in some pseudocode (permitting calls to `is_provable(expr)`).
|
||||
* Comprehend the sentence: It is important that we look for proofs of `X(DB) = D` in a stronger formal system than we use for proving `X(PB) = C`; if we do otherwise, the resulting variant of PrudentBot would lose the ability to cooperate with itself.
|
||||
* Are there any stronger conditions that will let us do somehow "better", by successfully defecting against more opponents, than PrudentBot? (Does this come down to tradeoffs about how easy it is for opponents to prove that you're going to cooperate with them?)
|
||||
* Understand the scope of [MIRI's implementation](https://github.com/machine-intelligence/provability).
|
18
hugo/content/posts/2024-08-15-github-workflows.md
Normal file
18
hugo/content/posts/2024-08-15-github-workflows.md
Normal file
@@ -0,0 +1,18 @@
|
||||
---
|
||||
lastmod: "2024-08-15T17:51:00.0000000+01:00"
|
||||
author: patrick
|
||||
date: "2024-08-15T17:51:00.0000000+01:00"
|
||||
title: New GitHub workflows
|
||||
summary: I've made a GitHub workflow to assert that all required GitHub checks are complete, and one to publish and attest NuGet packages.
|
||||
---
|
||||
|
||||
# [all-required-checks-complete](https://github.com/Smaug123/all-required-checks-complete-action)
|
||||
|
||||
The problem this solves is that GitHub's "required" checks are not actually required.
|
||||
A "required" step which is skipped because it depends on a failed step will count as successful.
|
||||
(This is folklore, but [here's one writeup](https://emmer.dev/blog/skippable-github-status-checks-aren-t-really-required/).)
|
||||
|
||||
# [publish-nuget](https://github.com/Smaug123/publish-nuget-action)
|
||||
|
||||
NuGet [does not lend itself](https://github.com/NuGet/NuGetGallery/issues/10026) to [GitHub artefact attestation](https://docs.github.com/en/actions/security-for-github-actions/using-artifact-attestations/using-artifact-attestations-to-establish-provenance-for-builds), so there's some annoying work to do to make that happen.
|
||||
This action performs that work!
|
56
hugo/content/posts/2024-08-26-woofware-arg-parser.md
Normal file
56
hugo/content/posts/2024-08-26-woofware-arg-parser.md
Normal file
@@ -0,0 +1,56 @@
|
||||
---
|
||||
lastmod: "2024-08-26T12:26:00.0000000+01:00"
|
||||
author: patrick
|
||||
categories:
|
||||
- uncategorized
|
||||
date: "2024-08-26T12:26:00.0000000+01:00"
|
||||
title: WoofWare.Myriad.Plugins learns to parse args
|
||||
summary: "My F# source generators have some new features, including an argument parser."
|
||||
---
|
||||
|
||||
This post is about [WoofWare.Myriad.Plugins](https://github.com/Smaug123/WoofWare.Myriad), a set of [F#](https://en.wikipedia.org/wiki/F_Sharp_(programming_language)) source generators ([see it on NuGet](https://www.nuget.org/packages/WoofWare.Myriad.Plugins)).
|
||||
Go and read [the README on GitHub](https://github.com/Smaug123/WoofWare.Myriad/blob/main/README.md) if you're interested.
|
||||
|
||||
They are particularly intended for `PublishAot` [ahead-of-time compilation](https://learn.microsoft.com/en-us/dotnet/core/deploying/native-aot/) contexts, in which reflection is heavily restricted, but also for anyone who doesn't want reflection for whatever reason (e.g. "to obtain the ability to step through code in a debugger", or "for more predictable speed").
|
||||
|
||||
Since [my last post], I've implemented the following:
|
||||
|
||||
* `[<JsonSerialize>]` (to stamp out `toJsonNode : 'T -> JsonNode` methods)
|
||||
* `[<CreateCatamorphism>]` (to build a non-stack-overflowing [catamorphism](https://fsharpforfunandprofit.com/posts/recursive-types-and-folds/) for an algebraic data type)
|
||||
* `[<ArgParser>]` (to stamp out an argument parser).
|
||||
|
||||
## `ArgParser`
|
||||
|
||||
Example:
|
||||
|
||||
```fsharp
|
||||
[<ArgParser>]
|
||||
type Foo =
|
||||
{
|
||||
[<ArgumentHelpText "Enable the frobnicator">]
|
||||
SomeFlag : bool
|
||||
A : int option
|
||||
[<ArgumentDefaultFunction>]
|
||||
B : Choice<int, int>
|
||||
[<ArgumentDefaultEnvironmentVariable "MY_ENV_VAR">]
|
||||
BWithEnv : Choice<int, int>
|
||||
C : float list
|
||||
// optionally:
|
||||
[<PositionalArgs>]
|
||||
Rest : string list // or e.g. `int list` if you want them parsed into a type too
|
||||
}
|
||||
static member DefaultB () = 4
|
||||
```
|
||||
|
||||
Features:
|
||||
|
||||
* Optional arguments of type `'a option`.
|
||||
* `[<ArgumentDefaultFunction>]` and `[<ArgumentDefaultEnvironmentVariable>]` to auto-populate default arguments which are not supplied. Default values are modelled as `Choice<'a, 'a>`, with `Choice1Of2` meaning "the user gave me this", and `Choice2Of2` meaning "this was populated from a default source".
|
||||
* Help text with `[<ArgumentHelpText>]`, summoned with `--help` in any position where the parser is expecting an argument, and also summoned during certain failures to parse.
|
||||
* Detailed control over `TimeSpan` parsing with `[<ParseExact>]` (and `[<InvariantCulture>]` if desired).
|
||||
* Accumulation of arguments supplied repeatedly: for example, `Path : FileInfo list` is populated with `--path /foo/bar --path /baz/quux`.
|
||||
* Handling of `--foo=bar` and `--foo bar` equivalently.
|
||||
* Booleans have arity 1 or 0, whichever leads to a successful parse: `--flag` and `--flag=true` and `--flag true` are equivalent.
|
||||
* Positional arguments can appear anywhere, although if they start with a `--` then it is best to put them after a trailing `--` separator: `--named-arg=blah -- --pos-arg1 pos-arg2 --pos-arg3`.
|
||||
|
||||
[my last post]: {{< ref "2023-12-31-woofware-myriad-plugins" >}}
|
28
hugo/content/posts/2024-09-07-massage.md
Normal file
28
hugo/content/posts/2024-09-07-massage.md
Normal file
@@ -0,0 +1,28 @@
|
||||
---
|
||||
lastmod: "2024-09-07T11:47:00.0000000+01:00"
|
||||
author: patrick
|
||||
categories:
|
||||
- uncategorized
|
||||
date: "2024-09-07T11:47:00.0000000+01:00"
|
||||
title: Lessons from a massage course
|
||||
summary: "I went to a one-day intro to massage taster course, and it was fun and interesting!"
|
||||
---
|
||||
|
||||
I recently attended the [Bodyology one-day intro to massage taster](https://bodyologymassagecourses.co.uk/courses/intro-course).
|
||||
Recommended!
|
||||
The instructor Dror was excellent, with a teaching style correctly based around telling you why things are done the way they are, and then giving you lots of time to practise finding how your own hands best achieve the goals.
|
||||
|
||||
# Why did I try massage?
|
||||
|
||||
1. The ever-present desire to find meaning (c.f. applying for the RAF reserves); it's common knowledge that [directly and viscerally helping others](https://80000hours.org/career-guide/job-satisfaction/) is something that people find very meaningful.
|
||||
2. Wouldn't that be a neat skill to be able to reveal that you're bizarrely, impossibly good at! ("Sometimes, magic is just someone spending more time on something than anyone else might reasonably expect.")
|
||||
|
||||
# Interesting lessons
|
||||
|
||||
* Move from the legs. This is obvious every single time it comes up anywhere, and it comes up all the time, but somehow I *still* never generalise the lesson so that I know it without being told in any given situation.
|
||||
* I find it *really* stressful to have no real-time feedback on what I'm doing. Pretty much everything I do has a tight feedback loop, but the feedback loop for massage is really long: it breaks the immersion to be constantly using your mouth-words during the session, and if the victim is face-down then your only source of feedback is literally just "try to read someone's back", unless you are much more empathic than I am (which would certainly come with practice). I was a lot more relaxed when my subject and I were maintaining pretty constant verbal communication.
|
||||
* This is even worse for head massage, where the subject tends to fall asleep (or get very close to it), which I guess is a positive signal but also is a complete lack of any other signals.
|
||||
* Massage also gives you no *objective* feedback, so it falls into the category of "things where my System 1 expects explicit positive feedback to be false". I can't stop myself interpreting other people's feedback as "this person is trying to make you feel better about your terrible performance", at least without a bit of time getting to know that person first.
|
||||
* Cultural hangups around grabbing a woman by the neck. There was an entire session on neck/traps/shoulder massage, and it took me a solid two minutes before I was able to grip the spinal erectors hard enough to have any massage-related effect at all. This is hard to do when for thirty years you've had a culture screaming "YOU WILL NOT GRAB A WOMAN BY THE NECK" at you! (I also suspect I was under more internal strain than I explicitly felt, because I choked up slightly when I gave a sentence explaining my light touch afterwards.)
|
||||
* A massage often begins with a simple laying-on-of-hands. This is actually a communication channel! Take it slow: you're greeting the subject, setting the terms of engagement, letting yourself adjust to their rhythm (mainly their breathing). A therapist who moves their hands around feels indecisive, and remember that time will feel like it's passing faster for the therapist because they're upright and in control. Different people communicate different things this way, which surprised me a lot. I really felt (for example) that, while I was the demo subject, the instructor was saying hello to me through his hands, and that I was replying through my body's breathing movement. (One breathing cycle lasts many seconds; if the therapist moves their hands before you've even finished one breath, that actually feels pretty rude: they're literally interrupting your communication.) By contrast, during a practice session, someone gave me a very firm and assertive greeting, "I am in control" (which is certainly not bad, it's just very different!).
|
||||
* Sunflower oil works just fine as a massage oil; in fact the instructor recommended it over other oils.
|
@@ -1,5 +1,5 @@
|
||||
---
|
||||
lastmod: "2023-09-02T13:31:58.0000000+01:00"
|
||||
lastmod: "2024-04-17T10:31:58.0000000+01:00"
|
||||
title: My reading list
|
||||
author: patrick
|
||||
layout: page
|
||||
@@ -12,17 +12,19 @@ This page holds a list of the books I am reading, and a list of books I have rea
|
||||
* [Don't Shoot the Dog] - Nonfiction book on animal training and operant conditioning: the art of getting obedience (from animals and humans alike) without using punishment. It has clarified my understanding of a whole variety of phenomena related to motivation and so on.
|
||||
* [Inadequate Equilibria](https://equilibriabook.com/), by Eliezer Yudkowsky. Fascinating look at why everything is broken and nobody can fix anything. I'm a sucker for ideas presented as Socratic dialogue.
|
||||
* [A Person Paper on Purity in Language][Person Paper], by Douglas Hofstadter (linked to the Wayback Machine version) - it is pretty shocking to realise just how much the English language discriminates against females, and how routine it is. Whether or not you think it's an issue, this is an excellent satire.
|
||||
* [Gödel, Escher, Bach], by Douglas Hofstadter (an incredible book on pretty much everything - possibly the most meta thing I've ever read). Revisiting it now, I realise that I already know quite a lot of the mathematical content from different sources, but then to the extent that I specialised in anything during Part III, I specialised in logic.
|
||||
* The [LessWrong] entry on [Cached Thoughts] - of the many fascinating LessWrong entries, this is probably the one that had the most profound and immediate effect on my thinking. I don't know if that effect was just a culmination of my previous readings, but this was the moment that I really got the idea that "human thinking was not designed, it's a bit of a miracle that we can think at all, and there are steps we can take to make our thinking less sloppy".
|
||||
* [Harry Potter and the Methods of Rationality][HPMoR] - it's a very long fanfic about what might happen if Harry came from a different intellectual background and if every character were actually *trying* at life. It successfully manages to find coherent explanations for many of the random inconsistencies of the original. Give it a try - if you don't like it by the time we reach Hogwarts, feel free to stop. It's got its own subreddit, of which the most pertinent post is probably [what HPMoR is about][HPMoR subreddit]. People either find HPMoR horribly dull or absolutely incredible, as far as I can tell.
|
||||
* Another LessWrong entry, this one on [effective altruism][EA LessWrong] ([factual summary][EA Wikipedia] at Wikipedia) - the holy grail of charitable giving is surely to get maximum bang for your buck. (On a vaguely related note, a link that for ethical reasons doesn't make it onto the list but seems worryingly insightful is a post from some random blog describing a horrible unit of currency, the "dead child", being the amount of money required to save the life of one child's life through charity - it makes very uncomfortable reading, so consider yourself duly warned that you might not want to read it. The idea is to make numbers like "£250,000 spent on a luxury dog kennel" make *sense* to us. The link is [this post on a horrible unit of currency][dead child].)
|
||||
* [The Name of the Wind] by Patrick Rothfuss is the fantasy book with the best story I've ever read. It's the start of a trilogy (the Kingkiller Chronicle) and, if you like fantasy (and maybe even if you don't), is a stupendously well-told book. I gave it to a friend who professes never to read, and I didn't see em again for another week. It's not uniformly liked, though: another friend described it as an obvious self-insert wish-fulfillment fantasy from beginning to end.
|
||||
* [Three Men in a Boat] - the funniest book I've read. After the first two pages, I can barely move after having dissolved in laughter, and it just gets better. I was banned from reading this in the presence of other people, probably because I was having too much fun.
|
||||
* [Midnight's Children] - justly famous mystical fiction, set in twentieth century India. Wonderful book, beautiful turns of phrase and awe-inspiring plot.
|
||||
* [Flowers for Algernon] - possibly the saddest book I've ever read, and at least one other person has agreed with me.
|
||||
* [Turn The Ship Around!] - book on the nature of leadership. Central thesis: if a great commander leaves a ship and the ship falls apart straight away, in what sense is it reasonable to say they were a "great" commander? Its teachings are weirdly similar, in fact to [Never Split the Difference], though they're approaching two very different problems.
|
||||
* The Debt to Pleasure, by John Lanchester - fiction/cookbook. One of the most erudite books I've read; this book really benefits from being read on a Kindle, with its inbuilt dictionary. A joy to read, excellent characterisation of the narrator. I'd advise not Googling the book before you read it (and ideally don't even read the blurb); there are spoilers to be found, and I think the best experience of this book would be to go in completely blind. Do read it, though; it has many beautiful turns of phrase, and is just generally extremely well written.
|
||||
* [Jonathan Strange & Mr Norrell], by Susanna Clarke. This book alternates between hilarious, whimsical, and deeply ominous or wild (like you're seeing the tiniest cross-section of a huge incomprehensible thing). In general style it's like E Nesbit if she were writing extremely competently for non-children. I was glued to it, and laughed out loud at regular intervals.
|
||||
* [The Name of the Wind] by Patrick Rothfuss is the fantasy book with the best story I've ever read. It's the start of a trilogy (the Kingkiller Chronicle) and, if you like fantasy (and maybe even if you don't), is a stupendously well-told book. I gave it to a friend who professes never to read, and I didn't see them again for another week. It's not uniformly liked, though: another friend described it as an obvious self-insert wish-fulfillment fantasy from beginning to end.
|
||||
* [Gödel, Escher, Bach], by Douglas Hofstadter (an incredible book on pretty much everything - possibly the most meta thing I've ever read). Revisiting it now, I realise that I already know quite a lot of the mathematical content from different sources, but then to the extent that I specialised in anything during Part III, I specialised in logic. For some reason many people don't like this book, and it is certainly very long, but decades later I still remember e.g. the Contracrostipunctus as being just mind-blowing.
|
||||
* [Harry Potter and the Methods of Rationality][HPMoR] - it's a very long fanfic about what might happen if Harry came from a different intellectual background and if every character were actually *trying* at life. It successfully manages to find coherent explanations for many of the random inconsistencies of the original. Give it a try - if you don't like it by the time we reach Hogwarts, feel free to stop. It's got its own subreddit, of which the most pertinent post is probably [what HPMoR is about][HPMoR subreddit]. People either find HPMoR horribly dull or absolutely incredible, as far as I can tell.
|
||||
|
||||
[Jonathan Strange & Mr Norrell]: https://en.wikipedia.org/wiki/Jonathan_Strange_%26_Mr_Norrell
|
||||
[Gödel, Escher, Bach]: https://en.wikipedia.org/wiki/G%C3%B6del,_Escher,_Bach
|
||||
[LessWrong]: http://www.lesswrong.com
|
||||
[Cached Thoughts]: http://lesswrong.com/lw/k5/cached_thoughts/
|
||||
@@ -40,13 +42,13 @@ This page holds a list of the books I am reading, and a list of books I have rea
|
||||
|
||||
# Currently reading
|
||||
|
||||
* In Praise of Shadows, by Junichiro Tanizaki
|
||||
* Building Secure and Reliable Systems, by the Google SRE team. This is genuinely a textbook, so it's quite slow going. A lot of this is *very* Google-centric, where it's assumed that everything is a microservice and any given query to a service will require hundreds of RPC calls. However, the general lessons seem to be valuable.
|
||||
* Accelerando, by Charles Stross
|
||||
|
||||
# Bought and ready to read
|
||||
|
||||
* The Attention Merchants, by Tim Wu
|
||||
* American Gods, by Neil Gaiman
|
||||
* 84, Charing Cross Road, by Helene Hanff
|
||||
|
||||
# To read
|
||||
|
||||
@@ -64,22 +66,26 @@ This page holds a list of the books I am reading, and a list of books I have rea
|
||||
* Linked, by Albert Lazlo Barabassi (study of networks)
|
||||
* Libriomancer, by Jim C Hines (fantasy fiction)
|
||||
* Breakfast of Champions, by Kurt Vonnegut (fiction of some sort)
|
||||
* Nature via Nurture, by Matt Ridley (study of interaction of genes and environment and development)
|
||||
* The Culture series, by Iain M Banks
|
||||
* A Place of Greater Safety, by Hilary Mantel
|
||||
* So Good They Can't Ignore You, by Cal Newport
|
||||
* 84, Charing Cross Road, by Helene Hanff
|
||||
* Black Box Thinking, by Matthew Syed
|
||||
* Impro, by Keith Johnstone
|
||||
|
||||
# Read some of and then put down
|
||||
|
||||
* [Legal Systems Very Different From Ours](http://web.archive.org/web/20220806200919/http://www.daviddfriedman.com/Legal%20Systems/LegalSystemsContents.htm): it's all in the title, really. Case studies of different legal systems, by the economist David Friedman. I read the first third or so of this, and it was a very interesting set of things to think about. How can a civilisation run itself without our systems of law courts? There have been many answers through the centuries.
|
||||
* [Extraordinary Popular Delusions and the Madness of Crowds](https://en.wikipedia.org/wiki/Extraordinary_Popular_Delusions_and_the_Madness_of_Crowds), by Charles Mackay - nonfiction about the ways in which the crowd can get things wrong. This book is very, very long; I made it through the first half of the first volume before giving up. A pretty eye-opening book, though: Mackay's description (from the year 1841!) of the South Sea Bubble is almost indistinguishable from the recent cryptocurrency crazes, right down to an extensive list of some of the crazy companies that were eventually made illegal ("for improving the art of making soap", "for a wheel of perpetual motion", "for extracting silver from lead", "for a grand American fishery") - all very reminiscent of the various shitcoins.
|
||||
* [Quantum Computing for the Very Curious](https://quantum.country/qcvc): essay to teach the fundamentals of quantum computing, with embedded spaced repetition cards.
|
||||
* True Names, by Vernor Vinge
|
||||
* Diaspora, by Greg Egan
|
||||
|
||||
# Have read
|
||||
|
||||
* Now It Can Be Told, by General Groves. I wasn't as taken with this book as I was with _The Making of the Atomic Bomb_; this book contained a bunch more individual callouts and "this particular person did a brilliant job" than are really necessary fifty years later. Still a bunch of excellent quotes, e.g. around how the US government paid him $35mm personally to get around procurement rules; _that's_ how you really try to win when you have trust in your employees!
|
||||
* Red Side Story, by Jasper Fforde (sequel to Shades of Grey). Solidly as I expected it to be; fairly enjoyable. Plot was largely predictable.
|
||||
* [Planecrash](https://www.projectlawful.com/). It turns out that self-insert sex fiction is not actually much better if you are self-aware about it. There's some excellent readable story in here, but you have to wade through hours and hours of sex and sex-politics to find it. Absolutely not worth reading from start to finish; just find someone to link the "dath ilan society description and basic coordination classes" highlights. These authors *really* need an editor; the work is literally at least 10x too long.
|
||||
* Tao Te Ching, by Lao Tzu, interpreted by Ursula Le Guin. Her poetry is *beautiful*. Not an easy read: I felt I was rushing at two hours for thirty-odd chapters to get the bare minimum of comprehension, but it's deep enough that each chapter would reward an hour of study. I'm currently going to improv classes, and this feels like it is secretly a book about improv!
|
||||
* Piranesi, by Susanna Clarke. Wonderful. Ethereal (but in a sort of grounded way), beautiful.
|
||||
* Impro, by Keith Johnstone. The first half of this book is very interesting, easy reading, and I suspect rather useful; I believe it's been helpful in my introductory improv lessons. (I don't know how useful it will be without practice of some sort, but I also suspect it's possible to practise without going full improv-classes.) The second half is an exploration of mask work, Commedia dell'arte, trance states, and possession, and I found that much less worth reading.
|
||||
* Diary of a Provincial Lady, by E. M. Delafield. Hilarious. I was laughing out loud every few pages. Strong recommend. This was so like real life.
|
||||
* [Folding Beijing](https://www.uncannymagazine.com/article/folding-beijing-2/), by Hao Jingfang. Interesting short story, although really I think it could have been half the length without losing much; the premise is not exactly complicated, and the story is really just a brief exploration of the premise.
|
||||
* Permutation City, by Greg Egan. Cool book! It's interesting to think about why I find the core premise implausible, but it certainly seemed novel to me. Pretty gripping. It seems to pair quite nicely with Robin Hanson's _The Age of Em_, which would be a nonfiction accompaniment.
|
||||
* Building Secure and Reliable Systems, by the Google SRE team. This is genuinely a textbook, so it's quite slow going. A lot of this is *very* Google-centric, where it's assumed that everything is a microservice and any given query to a service will require hundreds of RPC calls. However, the general lessons seem to be valuable.
|
||||
* A Handful of Dust, by Evelyn Waugh. Good Lord this is bleak. The kind of book which would definitely reward rereading; I feel like I got about a quarter of what was going on, there was so much subtext. Oddly a fun read, though!
|
||||
* The Remains of the Day, by Kazuo Ishiguro. Short, sweet, and tragic. Simple throwaway lines become retrospectively rich in meaning as you read on. Spoiler in rot13: gur haeryvnoyr aneengbe tvirf guvf fgenatr frafr bs grafvba guebhtubhg.
|
||||
* A Pocketful of Rye, by Agatha Christie. One of the Marples. Christie is generally excellent light reading, perhaps partly because her writing is all so familiar. This particular book I first read as an early teenager, but recently reread as part of a marathon in which we watched two adaptations and listened to a radio version; the exercise was actually quite interesting in seeing what the various adapters (and actors) chose to pull out.
|
||||
* The Hornblower series, by CS Forester. I read some of these over and over as a child, and they bear rereading as an adult. The later books become less interesting to me, though, as Hornblower is promoted and gets further from the action.
|
||||
@@ -140,6 +146,13 @@ This page holds a list of the books I am reading, and a list of books I have rea
|
||||
* Consciousness Explained, by Daniel Dennet (explaining the Multiple Drafts view of consciousness) - very interesting book, thought-provoking, and I've absorbed some of its contents into my world-view.
|
||||
* The Mind's I, by Douglas Hofstadter and Daniel Dennet (various musings on consciousness and the nature of the self) - this is a collection of pieces by other people, with commentary by Hofstadter and Dennet, which wasn't quite what I expected. I'd read several of the pieces before, although Hofstadter sparkled just as he usually does. I got bored after about the tenth excerpt, but certainly up to the eighth my attention was held.
|
||||
|
||||
# Read some of and then put down
|
||||
|
||||
* [The Complete Cosmicomics](https://en.wikipedia.org/wiki/The_Complete_Cosmicomics), by Italo Calvino. Whimsical indeed, but oddly enough I started finding them rather samey after about a third of the way through. Worth reading a couple of them (no particular ones seemed better than the others to me).
|
||||
* [Legal Systems Very Different From Ours](http://web.archive.org/web/20220806200919/http://www.daviddfriedman.com/Legal%20Systems/LegalSystemsContents.htm): it's all in the title, really. Case studies of different legal systems, by the economist David Friedman. I read the first third or so of this, and it was a very interesting set of things to think about. How can a civilisation run itself without our systems of law courts? There have been many answers through the centuries.
|
||||
* [Extraordinary Popular Delusions and the Madness of Crowds](https://en.wikipedia.org/wiki/Extraordinary_Popular_Delusions_and_the_Madness_of_Crowds), by Charles Mackay - nonfiction about the ways in which the crowd can get things wrong. This book is very, very long; I made it through the first half of the first volume before giving up. A pretty eye-opening book, though: Mackay's description (from the year 1841!) of the South Sea Bubble is almost indistinguishable from the recent cryptocurrency crazes, right down to an extensive list of some of the crazy companies that were eventually made illegal ("for improving the art of making soap", "for a wheel of perpetual motion", "for extracting silver from lead", "for a grand American fishery") - all very reminiscent of the various shitcoins.
|
||||
* [Quantum Computing for the Very Curious](https://quantum.country/qcvc): essay to teach the fundamentals of quantum computing, with embedded spaced repetition cards.
|
||||
|
||||
[1]: https://en.wikipedia.org/wiki/Flow_%28psychology%29 "Flow Wikipedia page"
|
||||
[Worm]: https://parahumans.wordpress.com/ "Worm (fiction)"
|
||||
[Pact]: https://pactwebserial.wordpress.com/
|
||||
|
@@ -1,18 +1,26 @@
|
||||
<details>
|
||||
{{ $summary := default "Click to view gallery" (.Get "summary") }}
|
||||
<summary>{{ $summary }}</summary>
|
||||
<div class="gallery">
|
||||
{{ $base := .Get "src" }}
|
||||
{{ $path := print "static/" (.Get "src") }}
|
||||
{{ $galleryName := default "gallery" (.Get "galleryName") }}
|
||||
|
||||
{{ range (readDir $path) }}
|
||||
{{- $thumbext := "-thumb" }}
|
||||
{{- $isthumb := .Name | findRE ($thumbext | printf "%s\\.") }}<!-- is the current file a thumbnail image? -->
|
||||
{{- $isimg := lower .Name | findRE "\\.(gif|jpg|jpeg|tiff|png|bmp)" }}<!-- is the current file an image? -->
|
||||
{{- if and $isimg (not $isthumb) }}
|
||||
{{- $thumb := .Name | replaceRE "(\\.)" ($thumbext | printf "%s.") }}
|
||||
{{- $thumb := .Name | replaceRE "(\\.[^.]+)" ($thumbext | printf "%s.jpg") }}
|
||||
{{- $alttextfile := .Name | replaceRE "(\\..+)" ".md" }}
|
||||
{{- $alttext := printf "%s/%s" $path $alttextfile | os.ReadFile }}
|
||||
<a data-fancybox="gallery" href="/{{ $base }}/{{ .Name }}">
|
||||
<a data-fancybox="{{ $galleryName }}" data-caption="{{ $alttext }}" href="/{{ $base }}/{{ .Name }}">
|
||||
<img src="/{{ $base }}/{{ $thumb }}" width=100 height=100 alt={{ $.Page.RenderString $alttext }}> <br/>
|
||||
</a>
|
||||
{{- end }}
|
||||
{{ end }}
|
||||
</div>
|
||||
<script>document.addEventListener('DOMContentLoaded', function() {
|
||||
Fancybox.bind('[data-fancybox="{{ $galleryName }}"]', {});
|
||||
});</script>
|
||||
</div>
|
||||
</details>
|
1
hugo/layouts/shortcodes/rawhtml.html
Normal file
1
hugo/layouts/shortcodes/rawhtml.html
Normal file
@@ -0,0 +1 @@
|
||||
{{.Inner}}
|
@@ -314,7 +314,7 @@ a:active {
|
||||
}
|
||||
|
||||
.post .post-content a {
|
||||
text-decoration: none;
|
||||
text-decoration: underline;
|
||||
letter-spacing: 1px;
|
||||
color: #2660ab;
|
||||
}
|
||||
@@ -915,4 +915,4 @@ print {
|
||||
.page-top {
|
||||
display: none;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
@@ -1,15 +1,12 @@
|
||||
{{- if (isset .Params "gallery") -}}
|
||||
<script src="https://cdnjs.cloudflare.com/ajax/libs/jquery/3.3.1/jquery.min.js"
|
||||
integrity="sha384-tsQFqpEReu7ZLhBV2VZlAu7zcOV+rXbYlF2cqB8txI/8aZajjp4Bqd+V6D5IgvKT"
|
||||
crossorigin="anonymous"></script>
|
||||
{{- $url := "https://cdnjs.cloudflare.com/ajax/libs/fancybox/3.4.0/jquery.fancybox.min.js" -}}
|
||||
{{- $hash := "sha384-fPPwDm9Mfp/tF9MgxjA4B33PPUlNmlXdP3oKSJgdAywm+cfAEYllAIRl/D3SBlpc" -}}
|
||||
{{- $url := "https://cdnjs.cloudflare.com/ajax/libs/fancyapps-ui/5.0.35/fancybox/fancybox.umd.js" -}}
|
||||
{{- $hash := "sha512-Jbl+VuuqPnKsz0QxpW0eFun5z3ftzXwFOGxA75I5+o7zlY5uFu+FmGp9mY3BEso+f3Ej4YtFtnUGeKwHU/YVvA==" -}}
|
||||
<script defer
|
||||
src="{{- $url -}}"
|
||||
integrity="{{- $hash -}}"
|
||||
crossorigin="anonymous"></script>
|
||||
{{- $url := "https://cdnjs.cloudflare.com/ajax/libs/fancybox/3.4.0/jquery.fancybox.min.css" -}}
|
||||
{{- $hash := "sha384-Ewh0nI9dXkThksh2nOTHmr8wAk5UlhiE2FiGSuZSnYkQ/G1W5wPuXGBnXodqD8GC" -}}
|
||||
{{- $url := "https://cdnjs.cloudflare.com/ajax/libs/fancyapps-ui/5.0.35/fancybox/fancybox.min.css" -}}
|
||||
{{- $hash := "sha512-iYdUaD/DKwJeYpOBlNLwBcGtJj/GSrFDzbPAqye/+IB/Fz6vwRekM2Wqi53sIgxCfaKp3uXpdT666ehkGP1qhw==" -}}
|
||||
<link rel="stylesheet"
|
||||
href="{{- $url -}}"
|
||||
integrity="{{- $hash -}}"
|
||||
|
Reference in New Issue
Block a user