Notices by きゅーけー (tojoqk@mastodon.tojo.tokyo), page 170

自前 OpenVPN サーバを GNU Guix System に移行した。easyrsa パッケージがないという理由で先送りしてたけど easyrsa は他のパッケージに深く依存しないスクリプトだったのでパッケージマネージャーに頼るほどのものではなかった。

気圧と体調の関連性に自然に気づける人すごいと思う。

気圧と体調、私にも関係あるのかもしれない。

org-babel を ACL2 に対応させるの acl2-mode とかを先に作らないといけなそうで大変そうで気が進まない。

本当は Jupyter Notebook ではなくて、org-mode を使いたい気持ちがあるんだけど、Jupyter Notebook でも私が求めている水準には達していたので org-babel に acl2 を対応させるまでは Jupyter Notebook を使いそう。

変えさ -> 返さ

デジタル庁のように Nginx のエラーページを変えさないように、50x のページも作った方がいいかな。でも静的ファイルしか置いてないのでエラーページを返せるなら記事も返せるはずなんだよな。。。

私が書いた記事のなかでこれが最も面白いと思う。https://www.tojo.tokyo/404-not-found.html

Jupyter notebook いいかもしれない。これで ACL2 の記事をいっぱい書けそう。

寝る直前に急いで書いたので明日色々直すかも……

acl2-kernel を使って ACL2 の記事を書いてみたhttps://www.tojo.tokyo/len-combinations.html

でも、(len (cons-all e x)) が (len x) と等しいとかは証明してないのに自動証明されたのは今までの感覚とはちょっと異なる。やっぱり ACL2 の振舞いについてまだまだ分かってないことがあるな。

たしかに、combinations 関数と comb 関数は似ているので、自動証明できるのはそんなに不思議な話ではない気もする。

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

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

頼まれごとして簡単なプログラムを書いたんだけど、最初は ACL2 でやろうとして、ちょっと時間かかりそうだったので GNU Guile、って思ったけど最終的に Racket で解いてしまった。battery included の便利さを実感してしまった。

GCL、4ヶ月前にコミットされてるし意外とメンテナンスされていのでは。環境を GNU で揃えるために、ACL2 も GCL で動かそうかな。https://git.savannah.gnu.org/cgit/gcl.git/log/

せめて「JavaScript を有効にしてください」とか言って欲しかった感ある。

GNU IceCat の Third Party Connection を監視できるやつ超良い。これでブロックしまくりながらインターネットするの楽しい。

Twitter でも機能しないな。

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