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

そもそも人の行動は環境によって制御されているため自由などないという考えに至ると、環境をコントロールできない状況にあるということがどれだけ不自由なのかが明白になる。完全な自由などないということを知ることにより、コンピュータにおける環境であるソフトウェアをコントロールできることの価値が明らかになるのではないだろうか。
人の行動が環境から自由でないからこそ、自由ソフトウェアは重要なんだ。

やかん

ブラウザの実装についてはなんも知らないけどいま GNU IceCat を使っていること自体が、Firefox が自由ソフトウェアであるありがたみだったのだ。

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

今の状態だと「 Guix を使ってれば超簡単にインストールできるよ！まずは Guix をインストールしてね！」って感じになっちゃうのでなんか用意しないといけない。

本の中では J-Bob っていう定理証明支援系を使うように促されるんだけど J-Bob のインターフェースは結構つらかった(ミスがあると全部 `nil` って返ってくる)し、環境構築もなんか大変だった。

少し試してたところ Jupyter Notebook との相性が凄くいい、あとはエラーメッセージを親切にして環境構築をしやすいようにすれば普通に使ってもらえる気がする。

定理証明支援系 Vikalpa のテストコードはこんな感じ:
https://git.tojo.tokyo/vikalpa.git/tree/tests/test-vikalpa.scm

`guix package --rollback` がない世界とかつらすぎる。

気軽にアップグレードできない問題、純粋関数型パッケージマネージャ(Nix とか Guix とか、私は Guix しか使ってない)が流行れば解消しそうな気がするのでもっと流行って欲しい。

ACL2 の証明は Emacs の方が便利なことが多いからそれは残るか。あとは Emacs 上で bash の操作をするのも残るはず。

やばいな、Jupyter Notebook をメインに使うようになった影響で Emacs の利用時間が大幅に減っている。
このままいくと、Emacs はちょこっとプログラムを編集して git の操作をするツールになってしまう。

guix-jupyter なるものを見つけたんだけどこれは神すぎる。もうこれだけでよかった。

Jupyter Notebook、名前のとおりノートに適してるので良い。

睡眠時間は短かいけど目覚めはいいな。

復活しました。6GB ディスクが空きました。

VACUUM FULL するのでしばらくダウンタイム発生します。

Jupyter Notebook に重要な情報が集まるようになったのでちゃんと定期的に自動バックアップするように設定した。

Mastodon に CI の通知をする設定はこれ。
https://git.tojo.tokyo/ci.git/tree/after?id=c7a1cfeb5b7e28b26fa73ae1c27fa517040abe04

Laimnar CI は自由度が高くて本当によい。
Laminar CI をベタ褒めしている記事はこれ。
https://www.tojo.tokyo/laminar-is-best.html

CI からの通知を Mastodon で受け取れるようにした。
https://mastodon.tojo.tokyo/@ci/106928168549286055

toot のテスト

たしかに、何度か経験ある。メモリ4GBのラップトップのメモリを食い尽くして反応しなくなってなんどか強制終了した記憶ある。なぜ速やかに OOM で殺されてくれないんだろうか。