diff options
Diffstat (limited to 'source/Felix/CommandLine.hs')
| -rw-r--r-- | source/Felix/CommandLine.hs | 911 |
1 files changed, 911 insertions, 0 deletions
diff --git a/source/Felix/CommandLine.hs b/source/Felix/CommandLine.hs new file mode 100644 index 0000000..448d698 --- /dev/null +++ b/source/Felix/CommandLine.hs @@ -0,0 +1,911 @@ +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE NoImplicitPrelude #-} + +module Felix.CommandLine + ( runCommandLine + , Input(..) + , VerificationOptions(..) + , Command(..) + , CommandOutcome(..) + , VerifiedOutputFailure(..) + , parseCommandArguments + , verificationCommandOutcome + , commandOutcomeExitCode + , renderCommandOutcome + ) where + +import Base +import Felix.OutputPlan qualified as Output +import Felix.Parse (ParseWorkspaceError) +import Felix.Parse qualified as Parse +import Felix.Provers qualified as Provers +import Felix.RequestDump qualified as RequestDump +import Felix.Source (SafeRelativePath) +import Felix.Source.Graph qualified as SourceGraph +import Felix.Store qualified as Store +import Felix.Verification qualified as Verification +import Felix.Version qualified as Version +import Felix.Workspace qualified as Workspace +import Felix.Render.Html.Export qualified as HtmlExport +import Felix.Render.Html.Layout qualified as HtmlLayout +import Felix.Render.Html.Output qualified as HtmlOutput +import Felix.Report.Location + +import Control.Monad (unless, when) +import Data.Maybe (catMaybes) +import Data.Text qualified as StrictText +import Data.Text.IO qualified as Text +import GHC.Conc qualified +import Numeric (showFFloat) +import Options.Applicative hiding (renderFailure) +import System.Environment (getArgs, lookupEnv) +import System.Exit (ExitCode(..), exitWith) +import System.IO (stderr) +import Text.Read (readMaybe) + + +newtype Input = Input + { inputFilePath :: FilePath + } + 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 + } + deriving stock (Show, Eq) + +data Command + = Version + | ParseOnly !Input + | Verify !Input !VerificationOptions + deriving stock (Show, Eq) + +data CommandOutcome + = CommandCompleted + | VerificationSucceeded + !Verification.VerificationReport + !Provers.SlowAtpReport + | VerificationCompletedWithGaps + !Verification.VerificationReport + !Provers.SlowAtpReport + | VerificationRejected + !Verification.VerificationReport + !Verification.FailedVerification + !Provers.SlowAtpReport + | VerificationCheckingRejected + !Verification.VerificationReport + !Verification.VerificationDriverError + !Provers.SlowAtpReport + | SourcePlanningFailed !ParseWorkspaceError + | ParseOnlyFailed !Workspace.AuthorityFreeParseError + | VerificationDriverFailed !Verification.VerificationDriverError + | VerificationSessionFailed + !Store.StorePath + !Verification.VerificationSessionError + | StorePlanningFailed !Store.StorePlanningError + | StoreIncompatible !Store.StorePath !Store.StoreIncompatibility + | StoreFailed !Store.StorePath !Store.StoreLifecycleError + | OutputPlanningFailed !Output.OutputPlanError + | HtmlLayoutFailed !HtmlLayout.HtmlLayoutError + | DumpObservationFailed !RequestDump.DumpObservationError + | VerifiedOutputFailed + !Verification.VerificationReport + !VerifiedOutputFailure + !Provers.SlowAtpReport + deriving stock (Show) + +data VerifiedOutputFailure + = VerifiedHtmlExportFailed !HtmlExport.HtmlExportError + | VerifiedHtmlOutputPlanningFailed !HtmlOutput.HtmlOutputError + | VerifiedHtmlPublicationFailed !HtmlOutput.HtmlPublicationError + | VerifiedHtmlLayoutUnavailable + deriving stock (Show) + +data HtmlPreflight = HtmlPreflight + !Workspace.WorkspaceEnvironment + !SourceGraph.ResolvedSourceGraph + !HtmlLayout.HtmlLayout + ![SafeRelativePath] + + +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) -> + Workspace.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 htmlPreflight -> + Store.withStoreLease storePlan \lease -> do + outputResult <- + Output.planVerificationOutputs + (Store.storeLeasePath lease) + (verificationDumpDestination options) + (fmap + (\(HtmlPreflight + _environment _graph _layout destinations) -> + ("html", destinations)) + htmlPreflight) + case outputResult of + Left failure -> + pure (OutputPlanningFailed failure) + Right outputPlan -> + openVerificationSession + input + options + lease + outputPlan + htmlPreflight + +discoverHtmlDestinations + :: Input + -> VerificationOptions + -> IO (Either CommandOutcome (Maybe HtmlPreflight)) +discoverHtmlDestinations input options + | not (verificationHtmlRequested options) = + pure (Right Nothing) + | otherwise = do + prepared <- prepareInputSourceGraph input + pure case prepared of + Left failure -> Left (SourcePlanningFailed failure) + Right (environment, graph) -> + case planHtmlDestinations environment graph of + Left failure -> Left (HtmlLayoutFailed failure) + Right (layout, destinations) -> + Right + (Just + (HtmlPreflight + environment graph layout destinations)) + +planHtmlDestinations + :: Workspace.WorkspaceEnvironment + -> SourceGraph.ResolvedSourceGraph + -> Either + HtmlLayout.HtmlLayoutError + (HtmlLayout.HtmlLayout, [SafeRelativePath]) +planHtmlDestinations environment graph = do + layout <- + HtmlLayout.layoutHtmlSourceGraph + (Workspace.workspaceHtmlMountPrefixes environment) + graph + pure + ( layout + , [ HtmlLayout.routeDestination route + | (_source, route) <- + HtmlLayout.htmlPageRoutes layout + ] + <> [HtmlLayout.routeDestination + (HtmlLayout.htmlSupportScriptRoute layout)] + ) + +prepareInputSourceGraph + :: Input + -> IO + (Either + ParseWorkspaceError + (Workspace.WorkspaceEnvironment, SourceGraph.ResolvedSourceGraph)) +prepareInputSourceGraph input = do + preparedEnvironment <- Workspace.prepareDefaultWorkspaceEnvironment + case preparedEnvironment of + Left failure -> pure (Left failure) + Right environment -> do + preparedRoot <- Workspace.prepareWorkspaceRoot + environment + (inputFilePath input) + case preparedRoot of + Left failure -> pure (Left failure) + Right root -> + fmap (fmap (\graph -> (environment, graph))) + (Workspace.prepareSourceGraph environment root) + +openVerificationSession + :: Input + -> VerificationOptions + -> Store.StoreLease + -> Output.VerificationOutputPlan + -> Maybe HtmlPreflight + -> IO CommandOutcome +openVerificationSession input options lease outputPlan htmlPreflight = do + opened <- Verification.withVerificationSession lease + (\session -> + runOpenVerification + input + options + outputPlan + htmlPreflight + session) + pure case opened of + Left + (Verification.VerificationSessionStoreError + (Store.StoreLifecycleOpenFailed + (Store.IncompatibleStore incompatibility))) -> + StoreIncompatible + (Store.storeLeasePath lease) + incompatibility + Left (Verification.VerificationSessionStoreError failure) -> + StoreFailed (Store.storeLeasePath lease) failure + Left failure -> + VerificationSessionFailed (Store.storeLeasePath lease) failure + Right outcome -> outcome + +runOpenVerification + :: Input + -> VerificationOptions + -> Output.VerificationOutputPlan + -> Maybe HtmlPreflight + -> Verification.VerificationSession + -> IO CommandOutcome +runOpenVerification input options outputPlan htmlPreflight session = do + observerResult <- + RequestDump.prepareRequestObserver + (Output.verificationDumpOutput outputPlan) + case observerResult of + Left failure -> + pure (DumpObservationFailed failure) + Right observer -> do + (preparedGraph, htmlOutputPreparation) <- case htmlPreflight of + Just (HtmlPreflight + environment graph layout _destinations) -> + pure + ( Right graph + , Just + ( Workspace.workspaceRendererSearchRoots environment + , layout + ) + ) + Nothing -> do + graphResult <- fmap snd <$> prepareInputSourceGraph input + pure (graphResult, Nothing) + case preparedGraph of + Left failure -> pure (SourcePlanningFailed failure) + Right graph -> do + vampirePath <- getVampireExecutable + jobs <- Provers.selectEffectiveJobs + (verificationJobsOverride options) + GHC.Conc.getNumProcessors + let vampire = + Provers.vampire + vampirePath + (verificationTimeLimit options) + (verificationMemoryLimit options) + validationMode = + case verificationStoreSelection options of + Store.FreshTemporaryStore -> + Verification.FreshStoreValidation + Store.DefaultStore -> + Verification.WarmStoreValidation + Store.ExplicitStore{} -> + Verification.WarmStoreValidation + request = Verification.CheckRequest + { Verification.checkSourceGraph = graph + , Verification.checkStoreValidationMode = + validationMode + , Verification.checkEffectiveJobs = jobs + , Verification.checkVampire = vampire + , Verification.checkRequestObserver = observer + } + observed <- RequestDump.captureDumpFailure + (Verification.checkWorkspace session request) + case observed of + Left failure -> pure (DumpObservationFailed failure) + Right (Left failure) -> + pure (VerificationDriverFailed failure) + Right (Right outcome) -> + finishVerification + outputPlan + htmlOutputPreparation + outcome + +finishVerification + :: Output.VerificationOutputPlan + -> Maybe ([FilePath], HtmlLayout.HtmlLayout) + -> Verification.CheckOutcome + -> IO CommandOutcome +finishVerification outputPlan selectedLayout outcome = + case result of + Verification.VerificationFailure{} -> + pure (verificationCommandOutcome result slowReport) + Verification.VerificationCheckingFailure{} -> + pure (verificationCommandOutcome result slowReport) + Verification.VerificationCompleted report presentation -> + publishHtmlIfRequested + outputPlan + selectedLayout + report + presentation + (VerificationSucceeded report slowReport) + slowReport + Verification.CompletedWithExplicitGaps report presentation -> + publishHtmlIfRequested + outputPlan + selectedLayout + report + presentation + (VerificationCompletedWithGaps report slowReport) + slowReport + where + result = Verification.checkVerificationResult outcome + slowReport = Verification.checkSlowAtpReport outcome + +publishHtmlIfRequested + :: Output.VerificationOutputPlan + -> Maybe ([FilePath], HtmlLayout.HtmlLayout) + -> Verification.VerificationReport + -> Verification.VerificationPresentation + -> CommandOutcome + -> Provers.SlowAtpReport + -> IO CommandOutcome +publishHtmlIfRequested + outputPlan selectedLayout report presentation successOutcome slowReport = + case Output.verificationHtmlRoutes outputPlan of + Nothing -> + pure successOutcome + Just routes -> do + case selectedLayout of + Nothing -> + pure + (VerifiedOutputFailed + report + VerifiedHtmlLayoutUnavailable + slowReport) + Just (rendererRoots, layout) -> do + prepared <- + HtmlExport.prepareHtmlExportWithLayoutFromRendererRoots + rendererRoots + layout + (Verification.verificationHtmlPresentation presentation) + case prepared of + Left failure -> + pure + (VerifiedOutputFailed + report + (VerifiedHtmlExportFailed failure) + slowReport) + Right artifacts -> + case HtmlOutput.planHtmlOutputAgainst routes artifacts of + Left failure -> + pure + (VerifiedOutputFailed + report + (VerifiedHtmlOutputPlanningFailed failure) + slowReport) + Right plan -> + HtmlOutput.writeHtmlOutput plan >>= \case + Left failure -> + pure + (VerifiedOutputFailed + report + (VerifiedHtmlPublicationFailed + failure) + slowReport) + Right () -> + pure successOutcome + +verificationCommandOutcome + :: Verification.VerificationResult + -> Provers.SlowAtpReport + -> CommandOutcome +verificationCommandOutcome result slowReport = case result of + Verification.VerificationCompleted report _presentation -> + VerificationSucceeded report slowReport + Verification.CompletedWithExplicitGaps report _presentation -> + VerificationCompletedWithGaps report slowReport + Verification.VerificationFailure report failure -> + VerificationRejected report failure slowReport + Verification.VerificationCheckingFailure report failure -> + VerificationCheckingRejected report failure slowReport + +commandOutcomeExitCode :: CommandOutcome -> ExitCode +commandOutcomeExitCode = \case + CommandCompleted -> + ExitSuccess + VerificationSucceeded{} -> + ExitSuccess + VerificationCompletedWithGaps{} -> + ExitSuccess + VerificationRejected _report failed _slow -> + case Verification.failedVerificationReason failed of + Verification.CountermodelFailure{} -> ExitFailure 1 + Verification.ContradictoryInputFailure{} -> ExitFailure 1 + Verification.IndeterminateFailure{} -> ExitFailure 2 + Verification.ProtocolFailure{} -> ExitFailure 2 + Verification.TransportFailure{} -> ExitFailure 2 + VerificationCheckingRejected _report failure _slow -> + case Verification.verificationDriverErrorKind failure of + Verification.VerificationSourceFailure -> ExitFailure 1 + Verification.VerificationInfrastructureFailure -> ExitFailure 2 + SourcePlanningFailed{} -> + ExitFailure 1 + ParseOnlyFailed{} -> + ExitFailure 1 + VerificationDriverFailed failure -> + case Verification.verificationDriverErrorKind failure of + Verification.VerificationSourceFailure -> ExitFailure 1 + Verification.VerificationInfrastructureFailure -> ExitFailure 2 + VerificationSessionFailed{} -> + ExitFailure 2 + StorePlanningFailed{} -> + ExitFailure 2 + StoreIncompatible{} -> + ExitFailure 2 + StoreFailed{} -> + ExitFailure 2 + OutputPlanningFailed{} -> + ExitFailure 2 + HtmlLayoutFailed{} -> + ExitFailure 2 + DumpObservationFailed{} -> + ExitFailure 2 + VerifiedOutputFailed{} -> + ExitFailure 2 + +renderCommandOutcome :: CommandOutcome -> IO () +renderCommandOutcome = \case + CommandCompleted -> + pure () + VerificationSucceeded report slowReport -> do + Text.hPutStrLn stderr "Verification successful." + renderVerificationReport report + renderSlowAtpReport slowReport + VerificationCompletedWithGaps report slowReport -> do + Text.hPutStrLn stderr + "Verification completed with explicit proof gaps." + renderVerificationReport report + renderSlowAtpReport slowReport + VerificationRejected report failure slowReport -> do + renderFailedVerification failure + renderVerificationReport report + renderSlowAtpReport slowReport + VerificationCheckingRejected report failure slowReport -> do + renderVerificationDriverFailure failure + renderVerificationReport report + renderSlowAtpReport slowReport + SourcePlanningFailed failure -> + renderFailure + ("Source planning failed: " + <> Parse.renderParseWorkspaceError failure) + ParseOnlyFailed failure -> + renderFailure + ("Parsing failed: " + <> Workspace.renderAuthorityFreeParseError failure) + VerificationDriverFailed failure -> + renderVerificationDriverFailure failure + VerificationSessionFailed path failure -> + renderFailure case failure of + Verification.VerificationSessionFoundationError{} -> + "The fixed foundation manifest is invalid." + Verification.VerificationSessionStoreError storeFailure -> + "Store failure at " + <> quotePath (Store.storePathFilePath path) + <> ": " + <> Store.renderStoreLifecycleError storeFailure + Verification.VerificationSessionTheoryMismatch expected actual -> + "Store theory mismatch at " + <> quotePath (Store.storePathFilePath path) + <> ": expected " + <> StrictText.pack (show expected) + <> ", found " + <> StrictText.pack (show actual) + 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 -> + renderFailure (RequestDump.renderDumpObservationError failure) + VerifiedOutputFailed report failure slowReport -> do + renderVerifiedOutputFailure failure + renderVerificationReport report + renderSlowAtpReport slowReport + +renderFailure :: Text -> IO () +renderFailure = + Text.hPutStrLn stderr + +renderVerificationDriverFailure + :: Verification.VerificationDriverError + -> IO () +renderVerificationDriverFailure = + renderFailure . Verification.renderVerificationDriverError + +quotePath :: FilePath -> Text +quotePath = StrictText.pack . show + +renderFailedVerification :: Verification.FailedVerification -> IO () +renderFailedVerification failed = + case Verification.failedVerificationReason failed of + Verification.CountermodelFailure 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." + Verification.ContradictoryInputFailure 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." + Verification.IndeterminateFailure tptp -> do + renderFailedTask tptp + Text.hPutStrLn stderr + ("Verification failed: prover returned an indeterminate result at " + <> locationToText location) + Verification.ProtocolFailure label message -> do + Text.hPutStrLn stderr + ("Prover error at " <> locationToText location <> ":") + Text.hPutStrLn stderr ("Task: " <> label) + Text.hPutStrLn stderr ("Error: " <> message) + Verification.TransportFailure processError -> do + Text.hPutStrLn stderr + ("Prover process error at " <> locationToText location <> ":") + Text.hPutStrLn stderr (StrictText.pack (show processError)) + where + location = Verification.failedVerificationLocation failed + +renderVerifiedOutputFailure :: VerifiedOutputFailure -> IO () +renderVerifiedOutputFailure = \case + VerifiedHtmlExportFailed failure -> + renderFailure + ("Verification succeeded, but HTML preparation failed: " + <> HtmlExport.renderHtmlExportError failure) + VerifiedHtmlOutputPlanningFailed failure -> + renderFailure + ("Verification succeeded, but prepared HTML did not match the reserved routes: " + <> HtmlOutput.renderHtmlOutputError failure) + VerifiedHtmlPublicationFailed failure -> do + renderFailure + "Verification succeeded, but HTML publication did not complete." + traverse_ + renderFailure + (HtmlOutput.renderHtmlPublicationError failure) + VerifiedHtmlLayoutUnavailable -> + renderFailure + "Verification succeeded, but the preflight HTML layout was unavailable." + +renderFailedTask :: Text -> IO () +renderFailedTask tptp = do + Text.hPutStrLn stderr "(Failed TPTP task follows.)" + Text.hPutStrLn stderr tptp + +renderVerificationReport :: Verification.VerificationReport -> IO () +renderVerificationReport report = do + Text.hPutStrLn stderr + ( "Direct source authorization summary: " + <> renderCount + sourceAxiomCount + "source axiom" + <> ", " + <> renderCount + omittedCount + "explicit proof gap" + <> "." + ) + for_ + (Verification.verificationDirectEscapes report) + \escape -> + Text.hPutStrLn stderr case Verification.reportedEscapeKind escape of + Verification.ReportedSourceAxiom -> + "Source axiom at " + <> locationToText + (Verification.reportedEscapeLocation escape) + Verification.ReportedOmitted -> + "Explicit proof gap at " + <> locationToText + (Verification.reportedEscapeLocation escape) + where + sourceAxiomCount = + length + [ () + | escape <- Verification.verificationDirectEscapes report + , Verification.reportedEscapeKind escape + == Verification.ReportedSourceAxiom + ] + omittedCount = + length + [ () + | escape <- Verification.verificationDirectEscapes report + , Verification.reportedEscapeKind escape + == Verification.ReportedOmitted + ] + renderCount amount noun = + StrictText.pack (show amount) + <> " " + <> noun + <> if amount == 1 then "" else "s" + +renderSlowAtpReport :: Provers.SlowAtpReport -> IO () +renderSlowAtpReport report = + unless (null (Provers.slowAtpTasks report)) do + Text.hPutStrLn stderr + "Slow Vampire tasks (executor wall time; run-local performance note):" + traverse_ renderTask (Provers.slowAtpTasks report) + let omitted = Provers.slowAtpOmittedTaskCount report + when (omitted > 0) + (Text.hPutStrLn stderr + ( StrictText.pack + (show (length (Provers.slowAtpTasks report))) + <> " slowest shown; " + <> StrictText.pack (show omitted) + <> " additional tasks took at least 5.0 seconds." + )) + where + renderTask task = + Text.hPutStrLn stderr + ( " " + <> renderAtpDuration (Provers.slowAtpDuration task) + <> " " + <> renderSlowAtpOutcome (Provers.slowAtpOutcome task) + <> " at " + <> locationToText (Provers.slowAtpLocation task) + <> " (module " + <> renderNatural + (Provers.workPositionModuleOrdinal + (Provers.slowAtpPosition task)) + <> ", request " + <> renderNatural + (Provers.workPositionLocalRequestOrdinal + (Provers.slowAtpPosition task)) + <> ", id " + <> StrictText.pack (show (Provers.slowAtpRequestId task)) + <> ")" + ) + + renderNatural = StrictText.pack . show + +renderAtpDuration :: Provers.AtpDuration -> Text +renderAtpDuration duration = + StrictText.pack + (showFFloat + (Just 2) + (fromIntegral (Provers.atpDurationNanoseconds duration) + / (1000000000 :: Double)) + "s") + +renderSlowAtpOutcome :: Provers.SlowAtpOutcome -> Text +renderSlowAtpOutcome = \case + Provers.SlowAtpAccepted -> "accepted" + Provers.SlowAtpRejected rejection -> + "rejected (" <> StrictText.pack (show rejection) <> ")" + Provers.SlowAtpProtocolFailed -> "protocol failure" + Provers.SlowAtpProcessFailed -> "process failure" + +getVampireExecutable :: IO FilePath +getVampireExecutable = + fromMaybe "vampire" <$> lookupEnv "FELIX_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 + } + +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.") + +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 + }) + 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 + ] + +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" |