1structure Systeml :> Systeml = struct 2 3(* This is the WINDOWS implementation of the Systeml functionality. 4 It is the very first thing compiled by the HOL build process so it 5 absolutely can not depend on any other HOL source code. *) 6 7structure Process = OS.Process 8structure Path = OS.Path 9structure FileSys = OS.FileSys 10 11fun dquote s = concat ["\"", s, "\""] 12 13fun concat_wspaces munge strl = String.concatWith " " (map munge strl) 14 15fun systeml l = let 16 val command = "call "^concat_wspaces dquote l 17in 18 Process.system command 19end 20 21fun systeml_out {outfile} c = 22 Process.system 23 ("call " ^ concat_wspaces dquote c ^ " > " ^ dquote outfile ^ " 2>&1") 24 25 26(* would like to be using Posix.Process.exec, but this seems flakey on 27 various machines (and is entirely unavailable on Moscow ML) *) 28fun exec (comm, args) = OS.Process.exit (systeml (comm::tl args)) 29 30val protect = dquote 31 32(* the _ps suffix stands for 'protected string', as opposed to the 'l' 33 of systeml, which stands for 'list' of strings (all of which are 34 presumed unprotected). The problem is that on Windows, if you pass 35 system a (protected) string such as 36 "c:/program files/bar/baz" "arg1" 37 then it has a fit. It seems the only way of getting it to play nicely 38 is to prefix the commandline with "call". *) 39fun system_ps s = Process.system ("call " ^ s) 40 41fun xable_string s = s^".exe" 42fun mk_xable file = 43 let val exe = file^".exe" 44 val _ = FileSys.remove exe handle _ => () 45 in 46 FileSys.rename{old=file, new=exe}; 47 OS.Process.success 48 end 49 50fun normPath s = Path.toString(Path.fromString s) 51 52fun fullPath slist = 53 normPath (List.foldl (fn (p1,p2) => Path.concat(p2,p1)) 54 (hd slist) (tl slist)) 55 56 fun get_first f [] = NONE 57 | get_first f (h::t) = case f h of NONE => get_first f t 58 | x => x 59 60 61 fun find_my_path () = let 62 (* assumes directory hasn't been changed yet *) 63 val myname = CommandLine.name() 64 val {dir,file} = Path.splitDirFile myname 65 in 66 if dir = "" then let 67 val pathdirs = String.tokens (fn c => c = #";") 68 (valOf (Process.getEnv "PATH")) 69 open FileSys 70 fun checkdir d = let 71 val f = Path.concat(d,file) 72 in 73 if access(f, [A_READ, A_EXEC]) then SOME f else NONE 74 end 75 in 76 valOf (get_first checkdir pathdirs) 77 end 78 else 79 Path.mkAbsolute {path = myname, relativeTo = FileSys.getDir()} 80 end 81 82 83val HOLDIR = "" 84val MOSMLDIR = "" 85val OS = "" 86val POLY = "" 87val POLYC = "" 88val POLY_VERSION = 0 89val POLYMLLIBDIR = "" 90val POLY_LDFLAGS = [] 91val POLY_LDFLAGS_STATIC = [] 92val CC = "" 93val DEPDIR = "" 94val GNUMAKE = "" 95val DYNLIB = "" 96val version = "" 97val ML_SYSNAME = "" 98val release = "" 99val DOT_PATH = "" 100val DEFAULT_STATE = fullPath [HOLDIR, "bin", "hol.state"] 101 102val isUnix = false 103local val cast : 'a -> int = Obj.magic 104in 105 fun pointer_eq (x:'a, y:'a) = (cast x = cast y) 106end 107 108val build_log_dir = fullPath [HOLDIR, "tools", "build-logs"] 109val build_log_file = fullPath [build_log_dir, "current-build-log"] 110val make_log_file = "current-make-log" 111val build_after_reloc_envvar = "HOL_REBUILD_HEAPS_ONLY" 112 113local 114 fun fopen file = (FileSys.remove file handle _ => (); TextIO.openOut file) 115 fun munge s = String.translate (fn #"/" => "\\" | c => str c) s 116 fun q s = "\""^munge s^"\"" 117in 118fun emit_hol_script target qend _ = 119 let val ostrm = fopen(target^".bat") 120 fun output s = TextIO.output(ostrm, s) 121 val sigobj = q (fullPath [HOLDIR, "sigobj"]) 122 val std_prelude = q (fullPath [HOLDIR, "std.prelude"]) 123 val mosml = q (fullPath [MOSMLDIR, "mosml"]) 124 in 125 output "@echo off\n"; 126 output "rem The bare HOL script\n"; 127 output "rem (automatically generated by HOL configuration)\n\n"; 128 output (String.concat["call ", mosml, " -P full -I ", sigobj, " ", 129 std_prelude, " %* ", q qend, "\n"]); 130 TextIO.closeOut ostrm; 131 target 132 end 133 134 135fun emit_hol_unquote_script target qend _ = 136 let val ostrm = fopen(target^".bat") 137 fun output s = TextIO.output(ostrm, s) 138 val qfilter = q (fullPath [HOLDIR, "bin", "unquote"]) 139 val sigobj = q (fullPath [HOLDIR, "sigobj"]) 140 val std_prelude = q (fullPath [HOLDIR, "std.prelude"]) 141 val mosml = q (fullPath [MOSMLDIR, "mosml"]) 142 val qinit = q (fullPath [HOLDIR, "tools", "unquote-init.sml"]) 143 in 144 output "@echo off\n"; 145 output "rem The HOL script (with quote preprocessing)\n"; 146 output "rem (automatically generated by HOL configuration)\n\n"; 147 output (String.concat ["call ", qfilter, " | ", mosml, 148 " -P full -I ", sigobj, " ", 149 std_prelude, " ", qinit, " %* ", 150 q qend, "\n"]); 151 TextIO.closeOut ostrm; 152 target 153 end 154end (* local *) 155 156fun quietbind s = () 157fun bindstr s = s 158 159end; (* struct *) 160