compile.org 9.34 KB
Newer Older
1 2
# -*- coding: utf-8 -*-
#+TITLE: Compiling against Spot
3
#+DESCRIPTION: How to compile C++11 programs using Spot
4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41
#+SETUPFILE: setup.org
#+HTML_LINK_UP: tut.html

This page is not about compiling Spot itself (for this, please refer
to the [[file:install.org][installation instructions]]), but about how to compile and
execute a C++ program written using Spot.  Even if some of those
explanations might be GNU/Linux specific, they may hint you amount how
to solve problems on other systems.

As an example we will take the following simple program, stored in a
file called =hello.cc=:

#+NAME: hello-word
#+BEGIN_SRC C++ :results verbatim :exports both
  #include <iostream>
  #include <spot/misc/version.hh>

  int main()
  {
    std::cout << "Hello world!\nThis is Spot " << spot::version() << ".\n";
    return 0;
  }
#+END_SRC

After compilation and execution, this should simply display some
greetings and the Spot version:

#+RESULTS: hello-word
: Hello world!
: This is Spot 1.99.6a.


To successfully compile this example program, we need a C++ compiler,
obvisously.  On this page, we are going to assume that you use =g++=
(version 4.8 or later), but other compilers like =clang++= share the
same user interface.  To successfully build the =hello= program, we
might need to tell the compiler several things:

42 43 44 45
1. The language that we use is C++11 (or C++14).  This usually
   requires passing an option like =-std=c++11=.  Note that with
   version 6 of =g++= the default is now to compile C++14, so this
   option is not necessary.
46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148
2. The C++ preprocessor should be able to find =spot/misc/version.hh=.
   This might require appending another directory to the include
   search path with =-I location=.
3. The linker should be able to find the Spot library (on Linux it would
   be called =libspot.so=, unless you forced a static compilation, in which
   case it would be  =libspot.a=).  This might require appending another
   directory to the library search path with =-L location= in addition to
   passing the =-lspot= option.

In the likely case linking was made against the shared library
=libspot.so=, the dynamic loader will have to locate =libspot.so=
everytime the =hello= program is started, so this too might require
some fiddling, for instance using the environment variable
=LD_LIBRARY_PATH= if the library has not been installed in a standard
location.


Below we review four typical scenarios that differ in how Spot
was compiled and installed.


* Case 1: You installed Spot using the Debian packages

In particular, you have installed the =libspot-dev= package: this is
the one that contains the header files.

In that case all the C++ headers have been installed under
=/usr/include/spot/=, and the shared library =libspot.so= has been
installed in some subdirectory of =/usr/lib/=.

In this scenario, the preprocessor, linker, and dynamic linker should
be able to find everything by default, and you should be able to
compile =hello.cc= and then execute =hello= with

#+BEGIN_SRC sh
g++ -std=c++11 hello.cc -lspot -o hello
./hello
#+END_SRC


* Case 2: You compiled Spot yourself, and installed it in the default location

It does not matter if you compiled from the GIT repository, or from
the latest tarball.  If you ran something like
#+BEGIN_SRC sh
./configure
make
sudo make install
#+END_SRC
to install Spot, then the default installation prefix is =/usr/local/=.

This means that all spot headers have been installed in
=/usr/local/include/spot/=, and the libraries (there is more than just
=libspot.so=, we will discuss that below) have been installed in
=/usr/local/lib/=.

Usually, these directories are searched by default, so
#+BEGIN_SRC sh
g++ -std=c++11 hello.cc -lspot -o hello
#+END_SRC
should still work.  But if that is not the case, add
#+BEGIN_SRC sh
g++ -std=c++11 -I/usr/local/include hello.cc -L/usr/local/lib -lspot -o hello
#+END_SRC

If running =./hello= fails with a message about not finding =libspot.so=,
first try to run =sudo ldconfig= to make sure =ld.so='s cache is up-to-date, and
if that does not help, use
#+BEGIN_SRC sh
export LD_LIBRARY_PATH=/usr/local/lib:"$LD_LIBRARY_PATH"
#+END_SRC
to tell the dynamic loader about this location.


* Case 3: You compiled Spot yourself, and installed it in a custom directory

For instance you might have used
#+BEGIN_SRC sh
./configure --prefix ~/usr
make
make install
#+END_SRC
to install everything in your home directory.  In that case the Spot
headers have been installed in =$HOME/usr/include/spot= and the
libraries in =$HOME/usr/lib=.

You would compile =hello.cc= with
#+BEGIN_SRC sh
g++ -std=c++11 -I$HOME/usr/include hello.cc -L$HOME/usr/lib -lspot -o hello
#+END_SRC
and execute with
#+BEGIN_SRC sh
export LD_LIBRARY_PATH=$HOME/usr/lib:"$LD_LIBRARY_PATH"
./hello
#+END_SRC
but it will be more convenient to define =LD_LIBRARY_PATH= once for
all in your shell's configuration, so that you do not have to redefine
it every time you want to run a binary that depends on Spot.


* Case 4: You compiled Spot yourself, but did not install it

We do not recommand this, but it is possible to compile programs
149
that uses an uninstalled version of Spot.
150

151 152
So you would just compile Spot in some directory (let's call it
=/dir/spot-X.Y/=) with
153 154 155 156 157 158 159 160 161 162 163 164 165 166 167
#+BEGIN_SRC sh
./configure
make
#+END_SRC

And then compile =hello.cc= by pointing the compiler to the above directory.

There are at least two traps with this scenario:
1. The subdirectory =/dir/spot-X.Y/spot/= contains the
   headers that would normally be installed in
   =/usr/local/include/spot/= using the same layout, but it also
   includes some private, internal headers.  These headers are
   normally not installed, so in the other scenarios you cannot use
   them.  In this setup however, you might use them by mistake.  Also
   that directory contains =*.cc= files implementing all the features
168
   of the library.  Clearly those file should be considered private as
169
   well.
170 171 172 173 174
2. The subdirectory =/dir/spot-X.Y/buddy/src= contains a few header
   files (for the BDD library) that would normally be installed
   directly in =/usr/local/include=, so this directory has to be
   searched for as well.
3. Spot uses [[http://www.gnu.org/software/libtool/][GNU Libtool]] to make it easy to build shared and static
175 176 177 178 179 180 181 182 183 184 185 186
   libraries portably.  All the process of compiling, linking, and
   installing libraries is done through the concept of /Libtool
   archive/ (some file with a =*.la= extension) that is an abstraction
   for a library (be it static, shared, or both), and its dependencies
   or options.  During =make install=, these /Libtool archives/ are
   transformed into actuall shared or static libraries, installed and
   configured properly.  But since in this scenario =make install= is
   not run, you have to deal with the /Libtool archives/ directly.


So compiling against a non-installed Spot would look like this:
#+BEGIN_SRC sh
187
/dir/spot-X.Y/libtool link g++ -std=c++11 -I/dir/spot-X.Y -I/dir/spot-X.Y/buddy/src hello.cc /dir/spot-X.Y/spot/libspot.la -o hello
188 189 190 191
#+END_SRC

Using =libtool link g++= instead of =g++= will cause =libtool= to
edit the =g++= command line, and replace
192
=/dir/spot-X.Y/spot/libspot.la= by whatever options are
193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208
needed to link against the library represented by this /Libtool
archive/.  Furthermore the resulting =hello= executable will not be a
binary, but a shell script that defines some necessary environment
variables (like =LD_LIBRARY_PATH= to make sure the Spot library is
found) before running the actual binary.

The fact that =hello= is a script can be a problem with some
development tools.  For instance running =gdb hello= will not work as
expected.  You would need to run =libtool execute gdb hello= to obtain
the desired result.  See the [[http://www.gnu.org/software/libtool/manual/][GNU Libtool manual]] for more details.

* Other libraries

If your program has to handle BDDs directly (for instance if you are
[[file:tut22.org][creating an automaton]] explicitely), or if your system does not support
one library requiring another, you will need to link with the =bddx=
209 210
library.  This should be as simple as adding =-lbddx= after =-lspot=
in the first three cases.
211

212
In the fourth case where =libtool= is used to link against
213 214 215 216
=libspot.la= linking against =libbddx.la= should not be necessary because
Libtool already handles such dependencies.  However the version of =libtool=
distributed with Debian is patched to ignore those dependencies, so in this
case you 2
217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246

* Additional suggestions

In all the above invocations to =g++=, we have focused on arguments
that are strictly necessary to link against Spot.  Obviously in
practice you may want to add other options like =-Wall -Wextra= for
more warnings, and optimization options like =-g -Og= when debugging
or =-O3= when not debugging.

The Spot library itself can be compiled in two modes.  Using
#+BEGIN_SRC sh
./configure --enable-devel
#+END_SRC
will turn on assertions, and debugging options, while
#+BEGIN_SRC sh
./configure --disable-devel
#+END_SRC
will disable assertions and enable more optimizations.

If you are writing programs against Spot, we recommand to compile Spot
with =--enable-devel= while your are developping your programs (the
assertions in Spot can be useful to diagnose problems in your program,
or in Spot), and then use =--disable-devel= once you are confident and
desire speed.

On all releases (i.e., version numbers ending with a digit) =configure=
will default to =--disable-devel=.

Development versions (i.e., versions ending with a letter) default to
=--enable-devel=.