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