diff --git a/HACKING b/HACKING
index e40590478..1ba7f1c9e 100644
--- a/HACKING
+++ b/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
----------------------
diff --git a/NEWS b/NEWS
index 4b36ee679..fc4fd6f40 100644
--- a/NEWS
+++ b/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
diff --git a/README b/README
index 6758d43dc..796e7b7ce 100644
--- a/README
+++ b/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.
- spot.html/ HTML reference manual for the library.
+ userdoc/ HTML documentation about command-line tools, and examples.
+ 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,
diff --git a/configure.ac b/configure.ac
index 420b42df2..7b18fd0d2 100644
--- a/configure.ac
+++ b/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
-# only require a relative path.
-AC_PATH_PROG([DOT], [dot])
+AC_CHECK_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
diff --git a/debian/rules b/debian/rules
index dde038b05..e9afe2f9d 100755
--- a/debian/rules
+++ b/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
diff --git a/doc/Doxyfile.in b/doc/Doxyfile.in
index 7948b7403..52ee00eaa 100644
--- a/doc/Doxyfile.in
+++ b/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
diff --git a/doc/Makefile.am b/doc/Makefile.am
index a1297a6f3..2d1053be4 100644
--- a/doc/Makefile.am
+++ b/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 .
-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
- $(MAKE) $(srcdir)/stamp
+ -rm -f 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
-# Spot documentation.
-dist_pkgdata_DATA = $(srcdir)/spot.tag
+DISTCLEANFILES = spot.tag spot.html stamp
.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:
diff --git a/doc/dot.in b/doc/dot.in
deleted file mode 100644
index f31007347..000000000
--- a/doc/dot.in
+++ /dev/null
@@ -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 .
-
-# 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@ "$@"