1structure Systeml :> Systeml = struct 2 3(* This is the UNIX implementation of the Systeml functionality. It is the 4 very first thing compiled by the HOL build process so it absolutely 5 can not depend on any other HOL source code. *) 6 7structure Path = OS.Path 8structure Process = OS.Process 9structure FileSys = OS.FileSys 10 11local 12 open Process 13 fun concat_wspaces munge strl = String.concatWith " " (map munge strl) 14in 15 16 val unix_meta_chars = [#"'", #"\"", #"|", #" ", #">", #"\t", #"\n", #"<", 17 #"\\", #"#"] 18 fun is_meta c = List.exists (fn y => c = y) unix_meta_chars 19 fun is_meta_string(s,i) = if i >= size s then false 20 else if is_meta (String.sub(s,i)) then true 21 else is_meta_string(s, i + 1) 22 fun unix_trans c = if is_meta c then "\\" ^ str c else str c 23 24 fun protect s = if is_meta_string(s,0) then String.translate unix_trans s 25 else s 26 27 val systeml = system o concat_wspaces protect 28 29 fun systeml_out {outfile} c = 30 system (concat_wspaces protect c ^ " > " ^ protect outfile ^ " 2>&1") 31 32 val system_ps = Process.system 33 (* see winNT-systeml.sml for an explanation of why what is a synonym under 34 unix needs to be slightly different on Windows. *) 35 36 (* would like to be using Posix.Process.exec, but this seems flakey on 37 various machines (and is entirely unavailable on Moscow ML) *) 38 fun exec (comm, args) = OS.Process.exit (systeml (comm::tl args)) 39 40 fun get_first f [] = NONE 41 | get_first f (h::t) = case f h of NONE => get_first f t 42 | x => x 43 44 45 fun find_my_path () = let 46 (* assumes directory hasn't been changed yet *) 47 val myname = CommandLine.name() 48 val {dir,file} = Path.splitDirFile myname 49 in 50 if dir = "" then let 51 val pathdirs = String.tokens (fn c => c = #":") 52 (valOf (Process.getEnv "PATH")) 53 open FileSys 54 fun checkdir d = let 55 val f = Path.concat(d,file) 56 in 57 if access(f, [A_READ, A_EXEC]) then SOME f else NONE 58 end 59 in 60 valOf (get_first checkdir pathdirs) 61 end 62 else 63 Path.mkAbsolute {path = myname,relativeTo = FileSys.getDir()} 64 end 65 66 fun xable_string s = s 67 68 fun mk_xable file = 69 let 70 val r = systeml ["chmod", "a+x", file] 71 in 72 if Process.isSuccess r then r 73 else if FileSys.access (file,[FileSys.A_EXEC]) then 74 (* if we can execute it, then continue with a warning *) 75 (* NB: MoSML docs say FileSys.access uses real uid/gid, not effective uid/gid, 76 so this test may be bogus if we are setuid. This is unlikely(!). *) 77 (print ("Non-fatal warning: couldn't set world execute permission on "^file^",\n but continuing anyway since at least the current user has execute permission.\n"); 78 OS.Process.success) 79 else (print ("unable to set execute permission on "^file^".\n"); 80 OS.Process.failure) 81 end 82 83 84fun normPath s = Path.toString(Path.fromString s) 85 86fun fullPath slist = 87 normPath (List.foldl (fn (p1,p2) => Path.concat(p2,p1)) 88 (hd slist) (tl slist)) 89 90 91(* these values are filled in by configure.sml *) 92val HOLDIR = "" 93val MOSMLDIR = "" 94val OS = "" 95val POLY = "" 96val POLYC = "" 97val POLY_VERSION = 0 98val POLYMLLIBDIR = "" 99val POLY_LDFLAGS = [] 100val POLY_LDFLAGS_STATIC = [] 101val CC = "" 102 103val DEPDIR = "" 104val GNUMAKE = "" 105val DYNLIB = "" 106val version = "" 107val ML_SYSNAME = "" 108val release = "" 109val DOT_PATH = "" 110val DEFAULT_STATE = fullPath [HOLDIR, "bin", "hol.state"] 111 112val isUnix = true 113local val cast : 'a -> int = Obj.magic 114in 115 fun pointer_eq (x:'a, y:'a) = (cast x = cast y) 116end 117 118val build_log_dir = fullPath [HOLDIR, "tools", "build-logs"] 119val build_log_file = fullPath [build_log_dir, "current-build-log"] 120val make_log_file = "current-make-log" 121val build_after_reloc_envvar = "HOL_REBUILD_HEAPS_ONLY" 122 123 124fun emit_hol_script target qend _ = let 125 val ostrm = TextIO.openOut target 126 fun output s = TextIO.output(ostrm, s) 127 val sigobj = protect (fullPath [HOLDIR, "sigobj"]) 128 val std_prelude = protect (fullPath [HOLDIR, "std.prelude"]) 129 val mosml = protect (fullPath [MOSMLDIR, "mosml"]) 130in 131 output "#!/bin/sh\n"; 132 output "# The bare HOL script\n"; 133 output "# (automatically generated by HOL configuration)\n\n"; 134 output (String.concat[mosml," -quietdec -P full -I ", sigobj, " ", 135 std_prelude, " $* ", protect qend, "\n"]); 136 TextIO.closeOut ostrm; 137 mk_xable target 138end 139 140 141fun emit_hol_unquote_script target qend _ = let 142 val ostrm = TextIO.openOut target 143 fun output s = TextIO.output(ostrm, s) 144 val qfilter = protect (fullPath [HOLDIR, "bin", "unquote"]) 145 val sigobj = protect (fullPath [HOLDIR, "sigobj"]) 146 val std_prelude = protect (fullPath [HOLDIR, "std.prelude"]) 147 val mosml = protect (fullPath [MOSMLDIR, "mosml"]) 148 val qinit = 149 protect (fullPath [HOLDIR, "tools", "unquote-init.sml"]) 150in 151 output "#!/bin/sh\n"; 152 output "# The HOL script (with quote preprocessing)\n"; 153 output "# (automatically generated by HOL configuration)\n\n"; 154 output (String.concat [qfilter, " | ", mosml," -quietdec -P full -I ", 155 sigobj, " ", std_prelude, " ", qinit, 156 " $* ", protect qend, "\n"]); 157 TextIO.closeOut ostrm; 158 mk_xable target 159end 160end (* local *) 161 162fun bindstr s = s 163 164end; (* struct *) 165