Require stores for verification commands

7 files changed, 1294 insertions, 365 deletions

diff --git a/source/Api.hs b/source/Api.hs
index dba529f..896127c 100644
--- a/source/Api.hs
+++ b/source/Api.hs
@@ -9,15 +9,19 @@ module Api
     ( tokenize, TokStream
     , scan
     , parse
+    , parseWorkspace
     , simpleStream
     , builtins
     , ParseException(..)
     , gloss, GlossError(..)
     , generateTasks
     , encodeTasks
-    , prepareDumpTasks
-    , dumpTask
     , verify, verifyStreaming, verifyMeasured
+    , verifyWithObserver
+    , VerificationRequestOrdinal
+    , verificationRequestOrdinalValue
+    , VerificationRequestObserver
+    , verificationRequestObserver
     , ProverAnswer
         ( CounterSatisfiable
         , ContradictoryAxioms
@@ -34,16 +38,9 @@ module Api
     , VerificationFailureReason(..)
     , exportHtml
     , prepareHtmlExport
-    , WithFilter(..)
-    , WithOmissions(..)
-    , WithVersion(..)
-    , WithLogging(..)
-    , WithDump(..)
-    , WithHtml(..)
-    , pattern WithoutDump
-    , WithParseOnly(..)
-    , Options(..)
-    , WithDumpPremselTraining(..)
+    , prepareHtmlExportResult
+    , prepareDefaultSourceGraph
+    , defaultHtmlMountPrefixes
     ) where
 
 
@@ -60,7 +57,8 @@ import Felix.Migration qualified as Migration
 import Felix.Parse (ParseException(..), ParseWorkspaceError(..), ParsedSourceWorkspace)
 import Felix.Parse qualified as Felix
 import Felix.Source
-import Filter(filterTask)
+import Felix.Source.Graph (ResolvedSourceGraph)
+import Felix.Source.Graph qualified as SourceGraph
 import Meaning
     ( GlossError(..)
     , meaning
@@ -77,15 +75,17 @@ import Syntax.Token
 import Tptp.UnsortedFirstOrder qualified as Tptp
 
 import Control.Monad.Logger
-import Control.Monad.Reader
+import Control.Monad (foldM)
+import Data.Bifunctor (first)
 import Data.List.NonEmpty qualified as NonEmpty
 import Data.Map.Strict qualified as Map
 import Data.Set qualified as Set
 import Data.Text qualified as StrictText
 import Data.Text.IO qualified as Text
 import Data.Vector qualified as Vector
+import Numeric.Natural (Natural)
 import System.FilePath.Posix
-import Text.Megaparsec hiding (parse, Token)
+import Text.Megaparsec hiding (parse, Token, try)
 import UnliftIO
 import UnliftIO.Directory
 import UnliftIO.Environment
@@ -164,8 +164,16 @@ scan input = do
 -- parsing fails.
 parse :: MonadIO io => FilePath -> io [Raw.Block]
 parse file = do
-    result <- liftIO (parseDefaultWorkspace file)
-    Felix.importedBeforeImporterBlocks <$> either throwWorkspaceError pure result
+    result <- parseWorkspace file
+    either throwWorkspaceError pure result
+
+parseWorkspace
+    :: MonadIO io
+    => FilePath
+    -> io (Either ParseWorkspaceError [Raw.Block])
+parseWorkspace file =
+    fmap Felix.importedBeforeImporterBlocks
+        <$> liftIO (parseDefaultWorkspace file)
 
 parseDefaultWorkspace
     :: FilePath
@@ -192,6 +200,18 @@ prepareDefaultSourceRequest file = do
         (Right mounts, Right request) ->
             Right (mounts, request)
 
+prepareDefaultSourceGraph
+    :: FilePath
+    -> IO (Either ParseWorkspaceError ResolvedSourceGraph)
+prepareDefaultSourceGraph file = do
+    prepared <- prepareDefaultSourceRequest file
+    case prepared of
+        Left sourceFailure ->
+            pure (Left sourceFailure)
+        Right (mounts, request) ->
+            first SourceWorkspaceError
+                <$> SourceGraph.buildResolvedSourceGraph mounts request
+
 prepareDefaultSourceMounts :: IO (Either SourceError SourceMounts)
 prepareDefaultSourceMounts = do
     currentDir <- getCurrentDirectory
@@ -241,13 +261,16 @@ gloss file = do
     liftIO
         (concat
             <$> traverse
-                (glossModule . Felix.parsedModuleBlocks)
+                (\parsed ->
+                    either throwIO pure
+                        (meaning
+                            (Felix.parsedModuleBlocks parsed)))
                 (toList
                     (Felix.parsedWorkspaceImportedBeforeImporter
                         workspace)))
 
 
-generateTasks :: (MonadIO io, MonadReader Options io) => FilePath -> io [Internal.Task]
+generateTasks :: MonadIO io => FilePath -> io [Internal.Task]
 generateTasks file = do
     obligations <-
         prepareCheckingTasks
@@ -256,35 +279,19 @@ generateTasks file = do
     pure (preparedObligationTask <$> obligations)
 
 prepareCheckingTasks
-    :: (MonadIO io, MonadReader Options io)
+    :: MonadIO io
     => (Internal.Task -> Internal.Task)
     -> FilePath
     -> io [PreparedObligation]
 prepareCheckingTasks prepareTask file = do
-    dumpPremselTraining <- asks withDumpPremselTraining
     blocks <- gloss file
     liftIO
         (checkPrepared
-            dumpPremselTraining
+            WithoutDumpPremselTraining
             prepareTask
             blocks)
 
-prepareDumpTasks :: (MonadIO io, MonadReader Options io) => FilePath -> io [(Int, Tptp.Task)]
-prepareDumpTasks file = do
-    filterOption <- asks withFilter
-    obligations <-
-        prepareCheckingTasks
-            (prepareTaskWithFilter filterOption)
-            file
-    pure
-        [ (index, preparedTptpSyntax
-            (preparedProverTptpTask
-                (preparedObligationProverTask obligation)))
-        | (index, obligation) <- zip [1..] obligations
-        ]
-
-
-encodeTasks :: (MonadIO io, MonadReader Options io) => FilePath -> io [Tptp.Task]
+encodeTasks :: MonadIO io => FilePath -> io [Tptp.Task]
 encodeTasks file = do
     obligations <-
         prepareCheckingTasks
@@ -297,16 +304,6 @@ encodeTasks file = do
         | obligation <- obligations
         ]
 
-prepareTaskWithFilter :: WithFilter -> Internal.Task -> Internal.Task
-prepareTaskWithFilter filterOption rawTask =
-    case filterOption of
-        WithFilter ->
-            filterTask task
-        WithoutFilter ->
-            task
-  where
-    task = contractionTask rawTask
-
 data VerificationResult
     = VerifiedWithTrustedVampire !VerificationReport
     | CompletedWithExplicitGaps !VerificationReport
@@ -367,6 +364,7 @@ data VerificationObservation = VerificationObservation
     , observedVampireRunCount :: !Int
     , observedFirstVampireStart :: !(Maybe Word64)
     , observedVampireExecutionNanoseconds :: !Word64
+    , observedNextRequestOrdinal :: !Natural
     }
 
 initialVerificationObservation :: VerificationObservation
@@ -383,8 +381,38 @@ initialVerificationObservation =
         , observedVampireRunCount = 0
         , observedFirstVampireStart = Nothing
         , observedVampireExecutionNanoseconds = 0
+        , observedNextRequestOrdinal = 1
         }
 
+newtype VerificationRequestOrdinal = VerificationRequestOrdinal Natural
+    deriving (Show, Eq, Ord)
+
+verificationRequestOrdinalValue
+    :: VerificationRequestOrdinal
+    -> Natural
+verificationRequestOrdinalValue
+        (VerificationRequestOrdinal value) =
+    value
+
+newtype VerificationRequestObserver = VerificationRequestObserver
+    { observeVerificationRequest
+        :: VerificationRequestOrdinal
+        -> PreparedVerificationRequest
+        -> IO ()
+    }
+
+verificationRequestObserver
+    :: (VerificationRequestOrdinal
+        -> PreparedVerificationRequest
+        -> IO ())
+    -> VerificationRequestObserver
+verificationRequestObserver =
+    VerificationRequestObserver
+
+ignoreVerificationRequests :: VerificationRequestObserver
+ignoreVerificationRequests =
+    VerificationRequestObserver \_ordinal _request -> pure ()
+
 data FailedVerification = FailedVerification
     { failedVerificationLocation :: !Location
     , failedVerificationFormula :: !Internal.Formula
@@ -428,7 +456,15 @@ newtype VerificationAborted =
 instance Exception VerificationAborted
 
 data VerificationDriverError
-    = VerificationObligationResolutionError
+    = VerificationWorkspaceError
+        !ParseWorkspaceError
+    | VerificationGlossError
+        !ResolvedSource
+        !GlossError
+    | VerificationCheckingError
+        !ResolvedSource
+        !CheckingError
+    | VerificationObligationResolutionError
         !ObligationResolutionError
     | VerificationLegacyModuleError
         !Legacy.LegacyModuleStageError
@@ -463,22 +499,57 @@ data CheckedWorkspace
     | CheckedTypedWorkspace !Typed.SealedTypedModule
 
 verifyStreaming
-    :: (MonadUnliftIO io, MonadLogger io, MonadReader Options io)
+    :: (MonadUnliftIO io, MonadLogger io)
     => Vampire
     -> FilePath
-    -> io VerificationResult
+    -> io (Either VerificationDriverError VerificationResult)
 verifyStreaming prover file =
-    fst <$> verifyMeasured prover file
+    fmap fst <$> verifyMeasured prover file
+
+verifyWithObserver
+    :: (MonadUnliftIO io, MonadLogger io)
+    => VerificationRequestObserver
+    -> Vampire
+    -> FilePath
+    -> io (Either VerificationDriverError VerificationResult)
+verifyWithObserver observer prover file =
+    fmap fst
+        <$> verifyMeasuredWithObserver observer prover file
 
 verifyMeasured
-    :: (MonadUnliftIO io, MonadLogger io, MonadReader Options io)
+    :: (MonadUnliftIO io, MonadLogger io)
     => Vampire
     -> FilePath
+    -> io
+        (Either
+            VerificationDriverError
+            (VerificationResult, VerificationMeasurements))
+verifyMeasured prover file =
+    verifyMeasuredWithObserver
+        ignoreVerificationRequests
+        prover
+        file
+
+verifyMeasuredWithObserver
+    :: (MonadUnliftIO io, MonadLogger io)
+    => VerificationRequestObserver
+    -> Vampire
+    -> FilePath
+    -> io
+        (Either
+            VerificationDriverError
+            (VerificationResult, VerificationMeasurements))
+verifyMeasuredWithObserver observer prover file =
+    try (verifyMeasuredThrowing observer prover file)
+
+verifyMeasuredThrowing
+    :: (MonadUnliftIO io, MonadLogger io)
+    => VerificationRequestObserver
+    -> Vampire
+    -> FilePath
     -> io (VerificationResult, VerificationMeasurements)
-verifyMeasured prover file = do
+verifyMeasuredThrowing requestObserver prover file = do
     invocationStart <- liftIO getMonotonicTimeNSec
-    dumpPremselTraining <- asks withDumpPremselTraining
-    filterOption <- asks withFilter
     ( admittedResult
       , parseMeasurements
       , sourcePreparation
@@ -499,6 +570,7 @@ verifyMeasured prover file = do
                     typedVampireResolver
                         runInIO
                         prover
+                        requestObserver
                         observationRef
             bootstrap <-
                 Typed.buildBootstrapPreludeSession
@@ -510,7 +582,9 @@ verifyMeasured prover file = do
             preparationStart <- getMonotonicTimeNSec
             prepared <-
                 prepareDefaultSourceRequest file
-                    >>= either throwWorkspaceError pure
+                    >>= either
+                        (throwIO . VerificationWorkspaceError)
+                        pure
             preparationEnd <- getMonotonicTimeNSec
             let (mounts, request) = prepared
             selection <-
@@ -534,7 +608,9 @@ verifyMeasured prover file = do
                     mounts
                     request
                     syntaxInputs
-                    >>= either throwWorkspaceError pure
+                    >>= either
+                        (throwIO . VerificationWorkspaceError)
+                        pure
             checkingStart <- getMonotonicTimeNSec
             admitted <-
                 (Right <$> case
@@ -546,8 +622,7 @@ verifyMeasured prover file = do
                                     foundation
                                     runInIO
                                     prover
-                                    dumpPremselTraining
-                                    filterOption
+                                    requestObserver
                                     observationRef
                                     parsed
                         Migration.TypedMigrationGraph ->
@@ -604,8 +679,7 @@ checkParsedWorkspace
     => Foundation.CheckedFoundation
     -> (forall a. io a -> IO a)
     -> Vampire
-    -> WithDumpPremselTraining
-    -> WithFilter
+    -> VerificationRequestObserver
     -> IORef VerificationObservation
     -> ParsedSourceWorkspace
     -> IO Transition.TransitionAdmittedModule
@@ -613,8 +687,7 @@ checkParsedWorkspace
         checkedFoundationValue
         runInIO
         prover
-        dumpPremselTraining
-        filterOption
+        requestObserver
         observationRef
         workspace = do
     assignments <-
@@ -660,6 +733,8 @@ checkParsedWorkspace
             assignment = do
         let parsedModule =
                 Legacy.assignedParsedModule assignment
+            source =
+                Felix.parsedModuleResolved parsedModule
             address =
                 Felix.parsedModuleAddress parsedModule
         moduleStart <- getMonotonicTimeNSec
@@ -683,18 +758,23 @@ checkParsedWorkspace
                     directImports)
         blocks <-
             glossModule
+                source
                 (Felix.parsedModuleBlocks parsedModule)
-        checked <-
-            runCheckingBlocks
-                blocks
-                (initialTransitionCheckingStateWithTaskPreparation
-                    dumpPremselTraining
-                    (prepareTaskWithFilter filterOption)
-                    builder
-                    (resolvePreparedBatch
-                        runInIO
-                        prover
-                        observationRef))
+        checked <- do
+            checkedResult <- try
+                (runCheckingBlocks
+                    blocks
+                    (initialTransitionCheckingState
+                        builder
+                        (resolvePreparedBatch
+                            runInIO
+                            prover
+                            requestObserver
+                            observationRef)))
+            either
+                (throwIO . VerificationCheckingError source)
+                pure
+                checkedResult
         finalBuilder <-
             maybe
                 (impossible
@@ -781,9 +861,10 @@ typedVampireResolver
      . (MonadIO io, MonadLogger io)
     => (forall value. io value -> IO value)
     -> Vampire
+    -> VerificationRequestObserver
     -> IORef VerificationObservation
     -> Declaration.VampireResolver
-typedVampireResolver runInIO prover observationRef =
+typedVampireResolver runInIO prover requestObserver observationRef =
     Declaration.vampireResolver \prepared -> do
         started <- getMonotonicTimeNSec
         observeVampireStart observationRef started
@@ -803,7 +884,11 @@ typedVampireResolver runInIO prover observationRef =
                         + fromIntegral
                             (preparedVerificationByteCount request)
                 }
-        result <- runInIO (runPreparedTypedProver prover prepared)
+        result <- runInIO
+            (runPreparedTypedProverWithObserver
+                (observeRequest observationRef requestObserver)
+                prover
+                prepared)
         finished <- getMonotonicTimeNSec
         observeVampireFinish observationRef (finished - started)
         pure result
@@ -960,20 +1045,26 @@ lookupImportedModule admittedByAddress address =
         (Map.lookup address admittedByAddress)
 
 glossModule
-    :: [Raw.Block]
+    :: ResolvedSource
+    -> [Raw.Block]
     -> IO [Internal.Block]
-glossModule rawBlocks =
-    either throwIO pure (meaning rawBlocks)
+glossModule source rawBlocks =
+    either
+        (throwIO . VerificationGlossError source)
+        pure
+        (meaning rawBlocks)
 
 resolvePreparedBatch
     :: forall io
      . (MonadIO io, MonadLogger io)
     => (forall a. io a -> IO a)
     -> Vampire
+    -> VerificationRequestObserver
     -> IORef VerificationObservation
     -> PreparedObligationBatch
     -> IO ResolvedObligationBatch
-resolvePreparedBatch runInIO prover observationRef batch = do
+resolvePreparedBatch
+        runInIO prover requestObserver observationRef batch = do
     observePreparedBatch observationRef batch
     resolved <-
         traverse
@@ -994,7 +1085,10 @@ resolvePreparedBatch runInIO prover observationRef batch = do
                     started
                 result <-
                     runInIO
-                        (runPreparedProver
+                        (runPreparedProverWithObserver
+                            (observeRequest
+                                observationRef
+                                requestObserver)
                             prover
                             (preparedObligationProverTask
                                 obligation))
@@ -1021,6 +1115,22 @@ resolvePreparedBatch runInIO prover observationRef batch = do
                                 impossible
                                     "successful prover result has no accepted Vampire run"
 
+observeRequest
+    :: IORef VerificationObservation
+    -> VerificationRequestObserver
+    -> PreparedVerificationRequest
+    -> IO ()
+observeRequest observationRef observer request = do
+    ordinal <- atomicModifyIORef' observationRef \observation ->
+        let current = observedNextRequestOrdinal observation
+        in
+            ( observation
+                { observedNextRequestOrdinal = current + 1
+                }
+            , VerificationRequestOrdinal current
+            )
+    observeVerificationRequest observer ordinal request
+
 observePreparedBatch
     :: IORef VerificationObservation
     -> PreparedObligationBatch
@@ -1406,12 +1516,13 @@ legacyVerificationReport admitted =
             (Transition.transitionAdmittedLegacyModule
                 admitted)
 
-verify :: (MonadUnliftIO io, MonadLogger io, MonadReader Options io) => Vampire -> FilePath -> io VerificationResult
+verify
+    :: (MonadUnliftIO io, MonadLogger io)
+    => Vampire
+    -> FilePath
+    -> io (Either VerificationDriverError VerificationResult)
 verify = verifyStreaming
 
-dumpTask :: MonadIO io => FilePath -> Tptp.Task -> io ()
-dumpTask file tptp = liftIO (Text.writeFile file (Tptp.toText tptp))
-
 exportHtml :: MonadUnliftIO io => FilePath -> io Text
 exportHtml file =
     HtmlExport.preparedHtmlRootDocument
@@ -1422,26 +1533,44 @@ prepareHtmlExport
     => FilePath
     -> io PreparedHtmlBundle
 prepareHtmlExport file =
-    HtmlExport.preparedHtmlOutputBundle
-        <$> prepareDefaultHtmlExport file
+    prepareHtmlExportResult file
+        >>= either throwIO pure
+
+prepareHtmlExportResult
+    :: MonadUnliftIO io
+    => FilePath
+    -> io (Either HtmlExport.HtmlExportError PreparedHtmlBundle)
+prepareHtmlExportResult file =
+    fmap HtmlExport.preparedHtmlOutputBundle
+        <$> prepareDefaultHtmlExportResult file
 
 prepareDefaultHtmlExport
     :: MonadUnliftIO io
     => FilePath
     -> io HtmlExport.PreparedHtmlExport
 prepareDefaultHtmlExport file = do
+    result <- prepareDefaultHtmlExportResult file
+    either throwIO pure result
+
+prepareDefaultHtmlExportResult
+    :: MonadUnliftIO io
+    => FilePath
+    -> io (Either HtmlExport.HtmlExportError HtmlExport.PreparedHtmlExport)
+prepareDefaultHtmlExportResult file = do
     hints <- findAndReadRendererFile "lexicon.tsv"
     prepared <- liftIO (prepareDefaultSourceRequest file)
-    (mounts, request) <-
-        either throwWorkspaceError pure prepared
-    exportResult <-
-        liftIO
-            (HtmlExport.prepareHtmlExport
-                defaultHtmlMountPrefixes
-                mounts
-                request
-                hints)
-    either throwIO pure exportResult
+    case prepared of
+        Left parseFailure ->
+            pure
+                (Left
+                    (HtmlExport.HtmlExportParseError parseFailure))
+        Right (mounts, request) ->
+            liftIO
+                (HtmlExport.prepareHtmlExport
+                    defaultHtmlMountPrefixes
+                    mounts
+                    request
+                    hints)
 
 defaultHtmlMountPrefixes :: [(SourceMountId, [Text])]
 defaultHtmlMountPrefixes =
@@ -1449,38 +1578,3 @@ defaultHtmlMountPrefixes =
     , (sourceMountId "library", ["library"])
     , (sourceMountId "debug", ["debug"])
     ]
-
-data WithFilter = WithoutFilter | WithFilter deriving (Show, Eq)
-
--- | Are proof omissions allowed?
-data WithOmissions = WithoutOmissions | WithOmissions deriving (Show, Eq)
-
--- | Should we show the version of the software?
-data WithVersion = WithoutVersion | WithVersion deriving (Show, Eq)
-
-data WithLogging = WithoutLogging | WithLogging deriving (Show, Eq)
-
--- | Should we dump all proof tasks? Where?
-newtype WithDump = WithDump FilePath deriving (Show, Eq)
-
--- | Should we export to HTML?
-data WithHtml = WithHtml | WithoutHtml deriving (Show, Eq)
-
-pattern WithoutDump :: WithDump
-pattern WithoutDump = WithDump ""
-
-data WithParseOnly = WithoutParseOnly | WithParseOnly deriving (Show, Eq)
-
-data Options = Options
-    { inputPath :: FilePath
-    , withDump :: WithDump
-    , withFilter :: WithFilter
-    , withLogging :: WithLogging
-    , withMemoryLimit :: Provers.MemoryLimit
-    , withOmissions :: WithOmissions
-    , withParseOnly :: WithParseOnly
-    , withTimeLimit :: Provers.TimeLimit
-    , withVersion :: WithVersion
-    , withHtml :: WithHtml
-    , withDumpPremselTraining :: WithDumpPremselTraining
-    }
diff --git a/source/Checking.hs b/source/Checking.hs
index 9491f5f..d41ada1 100644
--- a/source/Checking.hs
+++ b/source/Checking.hs
@@ -195,6 +195,17 @@ initialTransitionCheckingStateWithTaskPreparation
                 }
         )
 
+-- | Production V1 checking uses the complete contracted task and has no
+-- premise-selection or training mode.
+initialTransitionCheckingState
+    :: Transition.TransitionModuleBuilder
+    -> (PreparedObligationBatch -> IO ResolvedObligationBatch)
+    -> CheckingState
+initialTransitionCheckingState =
+    initialTransitionCheckingStateWithTaskPreparation
+        WithoutDumpPremselTraining
+        contractionTask
+
 initialCheckingStateWithBatchHandler
     :: WithDumpPremselTraining
     -> (Task -> Task)
diff --git a/source/CommandLine.hs b/source/CommandLine.hs
index 322de38..19f496a 100644
--- a/source/CommandLine.hs
+++ b/source/CommandLine.hs
@@ -1,25 +1,65 @@
+{-# LANGUAGE DerivingStrategies #-}
 {-# LANGUAGE NoImplicitPrelude #-}
-{-# LANGUAGE RecordWildCards #-}
 
 module CommandLine where
 
 import Api
 import Base
+import Checking.Foundation qualified as Foundation
+import Checking.Identity qualified as Identity
+import Felix.OutputPlan qualified as Output
+import Felix.Parse (ParseWorkspaceError)
+import Felix.Source
+import Felix.Source.Graph qualified as SourceGraph
+import Felix.Store qualified as Store
 import Provers qualified
+import Render.Html.Export qualified as HtmlExport
+import Render.Html.Layout qualified as HtmlLayout
 import Render.Html.Output qualified as HtmlOutput
-import Version qualified
 import Report.Location
+import Version qualified
 
+import Control.Exception (displayException)
+import Control.Exception qualified as Exception
+import Control.Monad (unless)
 import Control.Monad.Logger
-import Control.Monad.Reader
+import Data.ByteString qualified as ByteString
+import Data.Maybe (catMaybes)
 import Data.Text qualified as StrictText
 import Data.Text.IO qualified as Text
-import Options.Applicative
-import UnliftIO
-import UnliftIO.Directory
-import UnliftIO.Environment (lookupEnv)
+import Options.Applicative hiding (renderFailure)
+import System.Directory qualified as Directory
+import System.Environment (getArgs, lookupEnv)
 import System.Exit (ExitCode(..), exitWith)
-import System.FilePath.Posix
+import System.FilePath.Posix qualified as Posix
+import System.IO (stderr)
+
+
+newtype Input = Input
+    { inputFilePath :: FilePath
+    }
+    deriving stock (Show, Eq)
+
+data VerificationDiagnostics
+    = QuietVerification
+    | LogVerification
+    deriving stock (Show, Eq)
+
+data VerificationOptions = VerificationOptions
+    { verificationStoreSelection :: !Store.StoreSelection
+    , verificationTimeLimit :: !Provers.TimeLimit
+    , verificationMemoryLimit :: !Provers.MemoryLimit
+    , verificationDumpDestination :: !(Maybe FilePath)
+    , verificationHtmlRequested :: !Bool
+    , verificationDiagnostics :: !VerificationDiagnostics
+    }
+    deriving stock (Show, Eq)
+
+data Command
+    = Version
+    | ParseOnly !Input
+    | Verify !Input !VerificationOptions
+    deriving stock (Show, Eq)
 
 data CommandOutcome
     = CommandCompleted
@@ -27,83 +67,310 @@ data CommandOutcome
     | VerificationCompletedWithGaps !VerificationReport
     | VerificationRejected !Location !VerificationRejection
     | ProverFailed !Location !ProverFailure
-    deriving (Show, Eq)
+    | SourcePlanningFailed !ParseWorkspaceError
+    | ParseOnlyFailed !ParseWorkspaceError
+    | VerificationDriverFailed !VerificationDriverError
+    | StorePlanningFailed !Store.StorePlanningError
+    | StoreIncompatible !Store.StoreIncompatibility
+    | StoreFailed !Store.StoreLifecycleError
+    | OutputPlanningFailed !Output.OutputPlanError
+    | HtmlLayoutFailed !HtmlLayout.HtmlLayoutError
+    | DumpObservationFailed !DumpObservationError
+    | HtmlExportFailed !HtmlExport.HtmlExportError
+    | HtmlOutputPlanningFailed !HtmlOutput.HtmlOutputError
+    | HtmlPublicationFailed !HtmlOutput.HtmlPublicationError
+    deriving stock (Show)
 
 data VerificationRejection
     = CountermodelFound !Text
     | ContradictoryInputFound !Text
-    deriving (Show, Eq)
+    deriving stock (Show, Eq)
 
 data ProverFailure
     = ProverIndeterminate !Text
     | ProverProtocolFailure !Text !Text
     | ProverTransportFailure !Provers.ProverProcessError
-    deriving (Show, Eq)
+    deriving stock (Show, Eq)
+
+data DumpObservationError
+    = DumpDirectoryCreationFailed !FilePath !Text
+    | DumpRequestWriteFailed
+        !VerificationRequestOrdinal
+        !FilePath
+        !Text
+    deriving stock (Show, Eq)
+
+instance Exception.Exception DumpObservationError
+
 
 runCommandLine :: IO ()
 runCommandLine = do
-    options@Options{withLogging = logging} <- execParser (withInfo parseOptions)
-    outcome <- case logging of
-        WithoutLogging -> runNoLoggingT (runReaderT run options)
-        WithLogging -> runStderrLoggingT (runReaderT run options)
+    arguments <- getArgs
+    selected <- handleParseResult (parseCommandArguments arguments)
+    outcome <- runCommand selected
     renderCommandOutcome outcome
     exitWith (commandOutcomeExitCode outcome)
-    where
-        withInfo :: Parser a -> ParserInfo a
-        withInfo p = info (helper <*> p) (fullDesc <> header "Naproche/ZF")
-
-
-run
-    :: (MonadUnliftIO io, MonadLogger io, MonadReader Options io)
-    => io CommandOutcome
-run = do
-    opts <- ask
-    case withVersion opts of
-        WithVersion -> liftIO (Text.putStrLn Version.info)
-        WithoutVersion -> skip
-    case withOmissions opts of
-        WithoutOmissions ->
-            liftIO (Text.hPutStrLn stderr "--safe is not implemented yet.")
-        WithOmissions -> skip
-    case withDump opts of
-        WithoutDump -> skip
-        WithDump dir -> do
-            liftIO
-                (Text.hPutStrLn
-                    stderr
-                    "\ESC[1;36mCreating Dumpfiles.\ESC[0m")
-            tasks <- prepareDumpTasks (inputPath opts)
-            createDirectoryIfMissing True dir
-            forM_ [(dir </> show n <.> "p", task) | (n, task) <- tasks] (uncurry dumpTask)
-            liftIO (Text.hPutStrLn stderr "\ESC[35mDump ready.\ESC[0m")
-    case (withParseOnly opts, withHtml opts) of
-        (WithParseOnly, _) -> do
-            _ast <- parse (inputPath opts)
-            pure CommandCompleted
-        (WithoutParseOnly, WithHtml) -> do
-            bundle <- prepareHtmlExport (inputPath opts)
-            outputPlan <-
-                liftIO
-                    (HtmlOutput.planHtmlOutput "html" bundle)
-                    >>= either throwIO pure
-            publication <-
-                liftIO
-                    (HtmlOutput.writeHtmlOutput outputPlan)
-            either throwIO pure publication
-            pure CommandCompleted
-        (WithoutParseOnly, WithoutHtml) -> do
-            liftIO
-                (Text.hPutStrLn
-                    stderr
-                    "\ESC[1;96mStart of verification.\ESC[0m")
+
+rawCommandParserInfo :: ParserInfo RawCommand
+rawCommandParserInfo =
+    info
+        (helper <*> rawCommandParser)
+        (fullDesc <> header "Naproche/ZF")
+
+runCommand :: Command -> IO CommandOutcome
+runCommand = \case
+    Version -> do
+        Text.putStrLn Version.info
+        pure CommandCompleted
+    ParseOnly (Input input) ->
+        parseWorkspace input >>= \case
+            Left failure ->
+                pure (ParseOnlyFailed failure)
+            Right _blocks ->
+                pure CommandCompleted
+    Verify input options ->
+        runVerification input options
+
+runVerification
+    :: Input
+    -> VerificationOptions
+    -> IO CommandOutcome
+runVerification input options = do
+    plannedStore <-
+        Store.planStore
+            (verificationStoreSelection options)
+    case plannedStore of
+        Left failure ->
+            pure (StorePlanningFailed failure)
+        Right storePlan ->
+            Store.withStoreLease storePlan \lease -> do
+                sourcePlan <-
+                    prepareDefaultSourceGraph
+                        (inputFilePath input)
+                case sourcePlan of
+                    Left failure ->
+                        pure (SourcePlanningFailed failure)
+                    Right graph ->
+                        case planHtmlDestinations options graph of
+                            Left failure ->
+                                pure (HtmlLayoutFailed failure)
+                            Right htmlDestinations -> do
+                                outputResult <-
+                                    Output.planVerificationOutputs
+                                        (Store.storeLeasePath lease)
+                                        (verificationDumpDestination options)
+                                        (fmap ((,) "html") htmlDestinations)
+                                case outputResult of
+                                    Left failure ->
+                                        pure (OutputPlanningFailed failure)
+                                    Right outputPlan ->
+                                        openSelectedStore
+                                            input
+                                            options
+                                            lease
+                                            outputPlan
+
+planHtmlDestinations
+    :: VerificationOptions
+    -> SourceGraph.ResolvedSourceGraph
+    -> Either HtmlLayout.HtmlLayoutError (Maybe [SafeRelativePath])
+planHtmlDestinations options graph
+    | verificationHtmlRequested options = do
+        layout <-
+            HtmlLayout.layoutHtmlSourceGraph
+                defaultHtmlMountPrefixes
+                graph
+        pure
+            (Just
+                ( [ HtmlLayout.routeDestination route
+                  | (_source, route) <-
+                        HtmlLayout.htmlPageRoutes layout
+                  ]
+                    <> [HtmlLayout.routeDestination
+                            (HtmlLayout.htmlSupportScriptRoute layout)]
+                ))
+    | otherwise =
+        Right Nothing
+
+openSelectedStore
+    :: Input
+    -> VerificationOptions
+    -> Store.StoreLease
+    -> Output.VerificationOutputPlan
+    -> IO CommandOutcome
+openSelectedStore input options lease outputPlan =
+    case Foundation.checkedFoundation of
+        Left failures ->
+            pure
+                (VerificationDriverFailed
+                    (VerificationFoundationManifestError failures))
+        Right foundation -> do
+            opened <-
+                Store.withOpenStore
+                    lease
+                    (Identity.theoryId foundation)
+                    \_startup _store ->
+                        runOpenVerification
+                            input
+                            options
+                            outputPlan
+            pure
+                (case opened of
+                    Left
+                        (Store.StoreLifecycleOpenFailed
+                            (Store.IncompatibleStore incompatibility)) ->
+                                StoreIncompatible incompatibility
+                    Left failure ->
+                        StoreFailed failure
+                    Right outcome ->
+                        outcome)
+
+runOpenVerification
+    :: Input
+    -> VerificationOptions
+    -> Output.VerificationOutputPlan
+    -> IO CommandOutcome
+runOpenVerification input options outputPlan = do
+    observerResult <-
+        prepareRequestObserver
+            (Output.verificationDumpOutput outputPlan)
+    case observerResult of
+        Left failure ->
+            pure (DumpObservationFailed failure)
+        Right observer -> do
             vampirePath <- getVampireExecutable
             let vampire =
                     Provers.vampire
                         vampirePath
-                        (withTimeLimit opts)
-                        (withMemoryLimit opts)
-            result <- verify vampire (inputPath opts)
+                        (verificationTimeLimit options)
+                        (verificationMemoryLimit options)
+            observed <-
+                captureDumpFailure
+                    (case verificationDiagnostics options of
+                        QuietVerification ->
+                            runNoLoggingT
+                                (verifyWithObserver
+                                    observer
+                                    vampire
+                                    (inputFilePath input))
+                        LogVerification ->
+                            runStderrLoggingT
+                                (verifyWithObserver
+                                    observer
+                                    vampire
+                                    (inputFilePath input)))
+            case observed of
+                Left failure ->
+                    pure (DumpObservationFailed failure)
+                Right (Left failure) ->
+                    pure (VerificationDriverFailed failure)
+                Right (Right result) ->
+                    finishVerification
+                        input
+                        outputPlan
+                        result
+
+prepareRequestObserver
+    :: Maybe Output.DumpOutputPlan
+    -> IO
+        (Either
+            DumpObservationError
+            VerificationRequestObserver)
+prepareRequestObserver = \case
+    Nothing ->
+        pure
+            (Right
+                (verificationRequestObserver
+                    \_ordinal _request -> pure ()))
+    Just dumpPlan -> do
+        let root = Output.dumpOutputPath dumpPlan
+        created <- tryIOError
+            (Directory.createDirectoryIfMissing True root)
+        pure case created of
+            Left failure ->
+                Left
+                    (DumpDirectoryCreationFailed
+                        root
+                        (StrictText.pack
+                            (displayException failure)))
+            Right () ->
+                Right
+                    (verificationRequestObserver
+                        (writeDumpRequest root))
+
+writeDumpRequest
+    :: FilePath
+    -> VerificationRequestOrdinal
+    -> Provers.PreparedVerificationRequest
+    -> IO ()
+writeDumpRequest root ordinal request = do
+    let destination =
+            root
+                Posix.</> show
+                    (verificationRequestOrdinalValue ordinal)
+                Posix.<.> "p"
+    result <- tryIOError
+        (ByteString.writeFile
+            destination
+            (Provers.preparedVerificationBytes request))
+    case result of
+        Left failure ->
+            Exception.throwIO
+                (DumpRequestWriteFailed
+                    ordinal
+                    destination
+                    (StrictText.pack
+                        (displayException failure)))
+        Right () ->
+            pure ()
+
+captureDumpFailure
+    :: IO value
+    -> IO (Either DumpObservationError value)
+captureDumpFailure =
+    Exception.try
+
+finishVerification
+    :: Input
+    -> Output.VerificationOutputPlan
+    -> VerificationResult
+    -> IO CommandOutcome
+finishVerification input outputPlan result =
+    case result of
+        VerificationFailure{} ->
+            pure (verificationCommandOutcome result)
+        VerifiedWithTrustedVampire{} ->
+            publishHtmlIfRequested input outputPlan result
+        CompletedWithExplicitGaps{} ->
+            publishHtmlIfRequested input outputPlan result
+
+publishHtmlIfRequested
+    :: Input
+    -> Output.VerificationOutputPlan
+    -> VerificationResult
+    -> IO CommandOutcome
+publishHtmlIfRequested input outputPlan result =
+    case Output.verificationHtmlRoutes outputPlan of
+        Nothing ->
             pure (verificationCommandOutcome result)
+        Just routes -> do
+            prepared <-
+                prepareHtmlExportResult
+                    (inputFilePath input)
+            case prepared of
+                Left failure ->
+                    pure (HtmlExportFailed failure)
+                Right bundle ->
+                    case HtmlOutput.planHtmlOutputAgainst routes bundle of
+                        Left failure ->
+                            pure (HtmlOutputPlanningFailed failure)
+                        Right plan ->
+                            HtmlOutput.writeHtmlOutput plan >>= \case
+                                Left failure ->
+                                    pure (HtmlPublicationFailed failure)
+                                Right () ->
+                                    pure
+                                        (verificationCommandOutcome result)
 
 verificationCommandOutcome :: VerificationResult -> CommandOutcome
 verificationCommandOutcome = \case
@@ -144,6 +411,30 @@ commandOutcomeExitCode = \case
         ExitFailure 1
     ProverFailed{} ->
         ExitFailure 2
+    SourcePlanningFailed{} ->
+        ExitFailure 1
+    ParseOnlyFailed{} ->
+        ExitFailure 1
+    VerificationDriverFailed{} ->
+        ExitFailure 1
+    StorePlanningFailed{} ->
+        ExitFailure 2
+    StoreIncompatible{} ->
+        ExitFailure 2
+    StoreFailed{} ->
+        ExitFailure 2
+    OutputPlanningFailed{} ->
+        ExitFailure 2
+    HtmlLayoutFailed{} ->
+        ExitFailure 2
+    DumpObservationFailed{} ->
+        ExitFailure 2
+    HtmlExportFailed{} ->
+        ExitFailure 2
+    HtmlOutputPlanningFailed{} ->
+        ExitFailure 2
+    HtmlPublicationFailed{} ->
+        ExitFailure 2
 
 renderCommandOutcome :: CommandOutcome -> IO ()
 renderCommandOutcome = \case
@@ -160,6 +451,90 @@ renderCommandOutcome = \case
         renderVerificationRejection location rejection
     ProverFailed location failure ->
         renderProverFailure location failure
+    SourcePlanningFailed{} ->
+        renderFailure "Source planning failed."
+    ParseOnlyFailed{} ->
+        renderFailure "Parsing failed."
+    VerificationDriverFailed failure ->
+        renderVerificationDriverFailure failure
+    StorePlanningFailed{} ->
+        renderFailure "Store path planning failed."
+    StoreIncompatible{} ->
+        renderFailure
+            "The selected disposable store is incompatible with this Felix build."
+    StoreFailed{} ->
+        renderFailure "Store startup or integrity checking failed."
+    OutputPlanningFailed{} ->
+        renderFailure "Verification output preflight failed."
+    HtmlLayoutFailed{} ->
+        renderFailure "HTML route planning failed."
+    DumpObservationFailed failure ->
+        renderDumpObservationFailure failure
+    HtmlExportFailed{} ->
+        renderFailure "HTML preparation failed."
+    HtmlOutputPlanningFailed{} ->
+        renderFailure "Prepared HTML did not match the reserved routes."
+    HtmlPublicationFailed failure -> do
+        renderFailure "HTML publication failed."
+        unless
+            (null
+                (HtmlOutput.committedHtmlDestinations failure))
+            (Text.hPutStrLn stderr
+                "Some earlier HTML files were already published.")
+
+renderFailure :: Text -> IO ()
+renderFailure =
+    Text.hPutStrLn stderr
+
+renderVerificationDriverFailure
+    :: VerificationDriverError
+    -> IO ()
+renderVerificationDriverFailure = \case
+    VerificationWorkspaceError{} ->
+        renderFailure "Verification input parsing failed."
+    VerificationGlossError _source failure ->
+        renderFailure (StrictText.pack (show failure))
+    VerificationCheckingError source _failure ->
+        renderFailure
+            ("Verification checking failed in "
+                <> resolvedSourceDisplay source
+                <> ".")
+    VerificationTypedInputError source _failure ->
+        renderFailure
+            ("Typed module input failed in "
+                <> resolvedSourceDisplay source
+                <> ".")
+    VerificationTypedOpenError source _failure ->
+        renderFailure
+            ("Typed module startup failed in "
+                <> resolvedSourceDisplay source
+                <> ".")
+    VerificationTypedModuleError source _failure _prefix ->
+        renderFailure
+            ("Typed module checking failed in "
+                <> resolvedSourceDisplay source
+                <> ".")
+    _failure ->
+        renderFailure "Verification checking failed."
+
+resolvedSourceDisplay :: ResolvedSource -> Text
+resolvedSourceDisplay =
+    StrictText.pack . resolvedSourceLocationPath
+
+renderDumpObservationFailure :: DumpObservationError -> IO ()
+renderDumpObservationFailure = \case
+    DumpDirectoryCreationFailed path message ->
+        renderFailure
+            ("Could not create dump directory "
+                <> StrictText.pack (show path)
+                <> ": "
+                <> message)
+    DumpRequestWriteFailed _ordinal path message ->
+        renderFailure
+            ("Could not write request dump "
+                <> StrictText.pack (show path)
+                <> ": "
+                <> message)
 
 renderVerificationRejection
     :: Location
@@ -179,7 +554,7 @@ renderVerificationRejection location = \case
             ("Verification failed: contradictory axioms at "
                 <> locationToText location)
         Text.hPutStrLn stderr
-            "This is usually caused by an incorrect axiom or a theorem that has its proof omitted. It can also be caused by bugs or by using unsafe features. If no warnings were printed during verification and you are certain that there are no contradictions in your axiomatic setup, please report this as a bug."
+            "This is usually caused by an incorrect axiom or a theorem that has its proof omitted."
 
 renderProverFailure :: Location -> ProverFailure -> IO ()
 renderProverFailure location = \case
@@ -246,66 +621,168 @@ renderVerificationReport report = do
             <> noun
             <> if amount == 1 then "" else "s"
 
-
-getVampireExecutable :: MonadIO m => m FilePath
+getVampireExecutable :: IO FilePath
 getVampireExecutable =
     fromMaybe "vampire" <$> lookupEnv "NAPROCHE_ZF_VAMPIRE"
 
-parseOptions :: Parser Options
-parseOptions = do
-    inputPath <- strArgument (help "Source file" <> metavar "FILE")
-    withDump <- withDumpParser
-    withFilter <- withFilterParser
-    withLogging <- withLoggingParser
-    withMemoryLimit <- withMemoryLimitParser
-    withOmissions <- withOmissionsParser
-    withParseOnly <- withParseOnlyParser
-    withTimeLimit <- withTimeLimitParser
-    withVersion <- withVersionParser
-    withHtml <- withHtmlParser
-    withDumpPremselTraining <- withDumpPremselTrainingParser
-    pure Options{..}
-
-withTimeLimitParser :: Parser Provers.TimeLimit
-withTimeLimitParser = Provers.Seconds <$> option auto (long "timelimit" <> short 't' <> value dflt <> help "Time limit for each proof task in seconds.")
-    where
-        Provers.Seconds dflt = Provers.defaultTimeLimit
-
-withMemoryLimitParser :: Parser Provers.MemoryLimit
-withMemoryLimitParser = Provers.Megabytes <$> option auto (long "memlimit" <> short 'm' <> value dflt <> help "Memory limit for each proof task in MB.")
-    where
-        Provers.Megabytes dflt = Provers.defaultMemoryLimit
-
-withFilterParser :: Parser WithFilter
-withFilterParser = flag' WithoutFilter (long "nofilter" <> help "Do not perform relevance filtering.")
-    <|> flag' WithFilter (long "filter" <> help "Perform relevance filtering.")
-    <|> pure WithoutFilter
-
-withOmissionsParser :: Parser WithOmissions
-withOmissionsParser = flag' WithOmissions (long "unsafe" <> help "Allow proof omissions (on by default).")
-    <|> flag' WithoutOmissions (long "safe" <> help "Disallow proof omissions.")
-    <|> pure WithOmissions
-
-withParseOnlyParser :: Parser WithParseOnly
-withParseOnlyParser = flag' WithParseOnly (long "parseonly" <> help "Only parse and show the resulting AST (off by default).")
-    <|> pure WithoutParseOnly
-
-withVersionParser :: Parser WithVersion
-withVersionParser = flag' WithVersion (long "version" <> help "Show the current version (off by default).")
-    <|> pure WithoutVersion
-
-withLoggingParser :: Parser WithLogging
-withLoggingParser = flag' WithLogging (long "log" <> help "Enable logging (off by default).")
-    <|> pure WithoutLogging
-
-withDumpParser :: Parser WithDump
-withDumpParser = WithDump <$> strOption (long "dump" <> metavar "DUMPDIR" <> help "Dump all proof tasks in a separate directory.")
-    <|> pure WithoutDump
-
-withDumpPremselTrainingParser :: Parser WithDumpPremselTraining
-withDumpPremselTrainingParser = flag' WithDumpPremselTraining (long "premseldump" <> help "Dump training data for premise selection.")
-    <|> pure WithoutDumpPremselTraining
-
-withHtmlParser :: Parser WithHtml
-withHtmlParser = flag' WithHtml (long "html" <> help "Export to HTML (experimental).")
-    <|> pure WithoutHtml
+
+data RawCommand
+    = RawVersion
+    | RawFile !RawFileCommand
+
+data RawFileCommand = RawFileCommand
+    { rawInput :: !Input
+    , rawParseOnly :: !Bool
+    , rawStore :: !(Maybe FilePath)
+    , rawFresh :: !Bool
+    , rawTimeLimit :: !(Maybe Provers.TimeLimit)
+    , rawMemoryLimit :: !(Maybe Provers.MemoryLimit)
+    , rawDump :: !(Maybe FilePath)
+    , rawHtml :: !Bool
+    , rawLogging :: !Bool
+    }
+
+rawCommandParser :: Parser RawCommand
+rawCommandParser =
+    versionParser
+        <|> (RawFile <$> rawFileCommandParser)
+
+versionParser :: Parser RawCommand
+versionParser =
+    flag'
+        RawVersion
+        (long "version" <> help "Show the Felix version.")
+
+inputParser :: Parser Input
+inputParser =
+    Input
+        <$> strArgument
+            (help "Source file" <> metavar "FILE")
+
+rawFileCommandParser :: Parser RawFileCommand
+rawFileCommandParser =
+    RawFileCommand
+        <$> inputParser
+        <*> switch
+            (long "parseonly"
+                <> help "Resolve and parse source without verification.")
+        <*> optional
+            (strOption
+                (long "store"
+                    <> metavar "PATH"
+                    <> help "Use the disposable SQLite store at PATH."))
+        <*> switch
+            (long "fresh"
+                <> help "Use a fresh temporary disposable store.")
+        <*> optional timeLimitParser
+        <*> optional memoryLimitParser
+        <*> optional
+            (strOption
+                (long "dump"
+                    <> metavar "DUMPDIR"
+                    <> help "Dump exact Vampire requests as they execute."))
+        <*> switch
+            (long "html"
+                <> help "Publish verified HTML under ./html.")
+        <*> switch
+            (long "log"
+                <> help "Enable verification diagnostics.")
+
+parseCommandArguments :: [String] -> ParserResult Command
+parseCommandArguments arguments =
+    case execParserPure
+            defaultPrefs
+            rawCommandParserInfo
+            arguments of
+        Success raw ->
+            case validateRawCommand raw of
+                Left message ->
+                    Failure
+                        (parserFailure
+                            defaultPrefs
+                            rawCommandParserInfo
+                            (ErrorMsg message)
+                            [])
+                Right selected ->
+                    Success selected
+        Failure failure ->
+            Failure failure
+        CompletionInvoked completion ->
+            CompletionInvoked completion
+
+validateRawCommand :: RawCommand -> Either String Command
+validateRawCommand = \case
+    RawVersion ->
+        Right Version
+    RawFile raw
+        | rawParseOnly raw
+        , not (null verificationOnlyOptions) ->
+            Left
+                ("--parseonly cannot be combined with verification options: "
+                    <> unwords verificationOnlyOptions)
+        | rawParseOnly raw ->
+            Right (ParseOnly (rawInput raw))
+        | isJust (rawStore raw) && rawFresh raw ->
+            Left "--store and --fresh are mutually exclusive"
+        | otherwise ->
+            Right
+                (Verify
+                    (rawInput raw)
+                    VerificationOptions
+                        { verificationStoreSelection =
+                            case rawStore raw of
+                                Just path ->
+                                    Store.ExplicitStore path
+                                Nothing
+                                    | rawFresh raw ->
+                                        Store.FreshTemporaryStore
+                                    | otherwise ->
+                                        Store.DefaultStore
+                        , verificationTimeLimit =
+                            fromMaybe
+                                Provers.defaultTimeLimit
+                                (rawTimeLimit raw)
+                        , verificationMemoryLimit =
+                            fromMaybe
+                                Provers.defaultMemoryLimit
+                                (rawMemoryLimit raw)
+                        , verificationDumpDestination =
+                            rawDump raw
+                        , verificationHtmlRequested =
+                            rawHtml raw
+                        , verificationDiagnostics =
+                            if rawLogging raw
+                                then LogVerification
+                                else QuietVerification
+                        })
+      where
+        verificationOnlyOptions =
+            catMaybes
+                [ "--store" <$ rawStore raw
+                , if rawFresh raw then Just "--fresh" else Nothing
+                , "--timelimit" <$ rawTimeLimit raw
+                , "--memlimit" <$ rawMemoryLimit raw
+                , "--dump" <$ rawDump raw
+                , if rawHtml raw then Just "--html" else Nothing
+                , if rawLogging raw then Just "--log" else Nothing
+                ]
+
+timeLimitParser :: Parser Provers.TimeLimit
+timeLimitParser =
+    Provers.Seconds
+        <$> option auto
+            ( long "timelimit"
+                <> short 't'
+                <> metavar "SECONDS"
+                <> help "Time limit for each Vampire request."
+            )
+
+memoryLimitParser :: Parser Provers.MemoryLimit
+memoryLimitParser =
+    Provers.Megabytes
+        <$> option auto
+            ( long "memlimit"
+                <> short 'm'
+                <> metavar "MB"
+                <> help "Memory limit for each Vampire process."
+            )
diff --git a/source/Provers.hs b/source/Provers.hs
index e98d1df..7f85c29 100644
--- a/source/Provers.hs
+++ b/source/Provers.hs
@@ -47,7 +47,9 @@ module Provers
     , provedVampireRun
     , runProver
     , runPreparedProver
+    , runPreparedProverWithObserver
     , runPreparedTypedProver
+    , runPreparedTypedProverWithObserver
     , runVampireProcess
     ) where
 
@@ -526,12 +528,30 @@ runPreparedProver
         , Either ProverProcessError ProverAnswer
         )
 runPreparedProver
+        vampireCommand =
+    runPreparedProverWithObserver
+        (\_request -> pure ())
+        vampireCommand
+
+runPreparedProverWithObserver
+    :: (MonadIO io, MonadLogger io)
+    => (PreparedVerificationRequest -> IO ())
+    -> Vampire
+    -> PreparedProverTask
+    -> io
+        ( Location
+        , Formula
+        , Either ProverProcessError ProverAnswer
+        )
+runPreparedProverWithObserver
+        observer
         vampireCommand
         (PreparedProverTask task preparedTask preparedRequest) = do
     startTime <- liftIO getCurrentTime
     transcriptResult <-
         liftIO
-            (runPreparedVampireProcess
+            (runPreparedVampireProcessWithObserver
+                observer
                 vampireCommand
                 preparedRequest)
     let answer =
@@ -558,6 +578,19 @@ runPreparedTypedProver
     -> PreparedTypedProverTask ref local origin global
     -> io (Either ProverProcessError ProverAnswer)
 runPreparedTypedProver
+        vampireCommand =
+    runPreparedTypedProverWithObserver
+        (\_request -> pure ())
+        vampireCommand
+
+runPreparedTypedProverWithObserver
+    :: (MonadIO io, MonadLogger io)
+    => (PreparedVerificationRequest -> IO ())
+    -> Vampire
+    -> PreparedTypedProverTask ref local origin global
+    -> io (Either ProverProcessError ProverAnswer)
+runPreparedTypedProverWithObserver
+        observer
         vampireCommand
         (PreparedTypedProverTask
             _problem
@@ -566,7 +599,8 @@ runPreparedTypedProver
     startTime <- liftIO getCurrentTime
     transcriptResult <-
         liftIO
-            (runPreparedVampireProcess
+            (runPreparedVampireProcessWithObserver
+                observer
                 vampireCommand
                 preparedRequest)
     let answer =
@@ -638,6 +672,18 @@ runPreparedVampireProcess
     -> PreparedVerificationRequest
     -> IO (Either ProverProcessError CompletedTranscript)
 runPreparedVampireProcess
+    vampireCommand =
+    runPreparedVampireProcessWithObserver
+        (\_request -> pure ())
+        vampireCommand
+
+runPreparedVampireProcessWithObserver
+    :: (PreparedVerificationRequest -> IO ())
+    -> Vampire
+    -> PreparedVerificationRequest
+    -> IO (Either ProverProcessError CompletedTranscript)
+runPreparedVampireProcessWithObserver
+    observer
     vampireCommand@Vampire{vampireExecutable = executable}
     preparedRequest = do
         callbackStarted <- newIORef False
@@ -662,15 +708,17 @@ runPreparedVampireProcess
                                     impossible
                                         "runVampireProcess: missing process-group id"
                             restore
-                                (superviseVampireProcess
-                                    executable
-                                    (vampireTimeLimit vampireCommand)
-                                    preparedRequest
-                                    inputHandle
-                                    outputHandle
-                                    errorHandle
-                                    processGroup
-                                    processHandle)
+                                (do
+                                    observer preparedRequest
+                                    superviseVampireProcess
+                                        executable
+                                        (vampireTimeLimit vampireCommand)
+                                        preparedRequest
+                                        inputHandle
+                                        outputHandle
+                                        errorHandle
+                                        processGroup
+                                        processHandle)
                                 `Exception.onException`
                                     forceTerminateProcessGroup
                                         processGroup
diff --git a/source/Test/Golden.hs b/source/Test/Golden.hs
index 3c88b56..a62df9e 100644
--- a/source/Test/Golden.hs
+++ b/source/Test/Golden.hs
@@ -11,7 +11,6 @@ import Base
 import Provers (defaultTimeLimit)
 
 import Control.Monad.Logger
-import Control.Monad.Reader
 import Data.Text qualified as Text
 import Data.Text.IO qualified as TextIO
 import Data.Text.Lazy.IO qualified as LazyTextIO
@@ -22,27 +21,10 @@ import Test.Tasty.Golden (goldenVsFile, findByExtension)
 import Text.Pretty.Simple (pShowNoColor)
 import UnliftIO
 import UnliftIO.Environment
-import Api (Options(withDumpPremselTraining))
-
-testOptions :: Api.Options
-testOptions = Api.Options
-    { Api.withDumpPremselTraining = Api.WithoutDumpPremselTraining
-    , Api.withFilter = Api.WithoutFilter
-    , inputPath = error "testOptions: no inputPath"
-    , withDump = Api.WithoutDump
-    , withLogging = Api.WithoutLogging
-    , withMemoryLimit = Provers.defaultMemoryLimit
-    , withOmissions = Api.WithOmissions
-    , withParseOnly = Api.WithoutParseOnly
-    , withTimeLimit = Provers.defaultTimeLimit
-    , withVersion = Api.WithoutVersion
-    , withHtml = Api.WithoutHtml
-    }
-
 goldenTests :: IO TestTree
-goldenTests = runReaderT goldenTestGroup testOptions
+goldenTests = goldenTestGroup
 
-goldenTestGroup :: (MonadUnliftIO io, MonadReader Api.Options io) => io TestTree
+goldenTestGroup :: MonadUnliftIO io => io TestTree
 goldenTestGroup = testGroup "golden tests" <$> sequence
     [ tokenizing
     , scanning
@@ -82,7 +64,7 @@ createTripleDirectoriesIfMissing :: MonadIO io => Triple -> io ()
 createTripleDirectoriesIfMissing Triple{..} = liftIO $
     createDirectoryIfMissing True (takeDirectory output)
 
-makeGoldenTest :: (MonadUnliftIO io, MonadReader Api.Options io) => String -> (Triple -> io ()) -> io TestTree
+makeGoldenTest :: MonadUnliftIO io => String -> (Triple -> io ()) -> io TestTree
 makeGoldenTest stage action = do
     triples <- gatherTriples stage
     for triples createTripleDirectoriesIfMissing
@@ -96,42 +78,42 @@ makeGoldenTest stage action = do
         | triple@Triple{..} <- triples
         ]
 
-tokenizing :: (MonadUnliftIO io, MonadReader Api.Options io) => io TestTree
+tokenizing :: MonadUnliftIO io => io TestTree
 tokenizing = makeGoldenTest "tokenizing" $ \Triple{..} -> do
     tokenStream <- Api.tokenize input
     liftIO (LazyTextIO.writeFile output (pShowNoColor (Api.simpleStream tokenStream)))
 
 
-scanning :: (MonadUnliftIO io, MonadReader Api.Options io) => io TestTree
+scanning :: MonadUnliftIO io => io TestTree
 scanning = makeGoldenTest "scanning" $ \Triple{..} -> do
     lexicalItems <- Api.scan input
     liftIO (LazyTextIO.writeFile output (pShowNoColor lexicalItems))
 
-parsing :: (MonadUnliftIO io, MonadReader Api.Options io) => io TestTree
+parsing :: MonadUnliftIO io => io TestTree
 parsing = makeGoldenTest "parsing" $ \Triple{..} -> do
     parseResult <- Api.parse input
     liftIO (LazyTextIO.writeFile output (pShowNoColor parseResult))
 
 
-glossing :: (MonadUnliftIO io, MonadReader Api.Options io) => io TestTree
+glossing :: MonadUnliftIO io => io TestTree
 glossing = makeGoldenTest "glossing" $ \Triple{..} -> do
     interpretationResult <- Api.gloss input
     liftIO (LazyTextIO.writeFile output (pShowNoColor interpretationResult))
 
 
-generatingTasks :: (MonadUnliftIO io, MonadReader Api.Options io) => io TestTree
+generatingTasks :: MonadUnliftIO io => io TestTree
 generatingTasks = makeGoldenTest "generating tasks" $ \Triple{..} -> do
     tasks <- Api.generateTasks input
     liftIO $ LazyTextIO.writeFile output (pShowNoColor tasks)
 
 
-encodingTasks :: (MonadUnliftIO io, MonadReader Api.Options io) => io TestTree
+encodingTasks :: MonadUnliftIO io => io TestTree
 encodingTasks = makeGoldenTest "encoding tasks" $ \Triple{..} -> do
     tasks <- Api.encodeTasks input
     liftIO (TextIO.writeFile output (Text.intercalate "\n------------------\n" (toText <$> tasks)))
 
 
-verification :: (MonadUnliftIO io, MonadReader Api.Options io) => io TestTree
+verification :: MonadUnliftIO io => io TestTree
 verification = makeGoldenTest "verification" $ \Triple{..} -> do
     vampirePathPath <- (?? "vampire") <$> lookupEnv "NAPROCHE_ZF_VAMPIRE"
     let defaultVampire =
@@ -139,5 +121,7 @@ verification = makeGoldenTest "verification" $ \Triple{..} -> do
                 vampirePathPath
                 Provers.defaultTimeLimit
                 Provers.defaultMemoryLimit
-    answers <- runNoLoggingT (Api.verify defaultVampire input)
+    answers <-
+        runNoLoggingT (Api.verify defaultVampire input)
+            >>= either throwIO pure
     liftIO (LazyTextIO.writeFile output (pShowNoColor answers))
diff --git a/source/Test/Unit/CommandLine.hs b/source/Test/Unit/CommandLine.hs
index 9d6c71d..0a49fc4 100644
--- a/source/Test/Unit/CommandLine.hs
+++ b/source/Test/Unit/CommandLine.hs
@@ -5,11 +5,15 @@ module Test.Unit.CommandLine (unitTests) where
 import Base
 import Api (VerificationReport(..), VerificationRoute(..))
 import CommandLine
+import Felix.Store qualified as Store
 import Report.Location (pattern Nowhere)
 
 import Control.Exception (bracket)
+import Data.ByteString qualified as ByteString
 import Data.List qualified as List
 import Data.Text qualified as Text
+import Options.Applicative (ParserResult(..))
+import Options.Applicative qualified as Options
 import System.Directory qualified as Directory
 import System.Environment (getEnvironment)
 import System.Exit (ExitCode(..))
@@ -25,12 +29,24 @@ import Test.Tasty.HUnit
 unitTests :: TestTree
 unitTests =
     testGroup "Command line"
-        [ testCase "maps structured outcomes to process status" do
+        [ testCase "parses the closed command model"
+            parsesClosedCommands
+        , testCase "rejects conflicting command options"
+            rejectsConflictingOptions
+        , testCase "maps structured outcomes to process status" do
             for_ outcomeCases \(outcome, expectedExitCode) ->
                 commandOutcomeExitCode outcome
                     `shouldBe` expectedExitCode
         , testGroup "process boundary"
-            [ testCase "verified theorem exits successfully" do
+            [ testCase "version needs no input or store"
+                versionNeedsNoInputOrStore
+            , testCase "parse-only uses no store or Vampire"
+                parseOnlyUsesNoAuthority
+            , testCase "malformed source has a stable failure class"
+                malformedSourceHasStableFailure
+            , testCase "invalid output fails before default store startup"
+                invalidOutputPrecedesStoreStartup
+            , testCase "verified theorem exits successfully" do
                 (exitCode, stdout, stderr) <- runCliWithFakeVampire
                     [ "printf '%s\\n' '% SZS status Theorem for cli'"
                     , "exit 0"
@@ -75,9 +91,265 @@ unitTests =
                 exitCode `shouldBe` ExitFailure 2
                 stdout `shouldBe` ""
                 stderr `shouldContain` "ProverLaunchFailed"
+            , testCase "dumps the exact executed request once"
+                dumpsExactExecutedRequest
+            , testCase "launch failure dumps no request"
+                launchFailureDumpsNoRequest
+            , testCase "failed verification dumps only its executed prefix"
+                dumpsOnlyExecutedPrefix
+            , testCase "dump and HTML share one verification"
+                dumpAndHtmlVerifyOnce
+            , testCase "semantic failure publishes no HTML"
+                semanticFailurePublishesNoHtml
             ]
         ]
 
+parsesClosedCommands :: Assertion
+parsesClosedCommands = do
+    case parseCommandArguments ["--version"] of
+        Success Version ->
+            pure ()
+        other ->
+            assertFailure
+                ("unexpected version parse: " <> showParserResult other)
+    case parseCommandArguments ["input.tex", "--parseonly"] of
+        Success (ParseOnly (Input "input.tex")) ->
+            pure ()
+        other ->
+            assertFailure
+                ("unexpected parse-only parse: " <> showParserResult other)
+    case parseCommandArguments ["input.tex"] of
+        Success
+                (Verify
+                    (Input "input.tex")
+                    VerificationOptions
+                        { verificationStoreSelection =
+                            Store.DefaultStore
+                        }) ->
+            pure ()
+        other ->
+            assertFailure
+                ("unexpected default verify parse: "
+                    <> showParserResult other)
+    case parseCommandArguments ["input.tex", "--fresh"] of
+        Success
+                (Verify
+                    (Input "input.tex")
+                    VerificationOptions
+                        { verificationStoreSelection =
+                            Store.FreshTemporaryStore
+                        }) ->
+            pure ()
+        other ->
+            assertFailure
+                ("unexpected verify parse: " <> showParserResult other)
+
+rejectsConflictingOptions :: Assertion
+rejectsConflictingOptions = do
+    for_
+        [ ["input.tex", "--parseonly", "--fresh"]
+        , ["input.tex", "--parseonly", "--dump", "dump"]
+        , ["input.tex", "--parseonly", "--html"]
+        , ["input.tex", "--store", "store.sqlite", "--fresh"]
+        ]
+        \arguments ->
+            case parseCommandArguments arguments of
+                Failure _failure ->
+                    pure ()
+                other ->
+                    assertFailure
+                        ("conflicting options were accepted: "
+                            <> show arguments
+                            <> " as "
+                            <> showParserResult other)
+
+showParserResult :: ParserResult Command -> String
+showParserResult = \case
+    Success selected ->
+        show selected
+    Failure failure ->
+        fst (Options.renderFailure failure "zf")
+    CompletionInvoked _completion ->
+        "completion invoked"
+
+versionNeedsNoInputOrStore :: Assertion
+versionNeedsNoInputOrStore =
+    withCliFixture cliSource \fixture -> do
+        (exitCode, stdout, stderr) <-
+            runCliFixture fixture ["--version"]
+        exitCode `shouldBe` ExitSuccess
+        stdout `shouldContain` "Version 0.3.0.0"
+        stderr `shouldBe` ""
+        assertNoDefaultStore fixture
+
+parseOnlyUsesNoAuthority :: Assertion
+parseOnlyUsesNoAuthority =
+    withCliFixture cliSource \fixture -> do
+        writeFile
+            (cliFixtureVampire fixture)
+            "not executable"
+        (exitCode, stdout, stderr) <-
+            runCliFixture
+                fixture
+                ["input.tex", "--parseonly"]
+        exitCode `shouldBe` ExitSuccess
+        stdout `shouldBe` ""
+        stderr `shouldBe` ""
+        assertNoDefaultStore fixture
+
+malformedSourceHasStableFailure :: Assertion
+malformedSourceHasStableFailure =
+    withCliFixture malformedCliSource \fixture -> do
+        (exitCode, stdout, stderr) <-
+            runCliFixture
+                fixture
+                ["input.tex", "--parseonly"]
+        exitCode `shouldBe` ExitFailure 1
+        stdout `shouldBe` ""
+        stderr `shouldContain` "Parsing failed."
+        assertBool "does not print an internal error constructor"
+            (not ("SourceParseError" `List.isInfixOf` stderr))
+        assertNoDefaultStore fixture
+
+invalidOutputPrecedesStoreStartup :: Assertion
+invalidOutputPrecedesStoreStartup =
+    withCliFixture cliSource \fixture -> do
+        let dump = cliFixtureRoot fixture </> "dump"
+        Directory.createDirectory dump
+        writeFile (dump </> "stale.p") "stale"
+        (exitCode, stdout, stderr) <-
+            runCliFixture fixture
+                ["input.tex", "--dump", "dump"]
+        exitCode `shouldBe` ExitFailure 2
+        stdout `shouldBe` ""
+        stderr `shouldContain` "Verification output preflight failed."
+        assertNoDefaultStore fixture
+
+dumpsExactExecutedRequest :: Assertion
+dumpsExactExecutedRequest =
+    withCliFixture cliSource \fixture -> do
+        let captured = cliFixtureRoot fixture </> "captured.p"
+        writeExecutableScript
+            (cliFixtureVampire fixture)
+            [ "cat > " <> show captured
+            , "printf '%s\\n' '% SZS status Theorem for cli'"
+            ]
+        (exitCode, _stdout, stderr) <-
+            runCliFixture fixture
+                [ "input.tex"
+                , "--fresh"
+                , "--dump"
+                , "dump"
+                ]
+        exitCode `shouldBe` ExitSuccess
+        stderr `shouldContain` "Verification successful."
+        dumped <- ByteString.readFile
+            (cliFixtureRoot fixture </> "dump" </> "1.p")
+        sent <- ByteString.readFile captured
+        assertEqual "dump is the exact process input" sent dumped
+        assertBool "request is dumped only once"
+            . not
+            =<< Directory.doesPathExist
+                (cliFixtureRoot fixture </> "dump" </> "2.p")
+
+launchFailureDumpsNoRequest :: Assertion
+launchFailureDumpsNoRequest =
+    withCliFixture cliSource \fixture -> do
+        writeFile
+            (cliFixtureVampire fixture)
+            "not executable"
+        (exitCode, _stdout, stderr) <-
+            runCliFixture fixture
+                [ "input.tex"
+                , "--fresh"
+                , "--dump"
+                , "dump"
+                ]
+        exitCode `shouldBe` ExitFailure 2
+        stderr `shouldContain` "ProverLaunchFailed"
+        assertBool "no request was dumped before process launch"
+            . not
+            =<< Directory.doesPathExist
+                (cliFixtureRoot fixture </> "dump" </> "1.p")
+
+dumpsOnlyExecutedPrefix :: Assertion
+dumpsOnlyExecutedPrefix =
+    withCliFixture cliTwoSource \fixture -> do
+        writeExecutableScript
+            (cliFixtureVampire fixture)
+            [ "cat >/dev/null"
+            , "printf '%s\\n' '% SZS status CounterSatisfiable for cli'"
+            ]
+        (exitCode, _stdout, stderr) <-
+            runCliFixture fixture
+                [ "input.tex"
+                , "--fresh"
+                , "--dump"
+                , "dump"
+                ]
+        exitCode `shouldBe` ExitFailure 1
+        stderr `shouldContain` "prover found countermodel"
+        assertBool "executed request was dumped"
+            =<< Directory.doesFileExist
+                (cliFixtureRoot fixture </> "dump" </> "1.p")
+        assertBool "unexecuted request was not dumped"
+            . not
+            =<< Directory.doesPathExist
+                (cliFixtureRoot fixture </> "dump" </> "2.p")
+
+dumpAndHtmlVerifyOnce :: Assertion
+dumpAndHtmlVerifyOnce =
+    withCliFixture cliSource \fixture -> do
+        let countPath = cliFixtureRoot fixture </> "vampire-runs"
+        writeExecutableScript
+            (cliFixtureVampire fixture)
+            [ "cat >/dev/null"
+            , "printf '%s\\n' run >> " <> show countPath
+            , "printf '%s\\n' '% SZS status Theorem for cli'"
+            ]
+        (exitCode, _stdout, stderr) <-
+            runCliFixture fixture
+                [ "input.tex"
+                , "--fresh"
+                , "--dump"
+                , "dump"
+                , "--html"
+                ]
+        exitCode `shouldBe` ExitSuccess
+        stderr `shouldContain` "Verification successful."
+        runs <- List.lines <$> readFile countPath
+        assertEqual "one semantic verification" ["run"] runs
+        assertBool "request dump was published"
+            =<< Directory.doesFileExist
+                (cliFixtureRoot fixture </> "dump" </> "1.p")
+        assertBool "root HTML page was published"
+            =<< Directory.doesFileExist
+                (cliFixtureRoot fixture </> "html" </> "input.html")
+        assertBool "HTML support asset was published"
+            =<< Directory.doesFileExist
+                (cliFixtureRoot fixture
+                    </> "html"
+                    </> "_static"
+                    </> "naproche-html.js")
+
+semanticFailurePublishesNoHtml :: Assertion
+semanticFailurePublishesNoHtml =
+    withCliFixture cliSource \fixture -> do
+        writeExecutableScript
+            (cliFixtureVampire fixture)
+            [ "cat >/dev/null"
+            , "printf '%s\\n' '% SZS status CounterSatisfiable for cli'"
+            ]
+        (exitCode, _stdout, stderr) <-
+            runCliFixture fixture
+                ["input.tex", "--fresh", "--html"]
+        exitCode `shouldBe` ExitFailure 1
+        stderr `shouldContain` "prover found countermodel"
+        assertBool "semantic failure publishes no HTML"
+            . not
+            =<< Directory.doesPathExist
+                (cliFixtureRoot fixture </> "html")
+
 outcomeCases :: [(CommandOutcome, ExitCode)]
 outcomeCases =
     [ (CommandCompleted, ExitSuccess)
@@ -106,16 +378,8 @@ runCliWithFakeVampire
     -> IO (ExitCode, String, String)
 runCliWithFakeVampire scriptLines =
     runCliWithConfiguredVampire \vampirePath -> do
-        writeFile vampirePath
-            (unlines
-                ( [ "#!/bin/sh"
-                  , "cat >/dev/null"
-                  ]
-                    <> scriptLines
-                ))
-        permissions <- Directory.getPermissions vampirePath
-        Directory.setPermissions vampirePath
-            (Directory.setOwnerExecutable True permissions)
+        writeExecutableScript vampirePath
+            (["cat >/dev/null"] <> scriptLines)
 
 runCliWithConfiguredVampire
     :: (FilePath -> IO ())
@@ -128,31 +392,88 @@ runCliWithSourceAndConfiguredVampire
     -> (FilePath -> IO ())
     -> IO (ExitCode, String, String)
 runCliWithSourceAndConfiguredVampire source prepareVampire =
+    withCliFixture source \fixture -> do
+        prepareVampire (cliFixtureVampire fixture)
+        runCliFixture fixture ["input.tex", "--fresh"]
+
+data CliFixture = CliFixture
+    { cliFixtureRoot :: !FilePath
+    , cliFixtureExecutable :: !FilePath
+    , cliFixtureVampire :: !FilePath
+    , cliFixtureCacheRoot :: !FilePath
+    , cliFixtureEnvironment :: ![(String, String)]
+    }
+
+withCliFixture
+    :: String
+    -> (CliFixture -> IO value)
+    -> IO value
+withCliFixture source action =
     withTemporaryDirectory "felix-cli" \temp -> do
         zfExecutable <- requireZfExecutable
+        repositoryRoot <- Directory.getCurrentDirectory
         let sourcePath = temp </> "input.tex"
             vampirePath = temp </> "vampire"
             libraryPath = temp </> "library"
             debugPath = temp </> "debug"
+            cacheRoot = temp </> "cache"
         Directory.createDirectory libraryPath
         Directory.createDirectory debugPath
+        Directory.createDirectory cacheRoot
         writeFile sourcePath source
-        prepareVampire vampirePath
+        ByteString.readFile
+            (repositoryRoot </> "library" </> "lexicon.tsv")
+            >>= ByteString.writeFile
+                (libraryPath </> "lexicon.tsv")
         inheritedEnvironment <- getEnvironment
         let processEnvironment =
                 setEnvironmentVariable
-                    "NAPROCHE_ZF_VAMPIRE"
-                    vampirePath
+                    "XDG_CACHE_HOME"
+                    cacheRoot
                     (setEnvironmentVariable
-                        "NAPROCHE_LIB"
-                        libraryPath
-                        inheritedEnvironment)
-            command =
-                (proc zfExecutable ["input.tex"])
-                    { cwd = Just temp
-                    , env = Just processEnvironment
-                    }
-        readCreateProcessWithExitCode command ""
+                        "NAPROCHE_ZF_VAMPIRE"
+                        vampirePath
+                        (setEnvironmentVariable
+                            "NAPROCHE_LIB"
+                            libraryPath
+                            inheritedEnvironment))
+        action
+            CliFixture
+                { cliFixtureRoot = temp
+                , cliFixtureExecutable = zfExecutable
+                , cliFixtureVampire = vampirePath
+                , cliFixtureCacheRoot = cacheRoot
+                , cliFixtureEnvironment = processEnvironment
+                }
+
+runCliFixture
+    :: CliFixture
+    -> [String]
+    -> IO (ExitCode, String, String)
+runCliFixture fixture arguments =
+    readCreateProcessWithExitCode
+        ((proc
+            (cliFixtureExecutable fixture)
+            arguments)
+            { cwd = Just (cliFixtureRoot fixture)
+            , env = Just (cliFixtureEnvironment fixture)
+            })
+        ""
+
+assertNoDefaultStore :: CliFixture -> Assertion
+assertNoDefaultStore fixture =
+    assertBool "default store was not created"
+        . not
+        =<< Directory.doesPathExist
+            (cliFixtureCacheRoot fixture </> "felix")
+
+writeExecutableScript :: FilePath -> [String] -> IO ()
+writeExecutableScript path scriptLines = do
+    writeFile path
+        (unlines (["#!/bin/sh"] <> scriptLines))
+    permissions <- Directory.getPermissions path
+    Directory.setPermissions path
+        (Directory.setOwnerExecutable True permissions)
 
 requireZfExecutable :: IO FilePath
 requireZfExecutable = do
@@ -191,6 +512,25 @@ cliGapSource =
         , "\\end{proof}"
         ]
 
+cliTwoSource :: String
+cliTwoSource =
+    unlines
+        [ "\\begin{proposition}\\label{cli_first}"
+        , "    $\\forall x. x = x$."
+        , "\\end{proposition}"
+        , "\\begin{proposition}\\label{cli_second}"
+        , "    $\\forall y. y = y$."
+        , "\\end{proposition}"
+        ]
+
+malformedCliSource :: String
+malformedCliSource =
+    unlines
+        [ "\\begin{proposition}\\label{malformed}"
+        , "    This is not a proposition."
+        , "\\end{proposition}"
+        ]
+
 withTemporaryDirectory :: String -> (FilePath -> IO a) -> IO a
 withTemporaryDirectory template =
     bracket create Directory.removePathForcibly
diff --git a/source/Test/Unit/Module.hs b/source/Test/Unit/Module.hs
index 5df30ae..7ebc317 100644
--- a/source/Test/Unit/Module.hs
+++ b/source/Test/Unit/Module.hs
@@ -24,9 +24,7 @@ import Bound.Scope (fromScope)
 import Bound.Var (Var(..))
 import Data.ByteString qualified as ByteString
 import Data.Text.Encoding qualified as Text
-import Control.Exception (try)
 import Control.Monad.Logger (runNoLoggingT)
-import Control.Monad.Reader (runReaderT)
 import System.Directory (getCurrentDirectory)
 import System.FilePath.Posix qualified as Posix
 import Test.Tasty
@@ -298,20 +296,13 @@ resetsGlossStatePerModule = do
 rejectsUnsupportedTypedSource :: Assertion
 rejectsUnsupportedTypedSource = do
     result <-
-        try
-            (runNoLoggingT
-                (runReaderT
-                    (Api.verifyMeasured
-                        (Provers.vampire
-                            "vampire"
-                            Provers.defaultTimeLimit
-                            Provers.defaultMemoryLimit)
-                        "test/phase3/typed-unsupported.tex")
-                    testOptions))
-            :: IO
-                (Either
-                    Api.VerificationDriverError
-                    (Api.VerificationResult, Api.VerificationMeasurements))
+        runNoLoggingT
+            (Api.verifyMeasured
+                (Provers.vampire
+                    "vampire"
+                    Provers.defaultTimeLimit
+                    Provers.defaultMemoryLimit)
+                "test/phase3/typed-unsupported.tex")
     case result of
         Left
             (Api.VerificationTypedModuleError
@@ -347,16 +338,15 @@ routesProductionVerification = do
         importer
   where
     verifyFixture path =
-        runNoLoggingT
-            (runReaderT
-                (fst
-                    <$> Api.verifyMeasured
-                        (Provers.vampire
-                            "vampire"
-                            Provers.defaultTimeLimit
-                            Provers.defaultMemoryLimit)
-                        path)
-                testOptions)
+        fst
+            <$> (runNoLoggingT
+                (Api.verifyMeasured
+                    (Provers.vampire
+                        "vampire"
+                        Provers.defaultTimeLimit
+                        Provers.defaultMemoryLimit)
+                    path)
+                >>= expectRight)
 
     assertRoute label expected = \case
         Api.VerifiedWithTrustedVampire report ->
@@ -368,21 +358,6 @@ routesProductionVerification = do
         Api.VerificationFailure failure ->
             assertFailure (label <> " failed: " <> show failure)
 
-testOptions :: Api.Options
-testOptions = Api.Options
-    { Api.inputPath = ""
-    , Api.withDump = Api.WithoutDump
-    , Api.withFilter = Api.WithoutFilter
-    , Api.withLogging = Api.WithoutLogging
-    , Api.withMemoryLimit = Provers.defaultMemoryLimit
-    , Api.withOmissions = Api.WithOmissions
-    , Api.withParseOnly = Api.WithoutParseOnly
-    , Api.withTimeLimit = Provers.defaultTimeLimit
-    , Api.withVersion = Api.WithoutVersion
-    , Api.withHtml = Api.WithoutHtml
-    , Api.withDumpPremselTraining = Api.WithoutDumpPremselTraining
-    }
-
 unusedResolver :: Declaration.VampireResolver
 unusedResolver =
     Declaration.vampireResolver \_prepared ->