1#!/usr/bin/env python3 2# 3# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 4# 5# SPDX-License-Identifier: BSD-2-Clause 6# 7 8# 9# Generate an Isabelle "ROOT" build file containing all examples 10# in the given directories. 11# 12 13import os 14import optparse 15import glob 16 17# Parse arguments 18parser = optparse.OptionParser() 19parser.add_option("-o", "--output", dest="output", 20 help="output file", metavar="FILE") 21parser.add_option("-i", "--input-dir", dest="input_dir", 22 help="input directory", action="append", default=[], 23 metavar="DIR") 24parser.add_option("-s", "--session-name", dest="session_name", 25 help="isabelle session name", metavar="NAME") 26parser.add_option("-b", "--base-session", dest="base_session", 27 help="isabelle base session", metavar="NAME") 28parser.add_option("-d", "--named-session-dependency", dest="session_dependencies", 29 help="additional named session dependency", action="append", default=[], 30 metavar="NAME") 31parser.add_option("-q", "--quick-and-dirty", dest="quick_and_dirty", 32 help="ROOT file should compile with \"quick and dirty\" enabled.", 33 action="store_true", default=False) 34parser.add_option("-T", "--generate-theory", dest="theory_file", 35 action="store_true", default=False, 36 help="Generate a theory file instead of a ROOT file.") 37parser.add_option("--dir", dest="dirs", 38 help="additional session directory", action="append", 39 default=[], metavar="NAME") 40(options, args) = parser.parse_args() 41 42# Check arguments 43if len(args) != 0: 44 parser.error("Additional arguments passed in.") 45if options.output == None: 46 parser.error("Require an output filename.") 47if len(options.input_dir) == 0: 48 parser.error("Require at least one input directory.") 49if options.session_name == None and not options.theory_file: 50 parser.error("Require a session name.") 51if options.base_session == None and not options.theory_file: 52 parser.error("Require a base session.") 53output_dir = os.path.dirname(options.output) 54 55# Generate ROOT file. 56with open(options.output, "w") as output: 57 # Fetch list of files to test. 58 theories = [] 59 for d in options.input_dir: 60 theories += sorted(glob.glob(os.path.join(d, "*.thy"))) 61 62 if options.theory_file: 63 session_name = os.path.splitext(os.path.basename(options.output))[0] 64 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.dirs: 84 output.write(" directories\n") 85 for i in options.dirs: 86 output.write(" \"%s\"\n" % i) 87 if options.quick_and_dirty: 88 output.write(" theories [quick_and_dirty]\n") 89 else: 90 output.write(" theories\n") 91 for i in theories: 92 # Theories have the ".thy" stripped off. 93 thy = os.path.relpath(i, output_dir) 94 thy = os.path.splitext(thy)[0] 95 output.write(" \"%s\"\n" % thy) 96