191 |
191 |
192 |
192 |
193 |
193 |
194 /** skeleton for component **/ |
194 /** skeleton for component **/ |
195 |
195 |
196 def build_polyml_component(component: Path, sha1_root: Option[Path] = None) |
196 private def extract_sources(source_archive: Path, component_dir: Path) = |
197 { |
197 { |
198 if (component.is_dir) error("Directory already exists: " + component) |
198 if (source_archive.get_ext == "zip") { |
199 |
199 Isabelle_System.bash( |
200 val etc = component + Path.explode("etc") |
200 "unzip -x " + File.bash_path(source_archive.absolute), cwd = component_dir.file).check |
201 Isabelle_System.mkdirs(etc) |
201 } |
202 File.copy(Path.explode("~~/Admin/polyml/settings"), etc) |
202 else { |
203 File.copy(Path.explode("~~/Admin/polyml/README"), component) |
203 Isabelle_System.gnutar("-xzf " + File.bash_path(source_archive), dir = component_dir).check |
|
204 } |
|
205 |
|
206 val src_dir = component_dir + Path.explode("src") |
|
207 File.read_dir(component_dir) match { |
|
208 case List(s) => File.move(component_dir + Path.basic(s), src_dir) |
|
209 case _ => error("Source archive contains multiple directories") |
|
210 } |
|
211 |
|
212 val lines = split_lines(File.read(src_dir + Path.explode("RootX86.ML"))) |
|
213 val ml_files = |
|
214 for { |
|
215 line <- lines |
|
216 rest <- Library.try_unprefix("use", line) |
|
217 } yield "ML_file" + rest |
|
218 |
|
219 File.write(src_dir + Path.explode("ROOT.ML"), |
|
220 """(* Poly/ML Compiler root file. |
|
221 |
|
222 When this file is open in the Prover IDE, the ML files of the Poly/ML |
|
223 compiler can be explored interactively. This is a separate copy: it does |
|
224 not affect the running ML session. *) |
|
225 """ + ml_files.mkString("\n", "\n", "\n")) |
|
226 } |
|
227 |
|
228 def build_polyml_component( |
|
229 source_archive: Path, |
|
230 component_dir: Path, |
|
231 sha1_root: Option[Path] = None) |
|
232 { |
|
233 if (component_dir.is_file || component_dir.is_dir) |
|
234 error("Component directory already exists: " + component_dir) |
|
235 |
|
236 Isabelle_System.mkdirs(component_dir) |
|
237 extract_sources(source_archive, component_dir) |
|
238 |
|
239 File.copy(Path.explode("~~/Admin/polyml/README"), component_dir) |
|
240 |
|
241 val etc_dir = component_dir + Path.explode("etc") |
|
242 Isabelle_System.mkdirs(etc_dir) |
|
243 File.copy(Path.explode("~~/Admin/polyml/settings"), etc_dir) |
204 |
244 |
205 sha1_root match { |
245 sha1_root match { |
206 case Some(dir) => |
246 case Some(dir) => |
207 Mercurial.repository(dir).archive(File.standard_path(component + Path.explode("sha1"))) |
247 Mercurial.repository(dir).archive(File.standard_path(component_dir + Path.explode("sha1"))) |
208 case None => |
248 case None => |
209 } |
249 } |
210 } |
250 } |
211 |
251 |
212 |
252 |
257 { |
297 { |
258 Command_Line.tool0 { |
298 Command_Line.tool0 { |
259 var sha1_root: Option[Path] = None |
299 var sha1_root: Option[Path] = None |
260 |
300 |
261 val getopts = Getopts(""" |
301 val getopts = Getopts(""" |
262 Usage: isabelle build_polyml_component [OPTIONS] TARGET |
302 Usage: isabelle build_polyml_component [OPTIONS] SOURCE_ARCHIVE COMPONENT_DIR |
263 |
303 |
264 Options are: |
304 Options are: |
265 -s DIR sha1 sources, see https://isabelle.sketis.net/repos/sha1 |
305 -s DIR sha1 sources, see https://isabelle.sketis.net/repos/sha1 |
266 |
306 |
267 Make skeleton for Poly/ML component in directory TARGET. |
307 Make skeleton for Poly/ML component, based on official source archive |
|
308 (zip or tar.gz). |
268 """, |
309 """, |
269 "s:" -> (arg => sha1_root = Some(Path.explode(arg)))) |
310 "s:" -> (arg => sha1_root = Some(Path.explode(arg)))) |
270 |
311 |
271 val more_args = getopts(args) |
312 val more_args = getopts(args) |
272 val component = |
313 |
|
314 val (source_archive, component_dir) = |
273 more_args match { |
315 more_args match { |
274 case List(arg) => Path.explode(arg) |
316 case List(archive, dir) => (Path.explode(archive), Path.explode(dir)) |
275 case _ => getopts.usage() |
317 case _ => getopts.usage() |
276 } |
318 } |
277 build_polyml_component(component, sha1_root = sha1_root) |
319 build_polyml_component(source_archive, component_dir, sha1_root = sha1_root) |
278 } |
320 } |
279 }) |
321 }) |
280 } |
322 } |