1open HolKernel Parse boolLib testutils 2 3val _ = new_theory "phonytgt"; 4val op++ = OS.Path.concat 5 6val _ = let 7 val _ = tprint "Building output though all file exists" 8 val _ = OS.FileSys.chDir "test1" 9 val _ = OS.FileSys.remove "output" handle _ => () 10 val _ = Systeml.systeml [Systeml.HOLDIR ++ "bin" ++ "Holmake"] 11in 12 if OS.FileSys.access("output",[]) then OK() 13 else die "FAILED!" 14end 15 16val _ = OS.FileSys.chDir ".." 17 18val _ = save_thm("test1", TRUTH) 19 20val _ = let 21 val _ = tprint "Not building output as all file exists" 22 val _ = OS.FileSys.chDir "test2" 23 val _ = OS.FileSys.remove "output" handle _ => () 24 val _ = Systeml.systeml [Systeml.HOLDIR ++ "bin" ++ "Holmake"] 25in 26 if OS.FileSys.access("output",[]) then die "FAILED!" 27 else OK() 28end 29 30val _ = OS.FileSys.chDir ".." 31 32val _ = save_thm("test2", TRUTH) 33 34val _ = export_theory(); 35