1(* ----------------------------------------------------------------------
2              HOL configuration script
3
4
5   DO NOT EDIT THIS FILE UNLESS YOU HAVE TRIED AND FAILED WITH
6
7     smart-configure
8
9   AND
10
11     config-override.
12
13   ---------------------------------------------------------------------- *)
14
15
16(* Uncomment these lines and fill in correct values if smart-configure doesn't
17   get the correct values itself.  Then run
18
19      mosml < configure.sml
20
21   If you are specifying directories under Windows, we recommend you
22   use forward slashes (the "/" character) as a directory separator,
23   rather than the 'traditional' backslash (the "\" character).
24
25   The problem with the latter is that you have to double them up
26   (i.e., write "\\") in order to 'escape' them and make the string
27   valid for SML.  For example, write "c:/dir1/dir2/mosml", rather
28   than "c:\\dir1\\dir2\\mosml", and certainly DON'T write
29   "c:\dir1\dir2\mosml".
30*)
31
32
33(*
34val mosmldir:string =
35val holdir :string  =
36
37val OS :string      =
38                           (* Operating system; choices are:
39                                "linux", "solaris", "unix", "macosx",
40                                "winNT"   *)
41*)
42
43
44val CC:string       = "cc";       (* C compiler                       *)
45val GNUMAKE:string  = "make";     (* for bdd library and SMV          *)
46val DEPDIR:string   = ".HOLMK";   (* where Holmake dependencies kept  *)
47
48(*---------------------------------------------------------------------------
49          END user-settable parameters
50 ---------------------------------------------------------------------------*)
51
52val version_number = 12
53val release_string = "Kananaskis"
54
55
56val _ = Meta.quietdec := true;
57app load ["OS", "Substring", "BinIO", "Lexing", "Nonstdio"];
58
59
60fun check_is_dir role dir =
61    (FileSys.isDir dir handle e => false) orelse
62    (print "\n*** Bogus directory ("; print dir; print ") given for ";
63     print role; print "! ***\n";
64     Process.exit Process.failure)
65
66val _ = check_is_dir "mosmldir" mosmldir
67val _ = check_is_dir "holdir" holdir
68val _ =
69    if List.exists (fn s => s = OS)
70                   ["linux", "solaris", "unix", "winNT", "macosx"]
71    then ()
72    else (print ("\n*** Bad OS specified: "^OS^" ***\n");
73          Process.exit Process.failure)
74
75fun normPath s = Path.toString(Path.fromString s)
76fun itstrings f [] = raise Fail "itstrings: empty list"
77  | itstrings f [x] = x
78  | itstrings f (h::t) = f h (itstrings f t);
79
80fun fullPath slist = normPath
81   (itstrings (fn chunk => fn path => Path.concat (chunk,path)) slist);
82
83fun quote s = String.concat ["\"",String.toString s,"\""]
84fun optquote NONE = "NONE"
85  | optquote (SOME p) = "SOME " ^ quote p
86
87val holmakedir = fullPath [holdir, "tools", "Holmake"];
88val compiler = fullPath [mosmldir, "mosmlc"];
89
90(*---------------------------------------------------------------------------
91      File handling. The following implements a very simple line
92      replacement function: it searchs the source file for a line that
93      contains "redex" and then replaces the whole line by "residue". As it
94      searches, it copies lines to the target. Each replacement happens
95      once; the replacements occur in order. After the last replacement
96      is done, the rest of the source is copied to the target.
97 ---------------------------------------------------------------------------*)
98
99fun processLinesUntil (istrm,ostrm) (redex,residue) = let
100  open TextIO
101  fun loop () =
102      case inputLine istrm of
103        NONE   => ()
104      | SOME line => let
105          val ssline = Substring.full line
106          val (pref, suff) = Substring.position redex ssline
107        in
108          if Substring.size suff > 0
109          then TextIO.output(ostrm, residue)
110          else (TextIO.output(ostrm, line); loop())
111        end
112in
113  loop()
114end;
115
116fun fill_holes (src,target) repls =
117 let open TextIO
118     val istrm = openIn src
119     val ostrm = openOut target
120  in
121     List.app (processLinesUntil (istrm, ostrm)) repls;
122     output(ostrm, inputAll istrm);
123     closeIn istrm; closeOut ostrm
124  end;
125
126infix -->
127fun (x --> y) = (x,y);
128
129fun text_copy src dest = fill_holes(src, dest) [];
130
131fun bincopy src dest = let
132  val instr = BinIO.openIn src
133  val outstr = BinIO.openOut dest
134  fun loop () = let
135    val v = BinIO.inputN(instr, 1024)
136  in
137    if Word8Vector.length v = 0 then (BinIO.flushOut outstr;
138                                      BinIO.closeOut outstr;
139                                      BinIO.closeIn instr)
140    else (BinIO.output(outstr, v); loop())
141  end
142in
143  loop()
144end;
145
146
147
148(*---------------------------------------------------------------------------
149     Generate "Systeml" file in tools/Holmake and then load in that file,
150     thus defining the Systeml structure for the rest of the configuration
151     (with OS-specific stuff available).
152 ---------------------------------------------------------------------------*)
153
154exception GetOut;
155fun canread s = FileSys.access(s, [FileSys.A_READ])
156val sigobj = fullPath [holdir, "sigobj"]
157fun to_sigobj s = bincopy s (fullPath [sigobj, s]);
158
159(* default values ensure that later things fail if Systeml doesn't compile *)
160fun systeml x = (print "Systeml not correctly loaded.\n";
161                 Process.exit Process.failure);
162val mk_xable = systeml;
163val xable_string = systeml;
164
165val have_basis2002 = version_string <> "2.01";
166
167val OSkind = if OS="linux" orelse OS="solaris" orelse OS="macosx" then "unix"
168             else OS
169val _ = let
170  (* copy system-specific implementation of Systeml into place *)
171  val srcfile = fullPath [holmakedir, OSkind ^"-systeml.sml"]
172  val destfile = fullPath [holmakedir, "Systeml.sml"]
173  val sigfile = fullPath [holmakedir, "Systeml.sig"]
174in
175  print "\nLoading system specific functions\n";
176  use sigfile;
177  fill_holes (srcfile, destfile)
178  ["val HOLDIR ="   --> ("val HOLDIR = "^quote holdir^"\n"),
179   "val MOSMLDIR =" --> ("val MOSMLDIR = "^quote mosmldir^"\n"),
180   "val HAVE_BASIS2002 =" -->
181                        ("val HAVE_BASIS2002 = "^Bool.toString have_basis2002^
182                         "\n"),
183   "val OS ="       --> ("val OS = "^quote OS^"\n"),
184   "val CC ="       --> ("val CC = "^quote CC^"\n"),
185   "val DEPDIR ="   --> ("val DEPDIR = "^quote DEPDIR^"\n"),
186   "val GNUMAKE ="  --> ("val GNUMAKE = "^quote GNUMAKE^"\n"),
187   "val DYNLIB ="   --> ("val DYNLIB = "^Bool.toString dynlib_available^"\n"),
188   "val version ="  --> ("val version = "^Int.toString version_number^"\n"),
189   "val ML_SYSNAME =" --> "val ML_SYSNAME = \"mosml\"\n",
190   "val release ="  --> ("val release = "^quote release_string^"\n"),
191   "val DOT_PATH =" --> ("val DOT_PATH = "^optquote DOT_PATH^"\n")
192  ];
193  use destfile
194end;
195
196open Systeml;
197
198(* can now compile basis2002, if necessary *)
199
200
201let
202  val _ = not have_basis2002 orelse raise GetOut
203  val modTime = FileSys.modTime
204  val dir_0 = FileSys.getDir()
205  val _ = FileSys.chDir holmakedir
206  val uifile = fullPath [holmakedir, "basis2002.ui"]
207  val uofile = fullPath [holmakedir, "basis2002.uo"]
208  val smlfile = fullPath [holmakedir, "basis2002.sml"]
209  val rebuild_basis = not (canread uifile) orelse
210                      Time.>(modTime smlfile, modTime uifile)
211  val sigui = fullPath [sigobj, "basis2002.ui"]
212  val siguo = fullPath [sigobj, "basis2002.uo"]
213  val copy_basis = not (canread sigui) orelse not (canread siguo) orelse
214                   rebuild_basis orelse
215                   Time.>(modTime uifile, modTime sigui) orelse
216                   Time.>(modTime uofile, modTime siguo)
217in
218  print "Building basis2002 object code for Moscow ML 2.01 ";
219  if rebuild_basis then
220     (print "(compiling";
221      if Process.isSuccess
222             (systeml [compiler, "-c", "-toplevel", "basis2002.sml"])
223      then ()
224      else die "Couldn't compile basis2002.sml")
225  else print "(up-to-date";
226  if copy_basis then (print "; copying to sigobj)\n";
227                      app to_sigobj ["basis2002.ui", "basis2002.uo"])
228  else print ")\n";
229  FileSys.chDir dir_0
230end handle GetOut => ();
231
232(*---------------------------------------------------------------------------
233     Now compile Systeml.sml in tools/Holmake/
234 ---------------------------------------------------------------------------*)
235
236
237let
238  val _ = print "Compiling system specific functions ("
239  val modTime = FileSys.modTime
240  val dir_0 = FileSys.getDir()
241  val sigfile = fullPath [holmakedir, "Systeml.sig"]
242  val uifile = fullPath [holmakedir, "Systeml.ui"]
243  val basis_rebuild = let
244    val basisuifile = fullPath [holmakedir, "basis2002.ui"]
245  in
246    not have_basis2002 andalso
247    Time.>(modTime basisuifile, modTime sigfile)
248  end
249  val rebuild_sigfile =
250      not (canread uifile) orelse
251      Time.>(modTime sigfile, modTime uifile) orelse
252      (* if the ui in sigobj is too small to be a compiled mosml thing, it
253         is probably a Poly/ML thing from a previous installation. If it's
254         not there at all, we need to recompile and copy across too. *)
255      (FileSys.fileSize (fullPath [sigobj, "Systeml.ui"]) < 100
256       handle SysErr _ => true) orelse
257      basis_rebuild
258  fun die () = (print ")\nFailed to compile system-specific code\n";
259                Process.exit Process.failure)
260  val systeml = fn l =>
261                   if not (Process.isSuccess (systeml l)) then die() else ()
262in
263  FileSys.chDir holmakedir;
264  if rebuild_sigfile then
265    (systeml ([compiler, "-c"] @
266              (if have_basis2002 then [] else ["basis2002.ui"]) @
267              ["Systeml.sig"]);
268     app to_sigobj ["Systeml.sig", "Systeml.ui"];
269     print "sig ") else ();
270  systeml ([compiler, "-c"] @
271           (if have_basis2002 then [] else ["basis2002.ui"]) @
272           ["Systeml.sml"]);
273  to_sigobj "Systeml.uo";
274  print "sml)\n";
275  FileSys.chDir dir_0
276end;
277
278
279(*---------------------------------------------------------------------------
280          String and path operations.
281 ---------------------------------------------------------------------------*)
282
283fun echo s = (TextIO.output(TextIO.stdOut, s^"\n");
284              TextIO.flushOut TextIO.stdOut);
285
286val _ = echo "Beginning configuration.";
287
288(* ----------------------------------------------------------------------
289    remove the quotation filter from the bin directory, if it exists
290  ---------------------------------------------------------------------- *)
291
292val _ = let
293  val unquote = fullPath [holdir, "bin", xable_string "unquote"]
294in
295  if FileSys.access(unquote, [FileSys.A_READ]) then
296    (print "Removing old quotation filter from bin/\n";
297     FileSys.remove unquote
298     handle Interrupt => raise Interrupt
299          | _ => print "*** Tried to remove quotation filter from bin/ but \
300                       \couldn't!  Proceeding anyway.\n")
301  else ()
302end
303
304(* ----------------------------------------------------------------------
305    Compile our local copy of mllex
306   ---------------------------------------------------------------------- *)
307
308
309fun die s = (print s; print "\n"; Process.exit Process.failure)
310
311val _ = let
312  val _ = echo "Making tools/mllex/mllex.exe"
313  val cdir = FileSys.getDir()
314  val destdir = fullPath [holdir, "tools/mllex"]
315  val systeml = fn clist => if Process.isSuccess (systeml clist) then ()
316                            else die "Failed to build mllex"
317in
318  FileSys.chDir destdir;
319  systeml ([compiler, "-I", "../../sigobj", "-c", "-toplevel"] @
320           (if have_basis2002 then [] else ["basis2002.ui"]) @
321           ["mllex.sml"]);
322  systeml [compiler, "-c", "mllex.ui", "mosmlmain.sml"];
323  systeml [compiler, "-I", "../../sigobj", "-o", "mllex.exe", "mllex.uo",
324           "mosmlmain.uo"];
325  FileSys.chDir cdir
326end handle _ => die "Failed to build mllex.";
327
328
329(*---------------------------------------------------------------------------
330    Compile Holmake (bypassing the makefile in directory Holmake), then
331    put the executable bin/Holmake.
332 ---------------------------------------------------------------------------*)
333
334fun compile opts s =
335    if have_basis2002 then
336      Process.isSuccess (systeml ([compiler, "-c"] @ opts @ [s]))
337    else Process.isSuccess
338             (systeml ([compiler, "-c"] @ opts @ ["basis2002.ui", s]))
339
340
341val _ =
342 let val _ = echo "Making bin/Holmake."
343     val cdir      = FileSys.getDir()
344     val hmakedir  = normPath(Path.concat(holdir, "tools/Holmake"))
345     val _         = FileSys.chDir hmakedir
346     val bin       = fullPath [holdir,   "bin/Holmake"]
347     val mllex     = fullPath [holdir, "tools", "mllex", "mllex.exe"]
348     val systeml   = fn clist => if not (Process.isSuccess (systeml clist)) then
349                                   die "Holmake compilation failed."
350                                 else ()
351     fun link {extras,srcobj,tgt} = let
352       val pfx = if OS <> "winNT" then [compiler, "-standalone", "-o", tgt]
353                 else [compiler, "-o", tgt]
354       val b2002comp = if have_basis2002 then [] else ["basis2002.ui"]
355     in
356       systeml (pfx @ b2002comp @ extras @ [srcobj])
357     end
358  in
359    systeml [mllex, "QuoteFilter"];
360    compile [] "QuoteFilter.sml";
361    compile [] "QFRead.sig";
362    compile [] "QFRead.sml";
363    compile [] "FunctionalRecordUpdate.sml";
364    compile [] "GetOpt.sig";
365    compile [] "GetOpt.sml";
366    compile [] "HM_Core_Cline.sig";
367    compile [] "HM_Core_Cline.sml";
368    compile [] "Holdep_tokens.sig";
369    compile [] "Holdep_tokens.sml";
370    compile [] "holdeptool.sml";
371    compile [] "mosml_holdeptool.sml";
372    link{extras = [], srcobj = "mosml_holdeptool.uo",
373         tgt = fullPath[holdir, "bin", "holdeptool.exe"]};
374    compile ["-I", "mosml"] "Holdep.sig";
375    compile ["-I", "mosml"] "Holdep.sml";
376    compile [] "regexpMatch.sig";
377    compile [] "regexpMatch.sml";
378    compile [] "parse_glob.sig";
379    compile [] "parse_glob.sml";
380    compile [] "internal_functions.sig";
381    compile [] "internal_functions.sml";
382    compile [] "Holmake_tools_dtype.sml";
383    compile [] "holpathdb.sig";
384    compile [] "holpathdb.sml";
385    compile [] "Holmake_tools.sig";
386    compile [] "Holmake_tools.sml";
387    compile [] "Holmake_types.sig";
388    compile [] "Holmake_types.sml";
389    compile [] "ReadHMF.sig";
390    compile [] "ReadHMF.sml";
391    compile [] "HM_DepGraph.sig";
392    compile [] "HM_DepGraph.sml";
393    compile [] "HM_GraphBuildJ1.sig";
394    compile [] "HM_GraphBuildJ1.sml";
395    FileSys.chDir "mosml";
396    compile ["-I", ".."] "HM_Cline.sig";
397    compile ["-I", ".."] "HM_Cline.sml";
398    compile ["-I", ".."] "HM_BaseEnv.sig";
399    compile ["-I", ".."] "HM_BaseEnv.sml";
400    FileSys.chDir "..";
401    compile ["-I", "mosml"] "BuildCommand.sig";
402    FileSys.chDir "mosml";
403    compile ["-I", ".."] "BuildCommand.sml";
404    FileSys.chDir "..";
405    compile ["-I", "mosml"] "Holmake.sml";
406    compile [] "mosml_Holmake.sml";
407    link{extras = ["-I", "mosml"], tgt = bin, srcobj = "mosml_Holmake.uo"};
408    mk_xable bin;
409    FileSys.chDir cdir
410  end
411handle _ => (print "*** Couldn't build Holmake\n";
412             Process.exit Process.failure);
413
414(* ----------------------------------------------------------------------
415    Compile our local copy of mlyacc
416   ---------------------------------------------------------------------- *)
417
418val _ = let
419  val _ = echo "Making tooks/mlyacc/src/mlyacc.exe"
420  val cdir = FileSys.getDir()
421  val destdir = fullPath [holdir, "tools/mlyacc"]
422  val systeml = fn clist => if Process.isSuccess (systeml clist) then ()
423                            else die "Failed to build mlyacc"
424  val holmake = fullPath [holdir, "bin/Holmake"]
425in
426  FileSys.chDir destdir;
427  FileSys.chDir "mlyacclib";
428  systeml [holmake, "cleanAll"];
429  systeml [holmake, "all"];
430  FileSys.chDir "../src";
431  systeml [holmake, "cleanAll"];
432  systeml [holmake, "mlyacc.exe"];
433  FileSys.chDir cdir
434end
435
436(*---------------------------------------------------------------------------
437    Compile build.sml, and put it in bin/build.
438 ---------------------------------------------------------------------------*)
439
440val _ = let
441  open TextIO
442  val _ = echo "Making bin/build."
443  val cwd = FileSys.getDir()
444  val _ = FileSys.chDir (fullPath[holdir, "tools"])
445  (* cline stuff *)
446  val _ = if compile ["-I", holmakedir] "buildcline_dtype.sml" andalso
447             compile ["-I", holmakedir] "buildcline.sig" andalso
448             compile ["-I", holmakedir] "buildcline.sml"
449          then ()
450          else die "Failed to build buildcline module"
451  (* utils first *)
452  val _ = let
453    val utilsig = "buildutils.sig"
454    val utilsml = "buildutils.sml"
455  in
456    if compile ["-I", holmakedir] utilsig andalso
457       compile ["-I", holmakedir] utilsml
458    then ()
459    else die "Failed to build buildutils module"
460  end
461
462  val target = "build.sml"
463  val bin    = fullPath [holdir, "bin/build"]
464  val b2002p = if have_basis2002 then [] else ["basis2002.ui"]
465  val command =
466      [compiler, "-o", bin, "-I", holmakedir,
467       "-I", Path.concat(holmakedir, "mosml")] @
468      b2002p @ [target]
469in
470  if Process.isSuccess (systeml command) then ()
471  else (print "*** Failed to build build executable.\n";
472        Process.exit Process.failure) ;
473  FileSys.remove (fullPath [holdir,"tools/build.ui"]);
474  FileSys.remove (fullPath [holdir,"tools/build.uo"]);
475  mk_xable bin;
476  FileSys.chDir cwd
477end;
478
479
480(*---------------------------------------------------------------------------
481    Instantiate tools/hol-mode.src, and put it in tools/hol-mode.el
482 ---------------------------------------------------------------------------*)
483
484val _ =
485 let open TextIO
486     val _ = echo "Making hol-mode.el (for Emacs/XEmacs)"
487     val src = fullPath [holdir, "tools/hol-mode.src"]
488    val target = fullPath [holdir, "tools/hol-mode.el"]
489 in
490    fill_holes (src, target)
491      ["(defcustom hol-executable HOL-EXECUTABLE\n"
492        -->
493       ("(defcustom hol-executable \n  "^
494        quote (fullPath [holdir, "bin/hol"])^"\n"),
495       "(defcustom holmake-executable HOLMAKE-EXECUTABLE\n"
496        -->
497       ("(defcustom holmake-executable \n  "^
498        quote (fullPath [holdir, "bin/Holmake"])^"\n")]
499 end;
500
501
502(*---------------------------------------------------------------------------
503      Generate shell scripts for running HOL.
504 ---------------------------------------------------------------------------*)
505
506val _ =
507 let val _ = echo "Generating bin/hol."
508     val target      = fullPath [holdir, "bin/hol.bare"]
509     val qend        = fullPath [holdir, "tools/end-init.sml"]
510     val target_boss = fullPath [holdir, "bin/hol"]
511     val qend_boss   = fullPath [holdir, "tools/end-init-boss.sml"]
512 in
513   (* "unquote" scripts use the unquote executable to provide nice
514      handling of double-backquote characters *)
515   emit_hol_unquote_script target qend [];
516   emit_hol_unquote_script target_boss qend_boss []
517 end;
518
519val _ =
520 let val _ = echo "Generating bin/hol.noquote."
521     val target      = fullPath [holdir,   "bin/hol.bare.noquote"]
522     val target_boss = fullPath [holdir,   "bin/hol.noquote"]
523     val qend        = fullPath [holdir,   "tools/end-init.sml"]
524     val qend_boss   = fullPath [holdir,   "tools/end-init-boss.sml"]
525 in
526  emit_hol_script target qend [];
527  emit_hol_script target_boss qend_boss []
528 end;
529
530(* Remove Poly/HOL executables from bin, if they're there *)
531val _ = FileSys.remove (fullPath [holdir, "bin", "heapname"]) handle _ => ()
532val _ = FileSys.remove (fullPath [holdir, "bin", "buildheap"]) handle _ => ()
533
534
535(*---------------------------------------------------------------------------
536    Compile the quotation preprocessor used by bin/hol.unquote and
537    put it in bin/
538 ---------------------------------------------------------------------------*)
539
540val _ = let
541  val _ = print "Attempting to compile quote filter ... "
542  val tgt0 = fullPath [holdir, "tools/quote-filter/quote-filter"]
543  val tgt = fullPath [holdir, "bin/unquote"]
544  val cwd = FileSys.getDir()
545  val _ = FileSys.chDir (fullPath [holdir, "tools/quote-filter"])
546  val _ = systeml [fullPath [holdir, "bin/Holmake"], "cleanAll"]
547in
548  if Process.isSuccess (systeml [fullPath [holdir, "bin/Holmake"]]) then let
549      val instrm = BinIO.openIn tgt0
550      val ostrm = BinIO.openOut tgt
551      val v = BinIO.inputAll instrm
552    in
553      BinIO.output(ostrm, v);
554      BinIO.closeIn instrm;
555      BinIO.closeOut ostrm;
556      mk_xable tgt;
557      print "Quote-filter built\n"
558    end handle e => print "0.Quote-filter build failed (continuing anyway)\n"
559  else              print "1.Quote-filter build failed (continuing anyway)\n"
560  ;
561  FileSys.chDir cwd
562end
563
564(*---------------------------------------------------------------------------
565    Configure the muddy library.
566 ---------------------------------------------------------------------------*)
567
568local val CFLAGS =
569        case OS
570         of "linux"   => SOME " -Dunix -O3 -fPIC $(CINCLUDE)"
571          | "solaris" => SOME " -Dunix -O3 $(CINCLUDE)"
572          | "macosx"  => SOME " -Dunix -O3 $(CINCLUDE)"
573          |     _     => NONE
574      val DLLIBCOMP =
575        case OS
576         of "linux"   => SOME "ld -shared -o $@ $(COBJS) $(LIBS)"
577          | "solaris" => SOME "ld -G -B dynamic -o $@ $(COBJS) $(LIBS)"
578          | "macosx"  => SOME "gcc -bundle -flat_namespace -undefined suppress\
579                              \ -o $@ $(COBJS) $(LIBS)"
580          |    _      => NONE
581      val ALL =
582        if OS="linux" orelse OS="solaris" orelse OS="macosx"
583        then SOME " muddy.so"
584        else NONE
585in
586val _ =
587 let open TextIO
588     val _ = echo "Setting up the muddy library Makefile."
589     val src    = fullPath [holdir, "tools/makefile.muddy.src"]
590     val target = fullPath [holdir, "examples/muddy/muddyC/Makefile"]
591     val mosmlhome = Path.getParent mosmldir
592 in
593   case (CFLAGS, DLLIBCOMP, ALL) of
594     (SOME s1, SOME s2, SOME s3) => let
595       val (cflags, dllibcomp, all) = (s1, s2, s3)
596     in
597       fill_holes (src,target)
598       ["MOSMLHOME=\n"  -->  String.concat["MOSMLHOME=", mosmlhome,"\n"],
599        "CC=\n"         -->  String.concat["CC=", CC, "\n"],
600        "CFLAGS="       -->  String.concat["CFLAGS=",cflags,"\n"],
601        "all:\n"        -->  String.concat["all: ",all,"\n"],
602        "DLLIBCOMP"     -->  String.concat["\t", dllibcomp, "\n"]]
603     end
604   | _ =>  print (String.concat
605                  ["   Warning! (non-fatal):\n    The muddy package is not ",
606                   "expected to build in OS flavour ", quote OS, ".\n",
607                   "   On winNT, muddy will be installed from binaries.\n",
608                   "   End Warning.\n"])
609 end
610end; (* local *)
611
612val _ = print "\nFinished configuration!\n";
613