From: Gereon Kremer Date: Mon, 4 Oct 2021 20:59:28 +0000 (-0700) Subject: Various improvements to documentation (#7283) X-Git-Tag: cvc5-1.0.0~1126 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3630215cc02f7243fccba0a8078dd251a252abdc;p=cvc5.git 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 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) diff --git a/src/api/python/CMakeLists.txt b/src/api/python/CMakeLists.txt index dce0208cb..74d1d84fc 100644 --- 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 index 000000000..9116976c3 --- /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 7659740de..0f6b54dc6 100644 --- 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 `. + Requires to enable option :ref:`produce-unsat-cores `. :return: a set of terms representing the unsatisfiable core """