投稿

10月, 2019の投稿を表示しています

「はじめてのCoq」 予習用の環境構築について

「はじめてのCoq」ハンズオンにお申込みいただいてありがとうございます。 当日の演習課題部分(講義資料は含まれていません)を、GitHubに公開しました。 https://github.com/maruyama097/coq-tutorial どんな感じの演習課題なのかは、GitHubで確認できると思います。 git clone  https://github.com/maruyama097/coq-tutorial  していただければ、 ご自身のマシン上に展開できると思います。 ハンズオン、coqとcoq−jupyter(この資料は、coq−jupyterの上で動きます)のインストールの手間を省いて、クラウドとブラウザー・ベースでやろうと思っていたのですが、作業をしていて、あることに気づきました。今更ですが。 演習課題配っても、coqとcoq−jupyterをインストールしていない限りは、この資料動かないですね。(GitHubでは、イメージは見れるのですが、課題は動きません。) それに、ハンズオンの当日以外には、coqとcoq−jupyterの環境を、持っていない人は、資料を復習することも、自分でcoqの学習を進めることもできないですね。 ハンズオンのやり方を変えようと思っています。今回のハンズオンを機会に、自分のマシン上でcoqとcoq−jupyterが動くようにするのがいいのではと考え始めています。お時間があったら、coqとcoq−jupyterのインストールをおためしください。 一番簡単な、coqとcoq−jupyterのインストールの方法は、anacondaを使う方法だと思います。まず、anaconda をインストールします。次の資料が参考になると思います。 「Anaconda を Windows にインストールする手順」https://weblabo.oscasierra.net/python-anaconda-install-windows/ 「Anaconda を macOS にインストールする手順」https://weblabo.oscasierra.net/python-anaconda-install-macos/ いったん、anacondaがインストールされると、次の手順で、coqとcoq−jupy