21 May
2019
21 May
'19
12:22 p.m.
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.
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
21 May
21 May
2:41 p.m.
New subject: ltlsynt light
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
2:41 p.m.
New subject: ltlsynt light
Dear all, thank you for your quick replies!
For my purposes the solution proposed by Alexandre did work. However, as pointed out by
Victor, while libspot and others are no longer dynamically linked, some standard libraries
still are so. Fortunately for me, those libraries are available in the StarExec server.
Best,
Guillermo
On 21/05/2019, 12:22, "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.
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
2087
days inactive
2087
days old
2 comments
3 participants
participants (3)
-
Alexandre Duret-Lutz -
Perez Guillermo Alberto -
Victor Khomenko