WSLにcoq-jupyterをインストールする

記事の内容が古くなったので書き換えます。

Windows11のWSL(Ubuntu 22.04)で、JupyterLab上でCoqが使えるようにする。

1. WSL2(Ubuntu 22.04)のインストール

自前の環境では素直にインストールできなかったので、作業手順をまとめる。

1-1. Ubuntuのインストール

PowerShellを起動し、コマンドwsl --installを実行する。
途中でユーザ名とパスワードの入力がある。

PS> wsl --install
インストール中: Ubuntu
Ubuntu がインストールされました。
Ubuntu を起動しています...
Installing, this may take a few minutes...
Please create a default UNIX user account. The username does not need to match your Windows username.
For more information visit: https://aka.ms/wslusers
Enter new UNIX username: kioto （ユーザ名を入力）
New password:　（パスワードを入力）
Retype new password:　（上記と同じパスワードを入力）
passwd: password updated successfully
Installation successful!
To run a command as administrator (user "root"), use "sudo <command>".
See "man sudo_root" for details.

Welcome to Ubuntu 22.04.2 LTS (GNU/Linux 5.15.90.1-microsoft-standard-WSL2 x86_64)

 * Documentation:  https://help.ubuntu.com
 * Management:     https://landscape.canonical.com
 * Support:        https://ubuntu.com/advantage


This message is shown once a day. To disable it please create the
/home/kioto/.hushlogin file.
PS>

1-2. ネットワークの設定

インストール直後、DNSの設定が正しくないことが原因でaptコマンドでネットワークエラーが発生することがある。その場合は、以下の手順を実施する。

ネットワークエラーの原因は、/etc/resolv.confのnameserverの設定が正しくないためであるが、このファイルはWSL2が自動で生成している。
ここで/etc/resolv.confのファイル情報を見てみる。

$ ls -l /etc/resolv.conf
lrwxrwxrwx 1 root root 20 May  7 17:42 /etc/resolv.conf -> /mnt/wsl/resolv.conf
$ ls -l /mnt/wsl
docker-desktop/  docker-desktop-data/  resolv.conf

このように、元は/mnt/wsl/resolv.confにあるものがシンボリックリンクされていることが分かる。

(1) resolv.confの自動生成を抑制させる

ネットワークエラーの原因は、/etc/resolv.confのnameserverの設定が正しくないためであるが、このファイルはWSL2が自動で生成している。まずは、この自動生成を抑制させる設定を行う。

vi等のエディタを使用して、/etc/wsl.confに以下の行を追加する。

[network]
generateResolvConf = false

(2) /etc/resolv.confを作り直す

シンボリックリンクを削除して、vi等のエディタで新規に作成する。

$ sudo rm /etc/resolv.conf
$ sudo vi /etc/resolv.conf

ファイルの内容は以下の通り。8.8.8.8は適当なDNSサーバを指定する。

nameserver 8.8.8.8

pingなどで外部ネットワーク接続を確認する。

$ ping www.google.com
PING www.google.com (142.251.222.36) 56(84) bytes of data.
64 bytes from nrt13s72-in-f4.1e100.net (142.251.222.36): icmp_seq=1 ttl=55 time=10.8 ms
64 bytes from nrt13s72-in-f4.1e100.net (142.251.222.36): icmp_seq=2 ttl=55 time=9.87 ms
64 bytes from nrt13s72-in-f4.1e100.net (142.251.222.36): icmp_seq=3 ttl=55 time=15.3 ms
...

2. ソフトウェアのインストールと初期化

以下のコマンドを実行する。最初に一度実行しておくだけでよい。

sudo apt update
sudo apt upgrade -y
sudo apt install -y python3-pip coq jupyter-core
echo "PATH=~/.local/bin:\$PATH" >> ~/.bashrc
. ~/.bashrc
pip3 install --upgrade pip
pip3 install jupyterlab coq-jupyter
python3 -m coq_jupyter.install
jupyter lab --generate-config
jupyter lab password  # 対話形式でパスワードを設定

3. JupyterLabの起動

以下のコマンドを実行する。

jupyter lab

• Windows上のブラウザからhttp://127.0.0.1:8888/lab にアクセスすると、Jupyterのログイン画面が表示
• パスワード入力画面になるので、上記で設定したパスワードを入力すると入れる

4. 付録

チュートリアルの取得

Coqのチュートリアルをcloneでとってくる。そのディレクトリ下でjupyterを起動すると便利。

git clone https://github.com/maruyama097/coq-tutorial.git
cd coq-tutorial
jupyter lab

以上