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 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 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.
This PR adds (most of) the existing examples to the documentation, and does some other minor updates on the documentation. Some details:
- for consistency, all cpp examples are moved from examples/api to examples/api/cpp
- add capabilities for SMT-LIB examples, and two simple smt2 examples
- more docs/examples/*.rst files
- two new documentation categories: installation (how to obtain, compile and install cvc5) and binary (about the cvc5 binary)
