Pinned post

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

Pinned post
Pinned post

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

Pinned post

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

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

Show thread

去年から作ってた自作の定理証明支援系、実用的な状態にまで持っていくのが絶望的に難しいということで放置してたんだけど、『定理証明手習い』(ラムダノート社)を読むときに限って有用な可能性があるのでしばらくしたら記事を作ろうと思ってる。 

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

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

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

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

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

軽い気持ちで brew upgrade したら大変なことになっているのが今です

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

Show thread

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

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

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

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

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

Show thread

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

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

Mastodon に CI の通知をする設定はこれ。
git.tojo.tokyo/ci.git/tree/aft

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

Show thread

# :lispworks7.0'|
🐱メモリ食い潰し系は処理系だけ落ちれば良いけど大抵OSも道連れなことが多い。気付いて途中で割り込めればセーフだけど
🕥|

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

# :lispworks7.0'|
🐈個人的にはLisp処理系がメモリ食い潰して落ちる方が厄介だなと思ったりする(CLでもSchemeでも何度か経験ある)

Guile ではスタック溢れを気にせず再帰しよう
tojo.tokyo/guile-recursion.htm
🕙|

Show older
Mastodon

The social network of the future: No ads, no corporate surveillance, ethical design, and decentralization! Own your data with Mastodon!