1#!/usr/bin/env python
2#
3# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
4#
5# SPDX-License-Identifier: BSD-2-Clause
6#
7
8from __future__ import print_function
9import pexpect
10import optparse
11import re
12import sys
13
14
15def main():
16    # Parse arguments.
17    parser = optparse.OptionParser(usage="usage: %prog [options] <thy file>")
18    parser.add_option("-v", "--verbose", dest="verbose",
19                      help="Show Isabelle output", action="store_true", default=False)
20    (options, args) = parser.parse_args()
21    if len(args) != 1:
22        parser.error("Expected a single argument containing the Isabelle theory file to run.")
23
24    # Get the filename, and strip off the trailing ".thy".
25    filename = args[0]
26    if filename.endswith(".thy"):
27        filename = filename[:-4]
28
29    # Run Isabelle.
30    process = pexpect.spawn('isabelle-process',
31                            ['-r', '-q', '-f', '-e', 'use_thy \"%s\";' % filename, "Benchmark"], timeout=None)
32    if not options.verbose:
33        process.logfile = None
34    else:
35        process.logfile = sys.stdout
36
37    # Print header.
38    header = "%s Benchmark Results" % filename
39    print()
40    print(header)
41    print("=" * len(header))
42
43    # Wait for things to happen.
44    errors_detected = False
45    while True:
46        result = process.expect([
47            re.compile('^result:: (.*)$', re.MULTILINE),
48            re.compile('^category:: (.*)$', re.MULTILINE),
49            re.compile('^\*\*\* (.*)$', re.MULTILINE),
50            pexpect.EOF
51        ])
52        if result == 0:
53            # Benchmark result.
54            print("    " + process.match.group(1).strip("\r\n"))
55        elif result == 1:
56            # Category
57            print()
58            category = process.match.group(1).strip("\r\n")
59            print(category)
60            print("-" * len(category))
61            print()
62        elif result == 2:
63            # Error
64            if not errors_detected:
65                print("*** ERROR DETECTED")
66            errors_detected = True
67        else:
68            # EOF
69            print
70            break
71
72    # Exit
73    if errors_detected:
74        print("Errors during benchmark process.")
75        sys.exit(1)
76    sys.exit(0)
77
78
79if __name__ == "__main__":
80    main()
81