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