diff options
Diffstat (limited to 'source/CommandLine.hs')
| -rw-r--r-- | source/CommandLine.hs | 961 |
1 files changed, 0 insertions, 961 deletions
diff --git a/source/CommandLine.hs b/source/CommandLine.hs deleted file mode 100644 index ff970d3..0000000 --- a/source/CommandLine.hs +++ /dev/null @@ -1,961 +0,0 @@ -{-# LANGUAGE DerivingStrategies #-} -{-# LANGUAGE NoImplicitPrelude #-} - -module CommandLine where - -import Api -import Base -import Checking.Declaration qualified as Declaration -import Checking.Foundation qualified as Foundation -import Checking.Identity qualified as Identity -import Checking.Module qualified as Typed -import Felix.OutputPlan qualified as Output -import Felix.Parse (ParseWorkspaceError) -import Felix.Parse qualified as Parse -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 Report.Location -import Version qualified - -import Control.Exception (displayException) -import Control.Exception qualified as Exception -import Control.Monad.Logger -import Data.ByteString qualified as ByteString -import Data.Maybe (catMaybes) -import Data.Text qualified as StrictText -import Data.Text.IO qualified as Text -import GHC.Conc qualified -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 qualified as Posix -import System.IO (stderr) -import Text.Read (readMaybe) - - -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 - , verificationJobsOverride :: !(Maybe Provers.EffectiveJobs) - , 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 - | VerificationSucceeded !VerificationReport - | VerificationCompletedWithGaps !VerificationReport - | VerificationRejected - !VerificationReport - !Location - !VerificationRejection - | ProverFailed !VerificationReport !Location !ProverFailure - | VerificationCheckingRejected - !VerificationReport - !VerificationDriverError - | SourcePlanningFailed !ParseWorkspaceError - | ParseOnlyFailed !AuthorityFreeParseError - | VerificationDriverFailed !VerificationDriverError - | StorePlanningFailed !Store.StorePlanningError - | StoreIncompatible !Store.StorePath !Store.StoreIncompatibility - | StoreFailed !Store.StorePath !Store.StoreLifecycleError - | OutputPlanningFailed !Output.OutputPlanError - | HtmlLayoutFailed !HtmlLayout.HtmlLayoutError - | DumpObservationFailed !DumpObservationError - | HtmlExportFailed - !VerificationReport - !HtmlExport.HtmlExportError - | HtmlOutputPlanningFailed - !VerificationReport - !HtmlOutput.HtmlOutputError - | HtmlPublicationFailed - !VerificationReport - !HtmlOutput.HtmlPublicationError - deriving stock (Show) - -data VerificationRejection - = CountermodelFound !Text - | ContradictoryInputFound !Text - deriving stock (Show, Eq) - -data ProverFailure - = ProverIndeterminate !Text - | ProverProtocolFailure !Text !Text - | ProverTransportFailure !Provers.ProverProcessError - deriving stock (Show, Eq) - -data DumpObservationError - = DumpDirectoryCreationFailed !FilePath !Text - | DumpRequestWriteFailed - !WorkPosition - !FilePath - !Text - deriving stock (Show, Eq) - -instance Exception.Exception DumpObservationError - - -runCommandLine :: IO () -runCommandLine = do - arguments <- getArgs - selected <- handleParseResult (parseCommandArguments arguments) - outcome <- runCommand selected - renderCommandOutcome outcome - exitWith (commandOutcomeExitCode outcome) - -rawCommandParserInfo :: ParserInfo RawCommand -rawCommandParserInfo = - info - (helper <*> rawCommandParser) - (fullDesc <> header "Felix") - -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 -> do - htmlResult <- discoverHtmlDestinations input options - case htmlResult of - Left failure -> - pure failure - Right htmlDestinations -> - Store.withStoreLease storePlan \lease -> 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 - -discoverHtmlDestinations - :: Input - -> VerificationOptions - -> IO (Either CommandOutcome (Maybe [SafeRelativePath])) -discoverHtmlDestinations input options - | not (verificationHtmlRequested options) = - pure (Right Nothing) - | otherwise = do - sourcePlan <- - prepareDefaultSourceGraph - (inputFilePath input) - pure case sourcePlan of - Left failure -> - Left (SourcePlanningFailed failure) - Right graph -> - case planHtmlDestinations graph of - Left failure -> - Left (HtmlLayoutFailed failure) - Right destinations -> - Right (Just destinations) - -planHtmlDestinations - :: SourceGraph.ResolvedSourceGraph - -> Either HtmlLayout.HtmlLayoutError [SafeRelativePath] -planHtmlDestinations graph = do - layout <- - HtmlLayout.layoutHtmlSourceGraph - defaultHtmlMountPrefixes - graph - pure - ( [ HtmlLayout.routeDestination route - | (_source, route) <- - HtmlLayout.htmlPageRoutes layout - ] - <> [HtmlLayout.routeDestination - (HtmlLayout.htmlSupportScriptRoute layout)] - ) - -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 - store - pure - (case opened of - Left - (Store.StoreLifecycleOpenFailed - (Store.IncompatibleStore incompatibility)) -> - StoreIncompatible - (Store.storeLeasePath lease) - incompatibility - Left failure -> - StoreFailed - (Store.storeLeasePath lease) - failure - Right outcome -> - outcome) - -runOpenVerification - :: Input - -> VerificationOptions - -> Output.VerificationOutputPlan - -> Store.Store - -> IO CommandOutcome -runOpenVerification input options outputPlan store = do - observerResult <- - prepareRequestObserver - (Output.verificationDumpOutput outputPlan) - case observerResult of - Left failure -> - pure (DumpObservationFailed failure) - Right observer -> do - vampirePath <- getVampireExecutable - let vampire = - Provers.vampire - vampirePath - (verificationTimeLimit options) - (verificationMemoryLimit options) - validationMode = - case verificationStoreSelection options of - Store.FreshTemporaryStore -> - FreshStoreValidation - Store.DefaultStore -> - WarmStoreValidation - Store.ExplicitStore{} -> - WarmStoreValidation - jobs <- - Provers.selectEffectiveJobs - (verificationJobsOverride options) - GHC.Conc.getNumProcessors - observed <- - captureDumpFailure - (case verificationDiagnostics options of - QuietVerification -> - runNoLoggingT - (verifyWithObserverAndStoreModeAndJobs - store - validationMode - jobs - observer - vampire - (inputFilePath input)) - LogVerification -> - runStderrLoggingT - (verifyWithObserverAndStoreModeAndJobs - store - validationMode - jobs - observer - vampire - (inputFilePath input))) - case observed of - Left failure -> - pure (DumpObservationFailed failure) - Right (Left failure) -> - pure (VerificationDriverFailed failure) - Right (Right result) -> - finishVerification - 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 - -> WorkPosition - -> Provers.PreparedVerificationRequest - -> IO () -writeDumpRequest root position request = do - let destination = - root - Posix.</> ( show - (workPositionModuleOrdinal position) - <> "-" - <> show - (workPositionLocalRequestOrdinal position) - ) - Posix.<.> "p" - result <- tryIOError - (publishDumpFile - destination - (Provers.preparedVerificationBytes request)) - case result of - Left failure -> - Exception.throwIO - (DumpRequestWriteFailed - position - destination - (StrictText.pack - (displayException failure))) - Right () -> - pure () - -publishDumpFile :: FilePath -> ByteString.ByteString -> IO () -publishDumpFile destination bytes = do - let directory = Posix.takeDirectory destination - template = Posix.takeFileName destination <> ".tmp" - bracketOnError - (openBinaryTempFileWithDefaultPermissions directory template) - cleanupTemporary - \(temporary, handle) -> do - ByteString.hPut handle bytes - hFlush handle - hClose handle - Directory.renameFile temporary destination - -cleanupTemporary :: (FilePath, Handle) -> IO () -cleanupTemporary (temporary, handle) = do - void (tryIOError (hClose handle)) - void (tryIOError (Directory.removeFile temporary)) - -captureDumpFailure - :: IO value - -> IO (Either DumpObservationError value) -captureDumpFailure = - Exception.try - -finishVerification - :: Output.VerificationOutputPlan - -> VerificationResult - -> IO CommandOutcome -finishVerification outputPlan result = - case result of - VerificationFailure{} -> - pure (verificationCommandOutcome result) - VerificationCheckingFailure{} -> - pure (verificationCommandOutcome result) - VerificationCompleted report presentation -> - publishHtmlIfRequested - outputPlan - report - presentation - (VerificationSucceeded report) - CompletedWithExplicitGaps report presentation -> - publishHtmlIfRequested - outputPlan - report - presentation - (VerificationCompletedWithGaps report) - -publishHtmlIfRequested - :: Output.VerificationOutputPlan - -> VerificationReport - -> VerificationPresentation - -> CommandOutcome - -> IO CommandOutcome -publishHtmlIfRequested outputPlan report presentation successOutcome = - case Output.verificationHtmlRoutes outputPlan of - Nothing -> - pure successOutcome - Just routes -> do - prepared <- - prepareVerifiedHtmlExportResult presentation - case prepared of - Left failure -> - pure (HtmlExportFailed report failure) - Right artifacts -> - case HtmlOutput.planHtmlOutputAgainst routes artifacts of - Left failure -> - pure (HtmlOutputPlanningFailed report failure) - Right plan -> - HtmlOutput.writeHtmlOutput plan >>= \case - Left failure -> - pure (HtmlPublicationFailed report failure) - Right () -> - pure successOutcome - -verificationCommandOutcome :: VerificationResult -> CommandOutcome -verificationCommandOutcome = \case - VerificationCompleted report _presentation -> - VerificationSucceeded report - CompletedWithExplicitGaps report _presentation -> - VerificationCompletedWithGaps report - VerificationFailure - report - FailedVerification - { failedVerificationLocation = location - , failedVerificationReason = reason - } -> - case reason of - CountermodelFailure tptp -> - VerificationRejected - report location (CountermodelFound tptp) - ContradictoryInputFailure tptp -> - VerificationRejected - report location (ContradictoryInputFound tptp) - IndeterminateFailure tptp -> - ProverFailed report location (ProverIndeterminate tptp) - ProtocolFailure label message -> - ProverFailed - report location - (ProverProtocolFailure label message) - TransportFailure processError -> - ProverFailed - report location - (ProverTransportFailure processError) - VerificationCheckingFailure report failure -> - VerificationCheckingRejected report failure - -commandOutcomeExitCode :: CommandOutcome -> ExitCode -commandOutcomeExitCode = \case - CommandCompleted -> - ExitSuccess - VerificationSucceeded{} -> - ExitSuccess - VerificationCompletedWithGaps{} -> - ExitSuccess - VerificationRejected{} -> - ExitFailure 1 - ProverFailed{} -> - ExitFailure 2 - VerificationCheckingRejected{} -> - ExitFailure 1 - 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 - CommandCompleted -> - pure () - VerificationSucceeded report -> do - Text.hPutStrLn stderr "Verification successful." - renderVerificationReport report - VerificationCompletedWithGaps report -> do - Text.hPutStrLn stderr - "Verification completed with explicit proof gaps." - renderVerificationReport report - VerificationRejected report location rejection -> do - renderVerificationRejection location rejection - renderVerificationReport report - ProverFailed report location failure -> do - renderProverFailure location failure - renderVerificationReport report - VerificationCheckingRejected report failure -> do - renderVerificationDriverFailure failure - renderVerificationReport report - SourcePlanningFailed failure -> - renderFailure - ("Source planning failed: " - <> Parse.renderParseWorkspaceError failure) - ParseOnlyFailed failure -> - renderFailure - ("Parsing failed: " - <> renderAuthorityFreeParseError failure) - VerificationDriverFailed failure -> - renderVerificationDriverFailure failure - StorePlanningFailed failure -> - renderFailure - ("Store path planning failed: " - <> Store.renderStorePlanningError failure) - StoreIncompatible path failure -> - renderFailure - ("Disposable store " - <> quotePath (Store.storePathFilePath path) - <> " is incompatible: " - <> Store.renderStoreIncompatibility failure - <> ". Use --fresh, choose another --store path, or remove the disposable store.") - StoreFailed path failure -> - renderFailure - ("Store failure at " - <> quotePath (Store.storePathFilePath path) - <> ": " <> Store.renderStoreLifecycleError failure) - OutputPlanningFailed failure -> - renderFailure - ("Verification output preflight failed: " - <> Output.renderOutputPlanError failure) - HtmlLayoutFailed failure -> - renderFailure - ("HTML route planning failed: " - <> HtmlLayout.renderHtmlLayoutError failure) - DumpObservationFailed failure -> - renderDumpObservationFailure failure - HtmlExportFailed report failure -> do - renderFailure - ("Verification succeeded, but HTML preparation failed: " - <> HtmlExport.renderHtmlExportError failure) - renderVerificationReport report - HtmlOutputPlanningFailed report failure -> do - renderFailure - ("Verification succeeded, but prepared HTML did not match the reserved routes: " - <> HtmlOutput.renderHtmlOutputError failure) - renderVerificationReport report - HtmlPublicationFailed report failure -> do - renderFailure - "Verification succeeded, but HTML publication did not complete." - traverse_ - renderFailure - (HtmlOutput.renderHtmlPublicationError failure) - renderVerificationReport report - -renderFailure :: Text -> IO () -renderFailure = - Text.hPutStrLn stderr - -renderVerificationDriverFailure - :: VerificationDriverError - -> IO () -renderVerificationDriverFailure = - renderFailure . verificationDriverFailureMessage - -verificationDriverFailureMessage - :: VerificationDriverError - -> Text -verificationDriverFailureMessage = \case - VerificationWorkspaceError failure -> - "Verification input failed: " - <> Parse.renderParseWorkspaceError failure - VerificationTypedInputError source failure -> - "Typed module input failed in " - <> resolvedSourceDisplay source - <> ": " <> Typed.renderTypedModuleInputError failure - VerificationTypedOpenError source failure -> - "Typed module startup failed in " - <> resolvedSourceDisplay source - <> ": " <> Declaration.renderDriverOpenError failure - VerificationTypedCachedModuleError source failure -> - "Cached typed module is invalid in " - <> resolvedSourceDisplay source - <> ": " <> Typed.renderCachedTypedModuleError failure - VerificationTypedModuleError source failure _prefix -> - "Typed module checking failed in " - <> resolvedSourceDisplay source - <> ": " <> Typed.renderTypedModuleFailure failure - VerificationValidationIntegrityError source failure -> - "Typed module validation store is inconsistent in " - <> resolvedSourceDisplay source - <> ": " <> Declaration.renderValidationIntegrityError failure - VerificationAdmittedViewError source failure -> - "Typed admitted-source association is inconsistent in " - <> resolvedSourceDisplay source - <> ": " <> StrictText.pack (show failure) - VerificationParsedArtifactIntegrityError source failure -> - "Parsed artifact is inconsistent in " - <> resolvedSourceDisplay source - <> ": " <> StrictText.pack (show failure) - VerificationStoreFailure failure -> - "Verification store failed: " - <> Store.renderStoreFailure failure - VerificationStorePlanningFailure failure -> - "Verification store planning failed: " - <> Store.renderStorePlanningError failure - VerificationStoreLifecycleFailure failure -> - "Verification store lifecycle failed: " - <> Store.renderStoreLifecycleError failure - VerificationModuleArtifactKeyError{} -> - "Typed module artifact inputs are inconsistent." - VerificationModuleSchedulerInvariant message -> - "Typed module scheduler invariant failed: " <> message - VerificationFoundationManifestError{} -> - "The fixed foundation manifest is invalid." - VerificationMissingImportedModule address -> - "Verification could not find checked imported module " - <> StrictText.pack (show address) <> "." - VerificationMissingRootModule address -> - "Verification could not find checked root module " - <> StrictText.pack (show address) <> "." - VerificationFinalPreludeReadinessError{} -> - "The packaged final prelude failed." - -resolvedSourceDisplay :: ResolvedSource -> Text -resolvedSourceDisplay source = - sourceMountIdText (resolvedSourceMount source) - <> ":" - <> StrictText.pack (resolvedSourceLocationPath source) - -quotePath :: FilePath -> Text -quotePath = StrictText.pack . show - -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 - -> VerificationRejection - -> IO () -renderVerificationRejection location = \case - CountermodelFound tptp -> do - renderFailedTask tptp - Text.hPutStrLn stderr - ("Verification failed: prover found countermodel at " - <> locationToText location) - Text.hPutStrLn stderr - "This often happens when an explicit justification with \\cref{...} is missing some references." - ContradictoryInputFound tptp -> do - renderFailedTask tptp - Text.hPutStrLn stderr - ("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." - -renderProverFailure :: Location -> ProverFailure -> IO () -renderProverFailure location = \case - ProverIndeterminate tptp -> do - renderFailedTask tptp - Text.hPutStrLn stderr - ("Verification failed: prover returned an indeterminate result at " - <> locationToText location) - ProverProtocolFailure label message -> do - Text.hPutStrLn stderr - ("Prover error at " <> locationToText location <> ":") - Text.hPutStrLn stderr ("Task: " <> label) - Text.hPutStrLn stderr ("Error: " <> message) - ProverTransportFailure processError -> do - Text.hPutStrLn stderr - ("Prover process error at " <> locationToText location <> ":") - Text.hPutStrLn stderr (StrictText.pack (show processError)) - -renderFailedTask :: Text -> IO () -renderFailedTask tptp = do - Text.hPutStrLn stderr "(Failed TPTP task follows.)" - Text.hPutStrLn stderr tptp - -renderVerificationReport :: VerificationReport -> IO () -renderVerificationReport report = do - Text.hPutStrLn stderr - ( "Direct source authorization summary: " - <> renderCount - sourceAxiomCount - "source axiom" - <> ", " - <> renderCount - omittedCount - "explicit proof gap" - <> "." - ) - for_ - (verificationDirectEscapes report) - \escape -> - Text.hPutStrLn stderr case reportedEscapeKind escape of - ReportedSourceAxiom -> - "Source axiom at " - <> locationToText (reportedEscapeLocation escape) - ReportedOmitted -> - "Explicit proof gap at " - <> locationToText (reportedEscapeLocation escape) - where - sourceAxiomCount = - length - [ () - | escape <- verificationDirectEscapes report - , reportedEscapeKind escape == ReportedSourceAxiom - ] - omittedCount = - length - [ () - | escape <- verificationDirectEscapes report - , reportedEscapeKind escape == ReportedOmitted - ] - renderCount amount noun = - StrictText.pack (show amount) - <> " " - <> noun - <> if amount == 1 then "" else "s" - -getVampireExecutable :: IO FilePath -getVampireExecutable = - fromMaybe "vampire" <$> lookupEnv "NAPROCHE_ZF_VAMPIRE" - - -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) - , rawJobs :: !(Maybe Provers.EffectiveJobs) - , 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 jobsParser - <*> 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) - , verificationJobsOverride = rawJobs 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 - , "--jobs" <$ rawJobs 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." - ) - -jobsParser :: Parser Provers.EffectiveJobs -jobsParser = - option - (eitherReader parseJobs) - ( long "jobs" - <> short 'j' - <> metavar "JOBS" - <> help - "Run at most JOBS module checkers and Vampire invocations." - ) - where - parseJobs raw = - case readMaybe raw >>= Provers.effectiveJobs of - Just jobs -> Right jobs - Nothing -> Left "JOBS must be a positive integer" |