[Spot] SPOT error in make check

Alexandre Duret-Lutz adl at lrde.epita.fr
Sun Aug 23 21:19:33 CEST 2015


On Sun, Aug 23, 2015 at 10:16 AM, Christopher Ziegler <ziegler at 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 at 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


More information about the Spot mailing list