HOLのinstallの仕方

Menu Menu

MOSCOW ML を取って来る

wget http://www.cs.uu.nl/people/arthurvl/mosml-macosx.patch wget http://www.dina.kvl.dk/~sestoft/mosml/mos201src.tar.gz

HOLを取って来る

http://sourceforge.net/project/showfiles.php?group_id=31790

    kananaskis-4.tar.gz 

このあたりは、

    naha:/net/open/Language/HOL

にあります。

mosml は、

    tar zxvf mos201src.tar.gz

で、そこで

  patch -p0 < mosml-macosx.patch

でパッチを当てます。さらに、

    src/Makefile.inc

の/lib/cppを、/usr/bin/cpp に書き換えます。

    CPP=/usr/bin/cpp -P -traditional -Dunix -Umsdos

これで、

    make world
    make  install

すると、

    ~/mosml

が出来ます。

自分のシェルのパスに、

    $HOME/mosml/bin

を通します。

次は、HOLのinstall

hol/Tools の下にいって、

    mosml < smart-configure.sml

とします。

hol の下にいって、

    bin/build

します。