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