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'''
9Find the set of theory files that the given theories depend on.
10Basically a thin wrapper around 'isabelle build -l'.
11
12The main use for this script is to extract dependent theory files
13for stand-alone releases of the C parser and AutoCorres.
14'''
15
16import argparse
17import os
18import re
19import subprocess
20
21def run_isabelle_tool(isabelle_dir, cmdline, ignore_exit_code=False):
22    '''Run Isabelle with given command (e.g. ['build', '-l', 'HOL']).
23       The first argument should be the Isabelle directory.
24       If the command succeeded, return its standard output.'''
25    isabelle_exe = os.path.join(isabelle_dir, 'bin', 'isabelle')
26    try:
27        return subprocess.check_output([isabelle_exe] + cmdline)
28    except subprocess.CalledProcessError as e:
29        if ignore_exit_code:
30            return e.output
31        else:
32            raise
33
34def session_theory_deps(isabelle_dir, ROOT_dirs, sessions):
35    '''For the given sessions, retrieve the dependent sessions
36       and theory files (including the given sessions).
37       Returns a dict keyed by session name, containing lists of
38       theory file paths.'''
39
40    cmdline = ['build', '-l', '-n']
41    for d in ROOT_dirs:
42        cmdline += ['-d', d]
43    cmdline += sessions
44
45    deps = {}
46    this_session = None
47    session_name_re = r'[a-zA-Z0-9-_]+'
48    # `isabelle build` returns 1 if the session hasn't been built,
49    # even for a dry-run, so ignore the exit code
50    for l in run_isabelle_tool(
51            isabelle_dir, cmdline, ignore_exit_code=True).splitlines():
52        l = l.decode('utf-8')
53        # 'Session HOL/HOL-Word (main timing)'
54        m = re.match(r'Session (' + session_name_re + ')/(' + session_name_re + ')(?: \(.*\))?', l)
55        if m:
56            # start processing next session
57            _, session = m.groups()
58            this_session = session
59            assert session not in deps
60            deps[session] = []
61            continue
62
63        # '  /path/to/proof.thy'
64        if l.startswith('  '):
65            # another file in session
66            deps[this_session].append(l[2:])
67            continue
68
69        # There are some other junk lines, like '... elapsed time',
70        # which we ignore
71
72    return deps
73
74def theory_deps_in_dirs(isabelle_dir, ROOT_dirs, sessions, base_dirs):
75    '''Get dependent sessions and theories like session_theory_deps,
76       but only report theory files and sessions that involve one of
77       the given directories.'''
78    full_deps = session_theory_deps(isabelle_dir, ROOT_dirs, sessions)
79
80    if not base_dirs:
81        # no filtering
82        return full_deps
83
84    deps = {}
85    # remove unwanted theories
86    for session in full_deps:
87        session_trimmed_deps = []
88        for f in full_deps[session]:
89            keep = False
90            for base in base_dirs:
91                relpath = os.path.relpath(f, base)
92                if not relpath.startswith('../'):
93                    keep = True
94                    break
95            if keep:
96                session_trimmed_deps.append(f)
97        # if session has no wanted theories, also drop it
98        if session_trimmed_deps:
99            deps[session] = session_trimmed_deps
100    return deps
101
102def main():
103    parser = argparse.ArgumentParser(
104        description='Extract theory file dependencies of Isabelle sessions')
105    parser.add_argument('-d', metavar='DIR', action='append', default=[],
106        help='Directories containing ROOT or ROOTS files (default: .)')
107    parser.add_argument('-b', metavar='DIR', action='append', default=[],
108        help='Show theory files from these directories (default: all)')
109    parser.add_argument('-I', metavar='DIR', required=True,
110        help='Path to Isabelle system')
111    parser.add_argument('-r', action='store_true',
112        help='Print relative paths to -b directory (only one dir allowed)')
113    parser.add_argument('sessions', metavar='SESSIONS', nargs='+',
114        help='Isabelle session names')
115
116    opts = parser.parse_args()
117    if not opts.d:
118        opts.d = ['.']
119
120    # use absolute paths and resolve symlinks, to match `isabelle build -l`
121    opts.b = [os.path.realpath(d) for d in opts.b]
122    if opts.r and len(opts.b) != 1:
123        parser.error('must have exactly one directory for -b to use -r')
124
125    if not os.path.isdir(opts.I):
126        parser.error('expected a directory for -I option')
127    expected_isabelle = os.path.join(opts.I, 'bin', 'isabelle')
128    if not os.path.exists(expected_isabelle):
129        parser.error('Isabelle executable not found: %r' % expected_isabelle)
130
131    deps = theory_deps_in_dirs(opts.I, opts.d, opts.sessions, opts.b)
132    for session in deps:
133        for theory in deps[session]:
134            if opts.r:
135                theory = os.path.relpath(theory, opts.b[0])
136            print(theory)
137
138if __name__ == '__main__':
139    main()
140