Coq(とか)のバージョンを簡単に切り替えたいスクリプト

More than 1 year has passed since last update.

最近は trunk 使ってると早々に maybe bugged tactic 言われるので Universe Polymorphism 辛い。

何があったのか

以前に Emacs Lisp でごちゃぁ...っと書いた んですが、
よく考えたら別に Emacs Lisp で書く必要もないなぁと思いました。

Coq の場合、使うバイナリさえ変えればライブラリの読み込みとかもどうにかなるので、
switch-coq 的なコマンドを作って利用するバイナリを切り替えればよいのです。

何をやったのか

シンボリックリンクの行き先を切り替える方式にして、シェルスクリプトをちょちょいと書きました。

端的にまとめると、

  1. coq/ ディレクトリを適当な場所に用意する
  2. coq/ 下にバージョンごとのディレクトリ、あるいはシンボリックリンクを置く
  3. パスの通った場所に coq/version/bin へのシンボリックリンクを置く
  4. 3. のシンボリックリンクを切り替えるスクリプトを作る

となります。

スクリプトと仕様

以下にスクリプトを載せます。

switch-coq
#!/bin/bash

STABLE="8.4pl6"
BETA="8.5beta2"
TRUNK="trunk"

DEFAULT=${TRUNK}

if [ $# -ne 1 ]; then
    coqver=${DEFAULT}
else
    case $1 in
    t ) coqver=${TRUNK};;
    b ) coqver=${BETA};;
    s ) coqver=${STABLE};;
    * ) coqver=$1;;
    esac
fi

COQDIR="/usr/local/coq/${coqver}"
BINLINK="${HOME}/bin/coq"

if [ -d ${COQDIR} ]; then
    echo "change coq version into ${coqver}"
    unlink ${BINLINK}
    ln -s "${COQDIR}/bin/" ${BINLINK}
else
    echo "version ${coqver} not found."
fi

switch-coq は引数をひとつ取ることが出来て、バージョン名を直接与えればそのバージョンに、指定された文字を与えれば予め設定されたバージョンに切り替えようとします。

引数がない場合のデフォルト値もあると楽なので、そうしてあります。

バージョン名が不正だった場合、デフォルト値に設定するか否かは悩みどころですが、今回は変化を与えないことにしました。余計なことはしないスタイル。

下準備 of スクリプト使う

上のコードだけで大体使い方はわかると思うのですが、自分の脳の信頼性を考慮し、
スクリプトを動かす前の下準備を以下にざらりと列挙していきます。


まず、適当な場所に coq/ ディレクトリを用意します。
私は /usr/local/ 下に置きました。

$ mkdir -p /usr/local/coq

次に、 Coq をいっぱいインストールします。
バージョン毎に分けるには色々やりかたありますが、一番楽なのは

$ ./configure --local

してインストールする方式でしょうか。
あるいは --prefix オプションで直接 coq/ 下に置いてもよいかもしれませんが、
trunk は大抵 --local で入れるので、他のバージョンもそうしています。

coq/ 下に直接置かなかった場合はリンクを貼っておきましょう。

$ ln -s /coq/no/version/wo/oita/tokoro/ /usr/local/coq/version

そして、最後にパスの通った場所に Coq の bin/ へのリンクを置きます。
このリンクはスクリプトの BINLINK に対応しています。

$ ln -s /usr/local/coq/8.4pl6/bin ${HOME}/bin/coq

以上の準備を終えれば、スクリプトを利用できます。

補足

この方式別に Coq に限定する必要なくて、実際ちょちょいと書き換えて GHC の切り替えとかにも使ってるんですけど、
「まぁ、Coq タグつけてもいいかな、一応、これの続きだし」
ということでこんな感じです。

あと、シェルスクリプト周りにまるで強くないので、何かありましたらコメントいただけるとありがたいです。

注意事項

このスクリプトで切り替えを行っている時、Coq のライブラリをインストールする場合は make install を使いましょう。
make userinstall すると困ったことが起こります。

具体的に言うと、 Coq の標準ライブラリと名前が被っているモジュールがあった時、
参照されるモジュールが変わってしまって Coq のビルドが失敗します。

make install は Coq をインストールした場所が基準なのでバージョンごとに変わるのですが、 make userinstall は共通の場所になってしまうことが原因です。

以下に Makefile 内でインストール場所を設定している部分を引用しておきます。

##################
#                #
# Install Paths. #
#                #
##################

ifdef USERINSTALL
XDG_DATA_HOME?=$(HOME)/.local/share
COQLIBINSTALL=$(XDG_DATA_HOME)/coq
COQDOCINSTALL=$(XDG_DATA_HOME)/doc/coq
else
COQLIBINSTALL=${COQLIB}user-contrib
COQDOCINSTALL=${DOCDIR}user-contrib
endif

Coq のライブラリの Makefilecoq_makefile コマンドを使って自動生成するものなので、この部分に手を加えるのは手間です。

coq_makefile をいい感じに書き換えたところで Coq がライブラリを探す場所をどうにかせんといかんので、手を出したくないなぁって感じです。

make install しておくのが無難ですね。