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