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.

diff --git a/docs/conf.py.in b/docs/conf.py.in
index 37f7adfe8c4d3aa76a2b9a08c4f93f2506ecc3ad..23ef5da12ba4c9382da98c73be4706c70636b955 100644 (file)
--- a/docs/conf.py.in
+++ b/docs/conf.py.in
@@ -80,10 +80,52 @@ html_show_sourcelink = False
 
 html_extra_path = []
 
-
-ex_patterns = {
-        '<examples>': '/../examples',
-        '<z3pycompat>': '/' + 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'
+        },
+        '^<examples>.*\.py$': {
+                'title': 'Python',
+                'lang': 'python',
+                'group': 'py-regular'
+        },
+        '^<z3pycompat>.*\.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 = {
+        '^<examples>(.*)': {
+                'local': '/../examples{}',
+                'url': 'https://github.com/cvc5/cvc5/tree/master/examples{}',
+                'urlname': 'examples{}',
+        },
+        '<z3pycompat>(.*)': {
+                '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 b9a959f5fa769753cbcc10e25ffc5a40832f7d82..bc81cfd0c452ae0c650778a3dfd726fab611e39a 100644 (file)
--- 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:
+            '<regex>': {
+                'title': '<tab title>',
+                'lang': '<language identifier for synatax highlighting>',
+                'group': '<group identifier to detext missing examples>',
+            }
+
+        examples_file_patterns:
+            '<regex>': { # match groups are used to format the strings below
+                'local': '<pseudo-absolute path to local file>',
+                'url': '<url to download this file>', # optional
+                'urlname': '<text for the download link>',
+            }
     """
 
-    # Set tab title and language for syntax highlighting
-    types = {
-        '\.cpp$': {
-            'title': 'C++',
-            'lang': 'c++',
-            'group': 'c++'
-        },
-        '\.java$': {
-            'title': 'Java',
-            'lang': 'java',
-            'group': 'java'
-        },
-        '<examples>.*\.py$': {
-            'title': 'Python',
-            'lang': 'python',
-            'group': 'py-regular'
-        },
-        '<z3pycompat>.*\.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',