23 Aug
2015
23 Aug
'15
10:16 a.m.
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
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 also include the src/tests/test-suite.log in the attachment. I hope
this helps you finding a bug or something. Since the program works for
me now, I just wrote you because it said "Please report to spot@..." .
If you need more information (for example, which compiler I used etc.)
you can write me back.
Regards,
Christopher Ziegler
23 Aug
23 Aug
9:19 p.m.
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
24 Aug
24 Aug
10:26 a.m.
On Sun, Aug 23, 2015 at 9:19 PM, Alexandre Duret-Lutz <adl(a)lrde.epita.fr>
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.
I've implemented that. You can find a development version here:
http://teamcity.lrde.epita.fr/viewLog.html?buildTypeId=bt16&buildId=las…
If you have the time to build it run "make check" again, I would
appreciate a confirmation that both errors are gone; but if you don't,
no worries.
--
Alexandre Duret-Lutz
3599
days inactive
3600
days old
2 comments
2 participants
participants (2)
-
Alexandre Duret-Lutz -
Christopher Ziegler