Hello All,
I am installing HOL for the first time. I have already installed polyml as
per the instructions given by its developers.
However, I face the following problem while smart-configuring.
Can anybody point out what I should do to fix it?
[mpu@camugnano .../TheoremProvers/hol4.k.7]$ ../polyml.5.4.1/bin/poly <
./tools/smart-configure.sml
Poly/ML 5.4.1 Release
> # # # # # # # # # # #
HOL smart configuration.
Determining configuration parameters: holdir OS poly polymllibdir
OS: linux
poly:
/net/camugnano/dataL/mpu/CryptographyVerification/TheoremProvers/polyml.5.4.1/bin/poly
polymllibdir:
/net/camugnano/dataL/mpu/CryptographyVerification/TheoremProvers/polyml.5.4.1/lib
holdir:
/net/camugnano/dataL/mpu/CryptographyVerification/TheoremProvers/hol4.k.7
dynlib_available: false
Configuration will begin with above values. If they are wrong
press Control-C.
Will continue in 1 seconds.
Loading system specific functions
Compiling system specific functions (sig sml)
Beginning configuration.
Making tools/mllex/mllex.exe.
Poly/ML 5.4.1 Release
> # Making tools/mlyacc/mlyacc.exe.
/net/camugnano/dataL/mpu/CryptographyVerification/TheoremProvers/hol4.k.7/tools/mllex/mllex.exe:
error while loading shared libraries: libpolyml.so.3: cannot open shared
object file: No such file or directory
Failed to build mlyacc.
[mpu@camugnano .../TheoremProvers/hol4.k.7]$
Thanks
Mitra
------------------------------------------------------------------------------
Don't let slow site performance ruin your business. Deploy New Relic APM
Deploy New Relic app performance management and know exactly
what is happening inside your Ruby, Python, PHP, Java, and .NET app
Try New Relic at no cost today and get our sweet Data Nerd shirt too!
http://p.sf.net/sfu/newrelic-dev2dev
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
