Conversation

Notices

1. きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Saturday, 26-Mar-2022 02:41:22 JST きゅーけー

   ACL2 で org-babel するの ACL2 公式と同様に acl2 のコードを *shell* に投げ込む仕様という激ヤバなんでちょっと公開しにくいんだよなあ……。

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Saturday, 26-Mar-2022 02:43:50 JST きゅーけー

     in reply to

     たしかに *shell* バッファで作業しても実際のところなんら問題ないんだけどいつか事故りそう。

     私のPCに defun とか dethm みたいな名前の危険なコマンドを仕込まれるとやばいし、他の人い同じような危い目にあわせるわけにもいかない。(まあ侵入された時点で終わり感あるけど)