1(*--------------------------------------------------------------------------- 2 A special purpose version of make that "does the right thing" in 3 single directories for building HOL theories, and accompanying 4 SML libraries. 5 ---------------------------------------------------------------------------*) 6 7structure Holmake = 8struct 9 10open Systeml Holmake_tools Holmake_types 11infix forces_update_of |> 12 13fun x |> f = f x 14 15structure FileSys = OS.FileSys 16structure Path = OS.Path 17structure Process = OS.Process 18 19(* turn a variable name into a list *) 20fun envlist env id = let 21 open Holmake_types 22in 23 map dequote (tokenize (perform_substitution env [VREF id])) 24end 25 26fun main() = let 27 28val execname = Path.file (CommandLine.name()) 29fun warn s = (TextIO.output(TextIO.stdErr, execname^": "^s^"\n"); 30 TextIO.flushOut TextIO.stdErr) 31fun die s = (warn s; Process.exit Process.failure) 32val original_dir = hmdir.curdir() 33 34(* Global parameters, which get set at configuration time *) 35val HOLDIR0 = Systeml.HOLDIR; 36val DEPDIR = ".HOLMK"; 37val LOGDIR = ".hollogs"; 38 39(**** get_dependencies *) 40(* figures out whether or not a dependency file is a suitable place to read 41 information about current target or not, and then either does so, or makes 42 the dependency file and then reads from it. 43 44 f1 forces_update_of f2 45 iff 46 f1 exists /\ (f2 exists ==> f1 is newer than f2) 47*) 48 49(**** get dependencies from file *) 50 51 52 53(** Command line parsing *) 54 55(*** parse command line *) 56fun apply_updates fs v = List.foldl (fn (f,v) => #update f (warn,v)) v fs 57 58fun getcline args = let 59 open GetOpt 60in 61 getOpt {argOrder = Permute, 62 options = HM_Cline.option_descriptions, 63 errFn = die} 64 args 65end 66 67val (master_cline_options, targets) = getcline (CommandLine.arguments()) 68 69val (cline_hmakefile, cline_nohmf) = 70 List.foldl (fn (f,(hmf,nohmf)) => 71 ((case #hmakefile f of NONE => hmf | SOME s => SOME s), 72 nohmf orelse #no_hmf f)) 73 (NONE,false) 74 master_cline_options 75 76fun get_hmf_cline_updates () = 77 let 78 val hmakefile = 79 case cline_hmakefile of 80 NONE => "Holmakefile" 81 | SOME s => 82 if exists_readable s then s 83 else die ("Can't read holmakefile: "^s) 84 val hmenv0 = 85 if exists_readable hmakefile andalso not cline_nohmf then 86 #1 (ReadHMF.read hmakefile (base_environment())) 87 else 88 base_environment() 89 val hmf_cline = envlist hmenv0 "CLINE_OPTIONS" 90 val (hmf_options, hmf_rest) = getcline hmf_cline 91 val _ = if null hmf_rest then () 92 else 93 warn ("Unused c/line options in makefile: "^ 94 String.concatWith " " hmf_rest) 95 in 96 hmf_options 97 end 98 99fun chattiness_level switches = 100 case (#debug switches, #verbose switches, #quiet switches) of 101 (true, _, _) => 3 102 | (_, true, _) => 2 103 | (_, _, true) => 0 104 | _ => 1 105 106val option_value = 107 HM_Cline.default_options |> apply_updates (get_hmf_cline_updates()) 108 |> apply_updates master_cline_options 109val coption_value = #core option_value 110val usepfx = 111 #jobs (#core 112 (HM_Cline.default_options |> apply_updates master_cline_options)) = 113 1 114 115(* things that need to be read out of the first Holmakefile, and which will 116 govern the behaviour even when recursing into other directories that may 117 have their own Holmakefiles *) 118val (outputfns as {warn,tgtfatal,diag,info,chatty}) = 119 output_functions {chattiness = chattiness_level coption_value, 120 usepfx = usepfx} 121val do_logging_flag = #do_logging coption_value 122val no_lastmakercheck = #no_lastmaker_check coption_value 123val show_usage = #help coption_value 124val toplevel_no_prereqs = #no_prereqs coption_value 125val cline_additional_includes = #includes coption_value 126 127(* make the cline includes = [] so that these are only looked at once 128 (when the cline_additional_includes value is folded into dirinfo values 129 and eventually used in hm_recur). 130*) 131val pass_option_value = 132 HM_Cline.fupd_core (HM_Core_Cline.fupd_includes (fn _ => [])) option_value 133 134val _ = do_lastmade_checks outputfns {no_lastmakercheck = no_lastmakercheck} 135 136val _ = diag (fn _ => "CommandLine.name() = "^CommandLine.name()) 137val _ = diag (fn _ => "CommandLine.arguments() = "^ 138 String.concatWith ", " (CommandLine.arguments())) 139 140(* set up logging *) 141val logfilename = Systeml.make_log_file 142val hostname = if Systeml.isUnix then 143 case Mosml.run "hostname" [] "" of 144 Mosml.Success s => String.substring(s,0,size s - 1) ^ "-" 145 (* substring to drop \n in output *) 146 | _ => "" 147 else "" (* what to do under windows? *) 148 149fun finish_logging buildok = let 150in 151 if do_logging_flag andalso FileSys.access(logfilename, []) then let 152 open Date 153 val timestamp = fmt "%Y-%m-%dT%H%M" (fromTimeLocal (Time.now())) 154 val newname0 = hostname^timestamp 155 val newname = (if buildok then "" else "bad-") ^ newname0 156 in 157 FileSys.rename {old = logfilename, new = newname}; 158 buildok 159 end 160 else buildok 161end handle IO.Io _ => (warn "Had problems making permanent record of make log"; 162 buildok) 163 164val _ = Process.atExit (fn () => ignore (finish_logging false)) 165 166(* ---------------------------------------------------------------------- 167 168 maybe_recurse 169 170 this function doesn't handle all recursion, just one level's 171 worth. In other words, the master Holmake calls this function, and 172 this then arranges the recursive calls into the various include 173 directories that need to happen. The holmake that gets called in 174 those directories (via the hm parameter) will in turn call this 175 function for recursion at that level in the "tree". 176 177 The local_build/k parameter is how the maybe_recurse function 178 finishes off; this parameter is called when all of the necessary 179 recursion has been performed and work should be done in the 180 current ("local") directory. 181 182 Finally, what of the dirinfo? 183 184 This record includes 185 origin: the absolute path to the very first directory 186 includes: the includes that the local directory knows about 187 (which will have come from the command-line or 188 INCLUDES lines in the local Holmakefile 189 preincludes: similarly 190 visited: a set of visited directories (with directories 191 expressed as absolute paths) 192 193 The includes and preincludes are clearly useful when it comes time to 194 do any local work, but also specify how the recursion is to happen. 195 196 Now, the recursion into those directories may result in extra 197 includes and preincludes. 198 ---------------------------------------------------------------------- *) 199fun idm_lookup idm key = 200 case Binarymap.peek(idm, key) of 201 NONE => {pres = empty_dirset, incs = empty_dirset} 202 | SOME r => r 203 204fun extend_idmap k (v as {incs = i,pres = p}) idm0 = 205 case Binarymap.peek(idm0, k) of 206 NONE => Binarymap.insert(idm0, k, v) 207 | SOME {incs = i0, pres = p0} => 208 Binarymap.insert(idm0, k, 209 {incs = Binaryset.union(i0,i), 210 pres = Binaryset.union(p0,p)}) 211 212fun print_set ds = 213 "{" ^ 214 String.concatWith 215 ", " 216 (Binaryset.foldr (fn (d,acc) => hmdir.toString d :: acc) [] ds) ^ 217 "}" 218 219fun maybe_recurse {warn,diag,hm,dirinfo,dir,local_build=k,cleantgt} allincs = 220let 221 val {incdirmap,visited} = dirinfo 222 val _ = diag (fn _ => "maybe_recurse: includes (pre- & normal) = [" ^ 223 String.concatWith ", " allincs ^ "]") 224 val _ = diag (fn _ => 225 "maybe_recurse: incdmap on dir \"" ^ hmdir.toString dir ^ 226 " = " ^ print_set (#incs (idm_lookup incdirmap dir))) 227 val k = fn ii => (terminal_log ("Holmake: "^nice_dir (hmdir.toString dir)); 228 k ii) 229 val tgts = case cleantgt of SOME s => [s] | NONE => [] 230 fun recurse (acc as {visited,incdirmap}) newdir = let 231 in 232 if Binaryset.member(visited, newdir) then 233 (* even if you don't want to rebuild newdir, you still want to learn 234 about what it depends on so that the dependency map for this directory 235 is appropriately augmented *) 236 SOME {visited = visited, 237 incdirmap = 238 extend_idmap dir (idm_lookup incdirmap newdir) incdirmap} 239 else let 240 val _ = diag (fn _ => "Recursive call in " ^ hmdir.pretty_dir newdir) 241 val _ = diag (fn _ => "Visited set = " ^ print_set visited) 242 val _ = terminal_log ("Holmake: "^nice_dir (hmdir.toString newdir)) 243 val result = 244 case hm newdir acc tgts of 245 NONE => NONE 246 | SOME {visited,incdirmap = idm0} => 247 SOME {visited = visited, 248 incdirmap = extend_idmap dir (idm_lookup idm0 newdir) idm0} 249 in 250 diag (fn _ => "Finished work in "^hmdir.pretty_dir newdir); 251 terminal_log ("Holmake: "^nice_dir (hmdir.toString dir)); 252 FileSys.chDir (hmdir.toAbsPath dir); 253 case result of 254 SOME{visited,incdirmap} => 255 let 256 val {incs,pres} = idm_lookup incdirmap dir 257 in 258 diag (fn () => 259 "Recursively computed includes for " ^ hmdir.toString dir ^ 260 " = " ^ print_set incs); 261 diag (fn () => 262 "Recursively computed pre-includes for " ^ 263 hmdir.toString dir ^ 264 " = " ^ print_set pres) 265 end 266 | NONE => (); 267 result 268 end 269 end 270 fun do_em (accg as {incdirmap,...}) dirs = 271 case dirs of 272 [] => 273 let 274 val {pres, incs} = idm_lookup incdirmap dir 275 val f = Binaryset.foldr (fn (d,acc) => hmdir.toAbsPath d :: acc) [] 276 in 277 if k {includes=f incs,preincludes=f pres} then SOME accg 278 else NONE 279 end 280 | x::xs => 281 let 282 in 283 case recurse accg x of 284 SOME result => do_em result xs 285 | NONE => NONE 286 end 287 val visited = Binaryset.add(visited, dir) 288 fun canon i = hmdir.extendp {base = dir, extension = i} 289 val canonl = map canon 290 fun f idirs = map canon idirs 291in 292 do_em {visited = visited, incdirmap = incdirmap} (hmdir.sort (f allincs)) 293end 294 295(* directory specific stuff here *) 296type res = holmake_result 297fun Holmake nobuild dir dirinfo cline_additional_includes targets : res = let 298 val _ = OS.FileSys.chDir (hmdir.toAbsPath dir) 299 300 val option_value = 301 pass_option_value |> apply_updates (get_hmf_cline_updates()) 302 val coption_value = #core option_value 303 304 val allfast = #fast coption_value 305 val always_rebuild_deps = #rebuild_deps coption_value 306 val cline_recursive = #recursive coption_value 307 val debug = #debug coption_value 308 val dontmakes = #dontmakes coption_value 309 val user_hmakefile = #hmakefile coption_value 310 val cmdl_HOLDIR = #holdir coption_value 311 val cline_additional_includes = 312 cline_additional_includes @ #includes coption_value 313 val keep_going_flag = #keep_going coption_value 314 val no_action = #no_action coption_value 315 val no_hmakefile = #no_hmakefile coption_value 316 val no_overlay = #no_overlay coption_value 317 val no_prereqs = #no_prereqs coption_value 318 val opentheory = #opentheory coption_value 319 val quiet_flag = #quiet coption_value 320 val quit_on_failure = #quit_on_failure coption_value 321 val verbose = #verbose coption_value 322 (* find HOLDIR by first looking at command-line, then looking 323 for a value compiled into the code. 324 *) 325 val HOLDIR = case cmdl_HOLDIR of NONE => HOLDIR0 | SOME s => s 326 val SIGOBJ = normPath(Path.concat(HOLDIR, "sigobj")); 327 328 329(* prepare to do logging *) 330val () = if do_logging_flag then 331 if FileSys.access (logfilename, []) then 332 warn "Make log exists; new logging will concatenate on this file" 333 else let 334 (* touch the file *) 335 val outs = TextIO.openOut logfilename 336 in 337 TextIO.closeOut outs 338 end handle IO.Io _ => warn "Couldn't set up make log" 339 else () 340 341 342 343val hmakefile = 344 case user_hmakefile of 345 NONE => "Holmakefile" 346 | SOME s => 347 if exists_readable s then s 348 else die_with ("Couldn't read/find makefile: "^s) 349 350val base_env = HM_BaseEnv.make_base_env option_value 351 352val (hmakefile_env, extra_rules, first_target) = 353 if exists_readable hmakefile andalso not no_hmakefile 354 then let 355 val () = diag (fn _ => "Reading additional information from "^hmakefile) 356 in 357 ReadHMF.read hmakefile base_env 358 end 359 else (base_env, Holmake_types.empty_ruledb, NONE) 360 361val envlist = envlist hmakefile_env 362 363val hmake_includes = envlist "INCLUDES" 364val hmake_options = envlist "OPTIONS" 365val additional_includes = 366 remove_duplicates (cline_additional_includes @ hmake_includes) 367 368val hmake_preincludes = envlist "PRE_INCLUDES" 369val hmake_no_overlay = member "NO_OVERLAY" hmake_options 370val hmake_no_sigobj = member "NO_SIGOBJ" hmake_options 371val hmake_qof = member "QUIT_ON_FAILURE" hmake_options 372val hmake_noprereqs = member "NO_PREREQS" hmake_options 373val extra_cleans = envlist "EXTRA_CLEANS" 374 375val quit_on_failure = quit_on_failure orelse hmake_qof 376 377val _ = if cline_recursive andalso no_prereqs then 378 warn("-r forces recursion, taking precedence over --no_prereqs") 379 else () 380val no_prereqs = (no_prereqs orelse hmake_noprereqs) andalso not cline_recursive 381 382val _ = 383 if quit_on_failure andalso allfast then 384 warn "quit on (tactic) failure ignored for fast built theories" 385 else 386 () 387 388val no_sigobj = hmake_no_sigobj 389val actual_overlay = 390 if no_sigobj orelse no_overlay orelse hmake_no_overlay then NONE 391 else SOME DEFAULT_OVERLAY 392 393val std_include_flags = if no_sigobj then [] else [SIGOBJ] 394 395fun extra_deps t = 396 Option.map #dependencies 397 (Holmake_types.get_rule_info extra_rules hmakefile_env t) 398 399fun isPHONY t = 400 case extra_deps ".PHONY" of 401 NONE => false 402 | SOME l => member t l 403 404fun extra_commands t = 405 Option.map #commands 406 (Holmake_types.get_rule_info extra_rules hmakefile_env t) 407 408val extra_targets = Binarymap.foldr (fn (k,_,acc) => k::acc) [] extra_rules 409 410fun extra_rule_for t = Holmake_types.get_rule_info extra_rules hmakefile_env t 411 412(* treat targets as sets *) 413infix in_target 414fun (s in_target t) = case extra_deps t of NONE => false | SOME l => member s l 415 416(*** Compilation of files *) 417val binfo : HM_Cline.t BuildCommand.buildinfo_t = 418 {optv = option_value, hmake_options = hmake_options, 419 actual_overlay = actual_overlay, envlist = envlist, 420 hmenv = hmakefile_env, 421 quit_on_failure = quit_on_failure, outs = outputfns, 422 SIGOBJ = SIGOBJ} 423val {extra_impl_deps,build_graph} = BuildCommand.make_build_command binfo 424 425val _ = let 426in 427 diag (fn _ => "HOLDIR = "^HOLDIR); 428 diag (fn _ => "Targets = [" ^ String.concatWith ", " targets ^ "]"); 429 diag (fn _ => "Additional includes = [" ^ 430 String.concatWith ", " additional_includes ^ "]"); 431 diag (fn _ => "Using HOL sigobj dir = "^Bool.toString (not no_sigobj)); 432 diag (fn _ => HM_BaseEnv.debug_info option_value) 433end 434 435(** Top level sketch of algorithm *) 436(* 437 438 We have the following relationship --> where this arrow should be read 439 "leads to the production of in one step" 440 441 *.sml --> *.uo [ mosmlc -c ] 442 *.sig --> *.ui [ mosmlc -c ] 443 *Script.uo --> *Theory.sig *Theory.sml 444 [ running the *Script that can be produced from the .uo file ] 445 *Script.uo --> *.art 446 [ running the *Script with proof-recording enabled ] 447 *.art --> *.ot.art 448 [ opentheory info --article ] 449 450 (where I have included the tool that achieves the production of the 451 result in []s) 452 453 However, not all productions can go ahead with just the one principal 454 dependency present. Sometimes other files are required to be present 455 too. We don't know which other files which are required, but we can 456 find out by using Ken's holdep tool. (This works as follows: given the 457 name of the principal dependency for a production, it gives us the 458 name of the other dependencies that exist in the current directory.) 459 460 In theory, we could just run holdep everytime we were invoked, and 461 with a bit of luck we'll design things so it does look as if really 462 are computing the dependencies every time. However, this is 463 unnecessary work as we can cache this information in files and just 464 read it in from these. Of course, this introduces a sub-problem of 465 knowing that the information in the cache files is up-to-date, so 466 we will need to compare time-stamps in order to be sure that the 467 cached dependency information is up to date. 468 469 Another problem is that we might need to build a dependency DAG but 470 in a situation where elements of the principal dependency chain 471 were themselves out of date. 472*) 473 474(* The primary dependency chain does not depend on anything in the 475 file-system; it always looks the same. However, additional 476 dependencies depend on what holdep tells us. This function that 477 runs holdep, and puts the output into specified file, which will live 478 in DEPDIR somewhere. *) 479 480fun get_implicit_dependencies incinfo (f: File) : File list = let 481 val _ = diag (fn _ => "Calling get_implicit_dependencies on "^fromFile f) 482 val file_dependencies0 = 483 get_direct_dependencies {incinfo = incinfo, extra_targets = extra_targets, 484 output_functions = outputfns, 485 DEPDIR = DEPDIR} f 486 val file_dependencies = 487 case actual_overlay of 488 NONE => file_dependencies0 489 | SOME s => if isSome (holdep_arg f) then 490 toFile (fullPath [SIGOBJ, s]) :: file_dependencies0 491 else 492 file_dependencies0 493 fun requires_exec (SML (Theory _)) = true 494 | requires_exec (SIG (Theory _)) = true 495 | requires_exec (ART (RawArticle _)) = true 496 | requires_exec (DAT _) = true 497 | requires_exec _ = false 498in 499 if requires_exec f then let 500 (* because we have to build an executable in order to build a 501 theory, this build depends on all of the dependencies 502 (meaning the transitive closure of the direct dependency 503 relation) in their .UO form, not just .UI *) 504 val get_direct_dependencies = 505 get_direct_dependencies {incinfo = incinfo, DEPDIR = DEPDIR, 506 output_functions = outputfns, 507 extra_targets = extra_targets} 508 fun collect_all_dependencies sofar tovisit = 509 case tovisit of 510 [] => sofar 511 | (f::fs) => let 512 val deps = 513 if Path.dir (string_part f) <> "" then [] 514 else 515 case f of 516 UI x => (get_direct_dependencies f @ 517 get_direct_dependencies (UO x)) 518 | _ => get_direct_dependencies f 519 val newdeps = set_diff deps sofar 520 in 521 collect_all_dependencies (sofar @ newdeps) 522 (set_union newdeps fs) 523 end 524 val tcdeps = collect_all_dependencies [] [f] 525 val uo_deps = 526 List.mapPartial (fn (UI x) => SOME (UO x) | _ => NONE) tcdeps 527 val alldeps = set_union (set_union tcdeps uo_deps) 528 (set_union file_dependencies extra_impl_deps) 529 in 530 case f of 531 SML x => let 532 (* there may be theory files mentioned in the Theory.sml file that 533 aren't mentioned in the script file. If so, we are really 534 dependent on these, and should add them. They will be listed 535 in the dependencies for UO (Theory x). *) 536 val additional_theories = 537 if exists_readable (fromFile f) then 538 List.mapPartial 539 (fn (x as (UO (Theory s))) => SOME x | _ => NONE) 540 (get_implicit_dependencies incinfo (UO x)) 541 else [] 542 in 543 set_union alldeps additional_theories 544 end 545 | _ => alldeps 546 end 547 else 548 file_dependencies 549end 550 551fun get_explicit_dependencies (f : File) : File list = 552 case (extra_deps (fromFile f)) of 553 SOME deps => map toFile deps 554 | NONE => [] 555 556(** Build graph *) 557 558(* 559fun do_a_build_command incinfo target pdep secondaries = 560 case (extra_commands (fromFile target)) of 561 SOME (cs as _ :: _) => 562 Process.isSuccess (run_extra_commands (fromFile target) cs secondaries) 563 | _ (* i.e., NONE or SOME [] *) => let 564 val build_command = build_command incinfo 565 in 566 case target of 567 UO c => build_command (Compile secondaries) pdep 568 | UI c => build_command (Compile secondaries) pdep 569 | SML (Theory s) => build_command (BuildScript (s, secondaries)) pdep 570 | SIG (Theory s) => build_command (BuildScript (s, secondaries)) pdep 571 | ART (RawArticle s) => build_command (BuildArticle(s, secondaries)) pdep 572 | ART (ProcessedArticle s) => build_command (ProcessArticle s) pdep 573 | x => raise Fail "Can't happen" 574 (* can't happen because do_a_build_command is only 575 called on targets that have primary_dependents, 576 and those are those targets of the shapes already 577 matched in the previous cases *) 578 end 579*) 580 581exception CircularDependency 582exception BuildFailure 583exception NotFound 584 585fun no_full_extra_rule tgt = 586 case extra_commands (fromFile tgt) of 587 NONE => true 588 | SOME cl => null cl 589 590val done_some_work = ref false 591open HM_DepGraph 592 593fun is_script s = 594 case toFile s of 595 SML (Script _) => true 596 | _ => false 597 598fun de_script s = 599 case toFile s of 600 SML (Script s) => SOME s 601 | _ => NONE 602 603fun build_depgraph cdset incinfo target g0 : (t * node) = let 604 val pdep = primary_dependent target 605 val target_s = fromFile target 606 fun addF f n = (n,fromFile f) 607 fun nstatus g n = peeknode g n |> valOf |> #status 608 fun build tgt' g = 609 build_depgraph (Binaryset.add(cdset, target_s)) incinfo tgt' g 610 val _ = not (Binaryset.member(cdset, target_s)) orelse 611 die (target_s ^ " seems to depend on itself - failing") 612in 613 case target_node g0 target_s of 614 (x as SOME n) => (g0, n) 615 | NONE => 616 if Path.dir (string_part target) <> "" andalso 617 Path.dir (string_part target) <> "." andalso 618 no_full_extra_rule target 619 (* path outside of current directory *) 620 then 621 add_node {target = target_s, seqnum = 0, phony = false, 622 status = if exists_readable target_s then Succeeded 623 else Failed, 624 dir = hmdir.curdir(), 625 command = NoCmd, dependencies = []} g0 626 else if isSome pdep andalso no_full_extra_rule target then 627 let 628 val pdep = valOf pdep 629 val (g1, pnode) = build pdep g0 630 val secondaries = set_union (get_implicit_dependencies incinfo target) 631 (get_explicit_dependencies target) 632 fun foldthis (d, (g, secnodes)) = 633 let 634 val (g', n) = build d g 635 in 636 (g', addF d n::secnodes) 637 end 638 val (g2, depnodes : (HM_DepGraph.node * string) list) = 639 List.foldl foldthis (g1, [addF pdep pnode]) secondaries 640 val unbuilt_deps = 641 List.filter (fn (n,_) => let val stat = nstatus g2 n 642 in 643 stat = Pending orelse stat = Failed 644 end) 645 depnodes 646 val needs_building = 647 not (null unbuilt_deps) orelse 648 List.exists (fn d => d forces_update_of target_s) 649 (fromFile pdep :: map fromFile secondaries) 650 val bic = case toFile target_s of 651 SML (Theory s) => BIC_BuildScript s 652 | SIG (Theory s) => BIC_BuildScript s 653 | DAT s => BIC_BuildScript s 654 | _ => BIC_Compile 655 in 656 add_node {target = target_s, seqnum = 0, phony = false, 657 status = if needs_building then Pending else Succeeded, 658 command = BuiltInCmd bic, dir = hmdir.curdir(), 659 dependencies = depnodes } g2 660 end 661 else 662 case extra_rule_for target_s of 663 NONE => 664 add_node {target = target_s, seqnum = 0, phony = false, 665 status = if exists_readable target_s then Succeeded 666 else Failed, 667 command = NoCmd, dir = hmdir.curdir(), 668 dependencies = []} g0 669 | SOME {dependencies, commands, ...} => 670 let 671 fun foldthis (d, (g, secnodes)) = 672 let 673 val (g, n) = build d g 674 in 675 (g, addF d n::secnodes) 676 end 677 fun depfoldthis (s, (starp, deps)) = 678 if s <> "" andalso String.sub(s,0) = #"*" andalso 679 is_script s 680 (* is_script returns true for, e.g., *boolScript.sml *) 681 then 682 if isSome starp then 683 die ("Multiple starred script dependencies for "^target_s) 684 else 685 let 686 val s = String.extract(s,1,NONE) 687 in 688 (SOME s, s :: deps) 689 end 690 else (starp, s::deps) 691 val (starred_dep, dependencies) = 692 if null commands then 693 List.foldr depfoldthis (NONE, []) dependencies 694 else (NONE, dependencies) 695 696 val more_deps = 697 case starred_dep of 698 NONE => [] 699 | SOME s => 700 get_implicit_dependencies 701 incinfo 702 (SML(Theory (valOf (de_script s)))) 703 handle Option => die "more_deps invariant failure" 704 705 val (g1, depnodes) = 706 List.foldl foldthis (g0, []) 707 (more_deps @ map toFile dependencies) 708 709 val unbuilt_deps = 710 List.filter (fn (n,_) => let val stat = nstatus g1 n 711 in 712 stat = Pending orelse stat = Failed 713 end) 714 depnodes 715 val is_phony = isPHONY target_s 716 val needs_building_by_deps_existence = 717 (not (OS.FileSys.access(target_s, [])) orelse 718 not (null unbuilt_deps) orelse 719 List.exists (fn d => d forces_update_of target_s) 720 dependencies orelse 721 is_phony) 722 val needs_building = 723 needs_building_by_deps_existence andalso 724 not (null commands) 725 val status = if needs_building then Pending else Succeeded 726 fun foldthis (c, (depnode, seqnum, g)) = 727 let 728 val (g',n) = add_node {target = target_s, seqnum = seqnum, 729 status = status, phony = is_phony, 730 command = SomeCmd c, 731 dir = hmdir.curdir(), 732 dependencies = depnode @ depnodes } g 733 in 734 (* The "" is necessary to make multi-command, multi-target 735 rules work: when subsequent nodes (seqnum > 0) are added 736 to the graph targetting a target other than the first, 737 it is important that this new node merges with the 738 corresponding seqnum>0 node generated from the first 739 target *) 740 ([(n,"")], seqnum + 1, g') 741 end 742 in 743 if needs_building then 744 let 745 val (lastnodelist, _, g) = 746 List.foldl foldthis ([], 0, g1) commands 747 in 748 (g, #1 (hd lastnodelist)) 749 end 750 else 751 case starred_dep of 752 NONE => 753 add_node {target = target_s, seqnum = 0, phony = is_phony, 754 status = status, command = NoCmd, 755 dir = hmdir.curdir(), dependencies = depnodes} g1 756 | SOME scr => 757 (case toFile scr of 758 SML (Script s) => 759 let 760 val updstatus = 761 if needs_building_by_deps_existence then Pending 762 else Succeeded 763 in 764 add_node {target = target_s, seqnum = 0, 765 phony = false, status = updstatus, 766 command = BuiltInCmd (BIC_BuildScript s), 767 dir = hmdir.curdir(), 768 dependencies = depnodes} g1 769 end 770 | _ => die "Invariant failure in build_depgraph") 771 end 772end 773 774 775val allincludes = 776 cline_additional_includes @ hmake_includes 777 778fun add_sigobj {includes,preincludes} = 779 {includes = std_include_flags @ includes, 780 preincludes = preincludes} 781 782fun null_ii {includes,preincludes} = null includes andalso null preincludes 783 784val extended_dirinfo = 785 let 786 fun mkd s = hmdir.extendp{base = dir, extension = s} 787 val mkS = 788 List.foldl (fn (s, acc) => Binaryset.add(acc, mkd s)) empty_dirset 789 in 790 { 791 visited = #visited dirinfo, 792 incdirmap = 793 extend_idmap 794 dir 795 {incs= mkS allincludes, pres= mkS hmake_preincludes} 796 (#incdirmap dirinfo) 797 } 798 end 799 800val recurse_into_dirs = allincludes @ hmake_preincludes 801 802fun hm_recur ctgt k : holmake_result = let 803 val nobuild = toplevel_no_prereqs orelse no_prereqs 804 fun hm dir dirinfo targets = 805 Holmake nobuild dir dirinfo [] targets 806 val warn = if nobuild then (fn _ => ()) else warn 807in 808 maybe_recurse 809 {warn = warn, 810 diag = diag, 811 hm = hm, 812 dirinfo = extended_dirinfo, 813 dir = dir, 814 local_build = k, 815 cleantgt = ctgt} 816 recurse_into_dirs 817end 818 819fun create_graph tgts ii = 820 let 821 open HM_DepGraph 822 val empty_tgts = Binaryset.empty String.compare 823 val _ = diag(fn _ => "Building dep. graph with targets: " ^ 824 String.concatWith " " tgts) 825 val g = 826 List.foldl 827 (fn (t, g) => #1 (build_depgraph empty_tgts ii t g)) 828 empty 829 (map toFile tgts) 830 in 831 diag (fn _ => "Finished building dep graph (has " ^ 832 Int.toString (size g) ^ " nodes)"); 833 g 834 end 835 836fun clean_deps() = 837 ( Holmake_tools.clean_depdir {depdirname = DEPDIR} 838 ; Holmake_tools.clean_depdir {depdirname = LOGDIR} ) 839 840fun do_clean_target x = let 841 fun clean_action () = 842 (Holmake_tools.clean_dir {extra_cleans = extra_cleans}; true) 843in 844 case x of 845 "clean" => ((info "Cleaning directory of object files\n"; 846 clean_action(); 847 true) handle _ => false) 848 | "cleanDeps" => clean_deps() 849 | "cleanAll" => clean_action() andalso clean_deps() 850 | _ => die ("Bad clean target " ^ x) 851end 852 853fun basecont tgts ii = 854 if List.exists (fn x => member x ["clean", "cleanDeps", "cleanAll"]) tgts then 855 (app (ignore o do_clean_target) tgts; true) 856 else 857 let 858 open HM_DepGraph 859 val _ = if null_ii ii andalso hmdir.compare(dir,original_dir) = EQUAL then 860 () 861 else warn (bold ("Working in " ^ hmdir.pretty_dir dir)) 862 val ii = add_sigobj ii 863 val g = create_graph tgts ii 864 val _ = diag (fn _ => "Building from graph") 865 val res = build_graph ii g 866 val buildok = OS.Process.isSuccess res 867 val _ = diag (fn _ => "Built from graph with result " ^ 868 (if buildok then "OK" else "FAILED")) 869 in 870 finish_logging buildok 871 end 872 873fun no_action_cont tgts ii = 874 let 875 open HM_DepGraph 876 val ii = add_sigobj ii 877 val g = create_graph tgts ii 878 fun pr s = s 879 fun str (n,ni) = 880 "{" ^ node_toString n ^ "}: " ^ nodeInfo_toString pr ni ^ "\n" 881 in 882 List.app (print o str) (listNodes g); 883 true 884 end 885 886val stdcont = if no_action then no_action_cont else basecont 887 888val _ = not always_rebuild_deps orelse clean_deps() 889 890in 891 if nobuild then hm_recur NONE (fn _ => true) 892 else 893 case targets of 894 [] => let 895 val targets = generate_all_plausible_targets warn first_target 896 val targets = map fromFile targets 897 val _ = 898 let 899 val tgtstrings = 900 map 901 (fn s => if OS.FileSys.access(s, []) then s else s ^ "(*)") 902 targets 903 in 904 diag(fn _ => "Generated targets are: [" ^ 905 String.concatWith ", " tgtstrings ^ "]") 906 end 907 in 908 hm_recur NONE (stdcont targets) 909 end 910 | xs => let 911 val cleanTarget_opt = 912 List.find (fn x => member x ["clean", "cleanDeps", "cleanAll"]) xs 913 fun canon i = hmdir.extendp {base = dir, extension = i} 914 in 915 if isSome cleanTarget_opt andalso not cline_recursive then 916 (List.app (ignore o do_clean_target) xs; 917 finish_logging true; 918 SOME dirinfo) 919 else 920 hm_recur cleanTarget_opt (stdcont xs) 921 end 922end (* fun Holmake *) 923 924 925in 926 if show_usage then 927 print (GetOpt.usageInfo { 928 header = "Usage:\n " ^ CommandLine.name() ^ " [targets]\n\n\ 929 \Special targets are: clean, cleanDeps and cleanAll\n\n\ 930 \Extra options:", 931 options = HM_Cline.option_descriptions 932 }) 933 else let 934 open Process 935 val result = 936 Holmake false (* yes, build something *) 937 (hmdir.curdir()) 938 {visited = Binaryset.empty hmdir.compare, 939 incdirmap = empty_incdirmap} 940 cline_additional_includes 941 targets 942 handle Fail s => die ("Fail exception: "^s^"\n") 943 in 944 if isSome result then exit success 945 else exit failure 946 end 947 948end (* main *) 949 950end (* struct *) 951 952(** Local variable rubbish *) 953(* local variables: *) 954(* mode: sml *) 955(* outline-regexp: " *(\\*\\*+" *) 956(* end: *) 957