The `no_docstring` argument of
`sphinx.ext.autodoc.Documenter.add_content()` has been
[deprecated](https://www.sphinx-doc.org/en/master/changes.html) since
Sphinx 3.4.0 (released in December 2020). It seems that newer Sphinx
versions have removed that argument, which breaks our `EnumDocumenter`
(e.g., see the following
[example](https://github.com/cvc5/cvc5/runs/7081097179?check_suite_focus=true)).
This commit updates our use of
`sphinx.ext.autodoc.Documenter.add_content()`.
This PR moves some stuff around in our documentation. Most notably, it moves some sections out of the "Binary documentation" to become their own top-level sections. While doing so, it refactors a few things in options and statistics to be more agnostic to the way cvc5 is used. To allow for command-output being used in regular (not auto-generated) documentation, we add a new extension that takes care of injecting the build folder into a new wrapper run-command.
We recently added automatic download links for examples in our documentation, however they assumed everything to live inside the main cvc5 repo while, e.g., the examples for the z3py compat API do not. While #7896 provided a very simple fix, it mixes different concerns (rendering of tabs vs. locating the input files, though they should coincide right now).
This PR takes a more fundamental approach by extending the current pattern mechanism to allow for explicit url specification.
Closes#7896.
This PR adds a download link to all examples in the documentation
(that are included via the examples extension). I think we should do
this, as we have text like "download the example here" at several
places already...
This PR does multiple things:
- the kinds are changed from custom objects to a proper enum.Enum class
(including according changes to the cython code and the kind generation scripts)
- all examples and tests are modified to account for the change how to use kinds
(Kind instead of kinds)
- add docstrings to the kind enum values
- add a custom documenter that properly renders enums via autodoc
- extend doxygen setup so that we can write comments as rst (allowing us to copy
the documentation for kinds from the cpp api to the other apis)
This PR extends the custom sphinx extension for examples. It now allows for simple patterns in the file names and matches the file types using arbitrary regular expressions instead of just looking at the file extensions. This is necessary to integrate examples from the z3pycompat API: the examples live at a nontrivial place (in the build folder), which we inject via the file name patterns; we will have two separate examples which both end in .py but can be distinguished via the pattern used in the beginning.
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
This PR refactors the lexer used by sphinx for highlighting SMT-LIB files. This new lexer properly checks for word boundaries and uses the proper character sets from the SMT-LIB standard.
This migrates page https://cvc4.github.io/sets-and-relations.
It further adds the SMT2 version of examples/api/cpp/sets.cpp and adds
test/regress/regress0/rels/relations-ops.smt2 as smtlib example for
relations.
