Conversation

Notices

1. きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Thursday, 16-Sep-2021 17:46:50 JST きゅーけー

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

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

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

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Thursday, 16-Sep-2021 17:48:28 JST きゅーけー

     in reply to

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