summaryrefslogtreecommitdiff
path: root/source/CommandLine.hs
diff options
context:
space:
mode:
Diffstat (limited to 'source/CommandLine.hs')
-rw-r--r--source/CommandLine.hs248
1 files changed, 151 insertions, 97 deletions
diff --git a/source/CommandLine.hs b/source/CommandLine.hs
index 69b893a..9e3e72c 100644
--- a/source/CommandLine.hs
+++ b/source/CommandLine.hs
@@ -5,7 +5,6 @@ module CommandLine where
import Api
import Base
-import Checking qualified
import Checking.Declaration qualified as Declaration
import Checking.Foundation qualified as Foundation
import Checking.Identity qualified as Identity
@@ -30,12 +29,14 @@ 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
@@ -52,6 +53,7 @@ data VerificationOptions = VerificationOptions
{ verificationStoreSelection :: !Store.StoreSelection
, verificationTimeLimit :: !Provers.TimeLimit
, verificationMemoryLimit :: !Provers.MemoryLimit
+ , verificationJobsOverride :: !(Maybe Provers.EffectiveJobs)
, verificationDumpDestination :: !(Maybe FilePath)
, verificationHtmlRequested :: !Bool
, verificationDiagnostics :: !VerificationDiagnostics
@@ -68,10 +70,16 @@ data CommandOutcome
= CommandCompleted
| VerificationSucceeded !VerificationReport
| VerificationCompletedWithGaps !VerificationReport
- | VerificationRejected !Location !VerificationRejection
- | ProverFailed !Location !ProverFailure
+ | VerificationRejected
+ !VerificationReport
+ !Location
+ !VerificationRejection
+ | ProverFailed !VerificationReport !Location !ProverFailure
+ | VerificationCheckingRejected
+ !VerificationReport
+ !VerificationDriverError
| SourcePlanningFailed !ParseWorkspaceError
- | ParseOnlyFailed !ParseWorkspaceError
+ | ParseOnlyFailed !AuthorityFreeParseError
| VerificationDriverFailed !VerificationDriverError
| StorePlanningFailed !Store.StorePlanningError
| StoreIncompatible !Store.StorePath !Store.StoreIncompatibility
@@ -79,9 +87,15 @@ data CommandOutcome
| OutputPlanningFailed !Output.OutputPlanError
| HtmlLayoutFailed !HtmlLayout.HtmlLayoutError
| DumpObservationFailed !DumpObservationError
- | HtmlExportFailed !HtmlExport.HtmlExportError
- | HtmlOutputPlanningFailed !HtmlOutput.HtmlOutputError
- | HtmlPublicationFailed !HtmlOutput.HtmlPublicationError
+ | HtmlExportFailed
+ !VerificationReport
+ !HtmlExport.HtmlExportError
+ | HtmlOutputPlanningFailed
+ !VerificationReport
+ !HtmlOutput.HtmlOutputError
+ | HtmlPublicationFailed
+ !VerificationReport
+ !HtmlOutput.HtmlPublicationError
deriving stock (Show)
data VerificationRejection
@@ -98,7 +112,7 @@ data ProverFailure
data DumpObservationError
= DumpDirectoryCreationFailed !FilePath !Text
| DumpRequestWriteFailed
- !VerificationRequestOrdinal
+ !WorkPosition
!FilePath
!Text
deriving stock (Show, Eq)
@@ -118,7 +132,7 @@ rawCommandParserInfo :: ParserInfo RawCommand
rawCommandParserInfo =
info
(helper <*> rawCommandParser)
- (fullDesc <> header "Naproche/ZF")
+ (fullDesc <> header "Felix")
runCommand :: Command -> IO CommandOutcome
runCommand = \case
@@ -271,22 +285,28 @@ runOpenVerification input options outputPlan store = do
WarmStoreValidation
Store.ExplicitStore{} ->
WarmStoreValidation
+ jobs <-
+ Provers.selectEffectiveJobs
+ (verificationJobsOverride options)
+ GHC.Conc.getNumProcessors
observed <-
captureDumpFailure
(case verificationDiagnostics options of
QuietVerification ->
runNoLoggingT
- (verifyWithObserverAndStoreMode
+ (verifyWithObserverAndStoreModeAndJobs
store
validationMode
+ jobs
observer
vampire
(inputFilePath input))
LogVerification ->
runStderrLoggingT
- (verifyWithObserverAndStoreMode
+ (verifyWithObserverAndStoreModeAndJobs
store
validationMode
+ jobs
observer
vampire
(inputFilePath input)))
@@ -297,7 +317,6 @@ runOpenVerification input options outputPlan store = do
pure (VerificationDriverFailed failure)
Right (Right result) ->
finishVerification
- input
outputPlan
result
@@ -331,14 +350,18 @@ prepareRequestObserver = \case
writeDumpRequest
:: FilePath
- -> VerificationRequestOrdinal
+ -> WorkPosition
-> Provers.PreparedVerificationRequest
-> IO ()
-writeDumpRequest root ordinal request = do
+writeDumpRequest root position request = do
let destination =
root
- Posix.</> show
- (verificationRequestOrdinalValue ordinal)
+ Posix.</> ( show
+ (workPositionModuleOrdinal position)
+ <> "-"
+ <> show
+ (workPositionLocalRequestOrdinal position)
+ )
Posix.<.> "p"
result <- tryIOError
(publishDumpFile
@@ -348,7 +371,7 @@ writeDumpRequest root ordinal request = do
Left failure ->
Exception.throwIO
(DumpRequestWriteFailed
- ordinal
+ position
destination
(StrictText.pack
(displayException failure)))
@@ -380,73 +403,86 @@ captureDumpFailure =
Exception.try
finishVerification
- :: Input
- -> Output.VerificationOutputPlan
+ :: Output.VerificationOutputPlan
-> VerificationResult
-> IO CommandOutcome
-finishVerification input outputPlan result =
+finishVerification outputPlan result =
case result of
VerificationFailure{} ->
pure (verificationCommandOutcome result)
- VerifiedWithTrustedVampire{} ->
- publishHtmlIfRequested input outputPlan result
- CompletedWithExplicitGaps{} ->
- publishHtmlIfRequested input outputPlan result
+ VerificationCheckingFailure{} ->
+ pure (verificationCommandOutcome result)
+ VerificationCompleted report presentation ->
+ publishHtmlIfRequested
+ outputPlan
+ report
+ presentation
+ (VerificationSucceeded report)
+ CompletedWithExplicitGaps report presentation ->
+ publishHtmlIfRequested
+ outputPlan
+ report
+ presentation
+ (VerificationCompletedWithGaps report)
publishHtmlIfRequested
- :: Input
- -> Output.VerificationOutputPlan
- -> VerificationResult
+ :: Output.VerificationOutputPlan
+ -> VerificationReport
+ -> VerificationPresentation
+ -> CommandOutcome
-> IO CommandOutcome
-publishHtmlIfRequested input outputPlan result =
+publishHtmlIfRequested outputPlan report presentation successOutcome =
case Output.verificationHtmlRoutes outputPlan of
Nothing ->
- pure (verificationCommandOutcome result)
+ pure successOutcome
Just routes -> do
prepared <-
- prepareHtmlExportResult
- (inputFilePath input)
+ prepareVerifiedHtmlExportResult presentation
case prepared of
Left failure ->
- pure (HtmlExportFailed failure)
- Right bundle ->
- case HtmlOutput.planHtmlOutputAgainst routes bundle of
+ pure (HtmlExportFailed report failure)
+ Right artifacts ->
+ case HtmlOutput.planHtmlOutputAgainst routes artifacts of
Left failure ->
- pure (HtmlOutputPlanningFailed failure)
+ pure (HtmlOutputPlanningFailed report failure)
Right plan ->
HtmlOutput.writeHtmlOutput plan >>= \case
Left failure ->
- pure (HtmlPublicationFailed failure)
+ pure (HtmlPublicationFailed report failure)
Right () ->
- pure
- (verificationCommandOutcome result)
+ pure successOutcome
verificationCommandOutcome :: VerificationResult -> CommandOutcome
verificationCommandOutcome = \case
- VerifiedWithTrustedVampire report ->
+ VerificationCompleted report _presentation ->
VerificationSucceeded report
- CompletedWithExplicitGaps report ->
+ CompletedWithExplicitGaps report _presentation ->
VerificationCompletedWithGaps report
VerificationFailure
+ report
FailedVerification
{ failedVerificationLocation = location
, failedVerificationReason = reason
} ->
case reason of
CountermodelFailure tptp ->
- VerificationRejected location (CountermodelFound tptp)
+ VerificationRejected
+ report location (CountermodelFound tptp)
ContradictoryInputFailure tptp ->
- VerificationRejected location (ContradictoryInputFound tptp)
+ VerificationRejected
+ report location (ContradictoryInputFound tptp)
IndeterminateFailure tptp ->
- ProverFailed location (ProverIndeterminate tptp)
+ ProverFailed report location (ProverIndeterminate tptp)
ProtocolFailure label message ->
ProverFailed
- location
+ report location
(ProverProtocolFailure label message)
TransportFailure processError ->
ProverFailed
- location
+ report location
(ProverTransportFailure processError)
+ VerificationCheckingFailure report failure ->
+ VerificationCheckingRejected report failure
commandOutcomeExitCode :: CommandOutcome -> ExitCode
commandOutcomeExitCode = \case
@@ -460,6 +496,8 @@ commandOutcomeExitCode = \case
ExitFailure 1
ProverFailed{} ->
ExitFailure 2
+ VerificationCheckingRejected{} ->
+ ExitFailure 1
SourcePlanningFailed{} ->
ExitFailure 1
ParseOnlyFailed{} ->
@@ -496,10 +534,15 @@ renderCommandOutcome = \case
Text.hPutStrLn stderr
"Verification completed with explicit proof gaps."
renderVerificationReport report
- VerificationRejected location rejection ->
+ VerificationRejected report location rejection -> do
renderVerificationRejection location rejection
- ProverFailed location failure ->
+ 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: "
@@ -507,7 +550,7 @@ renderCommandOutcome = \case
ParseOnlyFailed failure ->
renderFailure
("Parsing failed: "
- <> Parse.renderParseWorkspaceError failure)
+ <> renderAuthorityFreeParseError failure)
VerificationDriverFailed failure ->
renderVerificationDriverFailure failure
StorePlanningFailed failure ->
@@ -536,18 +579,23 @@ renderCommandOutcome = \case
<> HtmlLayout.renderHtmlLayoutError failure)
DumpObservationFailed failure ->
renderDumpObservationFailure failure
- HtmlExportFailed failure ->
+ HtmlExportFailed report failure -> do
renderFailure
- ("HTML preparation failed: "
+ ("Verification succeeded, but HTML preparation failed: "
<> HtmlExport.renderHtmlExportError failure)
- HtmlOutputPlanningFailed failure ->
+ renderVerificationReport report
+ HtmlOutputPlanningFailed report failure -> do
renderFailure
- ("Prepared HTML did not match the reserved routes: "
+ ("Verification succeeded, but prepared HTML did not match the reserved routes: "
<> HtmlOutput.renderHtmlOutputError failure)
- HtmlPublicationFailed 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 =
@@ -566,14 +614,6 @@ verificationDriverFailureMessage = \case
VerificationWorkspaceError failure ->
"Verification input failed: "
<> Parse.renderParseWorkspaceError failure
- VerificationGlossError source failure ->
- "Verification elaboration failed in "
- <> resolvedSourceDisplay source <> ": "
- <> StrictText.pack (show failure)
- VerificationCheckingError source failure ->
- "Verification checking failed in "
- <> resolvedSourceDisplay source
- <> ": " <> Checking.renderCheckingError failure
VerificationTypedInputError source failure ->
"Typed module input failed in "
<> resolvedSourceDisplay source
@@ -594,6 +634,10 @@ verificationDriverFailureMessage = \case
"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
@@ -609,12 +653,8 @@ verificationDriverFailureMessage = \case
<> Store.renderStoreLifecycleError failure
VerificationModuleArtifactKeyError{} ->
"Typed module artifact inputs are inconsistent."
- VerificationObligationResolutionError{} ->
- "Verification obligation resolution was inconsistent."
- VerificationLegacyModuleError{} ->
- "Legacy module staging failed."
- VerificationTransitionModuleError{} ->
- "Transition module staging failed."
+ VerificationModuleSchedulerInvariant message ->
+ "Typed module scheduler invariant failed: " <> message
VerificationFoundationManifestError{} ->
"The fixed foundation manifest is invalid."
VerificationMissingImportedModule address ->
@@ -623,10 +663,6 @@ verificationDriverFailureMessage = \case
VerificationMissingRootModule address ->
"Verification could not find checked root module "
<> StrictText.pack (show address) <> "."
- VerificationMigrationManifestError{} ->
- "The verification migration manifest is invalid."
- VerificationMigrationRouteMismatch{} ->
- "The verification migration selection is not dependency-closed."
VerificationFinalPreludeReadinessError{} ->
"The packaged final prelude failed."
@@ -699,40 +735,39 @@ renderFailedTask tptp = do
renderVerificationReport :: VerificationReport -> IO ()
renderVerificationReport report = do
Text.hPutStrLn stderr
- ( "Authorization summary: "
- <> renderCount
- (verificationLegacyDeclaredAssumptionCount report)
- "legacy declared assumption"
- <> ", "
- <> renderCount
- (verificationTypedDeclaredAssumptionCount report)
- "typed declared assumption"
- <> ", "
+ ( "Direct source authorization summary: "
<> renderCount
- (verificationTrustedVampireCount report)
- "trusted Vampire obligation"
+ sourceAxiomCount
+ "source axiom"
<> ", "
<> renderCount
- (length
- (verificationExplicitGapLocations report))
+ omittedCount
"explicit proof gap"
- <> ", "
- <> renderCount
- (verificationTrustedLegacyRuleCount report)
- "trusted legacy declaration rule"
- <> ", "
- <> renderCount
- (verificationKernelProofCount report)
- "replayed kernel proof"
<> "."
)
for_
- (verificationExplicitGapLocations report)
- \location ->
- Text.hPutStrLn stderr
- ("Explicit proof gap at "
- <> locationToText location)
+ (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)
<> " "
@@ -755,6 +790,7 @@ data RawFileCommand = RawFileCommand
, rawFresh :: !Bool
, rawTimeLimit :: !(Maybe Provers.TimeLimit)
, rawMemoryLimit :: !(Maybe Provers.MemoryLimit)
+ , rawJobs :: !(Maybe Provers.EffectiveJobs)
, rawDump :: !(Maybe FilePath)
, rawHtml :: !Bool
, rawLogging :: !Bool
@@ -794,6 +830,7 @@ rawFileCommandParser =
<> help "Use a fresh temporary disposable store.")
<*> optional timeLimitParser
<*> optional memoryLimitParser
+ <*> optional jobsParser
<*> optional
(strOption
(long "dump"
@@ -864,6 +901,7 @@ validateRawCommand = \case
fromMaybe
Provers.defaultMemoryLimit
(rawMemoryLimit raw)
+ , verificationJobsOverride = rawJobs raw
, verificationDumpDestination =
rawDump raw
, verificationHtmlRequested =
@@ -880,6 +918,7 @@ validateRawCommand = \case
, 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
@@ -904,3 +943,18 @@ memoryLimitParser =
<> 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 processes."
+ )
+ where
+ parseJobs raw =
+ case readMaybe raw >>= Provers.effectiveJobs of
+ Just jobs -> Right jobs
+ Nothing -> Left "JOBS must be a positive integer"
generated by cgit v1.2.3 (git 2.39.1) at 2026-08-04 07:35:38 +0000