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 fun systeml_out {outfile} c = 29 system (concat_wspaces protect c ^ " > " ^ protect outfile ^ " 2>&1") 30 31 fun get_first f [] = NONE 32 | get_first f (h::t) = case f h of NONE => get_first f t 33 | x => x 34 35 36 fun find_my_path () = let 37 (* assumes directory hasn't been changed yet *) 38 val myname = CommandLine.name() 39 val {dir,file} = Path.splitDirFile myname 40 in 41 if dir = "" then let 42 val pathdirs = String.tokens (fn c => c = #":") 43 (valOf (Process.getEnv "PATH")) 44 open FileSys 45 fun checkdir d = let 46 val f = Path.concat(d,file) 47 in 48 if access(f, [A_READ, A_EXEC]) then SOME f else NONE 49 end 50 in 51 valOf (get_first checkdir pathdirs) 52 end 53 else 54 Path.mkAbsolute {path = myname, relativeTo = FileSys.getDir()} 55 end 56 57 val system_ps = Process.system 58 (* see winNT-systeml.sml for an explanation of why what is a synonym under 59 unix needs to be slightly different on Windows. *) 60 61 fun xable_string s = s 62 63 fun mk_xable file = 64 let 65 val r = systeml ["chmod", "a+x", file] 66 in 67 if Process.isSuccess r then r 68 else if FileSys.access (file,[FileSys.A_EXEC]) then 69 (* if we can execute it, then continue with a warning *) 70 (* NB: MoSML docs say FileSys.access uses real uid/gid, not effective uid/gid, 71 so this test may be bogus if we are setuid. This is unlikely(!). *) 72 (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"); 73 OS.Process.success) 74 else (print ("unable to set execute permission on "^file^".\n"); 75 OS.Process.failure) 76 end 77 78 79fun normPath s = Path.toString(Path.fromString s) 80 81fun fullPath slist = 82 normPath (List.foldl (fn (p1,p2) => Path.concat(p2,p1)) 83 (hd slist) (tl slist)) 84 85 86(* these values are filled in by configure.sml *) 87val HOLDIR = "" 88val MOSMLDIR = "" 89val POLYMLLIBDIR = "" 90val POLY = "" 91val POLYC = "" 92val POLY_VERSION = PolyML.Compiler.compilerVersionNumber 93val POLY_LDFLAGS = [] 94val POLY_LDFLAGS_STATIC = [] 95val CC = "" 96val OS = "" 97 98val DEPDIR = "" 99val GNUMAKE = "" 100val DYNLIB = "" 101val version = "" 102val ML_SYSNAME = "" 103val release = "" 104val DOT_PATH = "" 105val DEFAULT_STATE = fullPath [HOLDIR, "bin", "hol.state"] 106 107val isUnix = true 108 109val pointer_eq = PolyML.pointerEq 110 111fun exec (x as (comm,args)) = 112 (* macos execv fails if the calling process is multi-threaded. *) 113 (* Can't lift the check out of the function body because of the value 114 restriction *) 115 if OS <> "macosx" then Posix.Process.exec x 116 else OS.Process.exit (systeml (comm::tl args)) 117 118 119val build_log_dir = fullPath [HOLDIR, "tools-poly", "build-logs"] 120val build_log_file = fullPath [build_log_dir, "current-build-log"] 121val make_log_file = "current-make-log"; 122val build_after_reloc_envvar = "HOL_REBUILD_HEAPS_ONLY" 123 124fun base_interactive state scripts = 125 [POLY, "-q", "--use", fullPath [HOLDIR, "bin", "hol.ML"], state] @ scripts 126 127 128fun emit_hol_script target exe script = 129 let 130 val ostrm = TextIO.openOut target 131 fun output s = TextIO.output(ostrm, s) 132 in 133 output "#!/bin/sh\n"; 134 output "# The bare HOL script\n"; 135 output "# (automatically generated by HOL configuration)\n\n"; 136 output (fullPath [HOLDIR, "bin", "buildheap"] ^ 137 " --gcthreads=1 --repl --holstate=" ^ exe ^ " " ^ 138 String.concatWith " " script ^ " \"$@\"\n"); 139 TextIO.closeOut ostrm; 140 mk_xable target 141 end; 142 143 fun emit_hol_unquote_script target exe s = 144 let val ostrm = TextIO.openOut target 145 fun output s = TextIO.output(ostrm, s) 146 val qfilter = protect (fullPath [HOLDIR, "bin", "unquote"]) 147 val script = 148 List.map (fn s => protect (fullPath [HOLDIR, "tools-poly", s])) 149 s 150 in 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.concatWith " " 155 ([qfilter, "|"] @ base_interactive exe script) ^ "\n"); 156 TextIO.closeOut ostrm; 157 mk_xable target 158 end; 159end (* local *) 160 161fun bindstr mlcode = 162 "val _ = CompilerSpecific.quietbind \"" ^ String.toString mlcode ^ "\"" 163 164end; (* struct *) 165