1#!/usr/bin/env python 2# 3# 4# Copyright 2014, NICTA 5# 6# This software may be distributed and modified according to the terms of 7# the BSD 2-Clause license. Note that NO WARRANTY is provided. 8# See "LICENSE_BSD2.txt" for details. 9# 10# @TAG(NICTA_BSD) 11# 12# 13# Generate an Isabelle "ROOT" build file containing all examples 14# in the given directories. 15# 16 17import os 18import optparse 19import glob 20 21# Parse arguments 22parser = optparse.OptionParser() 23parser.add_option("-o", "--output", dest="output", 24 help="output file", metavar="FILE") 25parser.add_option("-i", "--input-dir", dest="input_dir", 26 help="input directory", action="append", default=[], 27 metavar="DIR") 28parser.add_option("-s", "--session-name", dest="session_name", 29 help="isabelle session name", metavar="NAME") 30parser.add_option("-b", "--base-session", dest="base_session", 31 help="isabelle base session", metavar="NAME") 32parser.add_option("-d", "--named-session-dependency", dest="session_dependencies", 33 help="additional named session dependency", action="append", default=[], 34 metavar="NAME") 35parser.add_option("-q", "--quick-and-dirty", dest="quick_and_dirty", 36 help="ROOT file should compile with \"quick and dirty\" enabled.", 37 action="store_true", default=False) 38parser.add_option("-T", "--generate-theory", dest="theory_file", 39 action="store_true", default=False, 40 help="Generate a theory file instead of a ROOT file.") 41(options, args) = parser.parse_args() 42 43# Check arguments 44if len(args) != 0: 45 parser.error("Additional arguments passed in.") 46if options.output == None: 47 parser.error("Require an output filename.") 48if len(options.input_dir) == 0: 49 parser.error("Require at least one input directory.") 50if options.session_name == None and not options.theory_file: 51 parser.error("Require a session name.") 52if options.base_session == None and not options.theory_file: 53 parser.error("Require a base session.") 54output_dir = os.path.dirname(options.output) 55 56# Generate ROOT file. 57with open(options.output, "w") as output: 58 # Fetch list of files to test. 59 theories = [] 60 for d in options.input_dir: 61 theories += sorted(glob.glob(os.path.join(d, "*.thy"))) 62 63 if options.theory_file: 64 session_name = os.path.splitext(os.path.basename(options.output))[0] 65 def import_name(file): 66 return os.path.splitext(os.path.relpath(file, os.path.dirname(options.output)))[0] 67 68 # Write a theory file. 69 output.write("theory %s imports\n" % session_name) 70 for i in theories: 71 # Theories have the ".thy" stripped off. 72 output.write(" \"%s\"\n" % import_name(i)) 73 output.write("begin\n") 74 output.write("\n") 75 output.write("end\n") 76 else: 77 # Write our ROOT file. 78 output.write("session \"%s\" = \"%s\" +\n" % (options.session_name, options.base_session)) 79 if options.session_dependencies: 80 output.write(" sessions\n") 81 for i in options.session_dependencies: 82 output.write(" \"%s\"\n" % i) 83 if options.quick_and_dirty: 84 output.write(" theories [quick_and_dirty]\n") 85 else: 86 output.write(" theories\n") 87 for i in theories: 88 # Theories have the ".thy" stripped off. 89 thy = os.path.relpath(i, output_dir) 90 thy = os.path.splitext(thy)[0] 91 output.write(" \"%s\"\n" % thy) 92