From 0b7c568795ab413cce5710f1cf736f6cd3261a7e Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Fri, 7 Jan 2022 14:25:38 -0800 Subject: [PATCH] Improve docs extension for examples (#7900) 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. --- docs/conf.py.in | 50 +++++++++++++++++++++++--- docs/ext/examples.py | 86 ++++++++++++++++++++------------------------ 2 files changed, 84 insertions(+), 52 deletions(-) diff --git a/docs/conf.py.in b/docs/conf.py.in index 37f7adfe8..23ef5da12 100644 --- a/docs/conf.py.in +++ b/docs/conf.py.in @@ -80,10 +80,52 @@ html_show_sourcelink = False html_extra_path = [] - -ex_patterns = { - '': '/../examples', - '': '/' + os.path.relpath('${CMAKE_BINARY_DIR}/deps/src/z3pycompat-EP', '${CMAKE_CURRENT_SOURCE_DIR}'), +# -- Configuration for examples extension ------------------------------------ +# Configuration for tabs: title, language and group for detecting missing files +examples_types = { + '\.cpp$': { + 'title': 'C++', + 'lang': 'c++', + 'group': 'c++' + }, + '\.java$': { + 'title': 'Java', + 'lang': 'java', + 'group': 'java' + }, + '^.*\.py$': { + 'title': 'Python', + 'lang': 'python', + 'group': 'py-regular' + }, + '^.*\.py$': { + 'title': 'Python z3py', + 'lang': 'python', + 'group': 'py-z3pycompat' + }, + '\.smt2$': { + 'title': 'SMT-LIBv2', + 'lang': 'smtlib', + 'group': 'smt2' + }, + '\.sy$': { + 'title': 'SyGuS', + 'lang': 'smtlib', + 'group': 'smt2' + }, +} +# Special file patterns +examples_file_patterns = { + '^(.*)': { + 'local': '/../examples{}', + 'url': 'https://github.com/cvc5/cvc5/tree/master/examples{}', + 'urlname': 'examples{}', + }, + '(.*)': { + 'local': '/' + os.path.relpath('${CMAKE_BINARY_DIR}/deps/src/z3pycompat-EP', '${CMAKE_CURRENT_SOURCE_DIR}') + '{}', + 'url': 'https://github.com/cvc5/cvc5_z3py_compat/tree/main{}', + 'urlname': 'cvc5_z3py_compat:{}', + } } # -- C++ / Breathe configuration --------------------------------------------- diff --git a/docs/ext/examples.py b/docs/ext/examples.py index b9a959f5f..bc81cfd0c 100644 --- a/docs/ext/examples.py +++ b/docs/ext/examples.py @@ -16,43 +16,26 @@ class APIExamples(SphinxDirective): The arguments should be proper filenames to source files. This directives tries to detect the language from the file extension - and supports the file extensions specified in `self.exts`. + and supports the file extensions specified in `examples_types`. + Additionally, `examples_file_patterns` allows to specify file name + patterns that allow using files from fixed directories more easily, and + to add proper download links. + + examples_types: + '': { + 'title': '', + 'lang': '', + 'group': '', + } + + examples_file_patterns: + '': { # match groups are used to format the strings below + 'local': '', + 'url': '', # optional + 'urlname': '', + } """ - # Set tab title and language for syntax highlighting - types = { - '\.cpp$': { - 'title': 'C++', - 'lang': 'c++', - 'group': 'c++' - }, - '\.java$': { - 'title': 'Java', - 'lang': 'java', - 'group': 'java' - }, - '.*\.py$': { - 'title': 'Python', - 'lang': 'python', - 'group': 'py-regular' - }, - '.*\.py$': { - 'title': 'Python z3py', - 'lang': 'python', - 'group': 'py-z3pycompat' - }, - '\.smt2$': { - 'title': 'SMT-LIBv2', - 'lang': 'smtlib', - 'group': 'smt2' - }, - '\.sy$': { - 'title': 'SyGuS', - 'lang': 'smtlib', - 'group': 'smt2' - }, - } - # The "arguments" are actually the content of the directive has_content = True @@ -65,18 +48,18 @@ class APIExamples(SphinxDirective): # collect everything in a list of strings content = ['.. tabs::', ''] - remaining = set([t['group'] for t in self.types.values()]) + remaining = set([t['group'] for t in self.env.config.examples_types.values()]) location = '{}:{}'.format(*self.get_source_info()) for file in self.content: # detect file extension lang = None title = None - for type in self.types: - if re.search(type, file) != None: - lang = self.types[type]['lang'] - title = self.types[type]['title'] - remaining.discard(self.types[type]['group']) + for pattern,data in self.env.config.examples_types.items(): + if re.search(pattern, file) != None: + lang = data['lang'] + title = data['title'] + remaining.discard(data['group']) break if lang == None: self.logger.warning( @@ -84,17 +67,23 @@ class APIExamples(SphinxDirective): title = os.path.splitext(file)[1] lang = title - for k, v in self.env.config.ex_patterns.items(): - file = file.replace(k, v) + url = None + urlname = None + for k, v in self.env.config.examples_file_patterns.items(): + m = re.match(k, file) + if m is not None: + file = v['local'].format(*m.groups()) + if 'url' in v: + url = v['url'].format(*m.groups()) + urlname = v['urlname'].format(*m.groups()) + break # generate tabs content.append(f' .. tab:: {title}') content.append(f'') - if file.startswith('/'): - # if the file is "absolute", we can provide a download link - urlname = os.path.relpath(os.path.join('..', file[1:]), os.path.join(self.srcdir, '..')) - url = f'https://github.com/cvc5/cvc5/tree/master/{urlname}' + if url is not None: + # we can provide a download link content.append(f' .. rst-class:: fa fa-download icon-margin') content.append(f' ') content.append(f' `{urlname} <{url}>`_') @@ -116,7 +105,8 @@ class APIExamples(SphinxDirective): def setup(app): APIExamples.srcdir = app.srcdir app.setup_extension('sphinx_tabs.tabs') - app.add_config_value('ex_patterns', {}, 'env') + app.add_config_value('examples_types', {}, 'env') + app.add_config_value('examples_file_patterns', {}, 'env') app.add_directive("api-examples", APIExamples) return { 'version': '0.1', -- 2.30.2