Bootstraping from the GIT repository ==================================== (If you are building from a tarball, skip this section.) Spot's gitlab page is at https://gitlab.lrde.epita.fr/spot/spot The GIT repository can be cloned with git clone https://gitlab.lrde.epita.fr/spot/spot.git Some files in SPOT's source tree are generated. They are distributed so that users do not need to tools to rebuild them, but we don't keep all of them under GIT because it can generate lots of changes or conflicts. Here are the tools you need to bootstrap the GIT tree, or more generally if you plan to regenerate some of the generated files. (None of these tools are required by end users installing a tarball since the generated files they produce are distributed.) GNU Autoconf >= 2.61 GNU Automake >= 1.11 GNU Libtool >= 2.4 GNU Flex (the version seems to matters, we used 2.5.35) GNU Bison >= 3.0 GNU Emacs (preferably >= 24 but it may work with older versions) Groff (a.k.a. GNU troff) >= 1.20 SWIG >= 3.0 (for its better C++11/C++14 support) Doxygen >= 1.4.0 Perl, with its Gettext module (it might be called something like liblocale-gettext-perl or p5-locale-gettext in your distribution) A complete LaTeX distribution, including latexmk and extra fonts like dsfont.sty. ImageMagick Python >= 3.3, IPython >= 2.3 GraphViz Java >= 1.7 (needed to run PlantUML while generating the doc) wget or curl (needed to download PlantUML) The following additional tools are used if they are present, or only for certain operations (like releases): pandoc used during Debian packaging for the conversion of IPython notebooks to html optipng used during "make dist" if present, to optimize distributed png images R used by some example in the documentation (the documentation will still compile without R, but that example will appear broken) ltl2ba used in the generated documentation and the test suite ltl2dstar likewise ltl3dra likewise spin likewise glucose >= 3.0 likewise lbtt >= 1.2.1a used in the test suite (ltlcross is now more powerful, but additional tests do not hurt) If you use Debian or a similar distribution, the Dockerfile at https://github.com/adl/spot-docker/blob/master/debuild/Dockerfile lists all the Debian packages that should be installed to build Debian packages out of the GIT tree. Additionally, the script https://github.com/adl/spot-docker/blob/master/debuild/install.sh installs the third-party tools that do not have Debian packages. Bootstrap the GIT tree by running % autoreconf -vfi and then go on with the usual % ./configure % make Tricks ====== Avoiding Doxygen runs --------------------- When there is no documentation built (e.g., after a fresh checkout of the GIT tree), when the configure.ac file has changed, or when the Doxygen configuration has changed, the doc will be rebuilt. This can take quite some time, even though recent version of Doxygen have started to parallelize things. If you have no interest in generating the documentation, just use the "magic touch": touch doc/stamp Do that right before running make. The timestamp of doc/stamp is compared to configure.ac and Doxygen.in to decide if the documentation is out-of-date. The above command pretends the documentation has just been built. Avoiding org-mode runs ---------------------- The files in doc/org/ are org-mode files (a mode of Emacs that we use to author documents that embed executable snippets), they are used to generate the doc/userdoc/ HTML documentation. If for some reason you don't have emacs, or you simply want not to rebuild these files, use another "magic touch": touch doc/org-stamp Silent Building with automake ----------------------------- The classical makefiles generated by automake are very verbose during build beacause they prints the full command line of every stage. This verbosity is very usefull to help (remotely) users to compile Spot. Nonetheless, for developpers, these compilations lines may be annoying. To reduce this verbosity, just run: make V=0 Executing a single test ----------------------- All tests in subdirectories of tests/ are executed through the tests/run script. That run script defines PATH and other environment variables necessary so that Shell and Python scripts will use the version of Spot under development. For instance to execute tests/core/acc.test, do: % cd tests % ./run core/acc.test A test run this way automatically executes in verbose mode. Any temporary file generated by the script can be found in tests/core/acc.dir/. Alternatively, if you use emacs, the .dir-locals.el configuration at the top of the project redefines the C-c C-c key for all shell and python scripts under the tests/ directory. So if you are working on tests/core/acc.test under emacs, hitting C-c C-c should be all you need to execute it. Debugging Libtool executables ----------------------------- The executables generated in the various testsuite directories of Spot are not real binaries. Because we use libtool to compile the spot library in a portable manner, these executables are just scripts that run the actual binary after setting some environment variables so that the OS can find the library in the build tree. A consequence is that tools like gdb or valgrind, that expect to work on a binary, will be confused by the script. Example: % cd bin % file ltl2tgba ltl2tgba: POSIX shell script text executable % gdb -q ltl2tgba "/home/adl/git/spot/bin/ltl2tgba/ltl2tgba": not in executable format: File format not recognized (gdb) quit The proper way to run any command on these fake binaries is via libtool: % ../../libtool --mode=execute file ltl2tgba /home/adl/git/spot/bin/.libs/lt-ltl2tgba: ELF 32-bit LSB executable, Intel 80386, version 1 (SYSV), dynamically linked (uses shared libs), for GNU/Linux 2.6.18, not stripped % ../../libtool --mode=execute gdb -q ltl2tgba Reading symbols from /home/adl/git/spot/bin/.libs/lt-ltl2tgba...done. (gdb) quit You can see that libtool turns ltl2tgba into .libs/lt-ltl2tgba, but it also sets environment variables so that the dependent shared libraries will be found. If you are building Spot from the GIT repository, the libtool script generated the root of the build tree should be the same as the libtool script that is installed on your system. So you can simply run libtool instead of ../../libtool. There is an undocumented feature of libtool that allows you to shorthand "libtool --mode=execute" as "libtool execute" or even "libtool e". But you might also find convenient to define an alias, a function, or a script to make that invocation even shorter. For instance: alias le='libtool --mode=execute ' (The trailing space makes it possible to follow this command by another aliased command.) Profiling with callgrind ------------------------ Install valgrind and kcachegrind. Then run the command you want to profile through valgrind's callgrind tool. For instance: % libtool e valgrind --tool=callgrind ltl2tgba -f 'GFa & GFb' This will output a file called 'callgrind.PID' where PID is the process ID printed during valgrind's run. Load this file with kcachegrind to get a graphical summary. % kcachegrind ./callgrind.PID Running coverage tests ---------------------- First, compile (and link) Spot with coverage enabled. % ./configure CXX='g++ --coverage' % make Then run the test suite (or any program you want to study). % make check Executing programs using Spot will generate a lot of *.gc* files everywhere. Collect these using lcov: % lcov --capture --directory src --output spot.info Finally generate a coverage report in HTML: % genhtml --legend --demangle-cpp --output-directory html spot.info This should create the directory html/. Link-time optimizations ----------------------- This is currently a bit tricky to setup, because the toolchain is not mature enough. However this is getting better and better. The Debian packages we build nightly are mostly built with link-time optimization (the shared library uses link-time optimization, but the command-line binary are built without because of some bug with exception propagation). You need: 1. a version of GCC (>= 4.9) with gold and pluing linker enabled. 2. a version of Libtool that knows how to deal with -flto flags (Libtool 2.4.2 will work) Here are example options to pass to configure to build a static version with link-time optimization: ./configure CC=gcc-4.9 CXX=g++-4.9 \ --disable-devel --disable-debug \ CFLAGS='-flto' CXXFLAGS='-flto' LDFLAGS='-fuse-linker-plugin' \ --disable-shared --enable-static If you want to build a shared library, see in debian/rules how it is done. Log driver for testsuite ------------------------ The PASS/FAIL status for each test of the testsuite is printed by tools/test-driver. This script can be changed to format the output differently. When we use Teamcity (for continuous integration) we change the output format to something that Teamcity will understand with: make check LOG_DRIVER=$PWD/tools/test-driver-teamcity Coding conventions ================== Here some of the conventions we follow in Spot, so that the code looks homogeneous. Please follow these strictly. Since this is free software, uniformity of the code matters a lot. Most of these conventions are derived from the GNU Coding Standards (http://www.gnu.org/prep/standards.html) with the notable exception that we do not put a space before the opening parenthesis in function calls (this is hardly readable when chaining method calls). Besides cosmetics, some of these conventions are also here to prevent bugs and make it easier to devise safety checks. The directory tests/sanity/ contains some scripts that are executed during 'make check' or 'make installcheck' to check some of the conventions discussed below. For instance we have a check to ensure that any header can be included twice, and we have another check to ensure that any header contains a include guard that follow our naming convention. This way we do not forget guards, and we do not forget to rename them when a file is copied into another one. C++14 ----- Spot uses some C++14 features, and therefore requires a C++14 compiler. g++ 5.x or clang++ 3.4 should be enough. We currently avoid C++17 features until C++17 compiler are widely available. Encoding -------- * Use UTF-8 for non-ASCII characters. * Do not use tabs for indentation in C++ files. Use only space to prevent issues with people assuming different tab widths. * If you edit files encoded in Latin-1 (the original default encoding for the project), feel free to convert them to UTF-8. In emacs the simplest way to convert the file is to add a comment with -*- coding: utf-8 -*- at the top or bottom of the file. There is some check in tests/sanity/ that will ensure that -*- coding: utf-8 -*- is used for all C++ files, but try to use it for all text files if they contain non-ascii characters. Includes -------- * Use #include with angle-brackets to refer to public headers of Spot; i.e., those that will be installed, or system headers that are already installed. E.g., #include #include * Use #include with double quotes to refer to private headers that are distributed with Spot. Those can be from Spot itself, or from third-party libraries that we ship. E.g., #include "utf8/utf8.hh" #include "spot/priv/trim.hh" #include "config.h" This style of #include should never occur in public headers. Exporting symbols ----------------- Since we are building a library, it is important to make a clear distinction between what is private and what is public. In our setup, everything is private by default and has to be explicitely made public. * If a private symbol is needed only by one module, keep it inside the *.cc file, in an anonymous namespace. Also mark it as static if it is a function or variable. This is the best way to let the compiler and linker know that the symbol is not used elsewhere. * If a symbol could be used by several modules of the library but should still be private to the library, use a *.hh/*.cc pair of files, but list both files in the _SOURCES variable of that directory (see for instance weight.hh in tgbaalgos/Makefile.am). This will ensure that the header is not installed. Needless to say, no public header should include such a private header. * The directory src/priv/ can be used to store files that are globaly private the library, and that do not really belongs to other directories. * Functions and classes that are public should be marked with the SPOT_API macro. This macro is defined in misc/common.hh, but you need not include it in a file that already includes another public header. * Do not make a symbol public just because you can. * Read http://www.akkadia.org/drepper/dsohowto.pdf for more information about how shared libraries work and why. Assertions ---------- * There are different types of assertions. Plain assert() is OK for invariants or post-conditions. When asserting a pre-condition, carefully consider who the caller might be: if it can be in user-code (either in C++ or Python), throw an exception (std::runtime_error, std::invalid_argument, and spot::parse_error are the three exception types catched by the Python bindings). * Do not call assert() in public *.hh files: even if the installed libspot has been compiled with -DNDEBUG, the *.hh files will be recompiled by users, probably without -DNDEBUG. So use SPOT_ASSERT() instead of assert(), this ensure asserts are only used inside libspot for debug builds. Comments -------- * The language to use is American English. * When comments are sentences, they should start with a capital and end with a dot. Dots that end sentences should be followed by two spaces (i.e., American typing convention), like in this paragraph. * Prefer C++-style comments (// foo) to C-style comments (/* foo */). Use /// for Doxygen comments. Formating --------- * Braces around instruction blocks are always on their own line. Braces around initializers lists need not be on their own. * Text within braces is two-space indented. { f(12); } * Anything after a control statement is two-space indented. This includes braces. if (test) { f(123); while (test2) g(456); } * Braces from function/structure/enum/class/namespace definitions are not indented. class foo { public: Foo(); protected: static int get_mumble(); }; * The above corresponds to the `gnu' indentation style under Emacs. * Put a space before the opening parenthesis in control statements if (test) { do { something(); } while (0); } * No space before parentheses in function calls. (`some()->foo()->bar()' is far more readable than `some ()->foo ()->bar ()') * No space after opening or before closing parentheses, however put a space after commas (as in english). func(arg1, arg2, arg3); * No useless parentheses in return statements. return 2; (not `return (2);') * Spaces around infix binary or ternary operators: 2 + 2; a = b; a <<= (3 + 5) * 3 + f(67 + (really ? 45 : 0)); * No space after prefix unary operators, or before postfix unary operators: if (!test && y++ != 0) { ++x; } * When an expression spans over several lines, prefer splitting it before operators. If it's inside a parenthesis, the following lines should be 1-indented w.r.t. the opening parenthesis. if (foo_this_is_long && bar > win(x, y, z) && !remaining_condition) { ... } * `else if' can be put as-is on a single line. * No line should be larger than 80 columns. If a line takes more than 80 columns, split it or rethink it. This makes it easier to print the code, allow people to work on small screens, makes it possible to display two files (or an editor and a terminal) side-by-side, ... This also puts some pressure on the programmer who writes code that has too much nested blocks: if you find yourself having to code between columns 60 and 80 because of identation, consider writing helper functions to simplify the structure of your code. * Labels or case statements are back-indented by two spaces, without space before the `:'. if (something) { top: bar = foo(); switch (something_else) { case first_case: f(); break; case second_case: g(); break; default: goto top; } } * Pointers and references are part of the type, and should be put near the type, not near the variable. int* p; // not `int *p;' list& l; // not `list &l;' void* magic(); // not `void *magic();' * Do not declare many variables on one line. Use int* p; int* q; instead of int *p, *q; The former declarations also allow you to comment each variable. * The include guard for src/somedir/foo.hh is SPOT_SOMEDIR_FOO_HH Naming ------ * Functions, methods, types, classes, etc. are named with lowercase letters, using an underscore to separate words. int compute_this_and_that(); class this_is_a_class; typedef int int_array[]; That is the style used in STL. * Private members end with an underscore. class my_class { public: ... int get_val() const; private: int name_; }; * Identifiers (even internal) starting with `_' are best avoided to limit clashes with system definitions. * Template arguments use capitalized name, with joined words. template class foo { ... }; * Enum members also use capitalized name, with joined words. * C Macros are all uppercase. * Use *.hxx for the implementation of templates that are private to Spot (i.e., not installed) and need to be included multiple times. SPOT macros ----------- A few macros are defined in misc/common.hh notably: * SPOT_FALLTHROUGH should be used to mark fall-throughs in switches: switch (foo) { case 1: f(); SPOT_FALLTHROUGH; case 2: g(); break; } * Use SPOT_UNREACHABLE() to mark places that are not reachable but that a compiler might not see as unreachable. * Use SPOT_API in front of functions and class that should be exported by the shared library. See "Exporting symbolss" above. * Use SPOT_ASSERT(...) if you ever have to put an assertion in some header file. See "Assertions" above. * Use SPOT_LIKELY / SPOT_UNLIKELY in case you need to help the compiler figure out the commont output of a test. Do not abuse this without checking the assembly output to make sure the effect is what you desired. Other style recommandations --------------------------- * The original C++98 code used 0 for null pointers (and never NULL). Feel free to replace these by uses of C++11's nullptr instead. * Limit the scope of local variables by defining them as late as possible. Do not reuse a local variables for two different things. * Do not systematically initialize local variables with 0 or other meaningless values. This hides errors to valgrind. * Avoid , , etc. in headers whenever possible. Prefer when predeclarations are sufficient, and then for instance use just in the corresponding .cc file. (A plain is needed when using std::cout, std::cerr, etc.) * Always declare helper functions and other local class definitions (used in a single .cc files) in anonymous namespaces. (The risk otherwise is to declare two classes with the same name: the linker will ignore one of the two silently. The resulting bugs are often difficult to understand.) * Always code as if the person who ends up maintaining your code is a violent psychopath who knows where you live.