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 |> 10 11open HM_GraphBuildJ1 12 13val MOSMLDIR0 = Systeml.MOSMLDIR; 14 15fun variant str = (* get an unused file name in the current directory *) 16 if FileSys.access(str,[]) 17 then let fun vary i = 18 let val s = str^Int.toString i 19 in if FileSys.access(s,[]) then vary (i+1) else s 20 end 21 in vary 0 22 end 23 else str; 24 25fun includify [] = [] 26 | includify (h::t) = "-I" :: h :: includify t 27 28val SYSTEML = Systeml.systeml 29val UNQUOTER = xable_string(fullPath [HOLDIR, "bin/unquote"]) 30fun has_unquoter() = FileSys.access(UNQUOTER, [FileSys.A_EXEC]) 31fun unquote_to intp file1 file2 = 32 SYSTEML (UNQUOTER :: (if intp then ["-i"] else []) @ [file1, file2]) 33 34 35val failed_script_cache = ref (Binaryset.empty String.compare) 36 37fun make_build_command (buildinfo : HM_Cline.t buildinfo_t) = let 38 val {optv,actual_overlay,SIGOBJ,outs,hmenv,...} = buildinfo 39 val {warn,tgtfatal,info,chatty,diag,...} = outs 40 val debug = #debug (#core optv) 41 val allfast = #fast (#core optv) 42 val keep_going = #keep_going (#core optv) 43 val quit_on_failure = #quit_on_failure (#core optv) 44 val quiet_flag = #quiet (#core optv) 45 val interactive_flag = #interactive (#core optv) 46 val no_overlay = #no_overlay (#core optv) 47 val overlay_stringl = case actual_overlay of NONE => [] | SOME s => [s] 48 val MOSMLDIR = case #mosmldir optv of NONE => MOSMLDIR0 | SOME s => s 49 val MOSMLCOMP = fullPath [MOSMLDIR, "mosmlc"] 50 fun compile debug args = let 51 val _ = if isSome debug then 52 print (" with command "^ spacify(MOSMLCOMP::args)^"\n") 53 else () 54 in 55 SYSTEML (MOSMLCOMP::args) 56 end 57 fun build_command g (ii as {preincludes,includes}) c arg = let 58 val include_flags = includify (preincludes @ includes) 59 exception CompileFailed 60 exception FileNotFound 61 in 62 case c of 63 Compile _ (* deps *) => 64 let 65 val file = fromFile arg 66 val intp = case arg of SML (Script _) => true | _ => false 67 val _ = exists_readable file orelse 68 (print ("Wanted to compile "^file^", but it wasn't there\n"); 69 raise FileNotFound) 70 val _ = info ("Compiling "^file) 71 open Process 72 val res = 73 if has_unquoter() then let 74 (* force to always use unquoter if present, so as to generate 75 location pragmas. Must test for existence, for bootstrapping. 76 *) 77 val _ = diag "build_command" (fn _ => "Using unquoter") 78 val clone = variant file 79 val _ = FileSys.rename {old=file, new=clone} 80 fun revert() = 81 if FileSys.access (clone, [FileSys.A_READ]) then 82 ((if isSome debug then 83 FileSys.rename{old=file, new=file ^ ".quoted"} 84 else 85 FileSys.remove file) handle _ => (); 86 FileSys.rename{old=clone, new=file}) 87 else () 88 in 89 (if Process.isSuccess (unquote_to intp clone file) 90 handle e => (revert(); 91 print ("Unquoting "^file^ 92 " raised exception\n"); 93 raise CompileFailed) 94 then 95 compile debug ("-q"::(include_flags @ ["-c"] @ 96 overlay_stringl @ [file])) before 97 revert() 98 else (print ("Unquoting "^file^" ran and failed\n"); 99 revert(); 100 raise CompileFailed)) 101 handle CompileFailed => raise CompileFailed 102 | e => (revert(); 103 print("Unable to compile: "^file^ 104 " - raised exception "^exnName e^"\n"); 105 raise CompileFailed) 106 end 107 else 108 compile debug ("-q"::(include_flags@ ("-c"::(overlay_stringl @ 109 [file])))) 110 in 111 Process.isSuccess res 112 end 113 | BuildArticle _ => (print "Can't handle article building yet"; 114 false) 115 | ProcessArticle _ => (print "Can't handle article processing yet"; 116 false) 117 | BuildScript (s, deps, ex) => 118 let 119 val _ = not (Binaryset.member(!failed_script_cache, s)) orelse 120 (print ("Not re-running "^s^"Script; believe it will fail\n"); 121 raise CompileFailed) 122 val scriptsml_file = SML (Script s) 123 val scriptsml = fromFile scriptsml_file 124 val script = s^"Script" 125 val scriptuo = script^".uo" 126 val scriptui = script^".ui" 127 open Process 128 (* first thing to do is to create the Script.uo file *) 129 val b = build_command g ii (Compile (deps, ex)) scriptsml_file 130 val _ = b orelse raise CompileFailed 131 val _ = print ("Linking "^scriptuo^ 132 " to produce theory-builder executable\n") 133 val objectfiles0 = 134 if allfast then ["fastbuild.uo", scriptuo] 135 else if quit_on_failure then [scriptuo] 136 else ["holmakebuild.uo", scriptuo] 137 val objectfiles = 138 if interactive_flag then "holmake_interactive.uo" :: objectfiles0 139 else objectfiles0 140 in 141 if 142 isSuccess ( 143 compile debug ( 144 include_flags @ ["-o", script, "holmake_holpathdb.uo"] @ 145 objectfiles 146 ) 147 ) 148 then 149 let 150 val _ = exists_readable script orelse 151 die_with ("Can't see script executable: "^script) 152 val status = Systeml.mk_xable script 153 val _ = OS.Process.isSuccess status orelse 154 die_with ("Couldn't make script "^script^" executable") 155 val script' = xable_string script |> hm_target.filestr_to_tgt 156 |> tgt_toString 157 val _ = diag "build_command" 158 (fn _ => "Created executable "^script') 159 val thysmlfile = s^"Theory.sml" 160 val thysigfile = s^"Theory.sig" 161 fun safedelete s = FileSys.remove s handle OS.SysErr _ => () 162 val _ = app safedelete [thysmlfile, thysigfile] 163 val res2 = Systeml.systeml [script'] 164 val _ = app safedelete [script', scriptuo, scriptui] 165 val () = if not (isSuccess res2) then 166 failed_script_cache := 167 Binaryset.add(!failed_script_cache, s) 168 else () 169 in 170 isSuccess res2 andalso 171 (exists_readable thysmlfile orelse 172 (print ("Couldn't find required output file: "^thysmlfile^ "\n"); 173 print ("Script file "^script'^ 174 " didn't produce "^thysmlfile^"; \n\ 175 \ maybe need export_theory() at end of "^ 176 scriptsml^"\n"); 177 false)) andalso 178 (exists_readable thysigfile orelse 179 (print ("Script file "^script'^" didn't produce "^ 180 thysigfile^"; \n\ 181 \ maybe need export_theory() at end of "^ 182 scriptsml^"\n"); 183 false)) 184 end 185 else (print ("Failed to build script file, "^script^"\n"); false) 186 end handle CompileFailed => false 187 | FileNotFound => false 188 end (* fun's let *) 189 fun mosml_build_command _ _ _ _ = NONE 190 val build_graph = graphbuildj1 { build_command = build_command, 191 mosml_build_command = mosml_build_command, 192 outs = outs, 193 keep_going = keep_going, 194 quiet = quiet_flag, 195 system = Systeml.system_ps, 196 hmenv = hmenv} 197in 198 {extra_impl_deps = [], build_graph = build_graph} 199end (* make_build_command's let *) 200 201end (* struct *) 202