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