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