95 isabelle_usedir_opts, base_image, dir_name) |
95 isabelle_usedir_opts, base_image, dir_name) |
96 |
96 |
97 |
97 |
98 def isabelle_dependency_only(env, case, paths, dep_paths, playground): |
98 def isabelle_dependency_only(env, case, paths, dep_paths, playground): |
99 |
99 |
100 p = paths[0] |
100 isabelle_home = paths[0] |
101 result = path.join(p, 'heaps') |
101 result = path.join(isabelle_home, 'heaps') |
102 os.makedirs(result) |
102 os.makedirs(result) |
103 for dep_path in dep_paths: |
103 for dep_path in dep_paths: |
104 subprocess.check_call(['cp', '-R'] + glob(dep_path + '/*') + [result]) |
104 subprocess.check_call(['cp', '-R'] + glob(dep_path + '/*') + [result]) |
105 |
105 |
106 return (True, 'ok', {}, {}, result) |
106 return (True, 'ok', {}, {}, result) |
107 |
107 |
108 |
108 |
109 def build_isabelle_image(subdir, base, img, env, case, paths, dep_paths, playground, more_settings=''): |
109 def build_isabelle_image(subdir, base, img, env, case, paths, dep_paths, playground, more_settings=''): |
110 |
110 |
111 p = paths[0] |
111 isabelle_home = paths[0] |
112 dep_path = dep_paths[0] |
112 dep_path = dep_paths[0] |
113 prepare_isabelle_repository(p, env.settings.contrib, dep_path, more_settings=more_settings) |
113 prepare_isabelle_repository(p, env.settings.contrib, dep_path, more_settings=more_settings) |
114 os.chdir(path.join(p, 'src', subdir)) |
114 os.chdir(path.join(isabelle_home, 'src', subdir)) |
115 |
115 |
116 (return_code, log) = isabelle_usedir(env, p, '-b', base, img) |
116 (return_code, log) = isabelle_usedir(env, isabelle_home, '-b', base, img) |
117 |
117 |
118 result = path.join(p, 'heaps') |
118 result = path.join(isabelle_home, 'heaps') |
119 return (return_code == 0, extract_isabelle_run_summary(log), |
119 return (return_code == 0, extract_isabelle_run_summary(log), |
120 {'timing': extract_isabelle_run_timing(log)}, {'log': log}, result) |
120 {'timing': extract_isabelle_run_timing(log)}, {'log': log}, result) |
121 |
121 |
122 |
122 |
123 def isabelle_makeall(env, case, paths, dep_paths, playground, more_settings='', target='all'): |
123 def isabelle_makeall(env, case, paths, dep_paths, playground, more_settings='', target='all'): |
124 |
124 |
125 p = paths[0] |
125 isabelle_home = paths[0] |
126 dep_path = dep_paths[0] |
126 dep_path = dep_paths[0] |
127 prepare_isabelle_repository(p, env.settings.contrib, dep_path, more_settings=more_settings) |
127 prepare_isabelle_repository(isabelle_home, env.settings.contrib, dep_path, more_settings=more_settings) |
128 os.chdir(p) |
128 os.chdir(isabelle_home) |
129 |
129 |
130 (return_code, log) = env.run_process('%s/bin/isabelle' % p, 'makeall', '-k', target) |
130 (return_code, log) = env.run_process('%s/bin/isabelle' % isabelle_home, 'makeall', '-k', target) |
131 |
131 |
132 return (return_code == 0, extract_isabelle_run_summary(log), |
132 return (return_code == 0, extract_isabelle_run_summary(log), |
133 {'timing': extract_isabelle_run_timing(log)}, {'log': log}, None) |
133 {'timing': extract_isabelle_run_timing(log)}, {'log': log}, None) |
134 |
134 |
135 |
135 |
137 |
137 |
138 @configuration(repos = [Isabelle], deps = []) |
138 @configuration(repos = [Isabelle], deps = []) |
139 def Pure(env, case, paths, dep_paths, playground): |
139 def Pure(env, case, paths, dep_paths, playground): |
140 """Pure image""" |
140 """Pure image""" |
141 |
141 |
142 p = paths[0] |
142 isabelle_home = paths[0] |
143 prepare_isabelle_repository(p, env.settings.contrib, '') |
143 prepare_isabelle_repository(isabelle_home, env.settings.contrib, '') |
144 os.chdir(path.join(p, 'src', 'Pure')) |
144 os.chdir(path.join(isabelle_home, 'src', 'Pure')) |
145 |
145 |
146 (return_code, log) = env.run_process('%s/bin/isabelle' % p, 'make', 'Pure') |
146 (return_code, log) = env.run_process('%s/bin/isabelle' % isabelle_home, 'make', 'Pure') |
147 |
147 |
148 result = path.join(p, 'heaps') |
148 result = path.join(isabelle_home, 'heaps') |
149 return (return_code == 0, extract_isabelle_run_summary(log), |
149 return (return_code == 0, extract_isabelle_run_summary(log), |
150 {'timing': extract_isabelle_run_timing(log)}, {'log': log}, result) |
150 {'timing': extract_isabelle_run_timing(log)}, {'log': log}, result) |
151 |
151 |
152 @configuration(repos = [Isabelle], deps = [(Pure, [0])]) |
152 @configuration(repos = [Isabelle], deps = [(Pure, [0])]) |
153 def FOL(*args): |
153 def FOL(*args): |