HACKING

Bootstrapping from the Git repository
=====================================

(If you are building from a tarball, skip this section.)

Spot's gitlab page is at

  https://gitlab.lre.epita.fr/spot/spot

The Git repository can be cloned with

  git clone https://gitlab.lre.epita.fr/spot/spot.git

Some files in SPOT's source tree are generated.  They are distributed
so that users do not need to install 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.69
  GNU Automake >= 1.11
  GNU Libtool >= 2.4
  GNU Flex >= 2.6
  GNU Bison >= 3.3
  GNU Emacs (preferably >= 24 but it may work with older versions)
  org-mode >= 9.1 (the version that comes bundled with recent
    emacs versions should usually be more recent than that; some
    Linux distribution may ship a more recent org-mode package
    separately from emacs).
  Groff (a.k.a. GNU troff) >= 1.20
  SWIG >= 4.2.0  (older versions may have trouble with Doxygen support)
    If you use Macports you consider installing the swig-python package
    in addition to the swig package.
  Doxygen >= 1.4.0  (preferably >= 1.10)
  R   used by some examples in the documentation
  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.8, IPython >= 2.3
  Jupyter >= 4, with nbconvert
  GraphViz
  Java >= 1.7 (needed to run PlantUML while generating the doc)
  wget or curl (needed to download PlantUML)
  pdf2svg (alternatively, pdftocairo from the poppler-utils package)

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
  svgo      for reducing SVG images before generating the tarball
            (install with: npm install -g svgo@1.3.2)
  ltl2ba    used in the generated documentation and the test suite
  ltl2dstar likewise
  ltl3dra   likewise
  spin      likewise
  syfco     likewise
  dot2tex   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)
  patchelf (or chrpath)
            used for fixing rpaths when installing Spot with pip

If you use Debian or a similar distribution, the Dockerfile at
https://gitlab.lre.epita.fr/spot/buildenv/-/blob/master/deb/stable-amd64/Dockerfile
lists all the Debian packages that should be installed to build
Debian packages out of the Git tree.  Additionally, the script
https://gitlab.lre.epita.fr/spot/buildenv/-/blob/master/deb/stable-amd64/install.sh
installs the third-party tools that do not have Debian packages.


After cloning the repository and installing the above dependencies,
bootstrap the repository by running the following command from the
top-level directory (the one containing this file).

  % autoreconf -vfi

and then go on with the usual

  % ./configure
  % make


Tips and Tricks
===============

Speeding up the compilation
---------------------------

By default, libraries will be compiled both in static and shared
forms: this require each source file to be compiled twice.  To halve
the compilation time, you may disable the static version by passing
option --disable-static to configure.

You should also tell make to compile several files in parallel with
`make -j4`, adjusting this to your number of CPUs.


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:

  % touch doc/org-stamp


Silent Building with automake
-----------------------------

The classical makefiles generated by automake are very verbose during
build because they print the full command line of every stage.  This
verbosity is very useful to help (remotely) users to compile Spot.
Nonetheless, these compilations lines may be annoying for some
developers.  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 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/.

Regenerating Jupyter notebooks
..............................

When a change to Spot's code causes the output of some Jupyter
notebook test to change (e.g., a different BDD variable ordering, or
a different state numbering), the stored outputs in the notebook need
to be regenerated.  This can be done with:

  % cd tests
  % ./run regen python/some-notebook.ipynb

This re-executes the notebook and overwrites it with the updated
outputs.  Please check the resulting diffs carefully before committing
the regenerated notebook.

The notebook tester compares each code cell's output with its stored
output.  For cells whose output can legitimately vary between runs or
builds (for example, an automaton produced by a SAT solver), add the
`output-is-nondeterministic` tag to that code cell's metadata.  The tester
will still execute the cell, but will skip comparing its output, so the
cell should check relevant properties of its result explicitly.

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 in 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.)

If you are using macOS, the installation of GDB can be hard, even when
using packages manager like MacPorts or Homebrew.  Indeed, Apple promotes
lldb over gdb.

As a consequence, the following command lines work perfectly on
pre El Capitan (OS X 10.11) versions

   % ../libtool --mode=execute lldb --  bin/ltl2tgba
   (lldb) r 'F a'

However, for newer versions the same command will (probably)
raise:

   dyld: Library not loaded: /usr/local/lib/libspot.0.dylib
      Referenced from: /Users/etienne/src/spot/bin/.libs/ltl2tgba
      Reason: image not found
      Process 11024 stopped

This is a side effect of "System Integrity Protection" introduced in El
Capitan.  From this version, calling tools from /usr/bin purges environment
variables.  Consequently the DYLD_LIBRARY_PATH is not exported.
Two solutions:
    - [not-recommended] disable "System Integrity Protection"
    - [recommended]     use the XCode lldb, not located in /usr/bin.

Then, to use lldb on macOS, just run the following command:
   % ../libtool --mode=execute /Applications/Xcode.app/Contents/Developer/usr/bin/lldb  --  bin/ltl2tgba
   (lldb) r 'F a'


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.  You can load this file with
kcachegrind to get a graphical summary of the profiling result.

  % 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 spot --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/.

Coverage tests are automatically performed by our continuous
integration builds.  You can find a report for each branch in the
artifacts of the debian-unstable-gcc-coverage job.


Link-time optimizations
-----------------------

This used to be bit tricky to setup, but is now quite well supported.
Our Debian packages are built with link-time optimization.

You need:
  1. a version of GCC (>= 4.9) with gold and plugin 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.  In the past, when we used teamcity (for continuous
integration) we changed the output format to something that teamcity
would understand with:

  make check LOG_DRIVER=$PWD/tools/test-driver-teamcity


Generating compile_commands.json
--------------------------------

The file compile_commands.json is used by many clang tools in order to
know how a single file is compiled (in particular, which include paths
should be used).  Autotools-based build systems do not support the
generation of this file, but there is a tool called "bear" (for "Build
EAR") that is packaged with most distribution that can be used here.
Simply run a full build through "bear" using something like this:

   % ./configure CC=clang-17 CXX=clang++-17
   % make -j8 clean # make sure your will rebuild everything
   % bear -- make -j8

This will simply intercept all command executions and record them in
the compile_commands.json database.  Depending on the tools you plan to
use, you probably want to compile everything with clang, as shown above.



Development workflow
====================

(Some of the details below, like git-push hooks and CI/CD runners,
are specific to Spot's GitLab instance at
https://gitlab.lre.epita.fr/spot/spot and may not apply if you are
working from a fork or a tarball.)

ChangeLog
---------

Spot's release tarball includes a ChangeLog that describes all changes
in the style used by the GNU project:
https://www.gnu.org/prep/standards/html_node/Style-of-Change-Logs.html

Spot generates this ChangeLog file from git's log, so you just need
to use this syntax in your commit messages.

There is also a separate ChangeLog file for BuDDy, so if you have to
modify BuDDy, be sure to do that in a separate commit whose commit
message starts with [buddy] and where the filenames in the log entry
are relative to the root of BuDDy's directory.

When pushing to a personal branch (with a slash in its name), "git
push" will warn you if files you have modified do not match the files
listed in the commit messages, so you can force-push a fix.  When
pushing to a non-personal branch (no slash, like "master", "next",
"stable") this warning becomes an error.


Commits
-------

As much as possible, try to split large features into multiple
incremental small commits that can be understood in isolation.

If you are building a new feature A that will require feature B,
make a commit that implements, tests, and documents B before starting
to work on a commit that implements A.


Rebase and fixups
-----------------

Once you have committed feature B, and started working on feature A,
it is possible that you discover that B was incorrectly done.  Just
use "git commit --fixup" and later "git rebase --autosquash" to
update the earlier commit about B.

As long as you are working on a personal branch, just rewrite the
history to pretend you got it right from the start.

Ideally, once the branch is feature-full, it should consist of a
series of incremental features each in their own commit, that will be
forward-merged.  (I.e., not an actual merge; we still prefer to get a
linear history.)

This is of course a best effort.  If you discover that what you wrote
10 commits ago needs to be redone differently, and that doing so would
break many intermediate commits, then just fix this in a new commit.


CI/CD & coverage
----------------

It's best to run "make check -j$(nproc)" on your computer and fix
any errors before pushing, because the CI builds use some computers
that are shared by other projects in the lab.

The CI builds will test the code in different configurations,
different compilers, and architectures, so they may fail even if the
tests pass on your computer.  For instance, if your code does
something like f(g(), h()), the order in which g() and h() are
evaluated is architecture dependent.  Intel does it one way, Arm the
other.  If g() and h() have side-effects (e.g., BDD operations,
formula constructors...) the different order can be felt in the test
suite.  Best to avoid those patterns.

One of the CI builds computes a coverage report.  You can use it to
check any newly added code, and see if there are obvious test cases
that are missing.  See also "Running coverage tests" above.


Test cases
----------

Tests as shell scripts or Python scripts should be preferred over
C++ tests.  C++ test cases require compilation, which slows down the
test suite.

Jupyter notebooks are slow to run, and painful to update when we
change the code, so they are best limited to test cases that can
double as documentation.

See "Coding conventions for Python Tests" below for more details about
writing Python tests and notebooks.


C++ 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++20
-----

  Spot uses some C++20 features, and therefore requires a C++20
  compiler.  g++ 10.x or clang++ 10 should be enough.

  We currently avoid C++23 features until C++23 compilers are widely
  available.  (FYI: we switched to C++11 in 2015, to C++14 in 2017,
  to C++17 in 2020, and to C++20 in 2026.)


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 <spot/misc/version.hh>
    #include <iostream>

  * 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 "config.h"
    #include "utf8/utf8.hh"
    #include "spot/priv/trim.hh"

    This style of #include should never occur in public headers.

  * "config.h" should be the first file included by any *.cc or *.c
    file, as it setups several macros for replacing missing functions.


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 explicitly
  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 priv/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 spot/priv/ can be used to store files that are
    globally private to the library, and that do not really belong 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.

  * When mentioning an issue number, in comments as well as in commit
    messages, use one of the following forms so that we can configure
    our editors to turn these into hyperlinks.

       Issue #123 / issue #123 / Fixes #123 / fixes #123

    When gitlab sees a commit message containing "Fixes #123" or
    "fixes #123" pushed to branch "next", it should automatically
    close the issue.

Formatting
---------

  * 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++ != -2)
      {
        ++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 indentation, 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.

  * Do not use include guards, just use "#pragma once".
    Even if that isn't standard; it is supported everywhere.

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 T, int NumberOfThings>
    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 symbols" 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 common output of a test.  Do not abuse
    this without checking the assembly output to make sure the effect
    is what you desired.

Other style recommendations
---------------------------

  * 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 variable for two different things.

  * Do not systematically initialize local variables with 0 or other
    meaningless values.  This hides errors to valgrind.

  * Avoid <iostream>, <ostream>, etc. in headers whenever possible.
    Prefer <iosfwd> when predeclarations are sufficient, and then
    for instance use just <ostream> in the corresponding .cc file.
    (A plain <iostream> 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.


Coding conventions for Python Tests
===================================

Unless you have some specific reason to write test cases in C++ (for
instance do test some specific C++ constructions, or to use valgrind),
prefer writing test cases in Python.  Writing test cases in C++
requires some compilation, which slows down the test suite.  Doing the
same test in Python is therefore faster, and it has the added benefit
of ensuring that the Python bindings works.

We have two types of Python tests: Python scripts or jupyter
notebooks.  Jupyter notebooks are usually used for a sequence of
examples and comments that can also serve as part of the
documentation.  Such jupyter notebooks should be added to the list of
code examples in doc/org/tut.org.  Testing a notebook is done by the
tests/python/ipnbdoctest.py scripts, which evaluate each cells, and
checks that the obtained result is equivalent to the result saved in
the notebook.  The process is a bit slow, so plain Python scripts
should be preferred for most tests.

If you do need a notebook to tests Jupyter-specific code but this
notebook should not be shown in the documentation, use a filename
starting with '_'.

Tests written as Python scripts should follow the same convention as
shell scripts: exit 0 for PASS, exit 77 for SKIP, and any other exit
code for FAIL.

Do not use assert() in those scripts, as (1) asserts can be disabled,
and (2) they provide poor insights in case of failures.  Instead do

   from unittest import TestCase
   tc = TestCase()

and then use tc.assertTrue(...), tc.assertEqual(..., ...),
tc.assertIn(..., ...), etc.  In case of failures, those will print
useful messages in the trace of the tests.  For instance multiline
strings that should have been equal will be presented with a diff.


Pip Installation
================

Spot's source distribution tarball (as produced by ``make dist``)
can be installed directly into a Python virtual environment via
``pip install``.  The package bundles the native CLI tools
(ltl2tgba, autfilt, ...), shared libraries, and Python (SWIG)
bindings.  The packaging infrastructure lives in two files at the
top of the source tree: ``setup.py`` and ``pyproject.toml``.

To build with correct rpaths, you need one of ``patchelf`` or
``chrpath`` on Linux (``patchelf`` is preferred); the build will fail
with a clear error if neither is found.  On macOS the
``install_name_tool`` (shipped with Xcode command-line tools) is used
automatically.


Trying a local installation
---------------------------

Build a source tarball and install it in a temporary virtual
environment.

  % make dist              # -> creates spot-X.Y.Z.dev.tar.gz
  % python3 -m venv /tmp/spot-test-venv
  % /tmp/spot-test-venv/bin/pip install spot-Z.Y.Z.dev.tar.gz

This will run ``./configure && make && make install`` from inside the
tarball and place everything in the virtual environment:

  /tmp/spot-test-venv/
    bin/                         # native CLI tools (ltl2tgba, autfilt, ...)
    lib/                         # shared libraries (libspot.so, ...)
    lib/python3.X/site-packages/ # Python package + SWIG .so extensions

Verify the installation:

  % /tmp/spot-test-venv/bin/python3 -c "import spot; print('OK')"
  % /tmp/spot-test-venv/bin/ltl2tgba --version