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@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
On Sun, Aug 23, 2015 at 10:16 AM, Christopher Ziegler ziegler@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@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,
On Sun, Aug 23, 2015 at 9:19 PM, Alexandre Duret-Lutz adl@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=last... 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 -
Christopher Ziegler