On Tue, May 21, 2019 at 12:22 PM Victor Khomenko <victor.khomenko@newcastle.ac.uk> wrote:

Dear Alexandre and Guillermo,

We tried to link Spot statically - Alexandre's suggestion did not quite work for us, but Danil had worked out a different method, see below.

What --disable-shared --enable-static change is how the libraries distributed with Spot get built. By default we build a shared AND a static version of each library. If you only build static versions of the libraries, the binaries will be linked to those. I think that's what Guillermo asked: no dependency on libspot.so. The binaries will still be dynamically linked to your system's libraries. (You need --disable-python as well, because Python bindings need shared libraries; I forgot that.) Getting fully static libraries is only slightly more complicated. First you need static versions of your system's library. Then you should make sure that libtool receives the "-all-static" option at link time. So: ./configure --disable-shared --disable-python make LDFLAGS=-all-static should *usually* be enough. On my Debian system, using -all-static like this is not enough when cross-compiling MinGW binaries. The executables still try to load libgcc_s_sjlj-1.dll and libstdc++-6.dll. So the command-line we use to build static MinGW binaries in our CI environment (https://gitlab.lrde.epita.fr/spot/spot/blob/90a88d0b5a916a6088b3fcd789ea6f30...) is more complicated than that. Finally stripping binaries is more commonly done by calling "make install-strip" instead of "make install". (This way you can still use the uninstalled version for debugging if needed.)

Regards, Victor.

------------------------

Hi Victor,

This looks much simpler than the way I figured out by try and error:

https://workcraft.org/devel/backend/spot

However the binaries are still dynamically linked after this:

~/spot/bin$ ldd ltl2tgba linux-vdso.so.1 => (0x00007fff6c9f8000) libstdc++.so.6 => /usr/lib/x86_64-linux-gnu/libstdc++.so.6 (0x00007fe09b967000) libm.so.6 => /lib/x86_64-linux-gnu/libm.so.6 (0x00007fe09b65e000) libgcc_s.so.1 => /lib/x86_64-linux-gnu/libgcc_s.so.1 (0x00007fe09b446000) libc.so.6 => /lib/x86_64-linux-gnu/libc.so.6 (0x00007fe09b07c000) /lib64/ld-linux-x86-64.so.2 (0x00007fe09bcf3000)

I think I will stick for what is working for us rather than trying to understand what goes wrong with these --disable-shared and --enable-static flags...

Maybe we should share our experience with Guillermo and also let Spot team know about the issue?

Cheers, Danil

...

-----Original Message----- From: Spot <spot-bounces@lrde.epita.fr> On Behalf Of Alexandre Duret- Lutz Sent: Tuesday, May 21, 2019 9:06 AM To: Guillermo Perez <gaperez64@gmail.com> Cc: spot <spot@lrde.epita.fr>; Guillermo A. Pérez <guillermoalberto.perez@uantwerpen.be> Subject: Re: [Spot] ltlsynt light

On Tue, May 21, 2019 at 9:47 AM Guillermo Perez <gaperez64@gmail.com> wrote:

...

Hello,

I am part of the SYNTCOMP organization team this year. Ltlsynt seems to me the easiest tool to migrate into the, new this year, StarExec competition architecture. However, while trying to prepare a binary, I found that spot generates 1. a .libs folder with libraries 2. very large dependencies like libspot.so

Is there a way to generate a statically-liked ltlsynt binary with no hidden dependencies and without all of spot in a dynamically-liked file? (E.g. an option like "make ltlsynt" would be ideal.)

Hi Guillarmo,

Like any libtool-based project, you can generate a statically-linked version of the Spot binaries with

./configure --disable-shared --enable-static make -j4

(don't forget to run "make clean" first if you are doing this on a previous build)

-- Alexandre Duret-Lutz _______________________________________________ Spot mailing list Spot@lrde.epita.fr https://lists.lrde.epita.fr/listinfo/spot

-- Alexandre Duret-Lutz