きゅーけー @tojoqk@mastodon.tojo.tokyo

過去に作った Jami のアカウントをなくしてしまったので、Jami のアカウントを再度作り直しました。今回はなくないようにちゃんとバックアップも取ってます。
私に Jami 経由で話しかけたいという謎な人はどうぞ。

id: e5fdfccb74c383420e6e647897dae018a4bd61fb

emacs に (setq system-time-locale nil) と記載しておくことで Emacs の異常動作を直せることが分かっ
た

あー、これは format-time-string に謎の副作用があるっぽいな。これ C のコードらしいのでつらい。

ある Emacs Lisp のコードを利用すると突然 org-mode のタイムスタンプが漢字から英語になっちゃう問題の原因っぽいものを特定した。

ダイナミックスコープを利用して一度 system-time-locale を "C" にして format-time-string をすると、再度 format-time-string をすると system-time-locale が "C" のままになる。

これはきつい。

う、ACL2 の arithmetic ライブラリをロードしようと思って調べたら雑な自分の記事がでてきてつらい……。Japan を有効にしてなければ出てこないだけ幸いである。

これ
> 証明に成功しました。定理ライブラリの力は凄いですね。
とか書いてあるやつなので検索されて見つけられるの恥かしいんだよな。

ACL2 でもやった(ただ計算によって比較しただけなので、この定理証明に ACL2 のうまみはない)。
これを一般化したようなものを証明できたら凄そうだけど大変そうなのでやらない。

こんな感じでちゃっちゃっと求められてしまう(動画のネタバレ回避のため閲覧注意)。

`cons` の型を確認したところ、どうやら Lisp の `cons` ではないことが分かった。まあ、こればっかりはしょうがないな……。Lisp のただの対としての cons は静的型付きだと結構無理あるし。

Typed Racket は無理を通していて、`cons` は Racket の `cons` のままなんだけど。

おお、+ が型クラスを使った型定義になってるー！すごい……。型クラスが Lisp の手に……。

Coalton が末尾再帰の形式にしてくれない件は sbcl であれば (optimize (speed 3) (safety 0)) を指定することで回避できた。

あ、coalton 側で tail recursion の最適化はしてくれないっぽいな。普通に SB-KERNEL::CONTROL-STACK-EXHAUSTED って言われてしまった。下の関数に (neko 100000) って入れただけなのに。これは回避法の模索が要るな。
Coalton が関数型言語である以上、処理系に依存してでも末尾再帰は最適化されて欲しいところがある。

おおお、ちゃんと Coalton 動くー！すごい。Common Lisp で静的型付きプログラミングできるし型クラスまであるぞ！

init が Guile で動いていることが分かる画像。

忙しい人はまあこれだけ見ればなんで山本一太群馬県知事が「魅力度ランキング」なるものに対してあんだけ攻撃的な態度(なお、本人としては冷静であり攻撃的な態度をしているとは認識していない様子)をとっているのか分かるだろう。
既に7月の時点で群馬県庁サイドによる「魅力度ランキング」に対する分析を終えていて、ブランド総合研究所は「魅力度ランキング」という名称に相応しい調査ができているとはいえず、杜撰なランキングであるという結論を出した上で、再度ブランド総合研究所が魅力度ランキングを発表し、メディアがそれを取り上げて社会的な影響を与えたという文脈があるわけだ。

いきなり山本一太知事が怒りくるったわけではないことがよく分かる。

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

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

謎の stash をしてしまった。絶対忘れそう。

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

コード: https://git.tojo.tokyo/acl2-theorems.git/tree/combinations.lisp?id=975418f4c2e1520649196458d3211e6ef9ec531a
ACL2 の出力: https://ci.tojo.tokyo/jobs/acl2-verify/412

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

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