いけたわ……。Emacs がダイナミックスコープであることを利用して let で org-capture-templates を束縛してから org-capture を呼び出す関数を定義すれば文脈に応じて別の org-capture を呼びだせる。
これで org-capture の可能性が爆発的に広がった。TODO で t が既に取られているから体温は T にするかーとかもう考えなくていいんだ……。

Show thread

お、NHK のニュースサイト、Nextcloud の External sitesで表示できるじゃん。これ禁止していないんだ。Nextcloud のダッシュボード使ってないし、これをブックマークしておけばよさそう。

さっきの頼まれごとの正体は文字列のリストから n 個を取りだす全ての組合せを求めて欲しいというものだったんだけど、ACL2 で実装した。とりあえず組合せの数に関する定理を書いたら補助定理なしで自動証明できてしまって驚いた。

コード: git.tojo.tokyo/acl2-theorems.g
ACL2 の出力: ci.tojo.tokyo/jobs/acl2-verify

Show thread

LibreJS に苦情を言う機能が付いてたんだけど、Contact ページの推測に失敗したみたい。

デジタル庁のサイトを GNU IceCat のデフォルト設定で開いたときの画面

ACL2 さん、これを自動証明してくるのは楽でいいんだけど自動証明されるのでデモにならなくて困るな。
(0 から n までの総和が n 番目の三角数であることを自動証明してくれた)

おお、permissions-policy: interest-cohort=() きてた!
これで FloC 対策完了だ。アップデートしてよかった。

ssh の公開鍵を送るのに Vultr コンソールのクリップボード機能を使ってみようと思ったら、ポインタがちょっとずれて、マストドンを再起動してしまった。

折角なのでスクショとっておいた。メンテナンスページへのリダイレクトがキャッシュされてしまってトップページに辿りつくことができない。問い合わせがたくさん来そうなミスで辛そう。

Show thread

うー、これはダサい。もっと小さい自由な Wifi の無線アダプタが欲しい。

Show thread

むー、GNU IceCat へインストールするの厳しそうだな。プロファイルを分けて起動するか……。

Show older
Mastodon

The social network of the future: No ads, no corporate surveillance, ethical design, and decentralization! Own your data with Mastodon!