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

って、思ったけど Vim の Org-mode のプラグイン作っている人いるじゃん。実は既に解決しているのでは。

jceb/vim-orgmode: UNMAINTAINED looking for maintainers! Text outlining and task management for Vim based on Emacs' Org-Modehttps://github.com/jceb/vim-orgmode

Vim でも VSCode でも Org-mode が使えるようになれば Org-mode の文書を Emacs ユーザーじゃない人とでもやりとりできるようになるんだ……。そうなってほしい……。

Emacs 以外でも Org-mode が使えるようになって欲しい気持ちがある。Org-mode は完全に Emacs の世界に閉じてしまっていて他者とのコミュニケーションが絶望的になるという問題を抱えている。

Org-mode のファイルはただのプレーンテキストなわけで技術的には Emacs でなくたっていいはずだから……。

Emacs の設定にたいして literate programming をするのは実際に可能で、下記を参考にしようと思ってる。

dotemacs/dotemacs.org at master · angrybacon/dotemacshttps://github.com/angrybacon/dotemacs/blob/master/dotemacs.org

どうせ公開しないんだし、もう Emacs の設定も Org-mode から出力するようにしちゃおうかな。

Emacs の設定は以前は公開してたんだけど、もうプライベートな設定が多すぎて公開するの無理だわ……。

記録するときは Emacs 上で C-c c s って押すだけ。

ちゃんと表計算してて睡眠時間は自動で記録されるようにもなってる。もう全部 Org-mode でいい……。

例えば、睡眠の記録は下記の設定でいける。強すぎる。

```("s" "睡眠の記録" table-line (file+headline "~/org/health.org" "睡眠の記録") "| %^U | %^U | %^{気分: 5段階} | | | %? |" :prepend t :jump-to-captured t)```

```(setq org-table-automatic-realign nil)```を設定しておかないと謎の空行が表に挿入されちゃうのでそれは注意。

最初は Nextcloud Health で記録してたんだけどちょっと融通が効かないのが問題になって Emacs の Org-mode に移行したんだ。

Org-mode に移行してからは融通は効くようにはなったんだけど、自分で表に追記するのがちょっと面倒なのがつらかった。でも Org-capture で追記できるこを知って解決しちゃった。Org-capture のインターフェースは Nextcloud Health よりも快適なんでこれで Org-mode が上位互換になった。

org-capture で table-line というのを使うことで表に追記できるということを知ってしまった……。これもう Emacs の Org-mode に勝てるツールこの世に存在しないんじゃないだろうか。体調について記録しないといけないのだけど、そもそも記録するのがつらい問題がこれで完全に解決した。

表に追記したらグラフも自動生成できるし、そのまま文書として html で出力できて良い感じの見た目になるのでもう隙がない。これは終わった。私は一生 Emacs を使うことになる。

めっちゃ揺れた

ACL2 だとあらゆる値が入っても停止性が証明できるように関数を書かないといけないので、真リストがくるという仮定を置かずに atom とか endp を使って基底部の判定をしないといけない。

わかる。あの構文のセンスはやばい。(lambda x x) とかもできる。

Scheme で手続き作るときに引数リストの cdr 部分に optional な引数が入るの、マジで天才的だと思ったわ

Lisp の真リストって社会的にそれを真リストとみなしているだけで真リストというデータ型があるわけじゃないからな。

cons := (λcab. c a b)とかがありがちな定義だったはず

機械語から遠い言語処理系の鶏と卵系の話、二村射影とかも面白い

RPythonについて軽く | κeenのHappy Hacκing Bloghttps://keens.github.io/blog/2017/12/12/rpythonnitsuitekaruku/

いや、ACL2 にも Lambda 式はある……。ただ第一級の値でないというだけで……。

マクロがあれば Lambda 式なくても耐えられる(暴論)。

定理証明の世界では直観主義論理が支配的な感じがしているけど、ACL2 のようなそうでない定理証明支援系もある。一階論理でも数学をやるんじゃなくてソフトウェアの性質について証明するならまあそんな困らないじゃないかと思ってる。