1open testutils 2 3val _ = tprint "Checking 'Holmake fooTheory' in subdir" 4 5val _ = OS.FileSys.chDir "subdir" 6 7val op++ = OS.Path.concat 8val result = 9 Systeml.systeml ([Globals.HOLDIR ++ "bin" ++ "Holmake"] @ 10 (if Systeml.ML_SYSNAME = "poly" then 11 ["--holstate", Globals.HOLDIR ++ "bin" ++ "hol.state0"] 12 else []) @ 13 ["fooTheory"]) 14 15val _ = if OS.Process.isSuccess result then 16 if OS.FileSys.access ("fooTheory.dat", [OS.FileSys.A_READ]) then 17 OK() 18 else die "fooTheory.dat doesn't exist" 19 else die "Holmake failed" 20