From 6dc5b7469cee015a3bcf25a1543123da6c8317fe Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Wed, 19 May 2021 07:55:53 +0200 Subject: 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. --- 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 +- 19 files changed, 128 insertions(+), 21 deletions(-) (limited to 'src/options') 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" -- cgit v1.2.3