Publish documentation

doc/doxygen-root/doxygen-markdown/append-last-modified-dates.py

@@ -0,0 +1,42 @@
+#!/usr/bin/env python3
+
+import git
+import logging
+import subprocess
+import sys
+from pathlib import Path
+
+def append_last_modified_date(repo, path):
+    """Append last modified date to a file"""
+
+    # Use the author date %ai as last modified date and not the commit date %ci
+    # The author date is what 'git log' prints from the command line
+    date = repo.git.log("-1", "--format=%ai", path)
+
+    with open(path, "a") as handle:
+        # append two newlines to guarantee a paragraph break in the
+        # new markdown file in the event the file does not already end
+        # with a newline
+        print(f"\n\nLast modified: {date}", file=handle)
+
+def append_last_modified_dates(paths):
+    paths = [Path(path).resolve() for path in paths]
+    if not paths:
+        logging.info("Failed to append last modified dates: list of files is empty")
+        sys.exit(1)
+
+    repo = git.Repo(paths[0], search_parent_directories=True)
+    if repo.is_dirty():
+        logging.info("Failed to append last modified dates: repository has uncommitted changes")
+        sys.exit(1)
+
+    for path in paths:
+        append_last_modified_date(repo, path)
+
+def main():
+    fmt = '%(levelname)s: %(message)s'
+    logging.basicConfig(level=logging.INFO, format=fmt)
+    append_last_modified_dates(sys.argv[1:])
+
+if __name__ == "__main__":
+    main()

doc/doxygen-root/doxygen-markdown/doxygen-markdown-preprocessor.py

@@ -0,0 +1,108 @@
+#!/usr/bin/env python3
+import argparse
+import logging
+import subprocess
+import os
+import re
+
+def create_parser(options=None, description=None):
+    """Create a parser for command line arguments."""
+
+    options = options or []
+    description = description or ""
+
+    flags = [option.get('flag') for option in options]
+    if '--verbose' not in flags:
+        options.append({'flag': '--verbose', 'action': 'store_true', 'help': 'Verbose output'})
+    if '--debug' not in flags:
+        options.append({'flag': '--debug', 'action': 'store_true', 'help': 'Debug output'})
+
+    parser = argparse.ArgumentParser(description=description)
+    for option in options:
+        flag = option.pop('flag')
+        parser.add_argument(flag, **option)
+    return parser
+
+def configure_logging(args):
+    """Configure logging level based on command line arguments."""
+
+    # Logging is configured by first invocation of basicConfig
+    fmt = '%(levelname)s: %(message)s'
+    if args.debug:
+        logging.basicConfig(level=logging.DEBUG, format=fmt)
+        return
+    if args.verbose:
+        logging.basicConfig(level=logging.INFO, format=fmt)
+        return
+    logging.basicConfig(format=fmt)
+
+def parse_arguments():
+
+    options = [
+        {'flag': '--pandoc-write',
+         'default': 'markdown_phpextra',
+         'help': 'pandoc --write option'},
+        {'flag': '--pandoc-wrap',
+         'default': 'none',
+         'help': 'pandoc --auto option'},
+        {'flag': 'file',
+         'nargs': '*',
+         'help': 'markdown files'},
+    ]
+    return create_parser(options, "Prepare markdown for doxygen").parse_args()
+
+
+def pandoc(path, pandoc_write, pandoc_wrap, pandoc_filter=None):
+    args = {
+        '--write': pandoc_write,
+        '--wrap', pandoc_wrap
+    }
+    if pandoc_filter:
+        args['--filter'] = Path(pandoc_filter).resolve()
+
+
+    lines = subprocess.run(['pandoc', **args, path],
+                           check=True,
+                           text=True,
+                           capture_output=True).stdout.splitlines()
+    return [patch_code_block(line) for line in lines]
+
+################################################################
+
+def test_patch_code_block():
+    assert patch_code_block("``` c") == "```c"
+    assert patch_code_block("``` sh") == "```sh"
+    assert patch_code_block("~~~ c") == "~~~c"
+    assert patch_code_block("~~~ sh") == "~~~sh"
+    assert patch_code_block("```c") == "```c"
+    assert patch_code_block("```   ") == "```  "
+
+def test_patch_link_target():
+    assert patch_link_target("../../helpful/cow/") == "helpful-cow.md"
+    assert patch_link_target("helpful/cow") == "helpful-cow.md"
+    assert patch_link_target("helpful/cow/") == "helpful-cow.md"
+    assert patch_link_target("helpful-cow/") == "helpful-cow.md"
+
+def test_patch_link():
+    assert patch_link("[a](../../helpful/cow/)") == "[a](helpful-cow.md)"
+    assert patch_link("[a](helpful/cow)") == "[a](helpful-cow.md)"
+    assert patch_link("[a](helpful/cow/)") == "[a](helpful-cow.md)"
+    assert patch_link("[a](helpful-cow/)") == "[a](helpful-cow.md)"
+
+def test_patch_links():
+    assert patch_links("a b [a](../../helpful/cow/) x [a](../../helpful/cow/)") == "a b [a](helpful-cow.md) x [a](helpful-cow.md)"
+
+################################################################
+
+def main():
+    args = parse_arguments()
+    configure_logging(args)
+
+    for path in args.file:
+        lines = pandoc(path, args.pandoc_write, args.pandoc_wrap)
+        lines = [patch_links(line) for line in lines]
+        for line in lines:
+            print(line)
+
+if __name__ == "__main__":
+    main()

doc/doxygen-root/doxygen-markdown/markdown.sh

@@ -0,0 +1,57 @@
+#!/bin/bash
+
+set -euo pipefail
+
+BINDIR=$(dirname $(realpath ${BASH_SOURCE[0]}))
+FILES=$(find . -name '*.md')
+
+# Append the last modified date to the end of every markdown file
+
+echo
+echo "Appending last modified dates to markdown files"
+$BINDIR/append-last-modified-dates.py $FILES
+
+# Doxygen parses incorrectly a link [what a link](what-a-link.md) that
+# is broken over two lines.
+# Doxygen requires that headings '# heading' have labels '{# heading}'
+# for section linking to work.  The markdown extension "php Markdown
+# Extra" supports section labels.
+# Use pandoc to remove line breaks from paragraphs and to output a
+# markdown extension with section labels.
+# Note: Need to read markdown as markdown_phpextra and not default
+# markdown to preserve doxygen pragmas like \ingroup.
+
+# Bug: This is currently interacting badly with \dot in cprover markdown
+
+# echo
+# echo "Running pandoc over markdown files"
+# for file in $FILES; do
+#     echo $file
+#     tmp=/tmp/${file%.*}1.md
+#     mkdir -p $(dirname $tmp)
+#     cp $file $tmp
+#     pandoc --read=markdown_phpextra --write=markdown_phpextra --wrap=none $tmp | \
+#         $BINDIR/pandoc-codeblock-repair.sh > $file
+# done
+
+cprovers=$(find . -name cprover-manual)
+cprover=${cprovers[0]}
+
+# Markdown files in cprover-manual have hierarchical links like
+# ../../pretty/cow/ that refer to the markdown file pretty-cow.md.
+# The site http://www.cprover.org/cprover-manual/ uses a javascript
+# script running in the browser to serve up pages from the
+# cprover-manual directory.  Use a pandoc filter to patch up the
+# cprover-manual links before running doxygen.
+
+echo
+echo "Running pandoc filter over cprover-manual markdown files"
+FILES=$(find $cprover -name '*.md')
+for file in $FILES; do
+    echo $file
+    tmp=/tmp/${file%.*}2.md
+    mkdir -p $(dirname $tmp)
+    cp $file $tmp
+    pandoc  --write=markdown_phpextra --wrap=none --filter=$BINDIR/pandoc-cprover-link-filter.py $tmp |
+        $BINDIR/pandoc-codeblock-repair.sh > $file
+done

doc/doxygen-root/doxygen-markdown/pandoc-codeblock-repair.sh

@@ -0,0 +1,10 @@
+#!/bin/sh
+
+# This script strips spaces from syntax highlighting for code blocks
+# in markdown documents.
+
+# Pandoc outputs ``` c and ~~~ c but and doxygen expects ```c and ~~~c.
+# Pandoc ouputs leading spaces before ``` and ~~~ when the code block is
+# part of a list item.
+
+sed 's/^\( *```\) */\1/' | sed 's/^\( *~~~\) */\1/'

doc/doxygen-root/doxygen-markdown/pandoc-cprover-link-filter.py

@@ -0,0 +1,50 @@
+#!/usr/bin/env python3
+
+# https://pandoc.org/MANUAL.html
+# https://pandoc.org/filters.html
+# AST: https://hackage.haskell.org/package/pandoc-types-1.22.2.1/docs/Text-Pandoc-Definition.html
+
+from pandocfilters import toJSONFilter, Link
+
+def patch_url(url):
+
+    # cbmc-tutorial.md links directly to source files used in examples; link to local copies instead
+    raw_url = 'https://raw.githubusercontent.com/diffblue/cbmc/develop/doc/cprover-manual/'
+    if url.startswith(raw_url):
+        return url[len(raw_url):]
+
+    if url.startswith('http://') or url.startswith('https://'):
+        return url
+
+    try:
+        path, label = url.rsplit('#', 1)
+    except ValueError:
+        path, label = url, ''
+
+    # Flatten hierarchical urls in cprover-manual to a flat set of markdown files
+    # Map a url like ../../helpful/cow/ to helpful-cow.md
+    # Map a url like . or .. to . (not index.md since index.md is doxygen mainpage)
+
+    parts = [part for part in path.split('/') if part and part != '.' and part != '..']
+    new_path = '-'.join(parts) + '.md' if parts else ''
+
+    new_url = f'{new_path}#{label}' if label else new_path
+    if new_url:
+        return new_url
+    return '.'
+
+def test_patch_url():
+    assert patch_url("../../helpful/cow/") == "helpful-cow.md"
+    assert patch_url("helpful/cow") == "helpful-cow.md"
+    assert patch_url("helpful/cow/") == "helpful-cow.md"
+    assert patch_url("helpful-cow/") == "helpful-cow.md"
+
+def patch_link(key, value, _format, _meta):
+    if key == 'Link':
+        attr, alt_text, link = value
+        url, title = link
+        return Link(attr, alt_text, [patch_url(url), title])
+    return None
+
+if __name__ == "__main__":
+    toJSONFilter(patch_link)