Various improvements to documentation (#7283)

This PR adds a couple of improvements to our documentation setup
- add an explicit dependency on the extension so that sphinx rebuilds pages appropriately when an extension is modified
- sphinx now emits warnings for examples that are not implemented in all languages (smt2, cpp, java and python)
- add -v to make the sphinx output more log-file friendly
- avoid a warning when the java bindings (and thus java docs) are not build
- replace file(WRITE by configure_file to avoid rather common erroneous rebuilds of python docs
- fix a reference to a label in the python docs
- suppress timestamps in javadoc output to avoid docs-ci being triggered for every PR
- improve placeholder message when java bindings are disabled

6 files changed, 26 insertions, 8 deletions

diff --git a/docs/CMakeLists.txt b/docs/CMakeLists.txt
index 15c51ed4f..d9a847954 100644
--- a/docs/CMakeLists.txt
+++ b/docs/CMakeLists.txt
@@ -28,7 +28,7 @@ add_custom_target(
   docs
   DEPENDS docs-cpp docs-java docs-python gen-options
   COMMAND
-    ${SPHINX_EXECUTABLE} -b html -c ${CMAKE_CURRENT_BINARY_DIR}
+    ${SPHINX_EXECUTABLE} -v -b html -c ${CMAKE_CURRENT_BINARY_DIR}
     # Tell Breathe where to find the Doxygen output
     -Dbreathe_projects.cvc5=${CPP_DOXYGEN_XML_DIR}
     -Dbreathe_projects.std=${CPP_DOXYGEN_XML_DIR} ${SPHINX_INPUT_DIR}
diff --git a/docs/api/java/CMakeLists.txt b/docs/api/java/CMakeLists.txt
index 5606357c6..6515fc29f 100644
--- a/docs/api/java/CMakeLists.txt
+++ b/docs/api/java/CMakeLists.txt
@@ -32,6 +32,7 @@ if(BUILD_BINDINGS_JAVA)
       --source-path ${CMAKE_SOURCE_DIR}/src/api/java/
       -d ${JAVADOC_OUTPUT_DIR}
       -cp ${CMAKE_BINARY_DIR}/src/api/java/cvc5.jar
+      -notimestamp
     DEPENDS cvc5jar ${SOURCES}
     COMMENT "Generating javadocs"
   )
diff --git a/docs/api/java/index.rst b/docs/api/java/index.rst
index 1aee013fc..f805880cc 100644
--- a/docs/api/java/index.rst
+++ b/docs/api/java/index.rst
@@ -1,4 +1,4 @@
 Java API Documentation
 ======================
 
-This file is just a placeholder that is replaced by javadocs index.html
\ No newline at end of file
+This documentation was built while Java bindings were disabled. This part of the documentation is empty. Please enable :code:`BUILD_BINDINGS_JAVA` in :code:`cmake` and build the documentation again.
diff --git a/docs/conf.py.in b/docs/conf.py.in
index 0df5b2397..71982b992 100644
--- a/docs/conf.py.in
+++ b/docs/conf.py.in
@@ -72,11 +72,9 @@ html_static_path = ['${CMAKE_CURRENT_SOURCE_DIR}/_static/']
 html_css_files = ['custom.css']
 html_show_sourcelink = False
 
-html_extra_path = [
-        "${CMAKE_BINARY_DIR}/docs/api/java/build/"
-]
+html_extra_path = []
 
-# -- Breathe configuration ---------------------------------------------------
+# -- C++ / Breathe configuration ---------------------------------------------
 breathe_default_project = "cvc5"
 breathe_domain_by_extension = {"h" : "cpp"}
 cpp_index_common_prefix = ["cvc5::api::"]
@@ -84,6 +82,12 @@ cpp_index_common_prefix = ["cvc5::api::"]
 # where to look for include-build-file
 ibf_folders = ['${CMAKE_CURRENT_BINARY_DIR}']
 
+
+# -- Java configuration ------------------------------------------------------
+if tags.has('bindings_java'):
+        html_extra_path.append('${CMAKE_BINARY_DIR}/docs/api/java/build/')
+
+
 # -- SMT-LIB syntax highlighting ---------------------------------------------
 from smtliblexer import SmtLibLexer
 from sphinx.highlighting import lexers
diff --git a/docs/ext/examples.py b/docs/ext/examples.py
index 9f8f7294e..7b62cee1b 100644
--- a/docs/ext/examples.py
+++ b/docs/ext/examples.py
@@ -1,11 +1,12 @@
 import os
 
 from docutils import nodes
-from docutils.parsers.rst import Directive
 from docutils.statemachine import StringList
+from sphinx.util import logging
+from sphinx.util.docutils import SphinxDirective
 
 
-class APIExamples(Directive):
+class APIExamples(SphinxDirective):
     """Add directive `api-examples` to be used as follows:
 
         .. api-examples::
@@ -28,17 +29,25 @@ class APIExamples(Directive):
     # The "arguments" are actually the content of the directive
     has_content = True
 
+    logger = logging.getLogger(__name__)
+
     def run(self):
+        self.state.document.settings.env.note_dependency(__file__)
         # collect everything in a list of strings
         content = ['.. tabs::', '']
 
+        remaining = set(self.exts.keys())
+        location = '{}:{}'.format(*self.get_source_info())
+
         for file in self.content:
             # detect file extension
             _, ext = os.path.splitext(file)
             if ext in self.exts:
                 title = self.exts[ext]['title']
                 lang = self.exts[ext]['lang']
+                remaining.remove(ext)
             else:
+                self.logger.warning(f'{location} is using unknown file extension "{ext}"')
                 title = ext
                 lang = ext
 
@@ -49,6 +58,9 @@ class APIExamples(Directive):
             content.append(f'            :language: {lang}')
             content.append(f'            :linenos:')
 
+        for r in remaining:
+            self.logger.warning(f'{location} has no {r} example!')
+
         # parse the string list
         node = nodes.Element()
         self.state.nested_parse(StringList(content), 0, node)
diff --git a/docs/ext/include_build_file.py b/docs/ext/include_build_file.py
index 02da60404..d6c4619d8 100644
--- a/docs/ext/include_build_file.py
+++ b/docs/ext/include_build_file.py
@@ -19,6 +19,7 @@ class IncludeBuildFile(SphinxDirective):
     has_content = True
 
     def run(self):
+        self.state.document.settings.env.note_dependency(__file__)
         filename = ''.join(self.content)
         for folder in self.env.config.ibf_folders:
             candidate = os.path.join(folder, filename)