diff --git a/ChangeLog b/ChangeLog index 4b05185cf..94af47e5b 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,8 @@ 2003-10-31 Alexandre Duret-Lutz + * README: More build instructions. + * HACKING: Update. + * doc/Makefile.am ($(srcdir)/spotref.pdf): Make sure to work in $(srcdir). diff --git a/HACKING b/HACKING index 1c3a518e5..87c5078c9 100644 --- a/HACKING +++ b/HACKING @@ -8,27 +8,34 @@ conflicts. Here are the tools you need to bootstrap the CVS tree, or more generally if you plan to regenerate some of the generated files. - + GNU Autoconf 2.57 - GNU Automake 1.7.3 + GNU Automake 1.7.8 GNU Flex (the version probably doesn't matter much, we used 2.5.4) The CVS version of GNU Bison (called 1.875b at the time of writing) SWIG 1.3.19 + Doxygen 1.3.4 Bootstrap the CVS tree by running autoreconf -vfi -and then go on with the usual +and then go on with the usual ./configure make + Coding conventions: =================== Here are the conventions we follow in Spot, so that the code looks -homogeneous. +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). Comments -------- @@ -39,16 +46,19 @@ Comments 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 on their own line. + * Braces are always on their own line. * Text within braces is two-space indented. { f(12); - + } * Anything after a control statement is two-space indented. This @@ -61,7 +71,7 @@ Formating g(456); } - * Braces from function/structure/enum/classe/namespace definitions + * Braces from function/structure/enum/class/namespace definitions are not indented. class foo @@ -73,9 +83,9 @@ Formating }; * The above corresponds to the `gnu' indentation style under Emacs. - - * Put return types or linkage specifiers on their own line in - function/method _definitions_ : + + * Put return types and linkage specifiers on their own line in + function/method _definitions_: static int Foo::get_mumble() @@ -85,9 +95,11 @@ Formating This makes it easier to grep functions in the code. - Function/method declarations can be put on one line. + Function/method declaration are usually written on one line: - * Space before parentheses in control statements + int get_bar(int i); + + * Put a space before the opening parenthesis in control statements if (test) { @@ -104,20 +116,19 @@ Formating * 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 befor postfix unary operators: if (!test && y++ != 0) @@ -135,11 +146,12 @@ Formating ... } - * If a line takes more than 80 columns, split it or rethink it. + * No line should be larger than 80 columns. + If a line takes more than 80 columns, split it or rethink it. - * Labels or case statements are left-indented by two spaces, + * Labels or case statements are back-indented by two spaces, without space before the `:'. - + if (something) { top: @@ -166,12 +178,12 @@ Naming 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. + * Private members end with an underscore. class my_class { @@ -193,7 +205,7 @@ Naming ... }; - * Enum mumblers also use capitalized name, with joined words. + * Enum members also use capitalized name, with joined words. * C Macros are all uppercase. @@ -214,4 +226,3 @@ Naming * The include guard for src/somedir/foo.hh is SPOT_SOMEDIR_FOO_HH - diff --git a/README b/README index 27b9b9375..0b9b995b1 100644 --- a/README +++ b/README @@ -1,3 +1,55 @@ +Installation +============ + +Requirements +------------ + +Spot requires a complete installation of Python (version 2.0 or +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. + + +Building and installing +----------------------- + +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 +flags specific to Spot: + + --with-gspn=DIR + Turns on GreatSPN support. DIR should designate the root of + GreatSPN source tree. (./configure will then run + DIR/SOURCES/contrib/version.sh to find the GreatSPN build tree.) + + GreatSPN had to be modified in order to be used as a library + (thanks Soheib Baarir and Yann Thierry-Mieg for this work), and + presently these modifications are only available on the GreatSPN + CVS repository hosted by the Università di Torino. + + --with-included-buddy + --with-included-lbtt + Once you have installed Spot the first time. Modified versions of + LBTT and BuDDy will be installed. The next time you reconfigure + Spot, configure will detect that these versions are already + installed, and will attempt to use these installed versions + directly (this is in case you had to modify one of these yourself + for another purpose). These two options will *force* the use, + build, and installation of the included versions of these package, + even when compatible versions are already installed. + + --enable-devel + Enable debugging symbols, turn off aggressive optimizations, and + turn on assertions. This options is effective by default in + development versions (version numbers ending with a letter). + + Layout of the source tree ========================= @@ -16,9 +68,9 @@ src/ Sources for libspot. tgbaparse/ Parser for explicit TGBAs. tgbatest/ Tests for tgba/, tgbaalgos/, and tgbaparse/. doc/ Documentation for libspot. - spot.html/ HTML manual. + spot.html/ HTML reference manual. spot.latex/ Sources for the PDF manual. (No distributed, can be rebuilt.) - spotref.pdf PDF manual. + spotref.pdf PDF reference manual. wrap/ Wrappers for other languages. python/ Python bindings for Spot and BuDDy tests/ Tests for these bindings