diff --git a/NEWS b/NEWS index 1e89b5d5f..071178a2b 100644 --- a/NEWS +++ b/NEWS @@ -22,6 +22,11 @@ New in spot 1.99.6a (not yet released) Python: + Documentation: + + * There is a new page explaining how to compile example programs and + and link them with Spot. https://spot.lrde.epita.fr/compile.html + Bug fixes: New in spot 1.99.6 (2015-12-04) diff --git a/doc/Makefile.am b/doc/Makefile.am index 8ffc44671..c8795af17 100644 --- a/doc/Makefile.am +++ b/doc/Makefile.am @@ -67,6 +67,7 @@ ORG_FILES = \ org/spot.css \ org/autfilt.org \ org/csv.org \ + org/compile.org \ org/dstar2tgba.org \ org/genltl.org \ org/hoa.org \ diff --git a/doc/org/compile.org b/doc/org/compile.org new file mode 100644 index 000000000..6cb1c0156 --- /dev/null +++ b/doc/org/compile.org @@ -0,0 +1,236 @@ +# -*- coding: utf-8 -*- +#+TITLE: Compiling against Spot +#+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 + #include + + 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: + +1. The language that we use is C++11 (or C++14). This usually requires + passing an option like =-std=c++11=. +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 +that uses an unstalled version of Spot. + +So you would just compile Spot in some directory (lets call it =/dir/spot-X.Y/=) with +#+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 + of the library. Clearly those should be considered as private as + well. +2. Spot uses [[http://www.gnu.org/software/libtool/][GNU Libtool]] to make it easy to build shared and static + 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 +/dir/spot-{{SPOTVERSION}}/libtool link g++ -std=c++11 -I/dir/spot-{{SPOTVERSION} hello.cc /dir/spot-{{SPOTVERSION}/spot/libspot.la -o hello +#+END_SRC + +Using =libtool link g++= instead of =g++= will cause =libtool= to +edit the =g++= command line, and replace +=/dir/spot-{{SPOTVERSION}/spot/libspot.la= by whatever options are +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= +library. This should be as simple as adding =-lbddx= after =-lspot= +in any of the above commands. This is not necessary when =libtool= +is used to link against =libspot.la=, because Libtool already handles +such dependencies. + + +* 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=. diff --git a/doc/org/tut.org b/doc/org/tut.org index 9e5ae92be..19ef37ef7 100644 --- a/doc/org/tut.org +++ b/doc/org/tut.org @@ -8,6 +8,9 @@ This section contains code examples for using Spot. This is a work in progress. Feel free to [[mailto:spot@lrde.epita.fr][send]] suggestion of small tasks you would like to see illustrated here. +If you have difficulties compiling the C++ examples, check out [[file:compile.org][these +instructions]]. + * Examples with Shell, Python, and C++ All the following pages show how to perform the same task using the @@ -23,7 +26,8 @@ three interfaces supported by Spot: shell commands, Python, or C++. - [[file:tut03.org][Constructing and transforming formulas]] -* Examples in C++ only +* Examples in +C++ only The following examples are too low-level to be implemented in shell or Python (at least at the moment), so they are purely C++ so far. diff --git a/doc/org/tut01.org b/doc/org/tut01.org index cc265deeb..e5363a6b6 100644 --- a/doc/org/tut01.org +++ b/doc/org/tut01.org @@ -67,6 +67,7 @@ We first start with the easy parser interface, similar to the one used above in the python bindings. Here parse errors would be returned as exceptions. +#+NAME: 1stex #+BEGIN_SRC C++ :results verbatim :exports both #include #include @@ -83,7 +84,9 @@ exceptions. } #+END_SRC -#+RESULTS: +After [[file:compile.org][compiling and executing]] we get: + +#+RESULTS: 1stex : GFp0 | FGp1 : p_{1} \land p_{2} \land \G p_{0} : & & p1 p2 G p0