KLMLean runtime error on Linux
Update (2014-06-02): with the author's assistance, this error was resolved. The key step was to recompile the .pl files into .sav files using SICStus. No doubt this procedure would also resolve the same error described on Windows further below, however I did not confirm this. The commands to perform this recompilation, from within SICStus, after first downloading from the link above the .pl files into your klmlean installation directory, and then replacing in the below /path/to/klmlean with the appropriate value for that directory, are:
compile('/path/to/klmlean/tpt.pl'), save_program('/path/to/klmlean/tpt.sav').
compile('/path/to/klmlean/tclt.pl'), save_program('/path/to/klmlean/tclt.sav').
compile('/path/to/klmlean/tct.pl'), save_program('/path/to/klmlean/tct.sav').
compile('/path/to/klmlean/trt.pl'), save_program('/path/to/klmlean/trt.sav').
compile('/path/to/klmlean/trtfree.pl'), save_program('/path/to/klmlean/trtfree.sav').
Now, to run KLMLean, enter the following command, after first replacing /path/to/sicstus (2 occurrences) and /path/to/klmlean with the correct values:java -classpath /path/to/sicstus/bin/jasper.jar:/path/to/klmlean/ -Djava.library.path=/path/to/sicstus/lib Vai
Note also that my test input below is not well-formed, because capital letters are invalid.
The following describes the error I encountered in my attempt to run the KLMLean application so as to add its features to my comparison of free proof tree software. I first attempted to run the application on a 64-bit Intel CPU ASUS laptop running 64-bit Fedora Linux. I followed the instructions on the page linked to above as best I could, tailoring them to Linux as seemed appropriate. In particular, I:
- Downloaded and extracted the KLMLean zip into /usr/local/klmlean.
- Downloaded and extracted JGraphT 0.7.0 into /usr/local/jgrapht-0.7.0.
- Downloaded and installed an evaluation version of SICStus Prolog to /usr/local/sicstus4.3.0.
- Created /usr/local/klmlean/run.sh with the following content:
#!/usr/bin/bash cd /usr/local/klmlean export PATH=$PATH:/usr/local/sicstus4.3.0/bin export CLASSPATH='.:/usr/local/sicstus4.3.0/lib/sicstus-4.3.0/bin/jasper.jar:/usr/local/jgrapht-0.7.0/jgrapht-jdk1.4.jar;/usr/local/jgrapht-0.7.0/jgrapht-jdk1.5.jar;/usr/local/jgrapht-0.7.0/lib/jgraph.jar' java Vai
- Marked /usr/local/klmlean/run.sh as an executable.
I already had a Java runtime environment installed. Upon executing /usr/local/klmlean/run.sh, KLMLean's graphical user interface appeared, and I was able to type a formula into the bottom formula bar (I typed "A => B"). When I clicked "Prove", however, the terminal window from which I'd run the program output the message "ERROR connecting to SICStus Prolog engine". I was thus unable to display any proofs.
KLMLean runtime error on Windows
Next, I attempted to run KLMLean on 64-bit Windows 7. In particular, I:
- Downloaded and extracted the KLMLean zip into C:\Users\netocrat\Software\klmlean.
- Downloaded and extracted JGraphT 0.7.0 into C:\Users\netocrat\Software\jgrapht-0.7..
- Downloaded and installed an evaluation version of SICStus Prolog to C:\Program Files\SICStus Prolog VC12 4.3.0.
- Installed Java SDK 7.0 update 55 to C:\Program Files\Java\jdk1.7.0_55.
- Edited C:\Users\netocrat\Software\klmlean\klmlean.bat to the following:
set path=c:\Program Files\Java\jdk1.7.0_55\bin;C:\Program Files\SICStus Prolog VC12 4.3.0\bin;C:\Programs\j2sdk1.4.2_13\jre\bin\client set classpath=C:\Program Files\SICStus Prolog VC12 4.3.0\bin\jasper.jar;C:\Users\netocrat\Software\klmlean;C:\Users\netocrat\Software\jgrapht-0.7.0\jgrapht-jdk1.4.jar;C:\Users\netocrat\Software\jgrapht-0.7.0\jgrapht-jdk1.5.jar;C:\Users\netocrat\Software\jgrapht-0.7.0\lib\jgraph.jar; java Vai
The results of running C:\Users\netocrat\Software\klmlean\klmlean.bat were then exactly the same as under Linux: KLMLean's GUI appeared, but when I clicked "Prove" after typing in a formula, the terminal window output "ERROR connecting to SICStus Prolog engine".
