{-# LANGUAGE NoImplicitPrelude #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RecordWildCards #-} module Felix.Provers ( Vampire , vampire , VampireTaskMode(..) , VampireStatus(..) , CanonicalAtpOutcome(..) , CanonicalAtpRejection(..) , VampireProtocolError(..) , classifyVampireProtocol , vampireStatusParser , TimeLimit(..) , MemoryLimit(..) , defaultTimeLimit , defaultMemoryLimit , ProverAnswer ( CounterSatisfiable , ContradictoryAxioms , Uncertain , Error ) , pattern Yes , ProverStream(..) , ProverOutputStream(..) , ProverProcessError(..) , VerificationDialect(..) , PreparedVerificationRequest , preparedVerificationDialect , preparedVerificationText , preparedVerificationBytes , preparedVerificationByteCount , preparedVerificationRequestId , PreparedTypedProverTask , prepareTypedProverTask , preparedTypedProverLogicalProblem , preparedTypedProverRequest , AcceptedVampireRun , acceptedVampireRequestId , provedVampireRun , runPreparedTypedProver , runPreparedTypedProverWithObserver , EffectiveJobs , effectiveJobs , effectiveJobsValue , selectEffectiveJobs , WorkPosition , workPosition , workPositionModuleOrdinal , workPositionLocalRequestOrdinal , VampireExecutor , VampireExecutorFault , VampireRequestOwner , VampireHandle , VampireTerminal(..) , renderVampireTerminalDiagnostic , VampireCompletion , vampireCompletionRequestId , vampireCompletionTerminal , AtpDuration , atpDurationNanoseconds , atpDurationFromNanoseconds , SlowAtpOutcome(..) , SlowAtpTask(..) , SlowAtpReport(..) , slowAtpOmittedTaskCount , slowAtpReportFromTasks , withVampireExecutor , withVampireExecutorUsingClock , withVampireRequestOwner , submitVampireRequest , awaitVampireRequest , awaitPreparedVampireRequest , cancelVampireRequest , runPreparedTypedProverWithExecutor , vampireExecutorSlowAtpReport ) where import Base import Felix.Checking.Authority qualified as Authority import Felix.Checking.Backend.Problem import Felix.Checking.Backend.Tptp import Control.Concurrent.STM ( STM , TBQueue , TMVar , TVar , atomically , check , modifyTVar' , newEmptyTMVarIO , newTBQueueIO , newTVarIO , orElse , readTMVar , readTBQueue , readTVar , readTVarIO , throwSTM , tryPutTMVar , tryReadTMVar , writeTBQueue , writeTVar ) import Control.Exception ( AsyncException , IOException , SomeException , displayException , fromException ) import Control.Exception qualified as Exception import Control.Monad (replicateM, unless, when) import Data.ByteString qualified as ByteString import Data.IntMap.Strict qualified as IntMap import Data.IORef ( IORef , atomicModifyIORef' , newIORef , readIORef , writeIORef ) import Data.Set qualified as Set import Data.Map.Strict qualified as Map import Data.Ord (Down(..)) import Data.Text qualified as Text import Data.Text.Encoding qualified as TextEncoding import Data.Text.Encoding.Error qualified as TextEncodingError import Numeric.Natural (Natural) import Felix.Report.Location (Location) import System.Exit (ExitCode(..)) import System.Posix.Signals (sigKILL, signalProcessGroup) import System.Posix.Types (ProcessGroupID) import System.Process ( CreateProcess(..) , ProcessHandle , StdStream(CreatePipe) , getPid , proc , waitForProcess , withCreateProcess ) import System.Timeout qualified as Timeout import Text.Megaparsec import Text.Megaparsec.Char qualified as Char import UnliftIO.Async ( async , cancel , concurrently , waitCatch , waitCatchSTM ) data Vampire = Vampire { vampireExecutable :: FilePath , vampireTimeLimit :: TimeLimit , vampireMemoryLimit :: MemoryLimit } deriving (Show, Eq) newtype TimeLimit = Seconds Word64 deriving (Show, Eq, Num) newtype MemoryLimit = Megabytes Word64 deriving (Show, Eq) defaultTimeLimit :: TimeLimit defaultTimeLimit = Seconds 10 defaultMemoryLimit :: MemoryLimit defaultMemoryLimit = Megabytes 5000 vampire :: FilePath -> TimeLimit -> MemoryLimit -> Vampire vampire = Vampire vampireArguments :: Vampire -> [String] vampireArguments Vampire{..} = [ "--input_syntax", "tptp" , "--mode", "casc" , "--time_limit", toSeconds vampireTimeLimit , "--memory_limit", toMegabytes vampireMemoryLimit , "--cores", "2" ] -- | A strictly positive invocation-local bound for module pipelines and -- top-level Vampire invocations. newtype EffectiveJobs = EffectiveJobs Int deriving (Show, Eq, Ord) effectiveJobs :: Int -> Maybe EffectiveJobs effectiveJobs amount | amount > 0 = Just (EffectiveJobs amount) | otherwise = Nothing effectiveJobsValue :: EffectiveJobs -> Int effectiveJobsValue (EffectiveJobs amount) = amount -- | Select the worker bound, with processor discovery injected for focused -- testing. Asynchronous cancellation is never mistaken for failed discovery. selectEffectiveJobs :: Maybe EffectiveJobs -> IO Int -> IO EffectiveJobs selectEffectiveJobs override detectProcessors = case override of Just selected -> pure selected Nothing -> do detectedResult <- Exception.try detectProcessors case detectedResult of Left detectionFailure | Just asynchronous <- (fromException detectionFailure :: Maybe AsyncException) -> Exception.throwIO asynchronous | otherwise -> fallback Right detectedRaw -> let detected = max 1 detectedRaw -- Two portfolio workers plus one module pipeline -- nominally consume about three logical CPUs. automaticJobs = max 1 ((detected + 1) `div` 3) in pure (EffectiveJobs automaticJobs) where fallback = pure (EffectiveJobs 1) -- | Stable runtime diagnostic position. It is deliberately separate from -- request, validation, cache, and mathematical identities. data WorkPosition = WorkPosition !Natural !Natural deriving (Show, Eq, Ord) workPosition :: Natural -> Natural -> WorkPosition workPosition = WorkPosition workPositionModuleOrdinal :: WorkPosition -> Natural workPositionModuleOrdinal (WorkPosition moduleOrdinal _localOrdinal) = moduleOrdinal workPositionLocalRequestOrdinal :: WorkPosition -> Natural workPositionLocalRequestOrdinal (WorkPosition _moduleOrdinal localOrdinal) = localOrdinal toSeconds :: TimeLimit -> String toSeconds (Seconds secs) = show secs toMegabytes :: MemoryLimit -> String toMegabytes (Megabytes mbs) = show mbs data VampireTaskMode = DirectTask | IndirectTask deriving (Show, Eq) data VampireStatus = StatusTheorem | StatusCounterSatisfiable | StatusContradictoryAxioms | StatusTimeout | StatusResourceOut | StatusGaveUp | StatusUnknown | UnsupportedStatus Text deriving (Show, Eq) data CanonicalAtpOutcome = Proved | Counterexample | ContradictoryInput | Indeterminate deriving (Show, Eq, Ord) -- | The closed non-accepting subset of canonical ATP outcomes. Protocol -- disagreement is represented separately from a semantic non-proof, while an -- accepting result is unrepresentable here. data CanonicalAtpRejection = RejectedCounterexample | RejectedContradictoryInput | RejectedIndeterminate deriving (Show, Eq) data VampireProtocolError = UnsuccessfulVampireExit ExitCode | UnsupportedVampireStatuses (Set Text) | MalformedVampireStatusLines (Set Text) | MissingVampireOutcome | ConflictingTerminalOutcomes (Set CanonicalAtpOutcome) deriving (Show, Eq) data CompleteCapturedStreams = CompleteCapturedStreams { completedStdout :: !Text , completedStderr :: !Text } deriving (Show, Eq) data CompletedTranscript = CompletedTranscript { completedExitCode :: !ExitCode , completedStreams :: !CompleteCapturedStreams } deriving (Show, Eq) data PartialCapturedStreams = PartialCapturedStreams { partialStdout :: !ByteString.ByteString , partialStderr :: !ByteString.ByteString } deriving (Eq) instance Show PartialCapturedStreams where showsPrec precedence PartialCapturedStreams{..} = showParen (precedence > applicationPrecedence) ( showString "PartialCapturedStreams " . shows ( ByteString.length partialStdout , ByteString.length partialStderr ) ) data BoundedBytes = BoundedBytes { boundedBytesOriginalCount :: !Int , boundedBytesRetained :: !ByteString.ByteString , boundedBytesTruncated :: !Bool } deriving (Eq) instance Show BoundedBytes where showsPrec precedence BoundedBytes{..} = showParen (precedence > applicationPrecedence) ( showString "BoundedBytes " . shows ( boundedBytesOriginalCount , ByteString.length boundedBytesRetained , boundedBytesTruncated ) ) data BoundedCapturedStreams = BoundedCapturedStreams { boundedStdout :: !BoundedBytes , boundedStderr :: !BoundedBytes } deriving (Show, Eq) data BoundedDiagnostic = BoundedDiagnostic { boundedDiagnosticSummary :: !Text , boundedDiagnosticStdout :: !BoundedBytes , boundedDiagnosticStderr :: !BoundedBytes } deriving (Show, Eq) -- | Classify parsed Vampire statuses without depending on stream or line order. classifyVampireProtocol :: VampireTaskMode -> ExitCode -> [VampireStatus] -> Either VampireProtocolError CanonicalAtpOutcome classifyVampireProtocol mode exitCode statuses = case exitCode of ExitFailure _ -> Left (UnsuccessfulVampireExit exitCode) ExitSuccess | not (Set.null unsupported) -> Left (UnsupportedVampireStatuses unsupported) | otherwise -> classifyOutcomes (Set.fromList [ outcome | status <- statuses , Just outcome <- [vampireStatusOutcome mode status] ]) where unsupported = Set.fromList [ status | UnsupportedStatus status <- statuses ] classifyOutcomes :: Set CanonicalAtpOutcome -> Either VampireProtocolError CanonicalAtpOutcome classifyOutcomes outcomes = case Set.toList terminalOutcomes of [] -> if Indeterminate `Set.member` outcomes then Right Indeterminate else Left MissingVampireOutcome [outcome] -> Right outcome _ -> Left (ConflictingTerminalOutcomes terminalOutcomes) where terminalOutcomes = Set.delete Indeterminate outcomes vampireStatusOutcome :: VampireTaskMode -> VampireStatus -> Maybe CanonicalAtpOutcome vampireStatusOutcome mode = \case StatusTheorem -> Just Proved StatusCounterSatisfiable -> Just Counterexample StatusContradictoryAxioms -> Just case mode of DirectTask -> ContradictoryInput IndirectTask -> Proved StatusTimeout -> Just Indeterminate StatusResourceOut -> Just Indeterminate StatusGaveUp -> Just Indeterminate StatusUnknown -> Just Indeterminate UnsupportedStatus{} -> Nothing data VerificationDialect = VerificationFof | VerificationTh0 deriving (Show, Eq) data PreparedVerificationRequest = PreparedVerificationRequest { preparedVerificationDialect :: !VerificationDialect , preparedVerificationMode :: !VampireTaskMode , preparedVerificationInput :: !ByteString.ByteString , preparedVerificationIdentity :: !Authority.PreparedRequestId } deriving (Eq) -- | Decode the one canonical serialized request only at a textual boundary. -- Prepared requests deliberately do not retain an equivalent 'Text' copy. preparedVerificationText :: PreparedVerificationRequest -> Text preparedVerificationText request = let encoded = preparedVerificationInput request withoutFinalNewline = case ByteString.unsnoc encoded of Just (body, 10) -> body _ -> encoded in TextEncoding.decodeUtf8 withoutFinalNewline preparedVerificationByteCount :: PreparedVerificationRequest -> Int preparedVerificationByteCount = ByteString.length . preparedVerificationInput preparedVerificationBytes :: PreparedVerificationRequest -> ByteString.ByteString preparedVerificationBytes = preparedVerificationInput preparedVerificationRequestId :: PreparedVerificationRequest -> Authority.PreparedRequestId preparedVerificationRequestId = preparedVerificationIdentity data PreparedTypedProverTask ref local origin global = PreparedTypedProverTask !(TypedProblem ref local origin global) !PreparedVerificationRequest prepareTypedProverTask :: (Ord local, Ord global) => VampireTaskMode -> TypedProblem ref local origin global -> Either (TypedTptpPreparationError local global) (PreparedTypedProverTask ref local origin global) prepareTypedProverTask mode problem = do prepared <- prepareTypedTptpProblem problem let dialect = case preparedTypedTptpRoute prepared of RouteFof -> VerificationFof RouteTh0 -> VerificationTh0 bytes = TextEncoding.encodeUtf8 (preparedTypedTptpTextNewline prepared) identity = Authority.preparedRequestId (case dialect of VerificationFof -> Authority.PreparedRequestFof VerificationTh0 -> Authority.PreparedRequestTh0) (case mode of DirectTask -> Authority.PreparedRequestDirect IndirectTask -> Authority.PreparedRequestIndirect) bytes preparedRequest = PreparedVerificationRequest { preparedVerificationDialect = dialect , preparedVerificationMode = mode , preparedVerificationInput = bytes , preparedVerificationIdentity = identity } pure (PreparedTypedProverTask problem preparedRequest) preparedTypedProverLogicalProblem :: PreparedTypedProverTask ref local origin global -> TypedProblem ref local origin global preparedTypedProverLogicalProblem (PreparedTypedProverTask problem _request) = problem preparedTypedProverRequest :: PreparedTypedProverTask ref local origin global -> PreparedVerificationRequest preparedTypedProverRequest (PreparedTypedProverTask _problem request) = request data AcceptedVampireRun = AcceptedVampireRun { acceptedVampireRequestId :: !Authority.PreparedRequestId } deriving (Eq) data ProverAnswer = ProvedAnswer AcceptedVampireRun | CounterSatisfiable Text | ContradictoryAxioms Text | Uncertain Text | Error Text Text deriving (Eq) pattern Yes :: ProverAnswer pattern Yes <- ProvedAnswer _ {-# COMPLETE Yes, CounterSatisfiable, ContradictoryAxioms, Uncertain, Error #-} instance Show ProverAnswer where showsPrec _ (ProvedAnswer _) = showString "Yes" showsPrec precedence (CounterSatisfiable task) = showParen (precedence > applicationPrecedence) (showString "CounterSatisfiable " . showsPrec (applicationPrecedence + 1) task) showsPrec precedence (ContradictoryAxioms task) = showParen (precedence > applicationPrecedence) (showString "ContradictoryAxioms " . showsPrec (applicationPrecedence + 1) task) showsPrec precedence (Uncertain task) = showParen (precedence > applicationPrecedence) (showString "Uncertain " . showsPrec (applicationPrecedence + 1) task) showsPrec precedence (Error errorLabel message) = showParen (precedence > applicationPrecedence) (showString "Error " . showsPrec (applicationPrecedence + 1) errorLabel . showChar ' ' . showsPrec (applicationPrecedence + 1) message) provedVampireRun :: ProverAnswer -> Maybe AcceptedVampireRun provedVampireRun = \case ProvedAnswer accepted -> Just accepted CounterSatisfiable{} -> Nothing ContradictoryAxioms{} -> Nothing Uncertain{} -> Nothing Error{} -> Nothing applicationPrecedence :: Int applicationPrecedence = 10 data ProverStream = ProverStdin | ProverStdout | ProverStderr deriving (Show, Eq) data ProverOutputStream = ProverOutputStdout | ProverOutputStderr deriving (Show, Eq) data ProverProcessError = ProverLaunchFailed !FilePath !Text | ProverCommunicationFailed !FilePath !ProverStream !Text | ProverOutputMalformedUtf8 !FilePath !ProverOutputStream !Text | ProverTimedOut !FilePath !TimeLimit !BoundedCapturedStreams | ProverOutputLimitExceeded !FilePath !ProverOutputStream !BoundedCapturedStreams | ProverTerminatedBySignal !FilePath !Int !BoundedCapturedStreams | ProverLifecycleFailed !FilePath !Text deriving (Show, Eq) data SupervisorAbort = SupervisorCommunicationFailed !ProverStream !Text | SupervisorOutputLimitExceeded !ProverOutputStream | SupervisorLifecycleFailed !Text deriving (Show) instance Exception.Exception SupervisorAbort data CaptureBuffer = CaptureBuffer { captureByteCount :: !Int , captureChunksReversed :: ![ByteString.ByteString] } vampireOutputByteLimit :: Int vampireOutputByteLimit = 16 * 1024 * 1024 vampireWallGraceSeconds :: Integer vampireWallGraceSeconds = 2 captureChunkSize :: Int captureChunkSize = 32 * 1024 runPreparedTypedProver :: Vampire -> PreparedTypedProverTask ref local origin global -> IO (Either ProverProcessError ProverAnswer) runPreparedTypedProver vampireCommand = runPreparedTypedProverWithObserver (\_request -> pure ()) vampireCommand runPreparedTypedProverWithObserver :: (PreparedVerificationRequest -> IO ()) -> Vampire -> PreparedTypedProverTask ref local origin global -> IO (Either ProverProcessError ProverAnswer) runPreparedTypedProverWithObserver observer vampireCommand (PreparedTypedProverTask _problem preparedRequest) = do terminal <- runPreparedVerificationTerminal observer vampireCommand preparedRequest completionProverResult preparedRequest (VampireCompletion (preparedVerificationRequestId preparedRequest) terminal) -- | Invocation-local bounded owner of Vampire subprocesses. The finite queue -- carries only immutable prepared bytes plus runtime diagnostic position; -- checker builders and typed tasks never cross this boundary. data VampireExecutor = VampireExecutor { executorQueue :: !(TBQueue ExecutorJob) , executorState :: !(TVar VampireExecutorState) , executorNextHandle :: !(TVar Int) , executorCommand :: !Vampire , executorRequestObserver :: !(WorkPosition -> PreparedVerificationRequest -> IO ()) , executorMonotonicClock :: !(IO Word64) , executorSlowAtpAccumulator :: !(TVar SlowAtpAccumulator) } data ExecutorJob = ExecutorJob { executorJobPosition :: !WorkPosition , executorJobLocation :: !Location , executorJobRequest :: !PreparedVerificationRequest , executorJobCancelled :: !(TVar Bool) , executorJobStarted :: !(TVar Bool) , executorJobCompletion :: !(TMVar VampireCompletion) } data VampireExecutorState = ExecutorRunning | ExecutorClosing | ExecutorFaulted !VampireExecutorFault -- | A global executor fault is distinct from one request's declared process -- or protocol outcome. Its bounded message carries no process transcript. newtype VampireExecutorFault = VampireExecutorFault Text deriving (Show) instance Exception.Exception VampireExecutorFault data VampireRequestOwner = VampireRequestOwner { requestOwnerExecutor :: !VampireExecutor , requestOwnerState :: !(TVar VampireRequestOwnerState) } data VampireRequestOwnerState = RequestOwnerOpen !(IntMap VampireHandle) | RequestOwnerClosed -- | An opaque, owner-scoped completion handle. It deliberately retains no -- prepared request, command, transcript, builder, or parser state. data VampireHandle = VampireHandle { vampireHandleOrdinal :: !Int , vampireHandleOwner :: !VampireRequestOwner , vampireHandleRequestId :: !Authority.PreparedRequestId , vampireHandleCancelled :: !(TVar Bool) , vampireHandleStarted :: !(TVar Bool) , vampireHandleCompletion :: !(TMVar VampireCompletion) } data VampireTerminal = VampireAccepted | VampireRejected !CanonicalAtpRejection !BoundedDiagnostic | VampireProtocolFailed !BoundedDiagnostic | VampireProcessFailed !ProverProcessError | VampireCancelled deriving (Show, Eq) data VampireCompletion = VampireCompletion { vampireCompletionRequestId :: !Authority.PreparedRequestId , vampireCompletionTerminal :: !VampireTerminal } deriving (Show, Eq) -- | Monotonic executor wall time in nanoseconds. newtype AtpDuration = AtpDuration Word64 deriving (Show, Eq, Ord) atpDurationNanoseconds :: AtpDuration -> Word64 atpDurationNanoseconds (AtpDuration nanoseconds) = nanoseconds atpDurationFromNanoseconds :: Word64 -> AtpDuration atpDurationFromNanoseconds = AtpDuration data SlowAtpOutcome = SlowAtpAccepted | SlowAtpRejected !CanonicalAtpRejection | SlowAtpProtocolFailed | SlowAtpProcessFailed deriving (Show, Eq) data SlowAtpTask = SlowAtpTask { slowAtpDuration :: !AtpDuration , slowAtpOutcome :: !SlowAtpOutcome , slowAtpPosition :: !WorkPosition , slowAtpLocation :: !Location , slowAtpRequestId :: !Authority.PreparedRequestId } deriving (Show, Eq) data SlowAtpReport = SlowAtpReport { slowAtpQualifyingTaskCount :: !Int , slowAtpTasks :: ![SlowAtpTask] } deriving (Show, Eq) slowAtpOmittedTaskCount :: SlowAtpReport -> Int slowAtpOmittedTaskCount report = slowAtpQualifyingTaskCount report - length (slowAtpTasks report) data SlowAtpRank = SlowAtpRank !AtpDuration !(Down WorkPosition) deriving (Eq, Ord) data SlowAtpAccumulator = SlowAtpAccumulator { slowAtpAccumulatorQualifyingTaskCount :: !Int , slowAtpAccumulatorRetained :: !(Map.Map SlowAtpRank SlowAtpTask) } slowAtpThreshold :: AtpDuration slowAtpThreshold = AtpDuration 5000000000 slowAtpRetainedLimit :: Int slowAtpRetainedLimit = 12 emptySlowAtpAccumulator :: SlowAtpAccumulator emptySlowAtpAccumulator = SlowAtpAccumulator 0 Map.empty recordSlowAtpTask :: SlowAtpTask -> SlowAtpAccumulator -> SlowAtpAccumulator recordSlowAtpTask task accumulator | slowAtpDuration task < slowAtpThreshold = accumulator | otherwise = accumulator { slowAtpAccumulatorQualifyingTaskCount = slowAtpAccumulatorQualifyingTaskCount accumulator + 1 , slowAtpAccumulatorRetained = bounded } where rank = SlowAtpRank (slowAtpDuration task) (Down (slowAtpPosition task)) inserted = Map.insert rank task (slowAtpAccumulatorRetained accumulator) bounded | Map.size inserted > slowAtpRetainedLimit = Map.deleteMin inserted | otherwise = inserted finalizeSlowAtpReport :: SlowAtpAccumulator -> SlowAtpReport finalizeSlowAtpReport accumulator = SlowAtpReport { slowAtpQualifyingTaskCount = slowAtpAccumulatorQualifyingTaskCount accumulator , slowAtpTasks = snd <$> Map.toDescList (slowAtpAccumulatorRetained accumulator) } -- | Pure report construction used by policy tests and the executor. slowAtpReportFromTasks :: [SlowAtpTask] -> SlowAtpReport slowAtpReportFromTasks = finalizeSlowAtpReport . foldl' (flip recordSlowAtpTask) emptySlowAtpAccumulator renderVampireTerminalDiagnostic :: VampireTerminal -> Maybe Text renderVampireTerminalDiagnostic = \case VampireAccepted -> Nothing VampireRejected _rejection diagnostic -> Just (renderBoundedDiagnostic diagnostic) VampireProtocolFailed diagnostic -> Just (renderBoundedDiagnostic diagnostic) VampireProcessFailed processFailure -> Just (Text.pack (show processFailure)) VampireCancelled -> Nothing data VampireExecutorClosed = VampireExecutorClosed deriving (Show) instance Exception.Exception VampireExecutorClosed data VampireRequestOwnerClosed = VampireRequestOwnerClosed deriving (Show) instance Exception.Exception VampireRequestOwnerClosed data RequestObserverFailure = RequestObserverFailure SomeException instance Show RequestObserverFailure where show (RequestObserverFailure observerError) = "request observer failed: " <> displayException observerError instance Exception.Exception RequestObserverFailure -- | Bracket exactly the selected number of workers. Cancelling the bracket -- cancels each worker; a worker owning a subprocess in turn terminates and -- reaps that process group through the ordinary supervisor boundary. withVampireExecutor :: EffectiveJobs -> Vampire -> (WorkPosition -> PreparedVerificationRequest -> IO ()) -> (VampireExecutor -> IO value) -> IO value withVampireExecutor selected command observer action = withVampireExecutorUsingClock getMonotonicTimeNSec selected command observer action -- | Executor constructor with an injected monotonic clock for focused timing -- policy tests. Production callers use 'withVampireExecutor'. withVampireExecutorUsingClock :: IO Word64 -> EffectiveJobs -> Vampire -> (WorkPosition -> PreparedVerificationRequest -> IO ()) -> (VampireExecutor -> IO value) -> IO value withVampireExecutorUsingClock clock selected command observer action = Exception.bracket acquire release (action . fst) where workerCount = effectiveJobsValue selected acquire = do queue <- newTBQueueIO (fromIntegral workerCount * 2) state <- newTVarIO ExecutorRunning nextHandle <- newTVarIO 0 slowTasks <- newTVarIO emptySlowAtpAccumulator let executor = VampireExecutor { executorQueue = queue , executorState = state , executorNextHandle = nextHandle , executorCommand = command , executorRequestObserver = observer , executorMonotonicClock = clock , executorSlowAtpAccumulator = slowTasks } workers <- replicateM workerCount (async (superviseExecutorWorker executor)) pure (executor, workers) release (executor, workers) = do atomically do state <- readTVar (executorState executor) case state of ExecutorRunning -> writeTVar (executorState executor) ExecutorClosing ExecutorClosing -> pure () ExecutorFaulted{} -> pure () traverse_ cancel workers traverse_ waitCatch workers -- | Bracket the complete set of handles submitted by one module pipeline. -- Normal early return, failure, and asynchronous cancellation all cancel and -- reap the remaining owned work before the scope is left. withVampireRequestOwner :: VampireExecutor -> (VampireRequestOwner -> IO value) -> IO value withVampireRequestOwner executor = Exception.bracket acquire release where acquire = VampireRequestOwner executor <$> newTVarIO (RequestOwnerOpen IntMap.empty) release owner = Exception.mask_ do handles <- atomically do state <- readTVar (requestOwnerState owner) case state of RequestOwnerClosed -> pure [] RequestOwnerOpen owned -> do writeTVar (requestOwnerState owner) RequestOwnerClosed pure (IntMap.elems owned) traverse_ signalVampireCancellation handles traverse_ awaitVampireCancellation handles traverse_ deregisterVampireHandle handles runPreparedTypedProverWithExecutor :: VampireRequestOwner -> WorkPosition -> Location -> PreparedTypedProverTask ref local origin global -> IO (Either ProverProcessError ProverAnswer) runPreparedTypedProverWithExecutor owner position location (PreparedTypedProverTask _problem preparedRequest) = do handle <- submitVampireRequest owner position location preparedRequest awaitPreparedVampireRequest preparedRequest handle `Exception.onException` cancelVampireRequest handle vampireExecutorSlowAtpReport :: VampireExecutor -> IO SlowAtpReport vampireExecutorSlowAtpReport executor = finalizeSlowAtpReport <$> readTVarIO (executorSlowAtpAccumulator executor) submitVampireRequest :: VampireRequestOwner -> WorkPosition -> Location -> PreparedVerificationRequest -> IO VampireHandle submitVampireRequest owner position location request = do -- Force the compact queue payload before masked ownership acquisition. _ <- Exception.evaluate (preparedVerificationByteCount request) _ <- Exception.evaluate (preparedVerificationRequestId request) Exception.mask_ do cancelled <- newTVarIO False started <- newTVarIO False completion <- newEmptyTMVarIO let executor = requestOwnerExecutor owner handle <- atomically do executorStatus <- readTVar (executorState executor) case executorStatus of ExecutorClosing -> throwSTM VampireExecutorClosed ExecutorFaulted fault -> throwSTM fault ExecutorRunning -> pure () ownerStatus <- readTVar (requestOwnerState owner) owned <- case ownerStatus of RequestOwnerClosed -> throwSTM VampireRequestOwnerClosed RequestOwnerOpen current -> pure current ordinal <- readTVar (executorNextHandle executor) writeTVar (executorNextHandle executor) (ordinal + 1) let acquired = VampireHandle { vampireHandleOrdinal = ordinal , vampireHandleOwner = owner , vampireHandleRequestId = preparedVerificationRequestId request , vampireHandleCancelled = cancelled , vampireHandleStarted = started , vampireHandleCompletion = completion } job = ExecutorJob { executorJobPosition = position , executorJobLocation = location , executorJobRequest = request , executorJobCancelled = cancelled , executorJobStarted = started , executorJobCompletion = completion } writeTBQueue (executorQueue executor) job writeTVar (requestOwnerState owner) (RequestOwnerOpen (IntMap.insert ordinal acquired owned)) pure acquired pure handle awaitVampireRequest :: VampireHandle -> IO VampireCompletion awaitVampireRequest handle = Exception.mask \restore -> do let executor = requestOwnerExecutor (vampireHandleOwner handle) completion <- restore (atomically do executorStatus <- readTVar (executorState executor) case executorStatus of ExecutorFaulted fault -> throwSTM fault ExecutorRunning -> readTMVar (vampireHandleCompletion handle) ExecutorClosing -> (readTMVar (vampireHandleCompletion handle)) `orElse` throwSTM VampireExecutorClosed) deregisterVampireHandle handle pure completion -- | Await one already submitted request and recover the ordinary typed -- prover result. The supplied immutable request is checked against every -- completion before any caller may interpret its terminal outcome. awaitPreparedVampireRequest :: PreparedVerificationRequest -> VampireHandle -> IO (Either ProverProcessError ProverAnswer) awaitPreparedVampireRequest request handle = awaitVampireRequest handle >>= completionProverResult request cancelVampireRequest :: VampireHandle -> IO () cancelVampireRequest handle = Exception.mask_ do signalVampireCancellation handle awaitVampireCancellation handle deregisterVampireHandle handle signalVampireCancellation :: VampireHandle -> IO () signalVampireCancellation handle = do let completion = VampireCompletion (vampireHandleRequestId handle) VampireCancelled _ <- Exception.evaluate completion atomically do writeTVar (vampireHandleCancelled handle) True started <- readTVar (vampireHandleStarted handle) unless started (void (publishVampireTerminalSTM (vampireHandleCompletion handle) completion)) awaitVampireCancellation :: VampireHandle -> IO () awaitVampireCancellation handle = -- A running worker acknowledges ordinary cancellation only after -- terminating and reaping its owned process group. After a global fault, -- the worker lifecycle flag is the acknowledgement because the terminal -- cell deliberately remains subordinate to that fault. atomically do executorStatus <- readTVar (executorState (requestOwnerExecutor (vampireHandleOwner handle))) case executorStatus of ExecutorFaulted{} -> do stillRunning <- readTVar (vampireHandleStarted handle) check (not stillRunning) _ -> void (readTMVar (vampireHandleCompletion handle)) deregisterVampireHandle :: VampireHandle -> IO () deregisterVampireHandle handle = atomically do let owner = vampireHandleOwner handle state <- readTVar (requestOwnerState owner) case state of RequestOwnerClosed -> pure () RequestOwnerOpen owned -> writeTVar (requestOwnerState owner) (RequestOwnerOpen (IntMap.delete (vampireHandleOrdinal handle) owned)) superviseExecutorWorker :: VampireExecutor -> IO () superviseExecutorWorker executor = do result <- Exception.try (executorWorker executor) case result of Right () -> pure () Left workerFailure -> do state <- readTVarIO (executorState executor) case state of ExecutorRunning -> recordExecutorFault executor workerFailure ExecutorClosing -> pure () ExecutorFaulted{} -> pure () recordExecutorFault :: VampireExecutor -> SomeException -> IO () recordExecutorFault executor workerFailure = atomically do state <- readTVar (executorState executor) case state of ExecutorRunning -> writeTVar (executorState executor) (ExecutorFaulted (VampireExecutorFault (boundedText (Text.pack (displayException workerFailure))))) ExecutorClosing -> pure () ExecutorFaulted{} -> pure () executorWorker :: VampireExecutor -> IO () executorWorker executor = do next <- atomically do state <- readTVar (executorState executor) case state of ExecutorRunning -> Just <$> readTBQueue (executorQueue executor) ExecutorClosing -> pure Nothing ExecutorFaulted{} -> pure Nothing case next of Nothing -> pure () Just job -> do shouldRun <- atomically do completed <- tryReadTMVar (executorJobCompletion job) case completed of Just _ -> pure False Nothing -> do writeTVar (executorJobStarted job) True pure True when shouldRun (executeJob executor job `Exception.finally` atomically (writeTVar (executorJobStarted job) False)) executorWorker executor data JobWait value = JobFinished !(Either SomeException value) | JobCancelled | JobExecutorStopped executeJob :: VampireExecutor -> ExecutorJob -> IO () executeJob executor job = Exception.mask \restore -> do running <- async (restore (timedExecutorRun executor job)) waited <- restore (atomically (do state <- readTVar (executorState executor) case state of ExecutorRunning -> (JobFinished <$> waitCatchSTM running) `orElse` (do cancelled <- readTVar (executorJobCancelled job) check cancelled pure JobCancelled) ExecutorClosing -> pure JobExecutorStopped ExecutorFaulted{} -> pure JobExecutorStopped)) `Exception.onException` (cancel running >> void (waitCatch running)) case waited of JobFinished result -> case result of Left workerFailure -> Exception.throwIO workerFailure Right terminal -> publishVampireTerminal (preparedVerificationRequestId (executorJobRequest job)) (executorJobCompletion job) terminal JobCancelled -> do cancel running void (waitCatch running) publishVampireTerminal (preparedVerificationRequestId (executorJobRequest job)) (executorJobCompletion job) VampireCancelled JobExecutorStopped -> do cancel running void (waitCatch running) timedExecutorRun :: VampireExecutor -> ExecutorJob -> IO VampireTerminal timedExecutorRun executor job = Exception.mask \restore -> do started <- executorMonotonicClock executor terminal <- restore (runPreparedVerificationTerminal (executorRequestObserver executor (executorJobPosition job)) (executorCommand executor) (executorJobRequest job)) finished <- executorMonotonicClock executor let task = SlowAtpTask { slowAtpDuration = AtpDuration (finished - started) , slowAtpOutcome = slowAtpOutcomeFromTerminal terminal , slowAtpPosition = executorJobPosition job , slowAtpLocation = executorJobLocation job , slowAtpRequestId = preparedVerificationRequestId (executorJobRequest job) } atomically (modifyTVar' (executorSlowAtpAccumulator executor) (recordSlowAtpTask task)) pure terminal slowAtpOutcomeFromTerminal :: VampireTerminal -> SlowAtpOutcome slowAtpOutcomeFromTerminal = \case VampireAccepted -> SlowAtpAccepted VampireRejected rejection _diagnostic -> SlowAtpRejected rejection VampireProtocolFailed{} -> SlowAtpProtocolFailed VampireProcessFailed{} -> SlowAtpProcessFailed VampireCancelled -> impossible "cancelled Vampire task was recorded as completed" publishVampireTerminal :: Authority.PreparedRequestId -> TMVar VampireCompletion -> VampireTerminal -> IO () publishVampireTerminal requestId completionCell terminal = do let completion = VampireCompletion requestId terminal _ <- Exception.evaluate completion void (atomically (publishVampireTerminalSTM completionCell completion)) publishVampireTerminalSTM :: TMVar VampireCompletion -> VampireCompletion -> STM Bool publishVampireTerminalSTM = tryPutTMVar runPreparedVerificationTerminal :: (PreparedVerificationRequest -> IO ()) -> Vampire -> PreparedVerificationRequest -> IO VampireTerminal runPreparedVerificationTerminal observer command request = do transcriptResult <- runPreparedVampireProcessWithObserver observer command request pure case transcriptResult of Left processFailure -> VampireProcessFailed processFailure Right transcript -> case classifyVampireCompleted (preparedVerificationMode request) transcript of Left protocolFailure -> VampireProtocolFailed (boundedTranscriptDiagnostic (Text.pack (show protocolFailure)) transcript) Right Proved -> VampireAccepted Right Counterexample -> VampireRejected RejectedCounterexample (boundedTranscriptDiagnostic "Vampire found a countermodel" transcript) Right ContradictoryInput -> VampireRejected RejectedContradictoryInput (boundedTranscriptDiagnostic "Vampire reported contradictory input" transcript) Right Indeterminate -> VampireRejected RejectedIndeterminate (boundedTranscriptDiagnostic "Vampire did not establish the obligation" transcript) completionProverResult :: PreparedVerificationRequest -> VampireCompletion -> IO (Either ProverProcessError ProverAnswer) completionProverResult request completion = do unless (actualId == expectedId) (Exception.throwIO (VampireExecutorFault "Vampire completion has the wrong request id")) case vampireCompletionTerminal completion of VampireAccepted -> pure (Right (ProvedAnswer (AcceptedVampireRun actualId))) VampireRejected rejection _diagnostic -> pure (Right (case rejection of RejectedCounterexample -> CounterSatisfiable task RejectedContradictoryInput -> ContradictoryAxioms task RejectedIndeterminate -> Uncertain task)) VampireProtocolFailed diagnostic -> pure (Right (Error "typed obligation" (renderBoundedDiagnostic diagnostic))) VampireProcessFailed processFailure -> pure (Left processFailure) VampireCancelled -> Exception.throwIO (VampireExecutorFault "active admission encountered a cancelled Vampire request") where expectedId = preparedVerificationRequestId request actualId = vampireCompletionRequestId completion task = preparedVerificationText request runPreparedVampireProcessWithObserver :: (PreparedVerificationRequest -> IO ()) -> Vampire -> PreparedVerificationRequest -> IO (Either ProverProcessError CompletedTranscript) runPreparedVampireProcessWithObserver observer vampireCommand@Vampire{vampireExecutable = executable} preparedRequest = do callbackStarted <- newIORef False processResult <- Exception.try (withCreateProcess (proc executable (vampireArguments vampireCommand)) { std_in = CreatePipe , std_out = CreatePipe , std_err = CreatePipe , create_group = True } \mIn mOut mErr processHandle -> Exception.mask \restore -> do writeIORef callbackStarted True case (mIn, mOut, mErr) of (Just inputHandle, Just outputHandle, Just errorHandle) -> do maybePid <- getPid processHandle processGroup <- case maybePid of Just pid -> pure (fromIntegral pid) Nothing -> impossible "Vampire supervisor: missing process-group id" restore (do runRequestObserver observer preparedRequest superviseVampireProcess executable (vampireTimeLimit vampireCommand) preparedRequest inputHandle outputHandle errorHandle processGroup processHandle) `Exception.onException` forceTerminateProcessGroup processGroup processHandle _ -> impossible "Vampire supervisor: expected CreatePipe handles") :: IO (Either SomeException (Either ProverProcessError CompletedTranscript)) case processResult of Right result -> pure result Left err | Just (RequestObserverFailure observerFailure) <- fromException err -> Exception.throwIO observerFailure | Just asynchronous <- (fromException err :: Maybe AsyncException) -> Exception.throwIO asynchronous | Just ioFailure <- (fromException err :: Maybe IOException) -> do started <- readIORef callbackStarted pure (Left (if started then ProverLifecycleFailed executable (boundedText (exceptionText ioFailure)) else ProverLaunchFailed executable (boundedText (exceptionText ioFailure)))) | otherwise -> Exception.throwIO err runRequestObserver :: (PreparedVerificationRequest -> IO ()) -> PreparedVerificationRequest -> IO () runRequestObserver observer request = observer request `Exception.catch` \observerError -> case fromException observerError :: Maybe AsyncException of Just asynchronous -> Exception.throwIO asynchronous Nothing -> Exception.throwIO (RequestObserverFailure observerError) superviseVampireProcess :: FilePath -> TimeLimit -> PreparedVerificationRequest -> Handle -> Handle -> Handle -> ProcessGroupID -> ProcessHandle -> IO (Either ProverProcessError CompletedTranscript) superviseVampireProcess executable timeLimit preparedRequest inputHandle outputHandle errorHandle processGroup processHandle = do stdoutCapture <- newIORef emptyCaptureBuffer stderrCapture <- newIORef emptyCaptureBuffer let terminateOwnedProcess = forceTerminateProcessGroup processGroup processHandle communicate = communicateWithVampire preparedRequest inputHandle outputHandle errorHandle stdoutCapture stderrCapture processHandle supervised <- Timeout.timeout (wallTimeoutMicroseconds timeLimit) (Exception.try communicate :: IO (Either SupervisorAbort ExitCode)) case supervised of Nothing -> do terminateOwnedProcess partial <- capturedStreams stdoutCapture stderrCapture pure (Left (ProverTimedOut executable timeLimit (boundedCapturedStreams partial))) Just (Left abort) -> do terminateOwnedProcess partial <- capturedStreams stdoutCapture stderrCapture pure (Left (supervisorAbortError executable partial abort)) Just (Right exitCode) -> do terminateRemainingProcessGroup processGroup partial <- capturedStreams stdoutCapture stderrCapture case exitCode of ExitFailure signalCode | signalCode < 0 -> pure (Left (ProverTerminatedBySignal executable (negate signalCode) (boundedCapturedStreams partial))) _ -> pure do stdout <- decodeOutput executable ProverOutputStdout (partialStdout partial) stderr <- decodeOutput executable ProverOutputStderr (partialStderr partial) Right CompletedTranscript { completedExitCode = exitCode , completedStreams = CompleteCapturedStreams { completedStdout = stdout , completedStderr = stderr } } communicateWithVampire :: PreparedVerificationRequest -> Handle -> Handle -> Handle -> IORef CaptureBuffer -> IORef CaptureBuffer -> ProcessHandle -> IO ExitCode communicateWithVampire preparedRequest inputHandle outputHandle errorHandle stdoutCapture stderrCapture processHandle = do _ <- concurrently (concurrently (captureCommunication ProverStdin (ByteString.hPut inputHandle (preparedVerificationInput preparedRequest) `Exception.finally` hClose inputHandle)) (captureOutput ProverOutputStdout outputHandle stdoutCapture)) (captureOutput ProverOutputStderr errorHandle stderrCapture) captureLifecycle (waitForProcess processHandle) captureCommunication :: ProverStream -> IO a -> IO a captureCommunication stream action = action `Exception.catch` \(err :: IOException) -> throwIO (SupervisorCommunicationFailed stream (exceptionText err)) captureOutput :: ProverOutputStream -> Handle -> IORef CaptureBuffer -> IO () captureOutput stream handle capture = captureCommunication (outputStream stream) go where go = do bytes <- ByteString.hGetSome handle captureChunkSize if ByteString.null bytes then pure () else do exceeded <- appendCapturedChunk capture bytes if exceeded then throwIO (SupervisorOutputLimitExceeded stream) else go outputStream :: ProverOutputStream -> ProverStream outputStream = \case ProverOutputStdout -> ProverStdout ProverOutputStderr -> ProverStderr captureLifecycle :: IO a -> IO a captureLifecycle action = action `Exception.catch` \(err :: IOException) -> throwIO (SupervisorLifecycleFailed (exceptionText err)) emptyCaptureBuffer :: CaptureBuffer emptyCaptureBuffer = CaptureBuffer { captureByteCount = 0 , captureChunksReversed = [] } appendCapturedChunk :: IORef CaptureBuffer -> ByteString.ByteString -> IO Bool appendCapturedChunk capture bytes = atomicModifyIORef' capture \buffer@CaptureBuffer{..} -> let remaining = vampireOutputByteLimit - captureByteCount retained = ByteString.take remaining bytes retainedLength = ByteString.length retained buffer' = buffer { captureByteCount = captureByteCount + retainedLength , captureChunksReversed = if ByteString.null retained then captureChunksReversed else retained : captureChunksReversed } in (buffer', ByteString.length bytes > remaining) capturedStreams :: IORef CaptureBuffer -> IORef CaptureBuffer -> IO PartialCapturedStreams capturedStreams stdoutCapture stderrCapture = PartialCapturedStreams <$> capturedBytes stdoutCapture <*> capturedBytes stderrCapture capturedBytes :: IORef CaptureBuffer -> IO ByteString.ByteString capturedBytes capture = ByteString.concat . reverse . captureChunksReversed <$> readIORef capture boundedTranscriptBytes :: Int boundedTranscriptBytes = 32 * 1024 boundedTranscriptHalf :: Int boundedTranscriptHalf = boundedTranscriptBytes `div` 2 boundedBytes :: ByteString.ByteString -> BoundedBytes boundedBytes bytes = let original = ByteString.length bytes in if original <= boundedTranscriptBytes then BoundedBytes { boundedBytesOriginalCount = original , boundedBytesRetained = bytes , boundedBytesTruncated = False } else BoundedBytes { boundedBytesOriginalCount = original , boundedBytesRetained = ByteString.take boundedTranscriptHalf bytes <> ByteString.drop (original - boundedTranscriptHalf) bytes , boundedBytesTruncated = True } boundedText :: Text -> Text boundedText = decodeBoundedBytes . boundedBytes . TextEncoding.encodeUtf8 decodeBoundedBytes :: BoundedBytes -> Text decodeBoundedBytes = TextEncoding.decodeUtf8With TextEncodingError.lenientDecode . boundedBytesRetained boundedCapturedStreams :: PartialCapturedStreams -> BoundedCapturedStreams boundedCapturedStreams PartialCapturedStreams{..} = BoundedCapturedStreams { boundedStdout = boundedBytes partialStdout , boundedStderr = boundedBytes partialStderr } boundedTranscriptDiagnostic :: Text -> CompletedTranscript -> BoundedDiagnostic boundedTranscriptDiagnostic summary CompletedTranscript{completedStreams = streams} = BoundedDiagnostic { boundedDiagnosticSummary = boundedText summary , boundedDiagnosticStdout = boundedBytes (TextEncoding.encodeUtf8 (completedStdout streams)) , boundedDiagnosticStderr = boundedBytes (TextEncoding.encodeUtf8 (completedStderr streams)) } renderBoundedDiagnostic :: BoundedDiagnostic -> Text renderBoundedDiagnostic BoundedDiagnostic{..} = Text.unlines [ boundedDiagnosticSummary , renderBoundedStream "stdout" boundedDiagnosticStdout , renderBoundedStream "stderr" boundedDiagnosticStderr ] renderBoundedStream :: Text -> BoundedBytes -> Text renderBoundedStream streamLabel bytes = streamLabel <> (if boundedBytesTruncated bytes then " (retained first and last 16 KiB of " <> Text.pack (show (boundedBytesOriginalCount bytes)) <> " bytes)" else "") <> ":\n" <> decodeBoundedBytes bytes supervisorAbortError :: FilePath -> PartialCapturedStreams -> SupervisorAbort -> ProverProcessError supervisorAbortError executable partial = \case SupervisorCommunicationFailed stream message -> ProverCommunicationFailed executable stream (boundedText message) SupervisorOutputLimitExceeded stream -> ProverOutputLimitExceeded executable stream (boundedCapturedStreams partial) SupervisorLifecycleFailed message -> ProverLifecycleFailed executable (boundedText message) wallTimeoutMicroseconds :: TimeLimit -> Int wallTimeoutMicroseconds (Seconds seconds) = fromInteger (min (toInteger (maxBound :: Int)) ((toInteger seconds + vampireWallGraceSeconds) * 1000000)) forceTerminateProcessGroup :: ProcessGroupID -> ProcessHandle -> IO () forceTerminateProcessGroup processGroup processHandle = Exception.uninterruptibleMask_ do terminateRemainingProcessGroup processGroup _ <- waitForProcess processHandle pure () terminateRemainingProcessGroup :: ProcessGroupID -> IO () terminateRemainingProcessGroup processGroup = ignoreMissingProcess (signalProcessGroup sigKILL processGroup) ignoreMissingProcess :: IO () -> IO () ignoreMissingProcess action = action `Exception.catch` \(err :: IOException) -> if isDoesNotExistError err then pure () else throwIO err decodeOutput :: FilePath -> ProverOutputStream -> ByteString.ByteString -> Either ProverProcessError Text decodeOutput executable stream bytes = case TextEncoding.decodeUtf8' bytes of Left err -> Left (ProverOutputMalformedUtf8 executable stream (boundedText (Text.pack (show err)))) Right output -> Right output exceptionText :: IOException -> Text exceptionText = Text.pack . displayException classifyVampireCompleted :: VampireTaskMode -> CompletedTranscript -> Either VampireProtocolError CanonicalAtpOutcome classifyVampireCompleted mode CompletedTranscript{..} = case completedExitCode of ExitFailure _ -> classifyVampireProtocol mode completedExitCode [] ExitSuccess -> do statuses <- statusesFromCompleteStreams completedStreams classifyVampireProtocol mode completedExitCode statuses statusesFromCompleteStreams :: CompleteCapturedStreams -> Either VampireProtocolError [VampireStatus] statusesFromCompleteStreams CompleteCapturedStreams{..} | Set.null malformed = Right statuses | otherwise = Left (MalformedVampireStatusLines malformed) where (malformed, statuses) = foldMap classifyLine (Text.lines completedStdout <> Text.lines completedStderr) classifyLine line = case parseMaybe vampireStatusParser line of Just status -> (mempty, [status]) Nothing | "SZS status" `Text.isInfixOf` line -> (Set.singleton line, []) | otherwise -> mempty vampireStatusFromText :: Text -> VampireStatus vampireStatusFromText = \case "Theorem" -> StatusTheorem "CounterSatisfiable" -> StatusCounterSatisfiable "ContradictoryAxioms" -> StatusContradictoryAxioms "Timeout" -> StatusTimeout "ResourceOut" -> StatusResourceOut "GaveUp" -> StatusGaveUp "Unknown" -> StatusUnknown status -> UnsupportedStatus status -- | Parse a Vampire SZS status line. -- -- Recognizes both standard lines like: -- % SZS status Timeout for 123 -- and lines prefixed by worker ids (seen with portfolio output), e.g.: -- % (2581105)SZS status Timeout for vampireStatusParser :: Parsec Void Text VampireStatus vampireStatusParser = do _ <- Char.char '%' Char.hspace optional do _ <- Char.char '(' _ <- some Char.digitChar _ <- Char.char ')' Char.hspace _ <- chunk "SZS" Char.hspace1 _ <- chunk "status" Char.hspace1 status <- takeWhile1P (Just "SZS status") (\character -> character /= ' ' && character /= '\t') _ <- takeRest pure (vampireStatusFromText status)