1(*--------------------------------------------------------------------------- 2 An ML script for building HOL 3 ---------------------------------------------------------------------------*) 4 5structure build = 6struct 7 8open buildutils 9datatype phase = Initial | Bare | Full 10 11(* utilities *) 12 13 fun main () = let 14 15 val _ = startup_check() 16 val phase = ref Initial 17 18 19 open buildutils 20 21(* ---------------------------------------------------------------------- 22 Analysing the command-line 23 ---------------------------------------------------------------------- *) 24 25val cline_record = process_cline () 26val {cmdline,build_theory_graph,selftest_level,...} = cline_record 27val {debug,jobcount,relocbuild,extra={SRCDIRS,...},...} = cline_record 28val {multithread,...} = cline_record 29 30open Systeml; 31 32fun phase_extras () = 33 case !phase of 34 Initial => ["--poly_not_hol"] 35 | Bare => ["--holstate", fullPath [HOLDIR, "bin", "hol.state0"]] 36 | Full => [] 37 38fun aug_systeml proc args = let 39 open Posix.Process 40 val env' = 41 "SELFTESTLEVEL="^Int.toString selftest_level :: Posix.ProcEnv.environ() 42in 43 case fork() of 44 NONE => (exece(proc,proc::args,env') 45 handle _ => die ("Exece of "^proc^" failed")) 46 | SOME cpid => let 47 val (_, result) = waitpid(W_CHILD cpid, []) 48 in 49 result 50 end 51end 52 53 54val Holmake = let 55 fun isSuccess Posix.Process.W_EXITED = true 56 | isSuccess _ = false 57 fun analysis hmstatus = let 58 open Posix.Process 59 in 60 case hmstatus of 61 W_EXITSTATUS w8 => "exited with code "^Word8.toString w8 62 | W_EXITED => "exited normally???" 63 | W_SIGNALED sg => "with signal " ^ 64 SysWord.toString (Posix.Signal.toWord sg) 65 | W_STOPPED sg => "stopped with signal " ^ 66 SysWord.toString (Posix.Signal.toWord sg) 67 end 68in 69 buildutils.Holmake aug_systeml isSuccess 70 (fn () => ("-j"^Int.toString jobcount) :: 71 ((if relocbuild then ["--relocbuild"] else []) @ 72 (if debug then ["--dbg"] else []) @ 73 (case multithread of 74 NONE => [] 75 | SOME i => ["--mt="^Int.toString i]) @ 76 phase_extras())) 77 analysis selftest_level 78end 79 80(* create a symbolic link - Unix only *) 81fun link b s1 s2 = 82 Posix.FileSys.symlink {new = s2, old = s1} 83 handle OS.SysErr (s, _) => 84 die ("Unable to link old file "^quote s1^" to new file " 85 ^quote s2^": "^s) 86 87fun symlink_check() = 88 if OS = "winNT" then 89 die "Sorry; symbolic linking isn't available under Windows NT" 90 else link 91val default_link = if OS = "winNT" then cp else link 92 93(*--------------------------------------------------------------------------- 94 Transport a compiled directory to another location. The 95 symlink argument says whether this is via a symbolic link, 96 or by copying. The ".uo", ".ui", ".so", ".xable" and ".sig" 97 files are transported. 98 ---------------------------------------------------------------------------*) 99 100fun upload ((src, regulardir), target, symlink) = 101 if regulardir = 0 then 102 (print ("Uploading files to "^target^"\n"); 103 map_dir (transfer_file symlink target) src) 104 handle OS.SysErr(s, erropt) => 105 die ("OS error: "^s^" - "^ 106 (case erropt of SOME s' => OS.errorMsg s' 107 | _ => "")) 108 else if selftest_level >= regulardir then 109 print ("Self-test directory "^src^" built successfully.\n") 110 else () 111 112(*--------------------------------------------------------------------------- 113 For each element in SRCDIRS, build it, then upload it to SIGOBJ. 114 This allows us to have the build process only occur w.r.t. SIGOBJ 115 (thus requiring only a single place to look for things). 116 ---------------------------------------------------------------------------*) 117 118fun buildDir symlink s = 119 if #1 s = fullPath [HOLDIR, "bin/hol.bare"] then phase := Bare 120 else if #1 s = fullPath [HOLDIR, "bin/hol"] then phase := Full 121 else 122 (build_dir Holmake selftest_level s; upload(s,SIGOBJ,symlink)) 123 124fun build_src symlink = List.app (buildDir symlink) SRCDIRS 125 126fun build_hol symlink = let 127in 128 clean_sigobj(); 129 setup_logfile(); 130 build_src symlink 131 handle SML90.Interrupt => (finish_logging false; die "Interrupted"); 132 finish_logging true; 133 make_buildstamp(); 134 build_help build_theory_graph; 135 print "\nHol built successfully.\n" 136end 137 138 139(*--------------------------------------------------------------------------- 140 Get rid of compiled code and dependency information. 141 ---------------------------------------------------------------------------*) 142 143val check_againstB = check_against EXECUTABLE 144val _ = check_againstB "tools-poly/smart-configure.sml" 145val _ = check_againstB "tools-poly/configure.sml" 146val _ = check_againstB "tools-poly/build.sml" 147val _ = check_againstB "tools/Holmake/Systeml.sig" 148 149val _ = let 150 val fP = fullPath 151 open OS.FileSys 152 val hmake = fP [HOLDIR,"bin",xable_string "Holmake"] 153in 154 if access(hmake, [A_READ, A_EXEC]) then 155 (app_sml_files (check_against hmake) 156 {dirname = fP [HOLDIR, "tools-poly", "Holmake"]}; 157 app_sml_files (check_against hmake) 158 {dirname = fP [HOLDIR, "tools", "Holmake"]}) 159 else 160 die ("No Holmake executable in " ^ fP [HOLDIR, "bin"]) 161end 162 163 164 165 166 167in 168 case cmdline of 169 [] => build_hol default_link 170 | _ => die "Multi-dir build not implemented yet" 171 172 end 173end (* struct *) 174