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