Generate command line options for sphinx docs (#6555)

This PR adds documentation about the command line options to the sphinx documentation. It is mostly a reformatted version of what --help would print.

6 files changed, 56 insertions, 1 deletions

diff --git a/docs/CMakeLists.txt b/docs/CMakeLists.txt
index 4c5d9aa6c..99c4f3ab3 100644
--- a/docs/CMakeLists.txt
+++ b/docs/CMakeLists.txt
@@ -26,7 +26,7 @@ set(SPHINX_OUTPUT_DIR ${CMAKE_CURRENT_BINARY_DIR}/sphinx)
 configure_file(conf.py.in ${CMAKE_CURRENT_BINARY_DIR}/conf.py)
 
 add_custom_target(docs ALL
-                  DEPENDS docs-cpp docs-python
+                  DEPENDS docs-cpp docs-python gen-options
                   COMMAND
                     ${SPHINX_EXECUTABLE} -b html
                     -c ${CMAKE_CURRENT_BINARY_DIR}
diff --git a/docs/_static/custom.css b/docs/_static/custom.css
index a0348f9ed..f657196ed 100644
--- a/docs/_static/custom.css
+++ b/docs/_static/custom.css
@@ -20,6 +20,7 @@ code.xref {
 
 .rst-content code {
     padding: 1px !important;
+    background: unset !important;
 }
 
 a {
diff --git a/docs/conf.py.in b/docs/conf.py.in
index f6e75b9b5..07a4d8a76 100644
--- a/docs/conf.py.in
+++ b/docs/conf.py.in
@@ -43,6 +43,7 @@ extensions = [
         'sphinxcontrib.bibtex',
         'sphinx_tabs.tabs',
         'examples',
+        'include_build_file',
 ]
 
 bibtex_bibfiles = ['references.bib']
@@ -69,3 +70,6 @@ html_css_files = ['custom.css']
 # -- Breathe configuration ---------------------------------------------------
 breathe_default_project = "cvc5"
 breathe_domain_by_extension = {"h" : "cpp"}
+
+# where to look for include-build-file
+ibf_folders = ['${CMAKE_CURRENT_BINARY_DIR}']
diff --git a/docs/ext/include_build_file.py b/docs/ext/include_build_file.py
new file mode 100644
index 000000000..02da60404
--- /dev/null
+++ b/docs/ext/include_build_file.py
@@ -0,0 +1,44 @@
+import os
+
+from docutils import nodes
+from docutils.parsers.rst import Directive
+from docutils.statemachine import StringList
+from sphinx.util.docutils import SphinxDirective
+from sphinx.util.nodes import nested_parse_with_titles
+
+class IncludeBuildFile(SphinxDirective):
+    """Add directive `include-build-file` to be used as follows:
+
+        .. include-build-file:: <filename>
+
+    The argument should be a filename of an rst files within one of the
+    folders given by the `ibf_folders` config option.
+    """
+
+    # The "arguments" are actually the content of the directive
+    has_content = True
+
+    def run(self):
+        filename = ''.join(self.content)
+        for folder in self.env.config.ibf_folders:
+            candidate = os.path.join(folder, filename)
+            if os.path.isfile(candidate):
+                filename = candidate
+                break
+        content = open(filename).readlines()
+        content = [line.rstrip('\n') for line in content]
+        # parse the string list
+        node = nodes.Element()
+        nested_parse_with_titles(self.state, StringList(content), node)
+        self.state.document.settings.env.note_dependency(filename)
+        return node.children
+
+
+def setup(app):
+    app.add_config_value('ibf_folders', [], 'env')
+    app.add_directive('include-build-file', IncludeBuildFile)
+    return {
+        'version': '0.1',
+        'parallel_read_safe': True,
+        'parallel_write_safe': True,
+    }
diff --git a/docs/index.rst b/docs/index.rst
index 14adad0fc..8d77790fb 100644
--- a/docs/index.rst
+++ b/docs/index.rst
@@ -19,3 +19,4 @@ cvc5 API Documentation
    python/python
    references
    examples/examples
+   options
diff --git a/docs/options.rst b/docs/options.rst
new file mode 100644
index 000000000..6f9c613e7
--- /dev/null
+++ b/docs/options.rst
@@ -0,0 +1,5 @@
+Commandline Options
+===================
+
+.. include-build-file:: options_generated.rst
+