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

diff --git a/docs/CMakeLists.txt b/docs/CMakeLists.txt
index 15c51ed4face653eb833f842cbe47cbe6f041739..d9a847954edc6fbdd0232d173c18c2aebfdd8f08 100644 (file)
--- 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 5606357c612a6904fa5b6acc1e508b1ddc36c572..6515fc29f1ca08c4ea8fdb63002e141640ec2700 100644 (file)
--- 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 1aee013fc45bfa313b279d04c45674df54ad010a..f805880ccf877679f4c6126581d1ccda1d697fbf 100644 (file)
--- 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 0df5b2397f76a6727974cb53fcb6c519cd1c1600..71982b992dc563f4cf743c7315717ed1914bbd9c 100644 (file)
--- 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 9f8f7294edcce1e96c11ac882c95941e1b13565f..7b62cee1b06694e196d7f2b3cc161781976f60e1 100644 (file)
--- 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 02da6040471000db2fbb2cf60943c3183842f60a..d6c4619d863ad9e049e630d7a63610da9095dd35 100644 (file)
--- 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)

diff --git a/src/api/python/CMakeLists.txt b/src/api/python/CMakeLists.txt
index dce0208cbc3fbdaed31a14a2392061f38d4971d2..74d1d84fc045dd5d98831cb70020f3a05f06f65c 100644 (file)
--- a/src/api/python/CMakeLists.txt
+++ b/src/api/python/CMakeLists.txt
@@ -111,11 +111,7 @@ python_extension_module(pycvc5)
 # Installation based on https://bloerg.net/2012/11/10/cmake-and-distutils.html
 # Create a wrapper python directory and generate a distutils setup.py file
 configure_file(setup.py.in setup.py)
-file(WRITE ${CMAKE_CURRENT_BINARY_DIR}/pycvc5/__init__.py
-"import sys
-from .pycvc5 import *
-# fake a submodule for dotted imports, e.g. from pycvc5.kinds import *
-sys.modules['%s.%s'%(__name__, kinds.__name__)] = kinds")
+configure_file(__init__.py.in pycvc5/__init__.py)
 
 # figure out if we're in a virtualenv
 execute_process(OUTPUT_VARIABLE IN_VIRTUALENV

diff --git a/src/api/python/__init__.py.in b/src/api/python/__init__.py.in
new file mode 100644 (file)
index 0000000..9116976
--- /dev/null
+++ b/src/api/python/__init__.py.in
@@ -0,0 +1,4 @@
+import sys
+from .pycvc5 import *
+# fake a submodule for dotted imports, e.g. from pycvc5.kinds import *
+sys.modules['%s.%s'%(__name__, kinds.__name__)] = kinds

diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index 7659740de28de8a5a117392bcd7277ff759f5523..0f6b54dc6a0f20e2cd5e86fda60c931dfa44c676 100644 (file)
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -1867,7 +1867,7 @@ cdef class Solver:
 
             ( get-unsat-core )
 
-        Requires to enable option :ref:`produce-unsat-cores <lbl-produce-unsat-cores>`.
+        Requires to enable option :ref:`produce-unsat-cores <lbl-option-produce-unsat-cores>`.
 
         :return: a set of terms representing the unsatisfiable core
         """