1structure buildutils :> buildutils = 2struct 3 4structure Path = OS.Path 5structure FileSys = OS.FileSys 6structure Process = OS.Process 7 8 9infix |> 10fun x |> f = f x 11 12(* path manipulation functions *) 13fun normPath s = Path.toString(Path.fromString s) 14fun itstrings f [] = raise Fail "itstrings: empty list" 15 | itstrings f [x] = x 16 | itstrings f (h::t) = f h (itstrings f t); 17fun fullPath slist = normPath 18 (itstrings (fn chunk => fn path => Path.concat (chunk,path)) slist); 19 20fun quote s = String.concat["\"", s, "\""]; 21 22fun safedelete s = FileSys.remove s handle OS.SysErr _ => () 23 24(* message emission *) 25fun die s = 26 let open TextIO 27 in 28 output(stdErr, s ^ "\n"); 29 flushOut stdErr; 30 Process.exit Process.failure 31 end 32fun warn s = 33 let open TextIO in output(stdErr, "*** " ^ s ^ "\n"); flushOut stdErr end; 34fun I x = x 35 36 37fun startup_check () = 38 let 39 val me = Systeml.find_my_path() 40 in 41 case Holmake_tools.check_distrib "build" of 42 NONE => () 43 | SOME whereami => 44 if whereami = me then () 45 else die "*** Don't run this instance of build in a foreign HOL directory" 46 end 47 48(* values from the Systeml structure, which is created at HOL configuration 49 time *) 50val OS = Systeml.OS; 51val HOLDIR = Systeml.HOLDIR 52val EXECUTABLE = Systeml.xable_string (fullPath [HOLDIR, "bin", "build"]) 53val DEPDIR = Systeml.DEPDIR 54val GNUMAKE = Systeml.GNUMAKE 55val DYNLIB = Systeml.DYNLIB 56 57fun SYSTEML clist = Process.isSuccess (Systeml.systeml clist) 58 59val dfltbuildseq = fullPath [HOLDIR, "tools", "build-sequence"] 60val dfltjobnum = 4 61 62val help_header = let 63 val istrm = TextIO.openIn (fullPath [HOLDIR, "tools", "buildhelp.txt"]) 64in 65 TextIO.inputAll istrm before TextIO.closeIn istrm 66end handle IO.Io _ => "\n\n<Build help file missing in action>\n\n" 67 68fun exit_with_help() = 69 (print (GetOpt.usageInfo {header = help_header, 70 options = buildcline.cline_opt_descrs}); 71 Process.exit Process.success) 72 73fun read_buildsequence {kernelname} bseq_fname = let 74 val kernelpath = fullPath [HOLDIR, "src", 75 case kernelname of 76 "stdknl" => "0" 77 | "expk" => "experimental-kernel" 78 | "otknl" => "0" 79 | _ => die ("Bad kernelname: "^kernelname) 80 ] 81 val readline = TextIO.inputLine 82 fun read_file acc visitedincludes (f as (fstr,fname)) oldstreams = 83 case readline fstr of 84 NONE => 85 let 86 val _ = TextIO.closeIn fstr 87 in 88 case oldstreams of 89 h::t => read_file acc visitedincludes h t 90 | [] => List.rev acc 91 end 92 | SOME s => let 93 (* drop trailing and leading whitespace *) 94 val ss = Substring.full s 95 val ss = Substring.dropl Char.isSpace ss 96 val ss = Substring.dropr Char.isSpace ss 97 98 (* drop trailing comment *) 99 val (hashpfx, hashsfx) = Substring.position "#" ss 100 fun skip() = read_file acc visitedincludes f oldstreams 101 in 102 if Substring.size hashpfx = 0 then 103 if Substring.isPrefix "#include " hashsfx then 104 let 105 val includefname = 106 Substring.string 107 (Substring.slice(hashsfx, size "#include ", NONE)) 108 val includefname_opt = 109 SOME (OS.Path.mkAbsolute 110 { path = includefname, 111 relativeTo = fullPath [HOLDIR, "tools"]}) 112 handle OS.Path.Path => NONE 113 in 114 case includefname_opt of 115 NONE => (warn ("Ignoring bad #include: " ^ includefname); 116 skip()) 117 | SOME includefname => 118 let 119 val includefname = OS.Path.mkCanonical includefname 120 (* necessary if user specified a non-canonical absolute 121 path *) 122 in 123 if Binaryset.member(visitedincludes, includefname) then 124 die ("Recursive request to #include "^ 125 includefname ^ "(in "^fname^")") 126 else let 127 val newstr_opt = SOME (TextIO.openIn includefname) 128 handle IO.Io _ => NONE 129 in 130 case newstr_opt of 131 SOME strm => 132 read_file acc 133 (Binaryset.add(visitedincludes, 134 includefname)) 135 (strm,includefname) 136 ((fstr,fname)::oldstreams) 137 | NONE => die ("Couldn't open #include-d file "^ 138 includefname ^ 139 "(included from "^fname^")") 140 end 141 end 142 end 143 else skip() 144 else 145 let 146 val s = Substring.string hashpfx 147 fun extract_testcount (s,acc) = 148 if String.sub(s,0) = #"!" then 149 extract_testcount (String.extract(s,1,NONE), acc+1) 150 else (s,acc) 151 fun extract_brackets name l r s = 152 if String.sub(s,0) = l then let 153 fun grabsys i = 154 if String.sub(s,i) = r then 155 (String.substring(s,1,i-1), 156 String.extract(s,i+1,NONE)) 157 else grabsys (i + 1) 158 in 159 grabsys 1 160 handle Subscript => 161 die ("Malformed "^name^" spec: "^s^ 162 " (from "^fname^")") 163 end 164 else ("", s) 165 val extract_mlsys = extract_brackets "system" #"[" #"]" 166 val extract_kernel = extract_brackets "kernel" #"(" #")" 167 val (mlsys,s) = extract_mlsys s 168 val (knl,s) = extract_kernel s 169 val (dirname0,testcount) = extract_testcount (s,0) 170 val dirname = 171 if dirname0 = "**KERNEL**" then kernelpath 172 else if Path.isAbsolute dirname0 then dirname0 173 else fullPath [HOLDIR, dirname0] 174 open FileSys 175 in 176 if (mlsys = "" orelse mlsys = Systeml.ML_SYSNAME) andalso 177 (knl = "" orelse knl = kernelname) then 178 if access (dirname, [A_READ, A_EXEC]) then 179 if isDir dirname orelse mlsys <> "" then 180 read_file ((dirname,testcount)::acc) 181 visitedincludes 182 f 183 oldstreams 184 else 185 die ("** File "^dirname0^ 186 " from build sequence file "^fname^ 187 " is not a directory") 188 else die ("** File "^s^" from build sequence file "^fname^ 189 " does not \ 190 \exist or is inacessible") 191 else read_file acc visitedincludes f oldstreams 192 end 193 end 194 val bseq_file = 195 TextIO.openIn bseq_fname 196 handle IO.Io _ => die ("Fatal error: couldn't open sequence file: "^ 197 bseq_fname) 198in 199 read_file [] (Binaryset.empty String.compare) (bseq_file,bseq_fname) [] 200end 201 202val option_filename = fullPath [HOLDIR, "tools", "lastbuildoptions"] 203 204fun read_earlier_options reader = let 205 val istrm = TextIO.openIn option_filename 206 fun recurse acc = 207 case reader istrm of 208 NONE => List.rev acc 209 | SOME s => recurse (String.substring(s,0,size s - 1)::acc) 210in 211 recurse [] before TextIO.closeIn istrm 212end handle IO.Io _ => [] 213 214fun write_options args = let 215 val ostrm = TextIO.openOut option_filename 216in 217 List.app (fn s => TextIO.output(ostrm, s ^ "\n")) args; 218 TextIO.closeOut ostrm 219end 220 221fun mem x xs = List.exists (fn y => x = y) xs 222fun delete x [] = [] 223 | delete x (h::t) = if x = h then delete x t else h::delete x t 224 225fun inter [] _ = [] 226 | inter (h::t) l = if mem h l then h :: inter t l else inter t l 227 228fun setdiff big small = 229 case small of 230 [] => big 231 | h::t => setdiff (delete h big) t 232 233 234 235fun findseq dflt numseen list = let 236 fun maybewarn () = 237 if numseen = 1 then 238 warn "Multiple build-sequence options; taking last one\n" 239 else () 240in 241 case list of 242 [] => NONE 243 | ["--seq"] => (warn "Trailing --seq option in last build info ignored"; 244 NONE) 245 | "--seq"::fname::t => let 246 val _ = maybewarn() 247 in 248 case findseq dflt (numseen + 1) t of 249 NONE => SOME fname 250 | v => v 251 end 252 | h :: t => findseq dflt numseen t 253end 254 255fun orlist slist = 256 case slist of 257 [] => "" 258 | [x] => x 259 | [x,y] => x ^ ", or " ^ y 260 | x::xs => x ^ ", " ^ orlist xs 261 262type ircd = {seqname:string,kernelspec:string} 263datatype cline_action = 264 Clean of string 265 | Normal of ircd buildcline_dtype.final_options 266exception DoClean of string 267 268fun write_kernelid s = 269 let 270 val strm = TextIO.openOut Holmake_tools.kernelid_fname 271 in 272 TextIO.output(strm, s ^ "\n"); 273 TextIO.closeOut strm 274 end handle IO.Io _ => die "Couldn't write kernelid to HOLDIR" 275 276fun apply_updates l t = 277 case l of 278 [] => t 279 | {update} :: rest => apply_updates rest (update (warn, t)) 280 281fun get_cline () = let 282 open GetOpt 283 val oldopts = read_earlier_options TextIO.inputLine 284 val (opts, rest) = getOpt { argOrder = RequireOrder, 285 options = buildcline.cline_opt_descrs, 286 errFn = die } (CommandLine.arguments()) 287 val option_record = apply_updates opts buildcline.initial 288 val _ = if #help option_record then exit_with_help() else () 289 val _ = 290 if mem "cleanAll" rest then raise DoClean "cleanAll" 291 else if mem "clean" rest then raise DoClean "clean" 292 else if mem "cleanForReloc" rest then raise DoClean "cleanForReloc" 293 else () 294 val seqspec = 295 case #seqname option_record of 296 NONE => 297 let 298 in 299 case findseq dfltbuildseq 0 oldopts of 300 NONE => dfltbuildseq 301 | SOME f => 302 if f = dfltbuildseq then f 303 else (warn ("Using build-sequence file "^f^ 304 " from earlier build command; \n\ 305 \ use -F option to override"); 306 f) 307 end 308 | SOME f => if f = "" then dfltbuildseq else f 309 val knlspec = 310 case #kernelspec option_record of 311 SOME s => String.extract(s,2,NONE) 312 | NONE => 313 (case 314 List.find (fn s => mem s ["--expk", "--otknl", "--stdknl"])oldopts 315 of 316 NONE => "stdknl" 317 | SOME s => 318 (warn ("Using kernel spec "^s^ " from earlier build command;\n\ 319 \ use one of --expk, --stdknl, --otknl to override"); 320 String.extract(s,2,NONE))) 321 val _ = write_kernelid knlspec 322 val buildgraph = 323 case #build_theory_graph option_record of 324 NONE => 325 (case List.find (fn s => s = "--graph" orelse s = "--nograph") oldopts 326 of 327 NONE => true 328 | SOME "--graph" => 329 (warn "Using --graph option from earlier build; \ 330 \use --nograph to override"; true) 331 | SOME "--nograph" => 332 (warn "Using --nograph option from earlier build; \ 333 \use --graph to override"; false) 334 | SOME _ => raise Fail "Really can't happen") 335 | SOME b => b 336 val bgoption = if buildgraph then [] else ["--nograph"] 337 val jcount = 338 case #jobcount option_record of 339 NONE => 340 (case List.find (fn s => String.isPrefix "-j" s) oldopts of 341 NONE => dfltjobnum 342 | SOME jns => 343 (case Int.fromString (String.extract(jns, 2, NONE)) of 344 NONE => (warn "Bogus -j spec in old build options file"; 345 dfltjobnum) 346 | SOME jn => if jn = dfltjobnum then jn 347 else (warn ("Using -j "^Int.toString jn^ 348 " from earlier build command; \ 349 \use -j to override"); 350 jn))) 351 | SOME jn => jn 352 val joption = "-j" ^ Int.toString jcount 353 val _ = 354 if seqspec = dfltbuildseq then 355 write_options ("--"^knlspec::joption::bgoption) 356 else 357 write_options ("--"^knlspec::"--seq"::seqspec::joption::bgoption) 358in 359 Normal {build_theory_graph = buildgraph, 360 cmdline = rest, 361 debug = #debug option_record, 362 selftest_level = case #selftest option_record of 363 NONE => 0 364 | SOME i => i, 365 extra = {seqname = seqspec, kernelspec = knlspec}, 366 jobcount = jcount, 367 multithread = #multithread option_record, 368 relocbuild = #relocbuild option_record} 369end handle DoClean s => (Clean s before safedelete Holmake_tools.kernelid_fname) 370 371(* ---------------------------------------------------------------------- 372 Some useful file-system utility functions 373 ---------------------------------------------------------------------- *) 374 375(* map a function over the files in a directory *) 376fun map_dir f dir = 377 let val dstrm = OS.FileSys.openDir dir 378 fun loop () = 379 case OS.FileSys.readDir dstrm 380 of NONE => [] 381 | SOME file => (dir,file)::loop() 382 val files = loop() 383 val _ = OS.FileSys.closeDir dstrm 384 in List.app f files 385 handle OS.SysErr(s, erropt) 386 => die ("OS error: "^s^" - "^ 387 (case erropt of SOME s' => OS.errorMsg s' | _ => "")) 388 | otherexn => die ("map_dir: "^General.exnMessage otherexn) 389 end; 390 391fun rem_file f = 392 OS.FileSys.remove f 393 handle _ => (warn ("Couldn't remove file "^f); ()); 394 395fun copy file path = (* Dead simple file copy *) 396 let open TextIO 397 val (istrm,ostrm) = (openIn file, openOut path) 398 fun loop() = 399 case input1 istrm 400 of SOME ch => (output1(ostrm,ch) ; loop()) 401 | NONE => (closeIn istrm; flushOut ostrm; closeOut ostrm) 402 in loop() 403 end; 404 405fun bincopy file path = (* Dead simple file copy - binary version *) 406 let open BinIO 407 val (istrm,ostrm) = (openIn file, openOut path) 408 fun loop() = 409 case input1 istrm 410 of SOME ch => (output1(ostrm,ch) ; loop()) 411 | NONE => (closeIn istrm; flushOut ostrm; closeOut ostrm) 412 in loop() 413 end; 414 415(* f is either bincopy or copy *) 416fun update_copy f src dest = let 417 val t0 = OS.FileSys.modTime src 418in 419 f src dest; 420 OS.FileSys.setTime(dest, SOME t0) 421end 422 423fun cp b = if b then update_copy bincopy else update_copy copy 424 425fun mv0 s1 s2 = let 426 val s1' = normPath s1 427 val s2' = normPath s2 428in 429 FileSys.rename{old=s1', new=s2'} 430end 431 432fun mv b = if b then mv0 else cp b 433 434fun moveTo dir action = let 435 val here = OS.FileSys.getDir() 436 val b = (OS.FileSys.chDir dir; true) handle _ => false 437 fun normalise s = OS.Path.mkAbsolute {path = s, relativeTo = dir} 438in 439 if b then (map normalise (action ()) before OS.FileSys.chDir here) 440 handle e => (OS.FileSys.chDir here; raise e) 441 else [] 442end 443 444fun hmakefile_data HOLDIR = 445 if OS.FileSys.access ("Holmakefile", [OS.FileSys.A_READ]) then let 446 open Holmake_types 447 val (env, _, _) = ReadHMF.read "Holmakefile" (base_environment()) 448 fun envlist id = 449 map dequote (tokenize (perform_substitution env [VREF id])) 450 in 451 {includes = envlist "PRE_INCLUDES" @ envlist "INCLUDES", 452 extra_cleans = envlist "EXTRA_CLEANS", 453 holheap = case envlist "HOLHEAP" of 454 [x] => SOME x 455 | _ => NONE} 456 end 457 else {includes = [], extra_cleans = [], holheap = NONE} 458 459fun clean0 HOLDIR = let 460 val {includes,extra_cleans,...} = hmakefile_data HOLDIR 461in 462 Holmake_tools.clean_dir {extra_cleans = extra_cleans} ; 463 includes 464end 465 466fun cleanAll0 HOLDIR = let 467 val {includes,extra_cleans,...} = hmakefile_data HOLDIR 468in 469 Holmake_tools.clean_dir {extra_cleans = extra_cleans}; 470 Holmake_tools.clean_depdir {depdirname = ".HOLMK"}; 471 Holmake_tools.clean_depdir {depdirname = ".hollogs"}; 472 includes 473end 474 475fun cleanForReloc0 HOLDIR = 476 let 477 val {includes,holheap,...} = hmakefile_data HOLDIR 478 in 479 Holmake_tools.clean_forReloc {holheap = holheap}; 480 Holmake_tools.clean_depdir {depdirname = ".HOLMK"}; 481 Holmake_tools.clean_depdir {depdirname = ".hollogs"}; 482 includes 483 end 484 485 486fun clean HOLDIR dirname = moveTo dirname (fn () => clean0 HOLDIR) 487fun cleanAll HOLDIR dirname = moveTo dirname (fn () => cleanAll0 HOLDIR) 488fun cleanForReloc HOLDIR dirname = 489 moveTo dirname (fn () => cleanForReloc0 HOLDIR) 490 491fun clean_dirs {HOLDIR,action} dirs = let 492 val seen = Binaryset.empty String.compare 493 fun recurse sofar todo = 494 case todo of 495 [] => () 496 | d::ds => let 497 in 498 if Binaryset.member(sofar, d) then recurse sofar ds 499 else let 500 val newincludes = action HOLDIR d 501 in 502 recurse (Binaryset.add(sofar,d)) (newincludes @ ds) 503 end 504 end 505in 506 recurse seen dirs 507end 508 509(* ---------------------------------------------------------------------- 510 In clean_sigobj, we need to avoid removing the systeml stuff that 511 will have been put into sigobj by the action of configure.sml 512 ---------------------------------------------------------------------- *) 513 514fun equal x y = (x=y); 515val SIGOBJ = fullPath [HOLDIR, "sigobj"]; 516 517fun clean_sigobj() = let 518 open Systeml 519 val _ = print ("Cleaning out "^SIGOBJ^"\n") 520 val lowcase = String.map Char.toLower 521 val sigobj_extras = 522 if ML_SYSNAME = "mosml" then ["basis2002"] else [] 523 fun sigobj_rem_file s = let 524 val f = Path.file s 525 val n = lowcase (hd (String.fields (equal #".") f)) 526 in 527 if mem n (["systeml", "readme"] @ sigobj_extras) then () 528 else rem_file s 529 end 530 val toolsuffix = if ML_SYSNAME = "poly" then "-poly" else "" 531 fun write_initial_srcfiles () = let 532 open TextIO 533 val outstr = openOut (fullPath [HOLDIR,"sigobj","SRCFILES"]) 534 in 535 output(outstr, 536 fullPath [HOLDIR, "tools" ^ toolsuffix, "Holmake", "Systeml"]); 537 output(outstr, "\n"); 538 closeOut(outstr) 539 end 540in 541 map_dir (sigobj_rem_file o normPath o OS.Path.concat) SIGOBJ; 542 write_initial_srcfiles (); 543 print (SIGOBJ ^ " cleaned\n") 544end; 545 546val EXECUTABLE = Systeml.xable_string (fullPath [HOLDIR, "bin", "build"]) 547 548fun full_clean (SRCDIRS:(string*int) list) f = 549 clean_sigobj() before 550 (* clean all kernel directories, regardless of which was actually built, 551 the help src directory too, and all the src directories, including 552 those with ! annotations *) 553 clean_dirs {HOLDIR=HOLDIR, action = f} 554 (fullPath [HOLDIR, "help", "src-sml"] :: 555 fullPath [HOLDIR, "src", "0"] :: 556 fullPath [HOLDIR, "src", "experimental-kernel"] :: 557 fullPath [HOLDIR, "src", "logging-kernel"] :: 558 map #1 SRCDIRS) 559 560fun app_sml_files f {dirname} = 561 let 562 open OS.FileSys OS.Path 563 val dstrm = openDir dirname 564 fun recurse () = 565 case readDir dstrm of 566 NONE => closeDir dstrm 567 | SOME p => ((case ext p of 568 SOME "sml" => f (concat(dirname,p)) 569 | SOME "sig" => f (concat(dirname,p)) 570 | _ => ()); 571 recurse()) 572 in 573 recurse () 574 end 575 576fun check_against executable s = let 577 open Time 578 val p = if OS.Path.isRelative s then fullPath [HOLDIR, s] 579 else s 580 val cfgtime = FileSys.modTime p 581in 582 if FileSys.modTime executable < cfgtime then 583 (warn ("WARNING! WARNING!"); 584 warn (" The executable "^executable^" is older than " ^ s ^ ";"); 585 warn (" this suggests you should reconfigure the system."); 586 warn (" Press Ctl-C now to abort the build; <RETURN> to continue."); 587 warn ("WARNING! WARNING!"); 588 if Systeml.POLY_VERSION = 551 orelse Systeml.POLY_VERSION = 552 then 589 ignore(TextIO.inputLine TextIO.stdIn) 590 (* see PolyML bug report at 591 https://www.mail-archive.com/polyml@inf.ed.ac.uk/msg00982.html *) 592 else (); 593 ignore (TextIO.inputLine TextIO.stdIn)) 594 else () 595end handle OS.SysErr _ => die ("File "^s^" has disappeared."); 596 597 598(* uploadfn is of type : bool -> string -> string -> unit 599 the boolean is whether or not the arguments are binary files 600 the strings are source and destination file-names, in that order 601*) 602fun transfer_file uploadfn targetdir (df as (dir,file)) = let 603 fun transfer binaryp (dir,file1,file2) = 604 uploadfn binaryp (fullPath [dir,file1]) (fullPath [targetdir,file2]) 605 fun idtransfer binaryp (dir,file) = 606 case Path.base file of 607 "selftest" => () 608 | _ => transfer binaryp (dir,file,file) 609 fun digest_sig file = 610 let val b = Path.base file 611 in if (String.extract(b,String.size b -4,NONE) = "-sig" 612 handle _ => false) 613 then SOME (String.extract(b,0,SOME (String.size b - 4))) 614 else NONE 615 end 616 fun augmentSRCFILES file = let 617 open TextIO 618 val ostrm = openAppend (Path.concat(SIGOBJ,"SRCFILES")) 619 in 620 output(ostrm,fullPath[dir,file]^"\n") ; 621 closeOut ostrm 622 end 623 624in 625 case Path.ext file of 626 SOME"ui" => idtransfer true df 627 | SOME"uo" => idtransfer true df 628 | SOME"so" => idtransfer true df (* for dynlibs *) 629 | SOME"xable" => idtransfer true df (* for executables *) 630 | SOME"sig" => (idtransfer false df; augmentSRCFILES (Path.base file)) 631 | SOME"sml" => (case digest_sig file of 632 NONE => () 633 | SOME file' => 634 (transfer false (dir,file, file' ^".sig"); 635 augmentSRCFILES file')) 636 | _ => () 637end; 638 639fun Gnumake dir = 640 if SYSTEML [GNUMAKE] then true 641 else (warn ("Build failed in directory "^dir ^" ("^GNUMAKE^" failed)."); 642 false) 643 644exception BuildExit 645fun build_dir Holmake selftest_level (dir, regulardir) = let 646 val _ = if selftest_level >= regulardir then () 647 else raise BuildExit 648 val _ = OS.FileSys.chDir dir 649 val truncdir = if String.isPrefix HOLDIR dir then 650 String.extract(dir, size HOLDIR + 1, NONE) 651 (* +1 to drop directory slash after holdir *) 652 else dir 653 val now_d = Date.fromTimeLocal (Time.now()) 654 val now_s = Date.fmt "%d %b, %H:%M:%S" now_d 655 val bold = Holmake_tools.bold 656 val _ = print (bold ("Building directory "^truncdir^" ["^now_s^"]\n")) 657in 658 case #file(OS.Path.splitDirFile dir) of 659 "muddyC" => let 660 in 661 case OS of 662 "winNT" => bincopy (fullPath [HOLDIR, "tools", "win-binaries", 663 "muddy.so"]) 664 (fullPath [HOLDIR, "examples", "muddy", "muddyC", 665 "muddy.so"]) 666 | other => if not (Gnumake dir) then 667 print(String.concat 668 ["\nmuddyLib has NOT been built!! ", 669 "(continuing anyway).\n\n"]) 670 else () 671 end 672 | "minisat" => let 673 in case OS of 674 "winNT" => bincopy (fullPath [HOLDIR, "tools", "win-binaries", 675 "minisat.exe"]) 676 (fullPath [HOLDIR, "src","HolSat","sat_solvers", 677 "minisat", "DELTHISminisat.exe"]) 678 | other => if not (Gnumake dir) then 679 print(String.concat 680 ["\nMiniSat has NOT been built!! ", 681 "(continuing anyway).\n\n"]) 682 else () 683 end 684 | "zc2hs" => let 685 in case OS of 686 "winNT" => bincopy (fullPath [HOLDIR, "tools", "win-binaries", 687 "zc2hs.exe"]) 688 (fullPath [HOLDIR, "src","HolSat","sat_solvers","zc2hs", "zc2hs.exe"]) 689 | other => if not (Gnumake dir) then 690 print(String.concat 691 ["\nzc2hs has NOT been built!! ", 692 "(continuing anyway).\n\n"]) 693 else () 694 end 695 | _ => Holmake dir 696end 697handle OS.SysErr(s, erropt) => 698 die ("OS error: "^s^" - "^ 699 (case erropt of SOME s' => OS.errorMsg s' | _ => "")) 700 | BuildExit => () 701 702fun write_theory_graph () = 703 case Systeml.DOT_PATH of 704 SOME dotexec => 705 if not (FileSys.access (dotexec, [FileSys.A_EXEC])) then 706 (* of course, this will likely be the case on Windows *) 707 warn ("Can't see dot executable at "^dotexec^"; not generating \ 708 \theory-graph\n\ 709 \*** You can try reconfiguring and providing an explicit path \n\ 710 \*** (val DOT_PATH = \"....\") in\n\ 711 \*** tools-poly/poly-includes.ML (Poly/ML)\n\ 712 \*** or\n\ 713 \*** config-override (Moscow ML)\n\ 714 \***\n\ 715 \*** (Under Poly/ML you will have to delete bin/hol.state0 as \ 716 \well)\n***\n\ 717 \*** (Or: build with --nograph to stop this \ 718 \message from appearing again)\n") 719 else 720 let 721 val _ = print "Generating theory-graph and HTML theory signatures; \ 722 \this may take a while\n" 723 val _ = print " (Use build's --nograph option to skip this step.)\n" 724 val pfp = Systeml.protect o fullPath 725 val result = 726 OS.Process.system(pfp [HOLDIR, "bin", "hol"] ^ " < " ^ 727 pfp [HOLDIR, "help", "src-sml", "DOT"]) 728 in 729 if OS.Process.isSuccess result then () 730 else warn "Theory graph construction failed.\n" 731 end 732 | NONE => warn "If you had a copy of the dot tool installed, I might try\n\ 733 \*** to build a theory graph at this point" 734 735fun Poly_compilehelp() = let 736 open Systeml 737in 738 system_ps (fullPath [HOLDIR, "tools", "mllex", "mllex.exe"] ^ " Lexer.lex"); 739 system_ps (fullPath [HOLDIR, "tools", "mlyacc", "src", "mlyacc.exe"] ^ " Parser.grm"); 740 system_ps (POLYC ^ " poly-makebase.ML -o makebase.exe"); 741 system_ps (POLYC ^ " poly-Doc2Html.ML -o Doc2Html.exe"); 742 system_ps (POLYC ^ " poly-Doc2Txt.ML -o Doc2Txt.exe"); 743 system_ps (POLYC ^ " poly-Doc2Tex.ML -o Doc2Tex.exe") 744end 745 746val HOLMAKE = fullPath [HOLDIR, "bin/Holmake"] 747val ML_SYSNAME = Systeml.ML_SYSNAME 748 749fun mosml_compilehelp () = ignore (SYSTEML [HOLMAKE, "all"]) 750 751fun build_adoc_files () = let 752 val docdirs = let 753 val instr = TextIO.openIn(fullPath [HOLDIR, "tools", 754 "documentation-directories"]) 755 val wholefile = TextIO.inputAll instr before TextIO.closeIn instr 756 in 757 map normPath (String.tokens Char.isSpace wholefile) 758 end handle _ => (print "Couldn't read documentation directories file\n"; 759 []) 760 val doc2txt = fullPath [HOLDIR, "help", "src-sml", "Doc2Txt.exe"] 761 fun make_adocs dir = let 762 val fulldir = fullPath [HOLDIR, dir] 763 in 764 if SYSTEML [doc2txt, fulldir, fulldir] then true 765 else 766 (print ("Generation of ASCII doc files failed in directory "^dir^"\n"); 767 false) 768 end 769in 770 List.all make_adocs docdirs 771end 772 773fun build_help graph = 774 let val dir = OS.Path.concat(OS.Path.concat (HOLDIR,"help"),"src-sml") 775 val _ = OS.FileSys.chDir dir 776 777 (* builds the documentation tools called below *) 778 val _ = if ML_SYSNAME = "poly" then ignore (Poly_compilehelp()) 779 else if ML_SYSNAME = "mosml" then mosml_compilehelp() 780 else raise Fail "Bogus ML_SYSNAME" 781 782 val doc2html = fullPath [dir,"Doc2Html.exe"] 783 val docpath = fullPath [HOLDIR, "help", "Docfiles"] 784 val htmlpath = fullPath [docpath, "HTML"] 785 val _ = if (OS.FileSys.isDir htmlpath handle _ => false) then () 786 else (print ("Creating directory "^htmlpath^"\n"); 787 OS.FileSys.mkDir htmlpath) 788 val cmd1 = [doc2html, docpath, htmlpath] 789 val cmd2 = [fullPath [dir,"makebase.exe"]] 790 val _ = print "Generating ASCII versions of Docfiles...\n" 791 val _ = if build_adoc_files () then print "...ASCII Docfiles done\n" 792 else () 793 in 794 print "Generating HTML versions of Docfiles...\n" 795 ; 796 if SYSTEML cmd1 then print "...HTML Docfiles done\n" 797 else die "Couldn't make html versions of Docfiles" 798 ; 799 if (print "Building Help DB\n"; SYSTEML cmd2) then () 800 else die "Couldn't make help database" 801 ; 802 if graph then write_theory_graph() 803 else () 804 end 805 806fun cleanDirP P d = 807 let 808 val dstrm = OS.FileSys.openDir d 809 fun getPs acc = 810 case OS.FileSys.readDir dstrm of 811 NONE => (OS.FileSys.closeDir dstrm; acc) 812 | SOME f => if P f then getPs (f::acc) 813 else getPs acc 814 val Ps = getPs [] 815 in 816 List.app (fn s => safedelete (fullPath [d, s])) Ps 817 end 818 819 820 821fun delete_heaps() = let 822 val deletes = let 823 val istrm = TextIO.openIn 824 (fullPath[HOLDIR, "tools-poly", "rebuild-excludes.txt"]) 825 fun chop s = String.substring(s, 0, String.size s - 1) 826 fun recurse acc = 827 case TextIO.inputLine istrm of 828 NONE => (TextIO.closeIn istrm ; acc) 829 | SOME s => recurse (chop s::acc) 830 in 831 recurse [] 832 end 833 (* Holmake --relocbuild has already happened in all directories, so can 834 skip the implicit need to recurse into all directories and remove the 835 .HOLMK and .hollogs directories. *) 836 val cd = OS.FileSys.getDir() 837 val _ = OS.FileSys.chDir HOLDIR 838 fun process_dline s = 839 let 840 val fs = internal_functions.wildcard s 841 in 842 List.app safedelete fs 843 end 844in 845 List.app process_dline deletes ; 846 OS.FileSys.chDir cd 847end 848 849fun process_cline () = 850 case get_cline () of 851 Clean s => 852 let 853 val (per_dir_action, post_action) = 854 case s of 855 "cleanAll" => (cleanAll, fn () => ()) 856 | "clean" => (clean, fn () => ()) 857 | "cleanForReloc" => (cleanForReloc, delete_heaps) 858 | _ => die ("Clean action = "^s^"???") 859 val knlseq = fullPath [HOLDIR, "tools", "sequences", "kernel"] 860 val SRCDIRS = 861 let 862 fun add kspec seq s = 863 Binaryset.addList(s,read_buildsequence {kernelname = kspec} seq) 864 fun cmp ((s1,_),(s2,_)) = String.compare(s1,s2) 865 val alldirs = 866 Binaryset.empty cmp |> add "stdknl" dfltbuildseq 867 |> add "expk" knlseq 868 |> add "otknl" knlseq 869 in 870 Binaryset.listItems alldirs 871 end 872 in 873 full_clean SRCDIRS per_dir_action; 874 post_action(); 875 Process.exit Process.success 876 end 877 | Normal {extra = {seqname,kernelspec}, cmdline, multithread, 878 build_theory_graph, jobcount, relocbuild, debug, 879 selftest_level} => 880 let 881 val SRCDIRS = read_buildsequence {kernelname = kernelspec} seqname 882 in 883 if mem "help" cmdline then 884 (build_help build_theory_graph; 885 Process.exit Process.success) 886 else 887 {build_theory_graph=build_theory_graph, 888 cmdline=cmdline, 889 debug = debug, 890 extra = {SRCDIRS = SRCDIRS}, 891 jobcount = jobcount, 892 multithread = multithread, 893 relocbuild = relocbuild, 894 selftest_level = selftest_level 895 } 896 end 897 898fun make_buildstamp () = 899 let open Path TextIO 900 val stamp_filename = concat(HOLDIR, concat("tools","build-stamp")) 901 val stamp_stream = openOut stamp_filename 902 val date_string = Date.toString (Date.fromTimeLocal (Time.now())) 903 in 904 output(stamp_stream, "built "^date_string); 905 closeOut stamp_stream 906end 907 908val logdir = Systeml.build_log_dir 909val logfilename = Systeml.build_log_file 910val hostname = if Systeml.isUnix then 911 case Mosml.run "hostname" [] "" of 912 Mosml.Success s => String.substring(s,0,size s - 1) ^ "-" 913 (* substring to drop \n in output *) 914 | _ => "" 915 else "" (* what to do under windows? *) 916 917fun setup_logfile () = let 918 open OS.FileSys 919 fun ensure_dir () = 920 if access (logdir, []) then 921 isDir logdir 922 else (mkDir logdir; true) 923in 924 if ensure_dir() then 925 if access (logfilename, []) then 926 warn "Build log exists; new logging will concatenate onto this file" 927 else let 928 (* touch the file *) 929 val outs = TextIO.openOut logfilename 930 in 931 TextIO.closeOut outs 932 end 933 else warn "Couldn't make or use build-logs directory" 934end handle IO.Io _ => warn "Couldn't set up build-logs" 935 936fun finish_logging buildok = let 937in 938 if OS.FileSys.access(logfilename, []) then let 939 open Date 940 val timestamp = fmt "%Y-%m-%dT%H%M" (fromTimeLocal (Time.now())) 941 val newname0 = hostname^timestamp 942 val newname = (if buildok then "" else "bad-") ^ newname0 943 in 944 OS.FileSys.rename {old = logfilename, new = fullPath [logdir, newname]} 945 end 946 else () 947end handle IO.Io _ => warn "Had problems making permanent record of build log" 948 949fun Holmake sysl isSuccess extra_args analyse_failstatus selftest_level dir = let 950 val hmstatus = sysl HOLMAKE ("--qof" :: extra_args()) 951in 952 if isSuccess hmstatus then 953 if selftest_level > 0 andalso 954 OS.FileSys.access("selftest.exe", [OS.FileSys.A_EXEC]) 955 then 956 (print "Performing self-test...\n"; 957 if SYSTEML [dir ^ "/selftest.exe", Int.toString selftest_level] 958 then 959 print "Self-test was successful\n" 960 else 961 die ("Selftest failed in directory "^dir)) 962 else 963 () 964 else let 965 val info = analyse_failstatus hmstatus 966 in 967 die ("Build failed in directory "^dir^ 968 (if info <> "" then " ("^info^")" else "")) 969 end 970end 971 972val () = OS.Process.atExit (fn () => finish_logging false) 973 (* this will do nothing if finish_logging happened normally first; 974 otherwise the log's bad version will be recorded *) 975 976 977 978 979end (* struct *) 980