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

二分木に要素を追加しても全てのノードのキーが、左の木の全てのノードのキーよりも大きく、右の木の全てのノードのキーよりも小さくなることを証明した。

補題を思い付くのが難しい。たぶん3時間くらいかかった。

https://gitlab.com/tojoqk/practice-acl2/-/blob/b9222e3aad3d4c8d9eb78a04f49621e56e13a718/binary-tree.lisp

#ACL2

ACL2 でブラックジャックの勝敗判定を実装してみた。
Lisp だけど全ての関数が停止することを証明しているし、重要な関数の戻り値が期待したものになることも証明している。静的型付けとは異なる証明への道へ歩み始めた。

https://gitlab.com/tojoqk/blackjack/

Guile で動く定理証明支援系を作った。だいたい自分の望むものは手に入ったので、とりあえずはこれを使って『定理証明手習い』を一周してみようと思う。

https://gitlab.com/tojoqk/vikalpa

開発者による支配から身を守るために自由ソフトウェアを使いましょう
https://www.tojo.tokyo/freedom-for-yourself.html

Amazon の定期便でコーラゼロを購入するのやめた。カフェイン依存を止めたい。

低位舌の問題は多岐に渡るのに、主に情報を発信しているのが歯科というのはちょっと違和感がある。

カレンダーやタスク管理により一般的な caldav を使うか、それとも org-mode で管理するかという迷いがあったんだけど、EXWM を使っていたら圧倒的に org-mode の方が快適なので org-mode にした。これでもう Emacs からは一生離れられなくなった。Orgzily という Android アプリがあって、これを使えば Android でもカレンダーやタスクの確認と編集ができるのでたぶん生きていける。

最近 laptop の環境を最高にすることしかしてない。org-mode を本格運用できるようになりそうだけど特に趣味開発的な進捗はないという感じ。

さっきの GNU IceCat で、GitLab にログインできない話、Guix System 使ってるせいだったらやだな。おまかん説は完全には否定できない……。

EXWM ユーザーなので、org-mode の babel をアプリのランチャーとして使ってる。結構快適だ。
具体的には
#+BEGIN_SRC emacs-lisp
(start-process-shell-command "GitLab" nil "chromium --app=chromium --app=https://gitlab.com/")
#+END_SRC
みたいに書いて `C-c C-c` で実行してる。

うう、全てのアドオンを無効にして試したけどやっぱだめだった。諦めよう。。。

ネットサーフィンしているときにプライバシーに気を使ったプラグインがたくさん入っている安全そうなやつを使って、Mastodon とか GitLab みたいな Web アプリには、ungoogled-chromium のデフォルト設定で起動するというのはそこそこ合理的な選択なのではないかと思っている。

Enhanced Tracking Protection を Custom に選択して全て無効にしてみたけどやはり、GNU IceCat で GitLab にログインできなかった。とりあえず、Web アプリぽいもの(GitLabを含む)は全て ungoogled-chromium の `--app=` を使って起動する運用であんまり困らなそうなので諦めたい。

正確には5秒待つとリロードされて、同じ画面が表示されてしまう。

しばらくまっても一生そのままですね……

GNU IceCat で GitLab にログインしようとすると、下記のメッセージが表示されてログインを施行することすらできない。

> Checking your browser before accessing gitlab.com.
>
> This process is automatic. Your browser will redirect to your requested content shortly.
>
> Please allow up to 5 seconds…

以前はそんなことは起きていなかったような気もする。

GNU IceCat で今困ってることリスト(たぶん LibreJS は関係ない)

* 何故か通知が機能しない
* GitLab にログインできない
* Jitsi Meet が使えない

こういうネットサーフィンを越えた領域の作業をするときに困るのは全部 Web アプリのせいなので、Web アプリには ungoogled-chromium を使うことにした。

普通にインターネットサーフィンをするときは IceCat を使ってWebアプリを起動する場合は ungoogled-chromium を使うという使い分けを始めた。