1structure BuildCommand :> BuildCommand = 2struct 3 4open Systeml Holmake_tools Holmake_types 5structure FileSys = OS.FileSys 6structure Path = OS.Path 7structure Process = OS.Process 8 9infix ++ 10fun p1 ++ p2 = Path.concat(p1,p2) 11val SIGOBJ = Systeml.HOLDIR ++ "sigobj" 12 13 14 15infix |> 16fun x |> f = f x 17 18val default_holstate = Systeml.DEFAULT_STATE 19 20val _ = holpathdb.extend_db {vname = "HOLDIR", path = Systeml.HOLDIR} 21 22open HM_GraphBuildJ1 23 24datatype cmd_line = Mosml_compile of string list * string 25 | Mosml_link of string * string list 26 | Mosml_error 27 28datatype buildresult = datatype multibuild.buildresult 29 30fun process_mosml_args (outs:Holmake_tools.output_functions) c = let 31 val {diag,...} = outs 32 val diag = fn s => diag "mosml_args" (fn _ => s) 33 fun isSource t = OS.Path.ext t = SOME "sig" orelse OS.Path.ext t = SOME "sml" 34 fun isObj t = OS.Path.ext t = SOME "uo" orelse OS.Path.ext t = SOME "ui" 35 val toks = String.tokens (fn c => c = #" ") c 36 val c = ref false 37 val q = ref false 38 val obj = ref NONE 39 val I = ref [] 40 val obj_files = ref ([] : string list) 41 val src_file = ref NONE 42 fun process_args [] = () 43 | process_args ("-c"::rest) = (c := true; process_args rest) 44 | process_args ("-q"::rest) = process_args rest 45 | process_args ("-toplevel"::rest) = process_args rest 46 | process_args ("-o"::arg::rest) = (obj := SOME arg; process_args rest) 47 | process_args ("-I"::arg::rest) = (I := arg::(!I); process_args rest) 48 | process_args (file::rest) = let 49 in 50 if file = HM_BaseEnv.mosml_indicator then () 51 else if isSource file then 52 src_file := SOME file 53 else if isObj file then 54 obj_files := file :: !obj_files 55 else (); 56 process_args rest 57 end 58in 59 process_args toks; 60 ((case (!c, !src_file, !obj_files, !obj) of 61 (true, SOME f, ofs, NONE) => Mosml_compile (List.rev ofs, f) 62 | (false, NONE, ofs, SOME f) => Mosml_link (f, List.rev ofs) 63 | _ => let 64 fun ostring NONE = "NONE" 65 | ostring (SOME s) = "SOME "^s 66 in 67 diag ("mosml error: c = "^Bool.toString (!c)^", src_file = "^ 68 ostring (!src_file) ^ ", obj = "^ostring (!obj)); 69 Mosml_error 70 end), 71 List.rev (!I)) 72end; 73 74 75 76 77fun posix_diagnostic stat = let 78 open Posix.Process 79in 80 case fromStatus stat of 81 W_EXITSTATUS w8 => "exited with code "^Word8.toString w8 82 | W_EXITED => "exited normally" 83 | W_SIGNALED sg => "with signal " ^ 84 SysWord.toString (Posix.Signal.toWord sg) 85 | W_STOPPED sg => "stopped with signal " ^ 86 SysWord.toString (Posix.Signal.toWord sg) 87end 88 89fun addPath incs (file : string) : dep = 90 let 91 val dir = OS.FileSys.getDir() 92 open hm_target 93 in 94 if OS.Path.dir file <> "" then filestr_to_tgt file 95 else let 96 val p = List.find (fn p => 97 FileSys.access (p ++ (file ^ ".ui"), [])) 98 (dir :: incs) 99 in 100 case p of 101 NONE => mk(hmdir.curdir(), toFile file) 102 | SOME p => mk(hmdir.fromPath {origin = dir, path = p}, toFile file) 103 end 104 end 105 106fun time_max(t1,t2) = if Time.<(t1,t2) then t2 else t1 107 108fun finish_compilation warn depMods0 filename tgt = 109 case OS.Process.getEnv Systeml.build_after_reloc_envvar of 110 NONE => OS.Process.success 111 | SOME "1" => 112 let 113 val filename_base = OS.Path.base filename 114 val depMods = List.filter (fn s => s <> filename_base) depMods0 115 fun getFTime fname = 116 SOME (OS.FileSys.modTime fname) handle OS.SysErr _ => NONE 117 fun combine fname t = 118 case getFTime fname of NONE => t | SOME t0 => time_max(t0,t) 119 fun foldthis (modn, t) = 120 t |> combine (modn ^ ".uo") |> combine (modn ^ ".ui") 121 val startTime = 122 case getFTime filename of 123 NONE => (warn("Can't see base file " ^ filename ^ 124 " though I just compiled it??"); 125 Time.zeroTime) 126 | SOME t => t 127 in 128 OS.FileSys.setTime (tgt, SOME (List.foldl foldthis startTime depMods)); 129 OS.Process.success 130 end 131 | SOME s => 132 (warn ("Ignoring strange value (" ^ s ^ ") in " ^ 133 Systeml.build_after_reloc_envvar ^ " environment variable"); 134 OS.Process.success) 135 136fun poly_compile warn diag quietp file I (deps : dep list) objs = let 137 open hm_target 138 val _ = diag (fn _ => "poly-compiling " ^ fromFile file ^ "\n deps = [" ^ 139 concatWithf tgt_toString ", " deps ^ "]\n objs = [" ^ 140 String.concatWith ", " objs ^ "]") 141 val modName = fromFileNoSuf file 142 val deps = let 143 open Binaryset 144 val dep_set0 = addList (empty_tgtset, deps) 145 val {deps = extra_deps, ...} = 146 Holdep.main {assumes = [], includes = I, diag = diag, 147 fname = fromFile file} 148 val dep_set = 149 addList (dep_set0, map filestr_to_tgt extra_deps) 150 in 151 listItems dep_set 152 end 153 val depfiles = map (toFile o tgt_toString) deps 154 val objfiles = map toFile objs 155 fun mapthis (Unhandled _) = NONE 156 | mapthis (DAT _) = NONE 157 | mapthis f = SOME (fromFileNoSuf f) 158 val depMods = List.mapPartial mapthis depfiles 159 val objMods = List.map (addPath I) (List.mapPartial mapthis objfiles) 160 fun usePathVars p = holpathdb.reverse_lookup {path = p} 161 val depMods = List.map usePathVars (depMods @ map tgt_toString objMods) 162 val say = if quietp then (fn s => ()) 163 else (fn s => TextIO.output(TextIO.stdOut, s ^ "\n")) 164 val _ = say ("HOLMOSMLC -c " ^ fromFile file) 165 val filename = tgt_toString (filestr_to_tgt (fromFile file)) 166 val _ = diag (fn _ => "Writing target with dependencies: " ^ 167 String.concatWith ", " depMods) 168in 169case file of 170 SIG _ => 171 (let 172 val tgt = modName ^ ".ui" 173 val outUi = TextIO.openOut tgt 174 in 175 TextIO.output (outUi, String.concatWith "\n" depMods); 176 TextIO.output (outUi, "\n"); 177 TextIO.output (outUi, usePathVars filename ^ "\n"); 178 TextIO.closeOut outUi; 179 finish_compilation warn depMods filename tgt 180 end 181 handle IO.Io _ => OS.Process.failure) 182| SML _ => 183 (let 184 val tgt = modName ^ ".uo" 185 val outUo = TextIO.openOut tgt 186 in 187 TextIO.output (outUo, String.concatWith "\n" depMods); 188 TextIO.output (outUo, "\n"); 189 TextIO.output (outUo, usePathVars filename ^ "\n"); 190 TextIO.closeOut outUo; 191 (if OS.FileSys.access (modName ^ ".sig", []) then 192 () 193 else 194 let val outUi = TextIO.openOut (modName ^ ".ui") 195 in 196 TextIO.closeOut outUi; 197 ignore (finish_compilation warn depMods filename (modName ^ ".ui")) 198 end); 199 finish_compilation warn depMods filename tgt 200 end 201 handle IO.Io _ => OS.Process.failure) 202| _ => raise Match 203end 204 205fun list_delete x [] = [] 206 | list_delete x (y::ys) = if x = y then ys else y :: list_delete x ys 207 208type 'a build_command = 'a HM_DepGraph.t -> 209 {preincludes : string list, includes : string list} -> 210 (dep,'a) Holmake_tools.buildcmds -> 211 File -> bool 212 213fun make_build_command (buildinfo : HM_Cline.t buildinfo_t) = let 214 val {optv,actual_overlay,envlist,quit_on_failure,outs,...} = 215 buildinfo 216 val hmenv = #hmenv buildinfo 217 val {warn,diag,tgtfatal,...} = outs 218 val keep_going = #keep_going (#core optv) 219 val debug = #debug (#core optv) 220 val opentheory = #opentheory (#core optv) 221 val allfast = #fast (#core optv) 222 val polynothol = #poly_not_hol optv 223 val relocbuild = #relocbuild optv orelse 224 (case OS.Process.getEnv Systeml.build_after_reloc_envvar of 225 SOME "1" => true 226 | _ => false) 227 val interactive_flag = #interactive (#core optv) 228 val quiet_flag = #quiet (#core optv) 229 val cmdl_HOLSTATE = #holstate optv 230 val jobs = #jobs (#core optv) 231 val time_limit = #time_limit optv 232 val chatty = if jobs = 1 then #chatty outs else (fn _ => ()) 233 val info = if jobs = 1 then #info outs else (fn _ => ()) 234 235 fun extra_poly_cline() = envlist "POLY_CLINE_OPTIONS" 236 237 fun poly_link quietp extra result files = 238 let 239 open hm_target 240 val _ = if not quietp then 241 TextIO.output(TextIO.stdOut, 242 "HOLMOSMLC -o " ^ result ^ " " ^ 243 String.concatWith " " 244 (map (fn s => s ^ ".uo") files) ^ 245 "\n") 246 else () 247 val out = TextIO.openOut result 248 fun p s = 249 (TextIO.output (out, s); TextIO.output (out, "\n")) 250 in 251 p "#!/bin/sh"; 252 p ("set -e"); 253 p (protect(fullPath [HOLDIR, "bin", "buildheap"]) ^ " --gcthreads=1 " ^ 254 (case #holheap extra of NONE => "--poly" 255 | SOME d => "--holstate="^tgt_toString d) ^ " " ^ 256 (if isSome debug then "--dbg " else "") ^ 257 String.concatWith " " (extra_poly_cline()) ^ " " ^ 258 String.concatWith " " (map protect files)); 259 p ("exit 0"); 260 TextIO.closeOut out; 261 Systeml.mk_xable result; 262 OS.Process.success 263 end handle IO.Io _ => OS.Process.failure 264 265 fun build_command g (ii as {preincludes,includes}) c arg = let 266 val diag = diag "build_command" 267 val _ = diag (fn _ => "build_command on "^fromFile arg) 268 val include_flags = preincludes @ includes 269 val overlay_stringl = case actual_overlay of NONE => [] | SOME s => [s] 270 exception CompileFailed 271 exception FileNotFound 272 val isSuccess = OS.Process.isSuccess 273 fun setup_script s depinfo extras = let 274 val scriptsml_file = SML (Script s) 275 val scriptsml = fromFile scriptsml_file 276 val script = s^"Script" 277 val scriptuo = script^".uo" 278 val scriptui = script^".ui" 279 (* first thing to do is to create the Script.uo file *) 280 val b = 281 case build_command g ii (Compile depinfo) scriptsml_file of 282 BR_OK => true 283 | BR_Failed => false 284 | BR_ClineK _ => raise Fail "Compilation resulted in commandline" 285 val _ = b orelse raise CompileFailed 286 val _ = info ("Linking "^scriptuo^" to produce theory-builder executable") 287 val objectfiles0 = 288 if allfast then ["fastbuild.uo", scriptuo] 289 else if quit_on_failure then [scriptuo] 290 else ["holmakebuild.uo", scriptuo] 291 val objectfiles0 = extras @ objectfiles0 292 val objectfiles = 293 if polynothol then 294 objectfiles0 295 else if interactive_flag then 296 (SIGOBJ ++ "holmake_interactive.uo") :: objectfiles0 297 else (SIGOBJ ++ "holmake_not_interactive.uo") :: objectfiles0 298 in 299 ((script,[scriptuo,scriptui,script]), objectfiles) 300 end 301 fun run_script g (extra:GraphExtra.t) (script, intermediates) objectfiles expecteds = 302 let 303 fun safedelete s = FileSys.remove s handle OS.SysErr _ => () 304 val _ = app safedelete expecteds 305 val useScript = fullPath [HOLDIR, "bin", "buildheap"] 306 val cline = 307 useScript::"--gcthreads=1":: 308 (case #multithread optv of 309 NONE => [] 310 | SOME i => ["--mt=" ^ Int.toString i]) @ 311 (case #holheap extra of NONE => "--poly" 312 | SOME d => "--holstate="^tgt_toString d) :: 313 extra_poly_cline() @ 314 ((if isSome debug then ["--dbg"] else []) @ objectfiles) @ 315 List.concat (map (fn f => ["-c", f]) expecteds) 316 fun cont wn res = 317 let 318 val _ = 319 if not (isSuccess res) then 320 wn ("Failed script build for "^script^" - "^ 321 posix_diagnostic res) 322 else () 323 val _ = if isSuccess res orelse debug = NONE then 324 app safedelete (script :: intermediates) 325 else () 326 in 327 isSuccess res 328 end 329 val script_part = 330 if String.isSuffix "Script" script then 331 String.substring(script, 0, size script - 6) 332 else raise Fail "Invariant failure in run_script" 333 val other_nodes = let 334 open HM_DepGraph 335 in 336 diag (fn _ => "Looking for other nodes with buildscript "^script); 337 find_nodes_by_command g 338 (BuiltInCmd (BIC_BuildScript script_part, empty_incinfo)) 339 (* incinfos not consulted for comparison so empty value ok here *) 340 end 341 in 342 BR_ClineK { cline = (useScript, cline), job_kont = cont, 343 other_nodes = other_nodes } 344 end 345 in 346 let 347 in 348 case (c : (dep,GraphExtra.t) buildcmds) of 349 Compile (deps,_) => 350 let 351 val file = fromFile arg 352 val _ = exists_readable file orelse 353 (warn ("Wanted to compile "^file^ 354 ", but it wasn't there\n"); 355 raise FileNotFound) 356 val res = poly_compile warn diag true arg include_flags deps [] 357 in 358 if OS.Process.isSuccess res then BR_OK else BR_Failed 359 end 360 | BuildScript (s, deps, extra : GraphExtra.t) => 361 let 362 val (scriptetc,objectfiles) = setup_script s (deps,extra) [] 363 in 364 run_script g extra scriptetc objectfiles 365 [s^"Theory.sml", s^"Theory.sig", s^"Theory.dat"] 366 end 367 | BuildArticle (s0, deps : dep list, extra) => 368 let 369 open hm_target 370 val s = s0 ^ ".art" 371 val dep_set = Binaryset.addList(empty_tgtset, deps) 372 val oldscript_str = s0 ^ "Script.sml" 373 val fakescript_str = s ^ "Script.sml" 374 val _ = Posix.FileSys.link {old = oldscript_str, 375 new = fakescript_str } 376 val loggingextras = 377 case opentheory of SOME uo => [uo] 378 | NONE => ["loggingHolKernel.uo"] 379 val deps = 380 (Binaryset.delete(dep_set, filestr_to_tgt oldscript_str) 381 |> Binaryset.listItems) @ 382 [filestr_to_tgt fakescript_str] 383 val ((script,inters),objectfiles) = 384 setup_script s (deps,extra) loggingextras 385 in 386 run_script g extra (script,fakescript_str :: inters) objectfiles [s] 387 end 388 | ProcessArticle (s,extra) => 389 let 390 val raw_art_file = ART (RawArticle s) 391 val art_file = ART (ProcessedArticle s) 392 val raw_art = fromFile raw_art_file 393 val art = fromFile art_file 394 val cline = 395 ("/bin/sh", 396 ["/bin/sh", "-c", 397 "opentheory info --article -o " ^ art ^ " " ^ raw_art]) 398 in 399 BR_ClineK {cline = cline, job_kont = (fn _ => OS.Process.isSuccess), 400 other_nodes = []} 401 end 402 end handle CompileFailed => BR_Failed 403 | FileNotFound => BR_Failed 404 end 405 fun mosml_build_command hm_env extra {noecho, ignore_error, command = c} deps= 406 let 407 open Holmake_types 408 val isHolmosmlcc = 409 String.isPrefix (perform_substitution hm_env [VREF "HOLMOSMLC-C"]) c 410 val isHolmosmlc = 411 String.isPrefix (perform_substitution hm_env [VREF "HOLMOSMLC"]) c 412 val isMosmlc = 413 String.isPrefix (perform_substitution hm_env [VREF "MOSMLC"]) c 414 val {diag,...} = outs 415 val diag = diag "mosml_build" 416 in 417 if isHolmosmlcc orelse isHolmosmlc orelse isMosmlc then let 418 val _ = diag (fn _ => "Processing mosml build command: "^c) 419 in 420 case process_mosml_args outs (if isHolmosmlcc then " -c " ^ c else c) of 421 (Mosml_compile (objs, src), I) => 422 SOME (poly_compile warn diag (noecho orelse quiet_flag) 423 (toFile src) 424 I 425 deps 426 objs) 427 | (Mosml_link (result, objs), I) => 428 let 429 in 430 diag (fn _ => "Moscow ML command is link -o "^result^" ["^ 431 String.concatWith ", " objs ^ "]"); 432 SOME (poly_link (noecho orelse quiet_flag) extra result 433 (map OS.Path.base objs)) 434 end 435 | (Mosml_error, _) => 436 (warn ("*** Couldn't interpret Moscow ML command: "^c); 437 SOME (OS.Process.failure)) 438 end 439 else NONE 440 end 441 val jobs = #jobs (#core optv) 442 open HM_DepGraph 443 fun pr s = s 444 fun interpret_graph (g,ok) = 445 (if ok then OS.Process.success else OS.Process.failure, g) 446 fun interpret_bres bres = 447 case bres of 448 BR_OK => true 449 | BR_ClineK{cline = (_,cl), job_kont = k, ...} => 450 k warn (Systeml.systeml cl) 451 | BR_Failed => false 452 453 454 fun system s = 455 Systeml.system_ps 456 (if relocbuild then Systeml.build_after_reloc_envvar ^ "=1 " ^ s 457 else s) 458 459 val build_graph = 460 if jobs = 1 then 461 (fn g => 462 graphbuildj1 { 463 build_command = (fn g => fn ii => fn cmds => fn f => 464 build_command g ii cmds f |> interpret_bres), 465 mosml_build_command = mosml_build_command, 466 outs = outs, 467 keep_going = keep_going, 468 quiet = quiet_flag, 469 hmenv = hmenv, 470 system = system } g) 471 else 472 (fn g => 473 multibuild.graphbuild { build_command = build_command, 474 relocbuild = relocbuild, 475 mosml_build_command = mosml_build_command, 476 warn = warn, tgtfatal = tgtfatal, 477 keep_going = keep_going, 478 diag = 479 (fn s => diag "multibuild" (fn _ => s)), 480 info = #info outs, 481 time_limit = time_limit, 482 quiet = quiet_flag, hmenv = hmenv, 483 jobs = jobs } g |> interpret_graph) 484in 485 {extra_impl_deps = [], 486 build_graph = build_graph} 487end 488 489end (* struct *) 490