Kenneth MacKenzie wrote:
Enea Zaffanella writes:
[...snip...]
b) What is the output of the command echo $LD_LIBRARY_PATH on your machine? Does it include the path to your installation place, that is /afs/inf.ed.ac.uk/user/k/kwxm/libraries/lib ?
Let us know if either a) or b) solves the problem.
I have to admit that I'm very confused by this. I don't have LD_LIBRARY_PATH set, and you're correct in suggesting that if I set it to point to the location of my libraries then the test works OK.
Good.
However, I've been able to compile and link my own programs without the use of LD_LIBRARY_PATH with no problems, and I can also compile your test program without using it.
The LD_LIBRARY_PATH environment variable has not much to do with compilation and (compile-time) linking. Rather, it comes into play when you run your program and it needs to link dynamically to a shared library.
Here are the commands which interfaces/OCcaml/tests/Makefile executes when it's compiling test1:
OCAMLRUNPARAM='l=1M' ocamlc -o test1.cmo -c -I /home/kwxm/libraries/lib -I .. -ccopt -g test1.ml OCAMLRUNPARAM='l=1M' ocamlc -o test1 \ -cc "g++" -I /home/kwxm/libraries/lib -I .. -ccopt -g \ -cclib ../../../src/.libs/libppl.so -cclib ../../../Watchdog/src/.libs/libpwl.so -cclib -lmlgmp -cclib -lmpfr `echo " -lm -L/home/kwxm/libraries/lib -lgmpxx -L/home/kwxm/libraries/lib -lgmp -R/home/kwxm/libraries/lib -R/home/kwxm/libraries/lib " | /bin/sed -e "s/ -R[^ ]*//g" -e "s/ -/ -cclib -/g"` \ ppl_ocaml.cma test1.cmo
Note that the second command, which does the linking, explicitly mentions things like libppl.so and -lgmpxx.
If you run the above commands and then use ldd, you get the following:
ldd test1 linux-gate.so.1 => (0xb7fc4000) libgmpxx.so.4 => not found libgmp.so.3 => /usr/lib/libgmp.so.3 (0xb7f4e000) libppl.so.7 => not found libpwl.so.4 => not found libmpfr.so.1 => /usr/lib/libmpfr.so.1 (0xb7f0b000) ...
That is ok : it can't find libgmpxx.so.4 because the corresponding directory is not listed in LD_LIBRARY_PATH.
On the other hand, it can't find the ppl and pwl .so files because these libraries have not been installed yet (and they too are in a directory which is not listed in LD_LIBRARY_PATH).
In fact, when we *run* the OCaml tests, the command that gets actually executed looks like the following (to be run from path interfaces/Ocaml/tests):
../../../libtool --mode=execute -dlopen ../../../src/libppl.la -dlopen ../../../Watchdog/src/libpwl.la ./test1
Note that here we are dlopen-ing the just built ppl and pwl libraries, because we want to link with *THESE* libraries and not any other previously installed ppl library (which might be a different version).
On the other hand, we do not dl-open libgmpxx, because this is the library which is installed in your system ... i.e., this is the one that should be normally accessible using ld and LD_LIBRARY_PATH.
So in spite of all the options, it still doesn't know where to find libgmpxx.so. It turns out that if you make a directory containing only libgmpxx.so.4 and point LD_LIBRARY_PATH to it, then test1 still fails because it can't find libppl.so.7, and similarly for libpwl.so.4. Once it's got all of these it works OK though.
I spent some time experimenting and found that I could do the compilation with much simpler commands. To avoid the danger of interacting with my own previously-compiled version of PPL and other libraries, I made a directory called ~/gmp containing libgmp.a and libgmp.so*, together with the files gmp.a, gmp.cma and gmp.cmxa from mlgmp. I can compile test1.ml by saying
ocamlc -c -o test1.cmo -I ~/gmp -I .. test1.ml
This is pretty much the same as what's in the makefile. I think that at this stage it just needs to be able to find the .cma files for the OCaml modules used by test1.
After this, I can link test1 with
ocamlc -o test1 ../ppl_ocaml.cma ~/gmp/gmp.cma test1.cmo \ -cclib -lppl -cclib -lpwl
(instead of using ../ppl_ocaml.cma you can also say -I .. ppl_ocaml.cma, and similarly for gmp)
After this test1 runs successfully.
Note that I don't have to refer to -lgmp or any of the other libraries (but you can't leave out -lppl or -lpwl). If you type "strings ../ppl_ocaml.cma" then at the very end you see some strings which mention stuff like -L/home/kwxm/libraries/lib and -lgmpxx, so I think the ocaml compiler records some of the information that's necessary for the final linking.
[Some time later...]
Ah, now I see that what makes the difference is including gmp.cma in the linking command. If you insert it just after libppl.so in the makefile then everything works OK, and I think most of the other options are unnecessary. I still don't understand exactly what's going on though. :(
That is interesting info. However, since you are not definitely sure that the thing above will always work and given that we are near to the release of ppl-0.10.1, I prefer to leave things as they are (having more link options than strictly needed should make no arm).
Kenneth
PS: my problematic BHRZ03 widening just finished, after 31 hours and 40 minutes. The result was the same as that of the H79 widening.
There is nothing really surprising ... that's life.
The BHRZ03 widening is meant to try and apply a whole range of heuristics to improve the precision of the H79 widening. It might fail to achieve such an improvement, in which case it falls back to the H79 widening.
As far as efficiency is concerned, as said earlier, whenever convex polyhedra come into play you need to keep an eye on the possibility of bumping into exponential behavior. Fortunately, the PPL library provides you with the tools (timeout and exception safety) needed to first identify the problem and then let the application skip to an alternative plan.
Cheers, Enea.