1(*quietdec := true; 2app load ["Mosml", "Process", "Path", "FileSys", "Timer", "Real", "Int", 3 "Bool", "OS"] ; 4open Mosml; 5*) 6val _ = PolyML.Compiler.prompt1:=""; 7val _ = PolyML.Compiler.prompt2:=""; 8val _ = PolyML.print_depth 0; 9 10(* utility functions *) 11fun warn s = TextIO.output(TextIO.stdErr, s ^ "\n") 12fun die s = (TextIO.output(TextIO.stdErr, s ^ "\n"); 13 OS.Process.exit OS.Process.failure) 14 15val _ = if PolyML.Compiler.compilerVersionNumber < 551 then 16 die "Must be running PolyML with version >= 5.5.1\n" 17 else () 18 19fun readdir s = let 20 val ds = OS.FileSys.openDir s 21 fun recurse acc = 22 case OS.FileSys.readDir ds of 23 NONE => acc 24 | SOME s => recurse (s::acc) 25in 26 recurse [] before OS.FileSys.closeDir ds 27end; 28 29fun mem x [] = false 30 | mem x (h::t) = x = h orelse mem x t 31 32fun frontlast [] = raise Fail "frontlast: failure" 33 | frontlast [h] = ([], h) 34 | frontlast (h::t) = let val (f,l) = frontlast t in (h::f, l) end; 35 36fun check_dir nm privs candidate = let 37 open OS.FileSys 38 val p = OS.Path.concat(candidate,nm) 39in 40 if access(p, privs) then SOME (OS.Path.dir (fullPath p)) else NONE 41end 42val check_poly = check_dir "poly" [OS.FileSys.A_EXEC] 43val check_libpoly = check_dir "libpolymain.a" [OS.FileSys.A_READ] 44fun check_polyc c = 45 Option.map (fn p => OS.Path.concat(p,"polyc")) 46 (check_dir "polyc" [OS.FileSys.A_EXEC] c) 47 48fun findpartial f [] = NONE 49 | findpartial f (h::t) = 50 case f h of NONE => findpartial f t | x => x 51 52(* sleeping, with an action every second *) 53fun delay limit action = let 54 fun loop cnt = 55 if cnt >= limit then () 56 else (action cnt; 57 Posix.Process.sleep (Time.fromSeconds 1); 58 loop (cnt + 1)) 59in 60 loop 0 61end; 62 63fun determining s = 64 (print (s^" "); delay 1 (fn _ => ())); 65 66(* action starts here *) 67print "\nHOL smart configuration.\n\n"; 68 69val poly = "" 70val polyc = NONE : string option 71val polymllibdir = ""; 72val DOT_PATH = SOME ""; 73val MLTON = SOME ""; 74 75val _ = let 76 val override = "tools-poly/poly-includes.ML" 77in 78 if OS.FileSys.access (override, [OS.FileSys.A_READ]) then 79 (print ("[Using override file "^override^"]\n\n"); 80 use override) 81 else () 82end; 83 84print "Determining configuration parameters: "; 85 86val currentdir = OS.FileSys.getDir(); 87 88fun dirify {arcs,isAbs,vol} = 89 OS.Path.toString {arcs = #1 (frontlast arcs), isAbs = isAbs, vol = vol}; 90 91determining "holdir"; 92 93val holdir = let 94 val cdir_files = readdir currentdir 95in 96 if mem "sigobj" cdir_files andalso mem "std.prelude" cdir_files then 97 currentdir 98 else if mem "smart-configure.sml" cdir_files andalso 99 mem "configure.sml" cdir_files 100 then dirify (OS.Path.fromString currentdir) 101 else die "\n\n*** Couldn't determine holdir; \ 102 \please run me from the root HOL directory" 103end; 104 105val _ = let 106in 107 OS.FileSys.chDir (OS.Path.concat (holdir, "tools-poly")); 108 use "poly/poly-init.ML"; 109 OS.FileSys.chDir currentdir 110end; 111 112 113val OS = let 114 val _ = determining "OS" 115 val {vol,...} = OS.Path.fromString currentdir 116in 117 if vol = "" then (* i.e. Unix *) 118 case Mosml.run "uname" ["-a"] "" of 119 Mosml.Success s => if String.isPrefix "Linux" s then 120 "linux" 121 else if String.isPrefix "SunOS" s then 122 "solaris" 123 else if String.isPrefix "Darwin" s then 124 "macosx" 125 else 126 "unix" 127 | Mosml.Failure s => (print "\nRunning uname failed with message: "; 128 print s; 129 OS.Process.exit OS.Process.failure) 130 else "winNT" 131end 132 133fun which arg = 134 let 135 open OS.FileSys 136 val sepc = if OS = "winNT" then #";" else #":" 137 fun check p = 138 let 139 val fname = OS.Path.concat(p, arg) 140 in 141 if access (fname, [A_READ, A_EXEC]) then 142 SOME 143 (OS.Path.mkAbsolute{path = fname, relativeTo = OS.FileSys.getDir()}) 144 else NONE 145 end 146 in 147 case OS.Process.getEnv "PATH" of 148 SOME path => 149 let 150 val paths = (if OS = "winNT" then ["."] else []) @ 151 String.fields (fn c => c = sepc) path 152 in 153 findpartial check paths 154 end 155 | NONE => if OS = "winNT" then check "." else NONE 156 end 157 158val polyinstruction = 159 "Please write file tools-poly/poly-includes.ML to specify it \ 160 \properly.\n\ 161 \This file should include a line of the form\n\n\ 162 \ val poly = \"path-to-poly\";" 163val (poly,polycopt) = 164 if poly = "" then let 165 val _ = determining "poly" 166 val nm = CommandLine.name() 167 val p as {arcs, isAbs, vol} = OS.Path.fromString nm 168 val cand = 169 if isAbs then SOME (dirify p) 170 else if length arcs > 1 then 171 SOME (OS.Path.mkAbsolute { path = dirify p, 172 relativeTo = OS.FileSys.getDir()}) 173 else (* examine PATH variable *) 174 case OS.Process.getEnv "PATH" of 175 NONE => NONE 176 | SOME elist => let 177 val sep = case OS of "winNT" => #";" | _ => #":" 178 val search_these = String.fields (fn c => c = sep) elist 179 in 180 findpartial check_poly search_these 181 end 182 in 183 case cand of 184 NONE => die 185 ("\n\nYou ran poly on the commandline, but it doesn't seem \ 186 \to be in your PATH.\n\ 187 \I need to know where your poly executable is.\n" ^ 188 polyinstruction) 189 | SOME c => let 190 in 191 case check_poly c of 192 SOME p => (OS.Path.concat(p,"poly"), check_polyc p) 193 | NONE => 194 die ("\n\nI tried to figure out where your poly executable is\ 195 \n\by examining your command-line.\n\ 196 \But directory "^c^ 197 "doesn't seem to contain a poly executable after \ 198 \all\n" ^ 199 polyinstruction) 200 end 201 end 202 else 203 case check_poly (OS.Path.dir poly) of 204 NONE => die ("\n\nYour overrides file specifies bogus location '" 205 ^poly^ 206 "'\nas the location of the poly executable.\n"^ 207 polyinstruction) 208 | SOME p => (OS.Path.concat(p, "poly"), check_polyc p) 209 210val polyc = 211 case polycopt of 212 NONE => die ("Couldn't find polyc executable\n" ^ polyinstruction) 213 | SOME p => p 214 215val polylibsister = let 216 val p as {arcs,isAbs,vol} = OS.Path.fromString poly 217 val (dirname, _) = frontlast arcs 218 val (parent, probably_bin) = frontlast dirname 219 val _ = if probably_bin <> "bin" then 220 warn "\nSurprised that poly is not in a \"bin\" directory" 221 else () 222in 223 OS.Path.toString { arcs = parent @ ["lib"], vol = vol, isAbs = isAbs } 224end 225 226val polylibinstruction = 227 "Please write file tools-poly/poly-includes.ML to specify it.\n\ 228 \This file should include a line of the form\n\n\ 229 \ val polymllibdir = \"path-to-dir-containing-libpolymain.a\";" 230 231val polymllibdir = 232 if polymllibdir = "" then let 233 val _ = determining "polymllibdir" 234 in 235 case check_libpoly polylibsister of 236 SOME c => c 237 | NONE => die ("\n\nLooked in poly's sister lib directory "^ 238 polylibsister ^ 239 "\nand couldn't find libpolymain.a\n" ^ 240 polylibinstruction) 241 242 end 243 else 244 case check_libpoly polymllibdir of 245 SOME c => c 246 | NONE => die ("\n\nYour overrides file specifies bogus location '" 247 ^polymllibdir ^ 248 "'\nas the location of libpolymain.a\n" ^ 249 polylibinstruction); 250 251val DOT_PATH = if DOT_PATH = SOME "" then which "dot" else DOT_PATH; 252 253val dynlib_available = false; 254 255val MLTON = if MLTON = SOME "" then which "mlton" else MLTON; 256 257print "\n"; 258 259fun verdict (prompt, value) = 260 if value = "" then 261 (print ("\n*** No value for "^prompt^ 262 "!! Write a tools-poly/poly-includes.ML file to fix this\n"); 263 OS.Process.exit OS.Process.failure) 264 else 265 (print (StringCvt.padRight #" " 20 (prompt^":")); 266 print value; 267 print "\n"); 268 269fun optverdict (prompt, optvalue) = 270 (print (StringCvt.padRight #" " 20 (prompt ^ ":")); 271 print (case optvalue of NONE => "NONE" | SOME p => "SOME "^p); 272 print "\n"); 273 274verdict ("OS", OS); 275verdict ("poly", poly); 276verdict ("polyc", polyc); 277verdict ("polymllibdir", polymllibdir); 278verdict ("holdir", holdir); 279optverdict ("DOT_PATH", DOT_PATH); 280optverdict ("MLTON", MLTON); 281 282print "\nConfiguration will begin with above values. If they are wrong\n"; 283print "press Control-C.\n\n"; 284 285delay 3 286 (fn n => print ("\rWill continue in "^Int.toString (3 - n)^" seconds.")) 287 handle Interrupt => (print "\n"; OS.Process.exit OS.Process.failure); 288 289print "\n"; 290 291val configfile = OS.Path.concat (OS.Path.concat (holdir, "tools-poly"), "configure.sml"); 292 293 294use configfile handle Fail s => die s; 295