On Sun, Aug 23, 2015 at 10:16 AM, Christopher Ziegler <ziegler(a)in.tum.de> wrote:
Hello Ladies and Gentlemen,
I used your program (SPOT) on Ubuntu 12.4. 32bit, configured it with the
two parameters --disable-python and --prefix=/home/my_username (for
which I don't need any sudo priviliges to read/write.
Then I did make check and the program reported the following:
See src/tests/test-suite.log
Please report to spot(a)lrde.epita.fr
Hi Christopher,
Thank you for reporting these two test-suite failures.
The failure of uniq.test is due to different locale (I can reproduce it
if I set LC_ALL=de_DE.UTF-8) affecting the output of the sort
command. The test will be fixed in the next release.
The failure of randpsl.test is an out-of-memory error during
the verification of a particularly ugly (because randomly-generated)
PSL formula. This very same issue was reported 2 months ago
against 1.99.1 but I only fixed the speed issue, and not the memory
issue
https://gitlab.lrde.epita.fr/spot/spot/issues/96
I guess the proper fix would be to have ltlcross detect its out-of-memory
errors, skip the tests it cannot perform, and report how many tests were
skipped because of memory issues.
However, I ran make install afterwards, and tried the
program and it
seems to work. But when I tried to do the same (last week or so), I
didn't use the --prefix parameter and I got an error, when I tried to
start the program: it said:
"error while loading shared libraries:
libspot.so.0: cannot open shared object file: No such file or
directory"
I'm not sure what "the program" refers to in your first paragraph.
I would expect that command line tools installed will Spot should
find the library where it has been installed (because they should
embed the path to it). But if you have another program that uses
Spot and does not find in the /usr/local/lib (the default place
where it is installed when you do not use --prefix), then this
can probably be fixed by running
sudo ldconfig
to update symlinks and cache files.
Best regards,
--
Alexandre Duret-Lutz