1open testutils 2 3val hmstr = OS.Path.concat (Globals.HOLDIR, OS.Path.concat("bin", "Holmake")) 4val _ = OS.FileSys.chDir "testdir"; 5 6fun hm testname tgts test = 7 (tprint testname ; 8 Systeml.systeml (hmstr::"-q"::tgts); 9 if test() then OK() else die "FAILED!") 10 11fun present n = OS.FileSys.access(n, [OS.FileSys.A_READ]) 12 13fun delete n = OS.FileSys.remove n handle SysErr _ => () 14 15fun testscenario hm = 16 let 17 in 18 hm "Cleaning" ["-r", "cleanAll"] 19 (fn () => List.all (not o present) 20 ["foo", "bar", "master", 21 "simpleTheory.sig", "simpleTheory.sml"]); 22 hm "Default make builds foo/bar/master" [] 23 (fn () => List.all present ["foo", "bar", "master"]); 24 hm "Cleaning" ["cleanAll"] 25 (fn () => List.all (not o present) 26 ["foo", "simpleTheory.sig", "simpleTheory.sml"]); 27 hm "Explicit make foo builds all" ["foo"] 28 (fn () => List.all present ["foo", "simpleTheory.sig", 29 "simpleTheory.sml"]); 30 31 delete "simpleTheory.sml"; 32 33 hm "rm thy.sml; build; no change" [] 34 (fn () => not (present "simpleTheory.sml")); 35 36 hm "rm thy.sml; build foo; no change" ["foo"] 37 (fn () => not (present "simpleTheory.sml")); 38 39 hm "rm thy.sml; build thy.sig; no change" ["simpleTheory.sig"] 40 (fn () => not (present "simpleTheory.sml")); 41 42 hm "rm thy.sml; build thy.sml; builds it" ["simpleTheory.sml"] 43 (fn () => present "simpleTheory.sml"); 44 45 delete "simpleTheory.sml"; 46 hm "rm thy.sml; build thy.sig thy.sml; builds it" 47 ["simpleTheory.sig", "simpleTheory.sml"] 48 (fn () => present "simpleTheory.sml"); 49 50 delete "simpleTheory.sml"; 51 hm "rm thy.sml; build thy.sml thy.sig; builds it" 52 ["simpleTheory.sml", "simpleTheory.sig"] 53 (fn () => present "simpleTheory.sml") 54end 55 56val _ = testscenario hm 57val _ = testscenario 58 (fn s => fn tgts => fn f => hm (s^" (-j1)") ("-j1"::tgts) f) 59