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