Hi all, I'm writing some code to interact with an ACL2 [0] process. I'd like to be able to write a function test :: String -> IO Bool that will attempt to prove something by forking an ACL2 process and screen scraping its output, to see whether the conjecture was proved. The code below [1] is close: it launches the process, sends the conjecture to ACL2, and reads ACL2's output line-by-line until it finds "Proof succeeded" or "attempt has failed". This works well enough for the simple case, but there is a problem. In readACL2Answer, the code shouldn't have to check for success *and* failure, since the conditions are complementary. But if I change that code to check only for success, then it is possible (and indeed it happens every time) that if I send ACL2 a conjecture it can't prove, readACL2Answer blocks indefinitely -- and the print statements show that hWaitForInput has said there is more data on the Handle but hGetLine blocks trying to read it. The reason for this, as far as I can tell, is that there *is* more data -- a character, for example -- but no newline, so hGetLine blocks waiting for a newline. However, if I'm reading the BufferMode documentation [3] correctly, the fact that I've set my streams to LineBuffering should mitigate that scenario. Concretely, I know that ACL2 runs in a REPL and the last thing it prints is in fact an incomplete line -- "ACL2 !>". I'd rather not have to read every line character by character just to detect the uncommon case. Should I just do it character by character? Am I reading the BufferMode docs wrong, and if so, what is the correct interpretation? Is there better approach for the original problem I'm trying to solve? Thanks for reading this far. =] -- Denis [0] http://www.cs.utexas.edu/users/moore/acl2/ [1] import System.Process import System.IO type Proc = (Handle, Handle, Handle, ProcessHandle) testThm = test "(equal x x)" -- something acl2 can prove testBad = test "(equal x (not x))" -- something it can't -- | Pass a conjecture form to ACL2, attempt to prove it, and return a boolean -- indicating whether ACL2 was able to prove it. test :: String -> IO Bool test thm = do i@(stdin, _, _, pid) <- setUpACL2 success <- testProc i thm hPutStrLn stdin "(good-bye)" putStrLn "saying goodbye" exitCode <- waitForProcess pid case exitCode of ExitSuccess -> return success ExitFailure i -> error ("ACL2 bad exit code: " ++ show i) -- | Pass a conjecture vio the given process' input stream, and return whether -- it is proved. testProc :: Proc -> String -> IO Bool testProc i@(stdin, stdout, _, pid) thm = do hSetBuffering stdout LineBuffering hSetBuffering stdin LineBuffering success <- testInACL2 ("(thm " ++ thm ++ ")") i putStrLn "found success value" return success succeedRx = mkRegex "Proof succeeded[.]" failedRx = mkRegex "attempt has failed[.]" -- create acl2 process and return handles setUpACL2 :: IO Proc setUpACL2 = runInteractiveCommand "acl2" testInACL2 :: String -> Proc -> IO Bool testInACL2 str (pin, pout, perr, pid) = do putStrLn "printing to acl2..." hPutStrLn pin str putStrLn "getting acl2 result..." readACL2Answer pout -- | How long we should wait for ACL2 to start saying something. Five -- seconds, currently. readTimeout = 100 readACL2Answer :: Handle -> IO Bool -- I *should* be required *only* to check for *success* in the matchRegex -- statement below, instead of checking for success and failure. But if I do -- that, and the theorem to be proved fails, this function blocks indefinitely -- (at least I observe a much greater than 5 second wait period), even though -- it should only block for `readTimeout' milliseconds. I'm not sure why this -- is, but at least there is an acceptable workaround. readACL2Answer pout = hWaitForInput pout readTimeout >>= (\isReady -> if isReady then do putStrLn "getting line" line <- hGetLine pout putStrLn $ "read line: " ++ line -- Check for success or failure. case (matchRegex succeedRx line, matchRegex failedRx line) of (Nothing, Nothing) -> readACL2Answer pout (Nothing, Just _) -> return False (Just _, _) -> return True else do putStrLn "not ready" return False) [3] http://haskell.org/ghc/docs/latest/html/libraries/base-3.0.0.0/System-IO.htm...