21 May
2019
21 May
'19
2:41 p.m.
On Tue, May 21, 2019 at 12:22 PM Victor Khomenko
<victor.khomenko(a)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/90a88d0b5a916a6088b3fcd789ea6f3…)
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(a)lrde.epita.fr> On Behalf Of Alexandre Duret-
> Lutz
> Sent: Tuesday, May 21, 2019 9:06 AM
> To: Guillermo Perez <gaperez64(a)gmail.com>
> Cc: spot <spot(a)lrde.epita.fr>fr>; Guillermo A. Pérez
> <guillermoalberto.perez(a)uantwerpen.be>
> Subject: Re: [Spot] ltlsynt light
>
> On Tue, May 21, 2019 at 9:47 AM Guillermo Perez <gaperez64(a)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(a)lrde.epita.fr
> https://lists.lrde.epita.fr/listinfo/spot
--
Alexandre Duret-Lutz