From: Gereon Kremer <nafur42@gmail.com>
Date: Wed, 19 May 2021 05:55:53 +0000 (+0200)
Subject: Generate command line options for sphinx docs (#6555)
X-Git-Tag: cvc5-1.0.0~1743
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6dc5b7469cee015a3bcf25a1543123da6c8317fe;p=cvc5.git

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.
---

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
+
diff --git a/src/options/CMakeLists.txt b/src/options/CMakeLists.txt
index 078c2ad31..997c6850a 100644
--- a/src/options/CMakeLists.txt
+++ b/src/options/CMakeLists.txt
@@ -74,10 +74,12 @@ add_custom_command(
     OUTPUT
       options.h options.cpp
       ${options_gen_cpp_files} ${options_gen_h_files}
+      ${CMAKE_BINARY_DIR}/docs/options_generated.rst
     COMMAND
       ${PYTHON_EXECUTABLE}
       ${CMAKE_CURRENT_LIST_DIR}/mkoptions.py
       ${CMAKE_CURRENT_LIST_DIR}
+      ${CMAKE_BINARY_DIR}
       ${CMAKE_CURRENT_BINARY_DIR}
       ${abs_toml_files}
     DEPENDS
diff --git a/src/options/arith_options.toml b/src/options/arith_options.toml
index a52f2144e..472657274 100644
--- a/src/options/arith_options.toml
+++ b/src/options/arith_options.toml
@@ -1,5 +1,5 @@
 id     = "ARITH"
-name   = "Arithmetic theory"
+name   = "Arithmetic Theory"
 
 [[option]]
   name       = "arithUnateLemmaMode"
diff --git a/src/options/arrays_options.toml b/src/options/arrays_options.toml
index 6017edfd5..4cb6dda1d 100644
--- a/src/options/arrays_options.toml
+++ b/src/options/arrays_options.toml
@@ -1,5 +1,5 @@
 id     = "ARRAYS"
-name   = "Arrays theory"
+name   = "Arrays Theory"
 
 [[option]]
   name       = "arraysOptimizeLinear"
diff --git a/src/options/booleans_options.toml b/src/options/booleans_options.toml
index 52725bb8e..4aa46cfa2 100644
--- a/src/options/booleans_options.toml
+++ b/src/options/booleans_options.toml
@@ -1,3 +1,3 @@
 id     = "BOOLEANS"
-name   = "Boolean theory"
+name   = "Boolean Theory"
 
diff --git a/src/options/builtin_options.toml b/src/options/builtin_options.toml
index b5f2ed593..e4d4296fa 100644
--- a/src/options/builtin_options.toml
+++ b/src/options/builtin_options.toml
@@ -1,3 +1,3 @@
 id     = "BUILTIN"
-name   = "Builtin theory"
+name   = "Builtin Theory"
 
diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml
index 6cbf9cf37..e5b96b54a 100644
--- a/src/options/bv_options.toml
+++ b/src/options/bv_options.toml
@@ -1,5 +1,5 @@
 id     = "BV"
-name   = "Bitvector theory"
+name   = "Bitvector Theory"
 
 [[option]]
   name       = "bvSatSolver"
diff --git a/src/options/datatypes_options.toml b/src/options/datatypes_options.toml
index 7c6a55095..80dedfb70 100644
--- a/src/options/datatypes_options.toml
+++ b/src/options/datatypes_options.toml
@@ -1,5 +1,5 @@
 id     = "DATATYPES"
-name   = "Datatypes theory"
+name   = "Datatypes Theory"
 
 # How to handle selectors applied to incorrect constructors.  If this option is set,
 # then we do not rewrite such a selector term to an arbitrary ground term.  
diff --git a/src/options/decision_options.toml b/src/options/decision_options.toml
index b3d18aebf..b6f5a5c1b 100644
--- a/src/options/decision_options.toml
+++ b/src/options/decision_options.toml
@@ -1,5 +1,5 @@
 id     = "DECISION"
-name   = "Decision heuristics"
+name   = "Decision Heuristics"
 
 [[option]]
   name       = "decisionMode"
diff --git a/src/options/expr_options.toml b/src/options/expr_options.toml
index 94a9db05b..ecd0bcf95 100644
--- a/src/options/expr_options.toml
+++ b/src/options/expr_options.toml
@@ -1,5 +1,5 @@
 id     = "EXPR"
-name   = "Expression package"
+name   = "Expression"
 
 [[option]]
   name       = "defaultExprDepth"
diff --git a/src/options/fp_options.toml b/src/options/fp_options.toml
index d726cec3b..6fd632a7c 100644
--- a/src/options/fp_options.toml
+++ b/src/options/fp_options.toml
@@ -1,5 +1,5 @@
 id     = "FP"
-name   = "Fp"
+name   = "Floating-Point"
 
 [[option]]
   name       = "fpExp"
diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py
index 4c3524456..4cc814a61 100644
--- a/src/options/mkoptions.py
+++ b/src/options/mkoptions.py
@@ -298,6 +298,104 @@ class Option(object):
                 self.long_opt = r[1]
 
 
+class SphinxGenerator:
+    def __init__(self):
+        self.common = []
+        self.others = {}
+
+    def add(self, module, option):
+        if option.category == 'undocumented':
+            return
+        if not option.long and not option.short:
+            return
+        names = []
+        if option.long:
+            if option.long_opt:
+                names.append('--{}={}'.format(option.long_name, option.long_opt))
+            else:
+                names.append('--{}'.format(option.long_name))
+        
+        if option.alias:
+            if option.long_opt:
+                names.extend(['--{}={}'.format(a, option.long_opt) for a in option.alias])
+            else:
+                names.extend(['--{}'.format(a) for a in option.alias])
+
+        if option.short:
+            if option.long_opt:
+                names.append('-{} {}'.format(option.short, option.long_opt))
+            else:
+                names.append('-{}'.format(option.short))
+        
+        modes = None
+        if option.mode:
+            modes = {}
+            for _, data in option.mode.items():
+                assert len(data) == 1
+                data = data[0]
+                modes[data['name']] = data.get('help', '')
+
+        data = {
+            'name': names,
+            'help': option.help,
+            'expert': option.category == 'expert',
+            'alternate': option.type == 'bool' and option.alternate,
+            'help_mode': option.help_mode,
+            'modes': modes,
+        }
+
+        if option.category == 'common':
+            self.common.append(data)
+        else:
+            if module.name not in self.others:
+                self.others[module.name] = []
+            self.others[module.name].append(data)
+    
+    def __render_option(self, res, opt):
+        desc = '``{}``'
+        val = '    {}'
+        if opt['expert']:
+            res.append('.. admonition:: This option is intended for Experts only!')
+            res.append('    ')
+            desc = '    ' + desc
+            val = '    ' + val
+
+        if opt['alternate']:
+            desc += ' (also ``--no-*``)'
+        res.append(desc.format(' | '.join(opt['name'])))
+        res.append(val.format(opt['help']))
+
+        if opt['modes']:
+            print(opt['modes'])
+            res.append(val.format(''))
+            res.append(val.format(opt['help_mode']))
+            res.append(val.format(''))
+            for k, v in opt['modes'].items():
+                res.append(val.format(':{}: {}'.format(k, v)))
+        res.append('    ')
+
+
+    def render(self, dstdir, filename):
+        res = []
+
+        res.append('Most Commonly-Used cvc5 Options')
+        res.append('===============================')
+        for opt in self.common:
+            self.__render_option(res, opt)
+
+        res.append('')
+        res.append('Additional cvc5 Options')
+        res.append('=======================')
+        for module in self.others:
+            res.append('')
+            res.append('{} Module'.format(module))
+            res.append('-' * (len(module) + 8))
+            for opt in self.others[module]:
+                self.__render_option(res, opt)
+
+        write_file(dstdir, filename, '\n'.join(res))
+
+
 def die(msg):
     sys.exit('[error] {}'.format(msg))
 
@@ -626,7 +724,7 @@ def add_getopt_long(long_name, argument_req, getopt_long):
             'required' if argument_req else 'no', value))
 
 
-def codegen_all_modules(modules, dst_dir, tpl_options_h, tpl_options_cpp):
+def codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, tpl_options_cpp):
     """
     Generate code for all option modules (options.cpp, options_holder.h).
     """
@@ -645,6 +743,8 @@ def codegen_all_modules(modules, dst_dir, tpl_options_h, tpl_options_cpp):
     setoption_handlers = []  # handlers for set-option command
     getoption_handlers = []  # handlers for get-option command
 
+    sphinxgen = SphinxGenerator()
+
     for module in modules:
         headers_module.append(format_include(module.header))
 
@@ -660,6 +760,8 @@ def codegen_all_modules(modules, dst_dir, tpl_options_h, tpl_options_cpp):
 
             docgen_option(option, help_common, help_others)
 
+            sphinxgen.add(module, option)
+
             # Generate handler call
             handler = None
             if option.handler:
@@ -885,6 +987,8 @@ def codegen_all_modules(modules, dst_dir, tpl_options_h, tpl_options_cpp):
         getoption_handlers='\n'.join(getoption_handlers)
     ))
 
+    if os.path.isdir('{}/docs/'.format(build_dir)):
+        sphinxgen.render('{}/docs/'.format(build_dir), 'options_generated.rst')
 
 def lstrip(prefix, s):
     """
@@ -1010,8 +1114,9 @@ def mkoptions_main():
         die('missing arguments')
 
     src_dir = sys.argv[1]
-    dst_dir = sys.argv[2]
-    filenames = sys.argv[3:]
+    build_dir = sys.argv[2]
+    dst_dir = sys.argv[3]
+    filenames = sys.argv[4:]
 
     # Check if given directories exist.
     for d in [src_dir, dst_dir]:
@@ -1052,7 +1157,7 @@ def mkoptions_main():
         codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp)
 
     # Create options.cpp and options_holder.h in destination directory
-    codegen_all_modules(modules, dst_dir, tpl_options_h, tpl_options_cpp)
+    codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, tpl_options_cpp)
 
 
 
diff --git a/src/options/prop_options.toml b/src/options/prop_options.toml
index 69dad8d63..26d7a451b 100644
--- a/src/options/prop_options.toml
+++ b/src/options/prop_options.toml
@@ -1,5 +1,5 @@
 id     = "PROP"
-name   = "SAT layer"
+name   = "SAT Layer"
 
 [[option]]
   name       = "satRandomFreq"
diff --git a/src/options/resource_manager_options.toml b/src/options/resource_manager_options.toml
index 88bacce1b..6d5c4d4cf 100644
--- a/src/options/resource_manager_options.toml
+++ b/src/options/resource_manager_options.toml
@@ -1,5 +1,5 @@
 id     = "RESMAN"
-name   = "Resource Manager options"
+name   = "Resource Manager"
 
 [[option]]
   name       = "cumulativeMillisecondLimit"
diff --git a/src/options/sep_options.toml b/src/options/sep_options.toml
index f45e78c98..7185a35df 100644
--- a/src/options/sep_options.toml
+++ b/src/options/sep_options.toml
@@ -1,5 +1,5 @@
 id     = "SEP"
-name   = "Sep"
+name   = "Separation Logic Theory"
 
 [[option]]
   name       = "sepCheckNeg"
diff --git a/src/options/sets_options.toml b/src/options/sets_options.toml
index db9cfa480..dee134ae4 100644
--- a/src/options/sets_options.toml
+++ b/src/options/sets_options.toml
@@ -1,5 +1,5 @@
 id     = "SETS"
-name   = "Sets"
+name   = "Sets Theory"
 
 [[option]]
   name       = "setsProxyLemmas"
diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 22d05f6f7..733c2239c 100644
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -1,5 +1,5 @@
 id     = "SMT"
-name   = "SMT layer"
+name   = "SMT Layer"
 
 [[option]]
   name       = "dumpModeString"
diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml
index 44c9c191f..958136494 100644
--- a/src/options/strings_options.toml
+++ b/src/options/strings_options.toml
@@ -1,5 +1,5 @@
 id     = "STRINGS"
-name   = "Strings theory"
+name   = "Strings Theory"
 
 [[option]]
   name       = "stringExp"
diff --git a/src/options/theory_options.toml b/src/options/theory_options.toml
index ec11d17ec..f47907683 100644
--- a/src/options/theory_options.toml
+++ b/src/options/theory_options.toml
@@ -1,5 +1,5 @@
 id     = "THEORY"
-name   = "Theory layer"
+name   = "Theory Layer"
 
 [[option]]
   name       = "theoryOfMode"
diff --git a/src/options/uf_options.toml b/src/options/uf_options.toml
index 81b119964..058d8be27 100644
--- a/src/options/uf_options.toml
+++ b/src/options/uf_options.toml
@@ -1,5 +1,5 @@
 id     = "UF"
-name   = "Uninterpreted functions theory"
+name   = "Uninterpreted Functions Theory"
 
 [[option]]
   name       = "ufSymmetryBreaker"