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

親ガチャの話までは受け入れられるけど、自由意志を否定する話になると受け入れられなくなる印象あるな。この2つの間のどこかに境界があるのだろうか。

夕方に寝た影響か全然眠れない。

しばらくパソコンの利用頻度が下がるので浮上頻度が下がりそう。このまえランニングコストをちょっと下げる対応をしておいて良かった。

Google 検索すると Chrome が見つかりやすいとかそういうことなんだろうか。

はっきりいってユーザーから見て Web ブラウザとかどれでもいいと思うんだけどなんで Chrome にそんな偏るんだ……。

鳴って→なって

私がインターネットに触った頃はなんか Firefox 人気だったし狐でなんかかわいいし Firefox が好きに鳴ってずっと Firefox を使ってたんだけどいつの間にかに Chrome 大人気になってた。何があったんだろう。

Web界の事情に少し疎いところがあってなんでそんなに Chrome が人気なのか謎なんだよな。

今の状態だと「 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 に重要な情報が集まるようになったのでちゃんと定期的に自動バックアップするように設定した。