From 6dc5b7469cee015a3bcf25a1543123da6c8317fe Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Wed, 19 May 2021 07:55:53 +0200 Subject: [PATCH] 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. --- docs/CMakeLists.txt | 2 +- docs/_static/custom.css | 1 + docs/conf.py.in | 4 + docs/ext/include_build_file.py | 44 +++++++++ docs/index.rst | 1 + docs/options.rst | 5 + src/options/CMakeLists.txt | 2 + src/options/arith_options.toml | 2 +- src/options/arrays_options.toml | 2 +- src/options/booleans_options.toml | 2 +- src/options/builtin_options.toml | 2 +- src/options/bv_options.toml | 2 +- src/options/datatypes_options.toml | 2 +- src/options/decision_options.toml | 2 +- src/options/expr_options.toml | 2 +- src/options/fp_options.toml | 2 +- src/options/mkoptions.py | 113 +++++++++++++++++++++- src/options/prop_options.toml | 2 +- src/options/resource_manager_options.toml | 2 +- src/options/sep_options.toml | 2 +- src/options/sets_options.toml | 2 +- src/options/smt_options.toml | 2 +- src/options/strings_options.toml | 2 +- src/options/theory_options.toml | 2 +- src/options/uf_options.toml | 2 +- 25 files changed, 184 insertions(+), 22 deletions(-) create mode 100644 docs/ext/include_build_file.py create mode 100644 docs/options.rst 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:: + + 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" -- 2.30.2