1(*--------------------------------------------------------------------------- 2 An ML script for building HOL 3 ---------------------------------------------------------------------------*) 4 5structure build = 6struct 7 8structure Process = OS.Process 9 10(* utilities *) 11 12(* ---------------------------------------------------------------------- 13 Magic to ensure that interruptions (SIGINTs) are actually seen by the 14 linked executable as Interrupt exceptions 15 ---------------------------------------------------------------------- *) 16 17prim_val catch_interrupt : bool -> unit = 1 "sys_catch_break"; 18val _ = catch_interrupt true; 19 20open buildutils 21val _ = startup_check() 22 23(* ---------------------------------------------------------------------- 24 Analysing the command-line 25 ---------------------------------------------------------------------- *) 26 27val cline_record = process_cline () 28val {cmdline,build_theory_graph,selftest_level,...} = cline_record 29val {extra={SRCDIRS},jobcount,relocbuild,debug,...} = cline_record 30 31 32open Systeml; 33 34val Holmake = let 35 fun sysl p args = Systeml.systeml (p::args) 36 val isSuccess = OS.Process.isSuccess 37in 38 buildutils.Holmake sysl isSuccess 39 (fn () => ["-j"^Int.toString jobcount] @ 40 (if debug then ["--dbg"] else [])) 41 (fn _ => "") 42 selftest_level 43end 44 45(* ---------------------------------------------------------------------- 46 Some useful file-system utility functions 47 ---------------------------------------------------------------------- *) 48 49(* create a symbolic link - Unix only *) 50fun link b s1 s2 = 51 let open Process 52 in if SYSTEML ["ln", "-s", s1, s2] then () 53 else die ("Unable to link file "^quote s1^" to file "^quote s2^".") 54 end 55 56fun symlink_check() = 57 if OS = "winNT" then 58 die "Sorry; symbolic linking isn't available under Windows NT" 59 else link 60val default_link = if OS = "winNT" then cp else link 61 62fun mem x [] = false 63 | mem x (y::ys) = x = y orelse mem x ys 64 65fun exns_link exns b s1 s2 = 66 if mem (OS.Path.file s1) exns then () else default_link b s1 s2 67 68(*--------------------------------------------------------------------------- 69 Transport a compiled directory to another location. The 70 symlink argument says whether this is via a symbolic link, 71 or by copying. The ".uo", ".ui", ".so", ".xable" and ".sig" 72 files are transported. 73 ---------------------------------------------------------------------------*) 74 75fun upload ((src, regulardir), target, symlink) = 76 if regulardir = 0 then 77 (print ("Uploading files to "^target^"\n"); 78 map_dir (transfer_file symlink target) src) 79 handle OS.SysErr(s, erropt) => 80 die ("OS error: "^s^" - "^ 81 (case erropt of SOME s' => OS.errorMsg s' 82 | _ => "")) 83 else if selftest_level >= regulardir then 84 print ("Self-test directory "^src^" built successfully.\n") 85 else () 86 87(*--------------------------------------------------------------------------- 88 For each element in SRCDIRS, build it, then upload it to SIGOBJ. 89 This allows us to have the build process only occur w.r.t. SIGOBJ 90 (thus requiring only a single place to look for things). 91 ---------------------------------------------------------------------------*) 92 93fun buildDir symlink s = 94 (build_dir Holmake selftest_level s; upload(s,SIGOBJ,symlink)); 95 96fun build_src symlink = List.app (buildDir symlink) SRCDIRS 97 98fun upload_holmake_files symlink = 99 upload ((fullPath[HOLDIR, "tools", "Holmake"], 0), SIGOBJ, symlink) 100 101val holmake_exns = [ 102 "Systeml.sig", "Systeml.ui", "Systeml.uo" 103] 104 105 106fun build_hol symlink = let 107in 108 clean_sigobj(); 109 setup_logfile(); 110 upload_holmake_files (exns_link holmake_exns); 111 build_src symlink 112 handle Interrupt => (finish_logging false; die "Interrupted"); 113 finish_logging true; 114 make_buildstamp(); 115 build_help build_theory_graph; 116 print "\nHol built successfully.\n" 117end 118 119 120(*--------------------------------------------------------------------------- 121 Get rid of compiled code and dependency information. 122 ---------------------------------------------------------------------------*) 123 124val check_againstB = check_against EXECUTABLE 125val _ = check_againstB "tools/smart-configure.sml" 126val _ = check_againstB "tools/configure.sml" 127val _ = check_againstB "tools/build.sml" 128val _ = check_againstB "tools/Holmake/Systeml.sig" 129val _ = check_againstB "tools/configure-mosml.sml" 130 131val _ = let 132 val fP = fullPath 133 open OS.FileSys 134 val hmake = fP [HOLDIR,"bin",xable_string "Holmake"] 135in 136 if access(hmake, [A_READ, A_EXEC]) then 137 app_sml_files (check_against hmake) 138 {dirname = fP [HOLDIR, "tools", "Holmake"]} 139 else 140 die ("No Holmake executable in " ^ fP [HOLDIR, "bin"]) 141end 142 143 144val _ = 145 case cmdline of 146 [] => build_hol default_link 147 | _ => die "Not implemented yet" 148 149end (* struct *) 150