1open testutils 2val cd = OS.FileSys.chDir 3 4infix ++ 5fun p1 ++ p2 = OS.Path.concat(p1,p2) 6 7val _ = cd "dir"; 8 9val hm = Globals.HOLDIR ++ "bin" ++ "Holmake" 10 11val _ = Systeml.systeml [hm, "cleanAll"] 12 13fun pluckk P k l = 14 case l of 15 [] => NONE 16 | h::t => if P h then SOME (k h t) 17 else pluckk P (fn h' => fn t => k h' (h::t)) t 18fun pluck P l = pluckk P (fn h => fn t => (h, t)) l 19 20fun grep pats f = 21 let 22 val istrm = TextIO.openIn f 23 fun return b = (TextIO.closeIn istrm; b) 24 fun recurse pats = 25 case pats of 26 [] => return true 27 | _ => 28 let 29 fun checking () = 30 case TextIO.inputLine istrm of 31 NONE => return false 32 | SOME line => 33 (case pluck (fn p => String.isSubstring p line) pats of 34 NONE => checking() 35 | SOME (_, t) => recurse t) 36 in 37 checking() 38 end 39 in 40 recurse pats 41 end 42 43val pats = ["Couldn't find required output file: emptyTheory", 44 "Couldn't find required output file: noproductTheory"] 45 46val desc = "failing Holmake with empty/non-producing scripts" 47val holstate_sfx = ["--holstate", Globals.HOLDIR ++ "bin" ++ "hol.state0"] 48val _ = if Systeml.ML_SYSNAME = "poly" then 49 let 50 val _ = tprint ("Checking parallel "^desc) 51 val res = Systeml.systeml_out {outfile="make.log"} 52 ([hm, "--qof", "-k", "-j4"] @ 53 holstate_sfx) 54 in 55 if OS.Process.isSuccess res then die "Holmake succeeded incorrectly" 56 else if grep pats "make.log" then OK() 57 else die "Couldn't see 'Couldn't find required output' output" 58 end 59 else () 60 61val _ = tprint ("Checking sequential " ^ desc) 62val res = Systeml.systeml_out {outfile="make.log"} 63 ([hm, "--qof", "-k", "-j1"] @ 64 (if Systeml.ML_SYSNAME = "poly" then 65 holstate_sfx 66 else [])) 67 68val _ = if OS.Process.isSuccess res then die "Holmake succeeded incorrectly" 69 else if grep pats "make.log" then OK() 70 else die "Couldn't see 'Couldn't find required output' output" 71