doc: implement --enable-doxygen and do not distribute the doc

Fixes #299.

* configure.ac, doc/Makefile.am: Adjust.
* NEWS, HACKING, README: Document the change.
* doc/dot.in: Delete, not used anymore.
* doc/Doxyfile.in: Adjust to not look for dot.
* debian/rules: Use --enable-doxygen.

HACKING

@@ -80,25 +80,6 @@ and then go on with the usual
 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
 ----------------------
 

NEWS

@@ -1,5 +1,13 @@
 New in spot 2.4.2.dev (not yet released)
 
+  Build:
+
+  - We no longuer distribute the doxygen-generated documentation in
+    the tarball of Spot to save space.  This documentation is still
+    available online at https://spot.lrde.epita.fr/doxygen/.  If you
+    want to build a local copy you can configure Spot with
+    --enable-doxygen, or simply run "cd doc && make doc".
+
   Tools:
 
   - genltl learned to generate a new family of formulas, taken from

README

@@ -115,6 +115,13 @@ flags specific to Spot:
     do not have a working Python 3.2+ installation or if you are
     attempting some cross-compilation.
 
+  --enable-doxygen
+    Generate the Doxygen documentation for the code as part of the
+    build.  This requires Doxygen to be installed.  Even if
+    --enable-doxygen has not been given, you can force the
+    documentation to be built by running "make doc" inside the doc/
+    directory.
+
   --enable-devel
     Enable debugging symbols, turn off aggressive optimizations, and
     turn on assertions.  This option is effective by default in
@@ -201,8 +208,8 @@ tests/            Test suite.
 doc/              Documentation for Spot.
    org/           Source of userdoc/ as org-mode files.
    tl/            Documentation of the Temporal Logic operators.
-   userdoc/       HTML documentation about the command-line tools.
+   userdoc/       HTML documentation about command-line tools, and examples.
-   spot.html/     HTML reference manual for the library.
+   spot.html/     HTML doc for C++ API (not distributed, use --enable-doxygen).
 bench/            Benchmarks for ...
    dtgbasat/      ... SAT-based minimization of DTGBA,
    emptchk/       ... emptiness-check algorithms,

configure.ac

@@ -53,6 +53,12 @@ AC_ARG_ENABLE([c++17],
                               [Compile in C++17 mode.])],
               [enable_17=yes], [enable_17=no])
 
+AC_ARG_ENABLE([doxygen],
+              [AC_HELP_STRING([--enable-doxygen]),
+  [enable generation of Doxygen documentation (requires Doxygen)])]
+  [enable_doxygen=yes], [enable_doxygen=no])
+AM_CONDITIONAL([ENABLE_DOXYGEN], [test "x${enable_doxygen:-no}" = xyes])
+
 # Activate C11 for gnulib tests
 AX_CHECK_COMPILE_FLAG([-std=c11], [CFLAGS="$CFLAGS -std=c11"])
 
@@ -164,9 +170,7 @@ if test x$enable_warnings = xyes; then
 fi
 
 AM_CONDITIONAL([NEVER], [false])
-# We need the absolute path for dot in the "doc/dot" script. Other places
+AC_CHECK_PROG([DOT], [dot])
-# only require a relative path.
-AC_PATH_PROG([DOT], [dot])
 AC_CHECK_PROG([LBT], [lbt], [lbt])
 AC_CHECK_PROG([LTL2BA], [ltl2ba], [ltl2ba])
 AC_CHECK_PROG([LTL3BA], [ltl3ba], [ltl3ba])
@@ -237,7 +241,6 @@ AC_CONFIG_FILES([
   tools/x-to-1
 ])
 AC_CONFIG_FILES([doc/org/g++wrap], [chmod +x doc/org/g++wrap])
-AC_CONFIG_FILES([doc/dot], [chmod +x doc/dot])
 AC_CONFIG_FILES([tests/run], [chmod +x tests/run])
 AC_OUTPUT
 

debian/rules

@@ -65,7 +65,8 @@ override_dh_auto_configure:
 	make clean
 	dh_auto_configure -- $(PRO2SETUP) $(LTOSETUP)	\
 	  --disable-devel --enable-optimizations	\
-	  --disable-static PYTHON=/usr/bin/$(PYDEFAULT)
+	  --disable-static --enable-doxygen \
+          PYTHON=/usr/bin/$(PYDEFAULT)
 	$(FLTOWORKAROUND)
 override_dh_auto_install: fix-js
 	dh_auto_install --destdir=$(CURDIR)/debian/tmp

doc/Doxyfile.in

@@ -1049,7 +1049,7 @@ GENERATE_HTML          = YES
 # The default directory is: html.
 # This tag requires that the tag GENERATE_HTML is set to YES.
 
-HTML_OUTPUT            = @srcdir@/spot.html
+HTML_OUTPUT            = spot.html
 
 # The HTML_FILE_EXTENSION tag can be used to specify the file extension for each
 # generated HTML page (for example: .htm, .php, .asp).
@@ -2296,7 +2296,7 @@ INTERACTIVE_SVG        = YES
 # found. If left blank, it is assumed the dot tool can be found in the path.
 # This tag requires that the tag HAVE_DOT is set to YES.
 
-DOT_PATH               = @srcdir@
+DOT_PATH               =
 
 # The DOTFILE_DIRS tag can be used to specify one or more directories that
 # contain dot files that are included in the documentation (see the \dotfile

doc/Makefile.am

@@ -20,39 +20,29 @@
 ## You should have received a copy of the GNU General Public License
 ## along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
-DOXYGEN = doxygen
-
 SUBDIRS = tl
 
-.PHONY: doc fast-doc
+DOXYGEN = doxygen
+if ENABLE_DOXYGEN
+  DOXY_STAMP = stamp
+endif
 
-all-local: $(srcdir)/stamp $(srcdir)/org-stamp
+all-local: $(DOXY_STAMP) $(srcdir)/org-stamp
 
+.PHONY: doc
 doc:
-	-rm -f $(srcdir)/stamp
+	-rm -f stamp
-	$(MAKE) $(srcdir)/stamp
+	$(MAKE) stamp
 
-fast-doc:
+stamp: $(srcdir)/Doxyfile.in $(top_srcdir)/configure.ac
 	$(MAKE) Doxyfile
-## Doxygen 1.8.x will easily segfault during the parallel runs of dot.
-## 1.8.11 is supposed to be fixed, but until this version reaches all
-## our build hosts, let's try to run doxygen a second time when the
-## first attempt fails.
-## https://bugzilla.gnome.org/show_bug.cgi?id=756241
-	$(DOXYGEN) || $(DOXYGEN)
-	touch $(srcdir)/stamp
-
-$(srcdir)/stamp: $(srcdir)/Doxyfile.in $(top_srcdir)/configure.ac
-	$(MAKE) Doxyfile dot
 	-rm -rf spot.html spot.latex
 	$(DOXYGEN)
 	touch $@
 
-$(srcdir)/spot.html $(srcdir)/spot.tag: $(srcdir)/stamp
+spot.html spot.tag: stamp
 
-# spot.tag is useful to third-party packages that must link to the
+DISTCLEANFILES = spot.tag spot.html stamp
-# Spot documentation.
-dist_pkgdata_DATA = $(srcdir)/spot.tag
 
 .PHONY: org org-man
 org:
@@ -153,12 +143,11 @@ $(srcdir)/userdoc: $(srcdir)/org-stamp
 EXTRA_DIST = \
   footer.html \
   mainpage.dox \
-  $(srcdir)/stamp \
-  $(srcdir)/spot.html \
   $(ORG_FILES) \
   $(srcdir)/org-stamp \
   $(srcdir)/userdoc
 
+
 dist-hook: optipng
 .PHONY: optipng
 optipng:

doc/dot.in

@@ -1,32 +0,0 @@
-#!/bin/sh
-# Copyright (C) 2010 Laboratoire de Recherche et Développement de
-# l'Epita (LRDE).
-#
-# This file is part of Spot, a model checking library.
-#
-# Spot is free software; you can redistribute it and/or modify it
-# under the terms of the GNU General Public License as published by
-# the Free Software Foundation; either version 3 of the License, or
-# (at your option) any later version.
-#
-# Spot is distributed in the hope that it will be useful, but WITHOUT
-# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
-# or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
-# License for more details.
-#
-# You should have received a copy of the GNU General Public License
-# along with this program.  If not, see <http://www.gnu.org/licenses/>.
-
-# Rewrite any -Tpng argument as -Tpng:gd, the resulting files are 10
-# times smaller because they are not anti-aliased.
-for arg
-do
-    case $arg in
-	-Tpng) set x "$@" -Tpng:gd;;
-	*)     set x "$@" "$arg";;
-    esac
-    shift # x
-    shift # $arg
-done
-
-@DOT@ "$@"