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 HAVE_BASIS2002 = false 90val POLYMLLIBDIR = "" 91val POLY = "" 92val POLYC = "" 93val POLY_VERSION = PolyML.Compiler.compilerVersionNumber 94val POLY_LDFLAGS = [] 95val POLY_LDFLAGS_STATIC = [] 96val CC = "" 97val OS = "" 98 99val DEPDIR = "" 100val GNUMAKE = "" 101val DYNLIB = "" 102val version = "" 103val ML_SYSNAME = "" 104val release = "" 105val DOT_PATH = "" 106val DEFAULT_STATE = fullPath [HOLDIR, "bin", "hol.state"] 107 108val isUnix = true 109 110val pointer_eq = PolyML.pointerEq 111 112fun exec (x as (comm,args)) = 113 (* macos execv fails if the calling process is multi-threaded. *) 114 (* Can't lift the check out of the function body because of the value 115 restriction *) 116 if OS <> "macosx" then Posix.Process.exec x 117 else OS.Process.exit (systeml (comm::tl args)) 118 119 120val build_log_dir = fullPath [HOLDIR, "tools-poly", "build-logs"] 121val build_log_file = fullPath [build_log_dir, "current-build-log"] 122val make_log_file = "current-make-log"; 123val build_after_reloc_envvar = "HOL_REBUILD_HEAPS_ONLY" 124 125fun base_interactive state scripts = 126 [POLY, "-q", "--use", fullPath [HOLDIR, "bin", "hol.ML"], state] @ scripts 127 128 129fun emit_hol_script target exe script = 130 let 131 val ostrm = TextIO.openOut target 132 fun output s = TextIO.output(ostrm, s) 133 in 134 output "#!/bin/sh\n"; 135 output "# The bare HOL script\n"; 136 output "# (automatically generated by HOL configuration)\n\n"; 137 output (fullPath [HOLDIR, "bin", "buildheap"] ^ 138 " --gcthreads=1 --repl --holstate=" ^ exe ^ " " ^ 139 String.concatWith " " script ^ " \"$@\"\n"); 140 TextIO.closeOut ostrm; 141 mk_xable target 142 end; 143 144 fun emit_hol_unquote_script target exe s = 145 let val ostrm = TextIO.openOut target 146 fun output s = TextIO.output(ostrm, s) 147 val qfilter = protect (fullPath [HOLDIR, "bin", "unquote"]) 148 val script = 149 List.map (fn s => protect (fullPath [HOLDIR, "tools-poly", s])) 150 s 151 in 152 output "#!/bin/sh\n"; 153 output "# The HOL script (with quote preprocessing)\n"; 154 output "# (automatically generated by HOL configuration)\n\n"; 155 output (String.concatWith " " 156 ([qfilter, "|"] @ base_interactive exe script) ^ "\n"); 157 TextIO.closeOut ostrm; 158 mk_xable target 159 end; 160end (* local *) 161 162end; (* struct *) 163