diff --git a/ChangeLog b/ChangeLog index 386bb8d4a..16a66fb85 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,10 @@ +2011-02-08 Alexandre Duret-Lutz + + Add some tricks into HACKING. + + * README: Typo. + * HACKING: s/CVS/GIT/ and add some tricks about libtool and doxygen. + 2011-02-08 Alexandre Duret-Lutz Adjust the WDBA test to count for sub-transitions. diff --git a/HACKING b/HACKING index 3c53adf4b..0d96d366d 100644 --- a/HACKING +++ b/HACKING @@ -1,12 +1,12 @@ -Bootstraping from CVS: +Bootstraping from 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 CVS because it can generate lots of changes or +all of them under GIT because it can generate lots of changes or conflicts. -Here are the tools you need to bootstrap the CVS tree, or more +Here are the tools you need to bootstrap the GIT tree, or more generally if you plan to regenerate some of the generated files. GNU Autoconf >= 2.61 @@ -17,7 +17,7 @@ generally if you plan to regenerate some of the generated files. SWIG >= 1.3.31 Doxygen >= 1.4.0 -Bootstrap the CVS tree by running +Bootstrap the GIT tree by running autoreconf -vfi @@ -27,6 +27,69 @@ and then go on with the usual 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. + + +Debugging Libtool executables +----------------------------- + +The executable 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 executable are just script that +run the actual binary after setting some environment variable 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 src/tgbatest + % file ltl2tgba + ltl2tgba: POSIX shell script text executable + % gdb -q ltl2tgba + "/home/adl/git/spot/src/tgbatest/ltl2tgba": not in executable format: File format not recognized + (gdb) quit + +The proper way to work on these libtool scripts is via the libtool +command: + + % ../../libtool --mode=execute file ltl2tgba + /home/adl/git/spot/src/tgbatest/.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/src/tgbatest/.libs/lt-ltl2tgba...done. + (gdb) quit + +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. + +You might also find conveniant to define a alias, a function, or a +script to shorten the invocation of "libtool --mode=execute". + +Also there is an undocumented feature of libtool that allows you to +shorthand "libtool --mode=execute" as "libtool execute" or even +"libtool e". + + Coding conventions: =================== diff --git a/README b/README index a51b67266..6d19add82 100644 --- a/README +++ b/README @@ -22,8 +22,8 @@ later). Especially, Python's headers files should be installed. Spot also uses modified versions of BuDDy (a binary decision diagram), and LBTT (an LTL to Büchi test bench). You do not need to install -these yourself, they are included in this package (directories buddy/ -and lbtt/), and will built and installed alongside of Spot. +these yourself: they are included in this package (directories buddy/ +and lbtt/) and will be built and installed alongside of Spot. Building and installing @@ -33,7 +33,7 @@ Spot follows the traditional `./configure && make && make check && make install' process. People unfamiliar with the GNU Build System should read the file INSTALL for generic instructions. -In additions to its usual options, ./configure will accept some +In addition to its usual options, ./configure will accept some flags specific to Spot: --with-gspn=DIR