証明ツールHOL
4をインストールした。
Macintoshの${HOME}/Applications/hol へインストール。
VDMToolsで生成した証明課題を証明するため。
hol/bin/buildの実行で下記のようなUncaught
exception発生したが、config-overrideファイルに下記を記述することで成功。
val
OS = "macosx";
val dynlib_available =
false;
val holdir =
"/Users/sahara/Applications/hol";
ーーーーーUncaught
exceptionーーーーーー
Exporting
theory "ctl2mu" ... done.
Theory
"ctl2mu" took 10.710s to build
Analysing
ctl2muTheory.sml
Analysing
ctl2muTheory.sig
Compiling
ctl2muTheory.sig
Compiling
ctl2muTheory.sml
Analysing
ctl2muTools.sml
Compiling
ctl2muTools.sml
Analysing
ctlCheck.sml
Analysing
ctlTools.sml
Analysing
ctlSyntax.sml
Compiling
ctlSyntax.sml
Compiling
ctlTools.sml
Compiling
ctlCheck.sml
Analysing
decompScript.sml
Analysing
lazyTools.sml
Compiling
lazyTools.sml
Compiling
decompScript.sml
Linking decompScript.uo
to produce theory-builder
executable
Uncaught
exception:
Fail:
dlopen(/Users/sahara/Applications/hol/sigobj/muddy.so, 2): Symbol not found:
_stat_alloc
Referenced from:
/Users/sahara/Applications/hol/sigobj/muddy.so
Expected in: flaBuild failed in directory
/Users/sahara/Applications/hol/src/HolCheck
Posted: 月 - 6月 11, 2007 at 03:44 午後