summaryrefslogtreecommitdiff
path: root/source/Api.hs
diff options
context:
space:
mode:
Diffstat (limited to 'source/Api.hs')
-rw-r--r--source/Api.hs1973
1 files changed, 0 insertions, 1973 deletions
diff --git a/source/Api.hs b/source/Api.hs
deleted file mode 100644
index d9fca1d..0000000
--- a/source/Api.hs
+++ /dev/null
@@ -1,1973 +0,0 @@
-{-# LANGUAGE ExplicitForAll #-}
-{-# LANGUAGE MultiWayIf #-}
-{-# LANGUAGE NoImplicitPrelude #-}
-{-# LANGUAGE TupleSections #-}
-{-# LANGUAGE NoMonomorphismRestriction #-}
-{-# LANGUAGE RankNTypes #-}
-
-module Api
- ( tokenize, TokStream
- , scan
- , parse
- , parseWorkspace
- , AuthorityFreeParseError(..)
- , renderAuthorityFreeParseError
- , simpleStream
- , builtins
- , ParseException(..)
- , verify, verifyMeasured
- , verifyWithObserverAndStoreMode
- , verifyMeasuredWithObserverAndStoreMode
- , verifyWithObserverAndStoreModeAndJobs
- , verifyMeasuredWithObserverAndStoreModeAndJobs
- , StoreValidationMode(..)
- , WorkPosition
- , workPosition
- , workPositionModuleOrdinal
- , workPositionLocalRequestOrdinal
- , VerificationRequestObserver
- , verificationRequestObserver
- , ProverAnswer
- ( CounterSatisfiable
- , ContradictoryAxioms
- , Uncertain
- , Error
- )
- , pattern Yes
- , VerificationResult(..)
- , VerificationPresentation
- , ReportedEscapeKind(..)
- , ReportedEscape(..)
- , VerificationReport(..)
- , VerificationMeasurements(..)
- , VerificationDriverError(..)
- , FailedVerification(..)
- , VerificationFailureReason(..)
- , prepareVerifiedHtmlExportResult
- , prepareDefaultSourceGraph
- , defaultHtmlMountPrefixes
- ) where
-
-
-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 Checking.Semantic qualified as Semantic
-import Felix.Module (localDeclarationOrdinal)
-import Felix.Parse (ParseException(..), ParseWorkspaceError(..), ParsedSourceWorkspace)
-import Felix.Parse qualified as Felix
-import Felix.Prelude qualified as Prelude
-import Felix.Source
-import Felix.Store qualified as Store
-import Felix.Source.Graph (ResolvedSourceGraph)
-import Felix.Source.Graph qualified as SourceGraph
-import Provers
-import Render.Html.Export qualified as HtmlExport
-import Render.Html.Output (PreparedHtmlArtifact)
-import Report.Location
-import Syntax.Abstract qualified as Raw
-import Syntax.Adapt (scanChunk, ScannedLexicalItem)
-import Syntax.Interface qualified as Syntax
-import Syntax.Lexicon (builtins)
-import Syntax.Token
-
-import Control.Exception qualified as Exception
-import Control.Monad.Logger
-import Control.Monad (unless)
-import Data.Bifunctor (first)
-import Data.List.NonEmpty qualified as NonEmpty
-import Data.Map.Strict qualified as Map
-import Data.Text qualified as StrictText
-import Data.Text.Encoding.Error (UnicodeException)
-import Data.Text.IO qualified as Text
-import Numeric.Natural (Natural)
-import System.FilePath.Posix
-import Text.Megaparsec hiding (failure, parse, Token, try)
-import UnliftIO
-import UnliftIO.Async qualified as Async
-import UnliftIO.Directory
-import UnliftIO.Environment
-
--- Renderer data follows the established current-directory, configured-library,
--- and debug-directory lookup policy.
-findAndReadRendererFile
- :: FilePath
- -> IO (Either HtmlExport.HtmlExportError Text)
-findAndReadRendererFile path = do
- rootsResult <- tryRendererIO do
- currentDir <- getCurrentDirectory
- configuredLibrary <- lookupEnv "NAPROCHE_LIB"
- let libraryDir =
- fromMaybe
- (currentDir </> "library")
- configuredLibrary
- pure
- [ currentDir </> path
- , libraryDir </> path
- , currentDir </> "debug" </> path
- ]
- case rootsResult of
- Left failure ->
- pure
- (Left
- (HtmlExport.HtmlRendererDataLookupFailed
- path
- (StrictText.pack
- (displayException failure))))
- Right candidates -> do
- selected <- selectRendererData path candidates
- case selected of
- Left failure ->
- pure (Left failure)
- Right selectedPath -> do
- readResult <- tryRendererRead
- (Text.readFile selectedPath)
- pure case readResult of
- Left reason ->
- Left
- (HtmlExport.HtmlRendererDataReadFailed
- selectedPath
- reason)
- Right contents ->
- Right contents
-
-selectRendererData
- :: FilePath
- -> [FilePath]
- -> IO (Either HtmlExport.HtmlExportError FilePath)
-selectRendererData requested candidates =
- go candidates
- where
- go = \case
- [] ->
- pure
- (Left
- (HtmlExport.HtmlRendererDataNotFound
- requested
- candidates))
- candidate : remaining -> do
- inspected <- tryRendererIO
- (doesFileExist candidate)
- case inspected of
- Left failure ->
- pure
- (Left
- (HtmlExport.HtmlRendererDataLookupFailed
- candidate
- (StrictText.pack
- (displayException failure))))
- Right True ->
- pure (Right candidate)
- Right False ->
- go remaining
-
-tryRendererIO :: IO value -> IO (Either IOException value)
-tryRendererIO = Exception.try
-
-tryRendererRead :: IO value -> IO (Either Text value)
-tryRendererRead action =
- Exception.catch
- (Exception.catch
- (Right <$> action)
- renderIOException)
- renderUnicodeException
- where
- renderIOException :: IOException -> IO (Either Text value)
- renderIOException =
- pure . Left . StrictText.pack . displayException
-
- renderUnicodeException
- :: UnicodeException
- -> IO (Either Text value)
- renderUnicodeException =
- pure . Left . StrictText.pack . displayException
-
-lexFile :: MonadIO io => FilePath -> io (Text, [[Located Token]])
-lexFile file = do
- prepared <- liftIO (prepareDefaultSourceRequest file)
- (mounts, request) <- either throwWorkspaceError pure prepared
- loaded <-
- liftIO (resolveAndLoadRoot mounts request)
- >>= either throwIO pure
- let source = loadedSource loaded
- raw = loadedText loaded
- locationPath = resolvedSourceLocationPath source
- canonicalPath =
- canonicalPathFilePath
- (resolvedSourceCanonicalPath source)
- registration <-
- registerFilePathWithDisplay
- canonicalPath
- locationPath
- fileId <- either
- (throwIO . SourceLocationRegistrationFailed source)
- pure
- registration
- case runLexer fileId locationPath raw of
- Left tokenError ->
- throwIO (TokenError (errorBundlePretty tokenError))
- Right (_imports, chunks) ->
- pure (raw, chunks)
-
--- | Throws a 'ParseException' when tokenizing fails.
-tokenize :: MonadIO io => FilePath -> io TokStream
-tokenize file = do
- (raw, chunks) <- lexFile file
- pure (TokStream raw chunks)
-
--- | Scan the given file for lexical items. The actual parsing process
--- builds one workspace lexicon instead.
-scan :: MonadIO io => FilePath -> io [ScannedLexicalItem]
-scan input = do
- tokenStream <- tokenize input
- fmap (concatMap (fmap unLocated)) $
- traverse
- (either (throwIO . LexicalScanFailure) pure . scanChunk)
- (unTokStream tokenStream)
-
-
--- | Parse a file. Throws an 'AuthorityFreeParseError' when packaged-prelude
--- loading/parsing or ordinary workspace parsing fails.
-parse :: MonadIO io => FilePath -> io [Raw.Block]
-parse file = do
- result <- parseWorkspace file
- either throwIO pure result
-
-data AuthorityFreeParseError
- = AuthorityFreePreludeLoadFailed !Prelude.PreludeLoadError
- | AuthorityFreePreludeParseFailed !Prelude.PreludeParseError
- | AuthorityFreeWorkspaceFailed !ParseWorkspaceError
- deriving (Show)
-
-instance Exception AuthorityFreeParseError
-
-renderAuthorityFreeParseError :: AuthorityFreeParseError -> Text
-renderAuthorityFreeParseError = \case
- AuthorityFreePreludeLoadFailed failure ->
- "packaged final prelude loading failed: "
- <> Prelude.renderPreludeLoadError failure
- AuthorityFreePreludeParseFailed failure ->
- "packaged final prelude parsing failed: "
- <> Prelude.renderPreludeParseError failure
- AuthorityFreeWorkspaceFailed failure ->
- Felix.renderParseWorkspaceError failure
-
-parseWorkspace
- :: MonadIO io
- => FilePath
- -> io (Either AuthorityFreeParseError [Raw.Block])
-parseWorkspace file =
- fmap Felix.importedBeforeImporterBlocks
- <$> liftIO (parseDefaultWorkspaceWithPrelude file)
-
-parseDefaultWorkspaceWithPrelude
- :: FilePath
- -> IO
- (Either
- AuthorityFreeParseError
- ParsedSourceWorkspace)
-parseDefaultWorkspaceWithPrelude file =
- Prelude.loadReservedPreludeSourceInput >>= \case
- Left failure ->
- pure (Left (AuthorityFreePreludeLoadFailed failure))
- Right source ->
- Prelude.parseReservedPreludeSource source >>= \case
- Left failure ->
- pure (Left (AuthorityFreePreludeParseFailed failure))
- Right prelude -> do
- prepared <- prepareDefaultSourceRequest file
- case prepared of
- Left failure ->
- pure
- (Left
- (AuthorityFreeWorkspaceFailed failure))
- Right (mounts, request) -> do
- let syntax =
- Felix.identifiedParsedModuleSyntaxInterface
- (Prelude.reservedParsedPreludeModule
- prelude)
- fmap
- (first AuthorityFreeWorkspaceFailed . fmap fst)
- (Felix.parseSourceWorkspaceMeasuredWithSyntaxInputsAndGraphValidation
- mounts
- request
- (const [syntax])
- (Prelude.rejectOrdinaryPreludeSourceGraph
- source))
-
-prepareDefaultSourceRequest
- :: FilePath
- -> IO (Either ParseWorkspaceError (SourceMounts, RootRequest))
-prepareDefaultSourceRequest file = do
- mountsResult <- prepareDefaultSourceMounts
- requestResult <- classifyRootRequest file
- pure case (mountsResult, requestResult) of
- (Left err, _) ->
- Left (SourceWorkspaceError err)
- (_, Left err) ->
- Left (SourceWorkspaceError err)
- (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
- configuredLibrary <- lookupEnv "NAPROCHE_LIB"
- let libraryDir = configuredLibrary ?? (currentDir </> "library")
- debugDir = currentDir </> "debug"
- prepareSourceMounts
- [ (sourceMountId "project", currentDir)
- , (sourceMountId "library", libraryDir)
- , (sourceMountId "debug", debugDir)
- ]
-
-classifyRootRequest :: FilePath -> IO (Either SourceError RootRequest)
-classifyRootRequest file
- | isAbsolute file =
- existingRoot file
- | otherwise =
- pure (searchedRoot file)
-
-throwWorkspaceError :: MonadIO io => ParseWorkspaceError -> io a
-throwWorkspaceError = \case
- SourceWorkspaceError err ->
- throwIO err
- err@(SourceLexiconCollision _) ->
- throwIO err
- err@(SourceSyntaxPragmaError _source _pragmaError) ->
- throwIO err
- err@(SourceSyntaxDeclarationError _source _declarationError) ->
- throwIO err
- err@(SourceSyntaxMaterializationError _materializationError) ->
- throwIO err
- err@(SourceParsedModuleKeyError _source _keyError) ->
- throwIO err
- SourceParseError _source err ->
- throwIO err
-
-
-simpleStream :: TokStream -> [[Token]]
-simpleStream TokStream{unTokStream=chunks} = [unLocated <$> ch | ch <- chunks]
-
-data VerificationResult
- = VerificationCompleted
- !VerificationReport
- !VerificationPresentation
- | CompletedWithExplicitGaps
- !VerificationReport
- !VerificationPresentation
- | VerificationFailure !VerificationReport !FailedVerification
- | VerificationCheckingFailure
- !VerificationReport
- !VerificationDriverError
- deriving (Show)
-
--- | Strict owner-independent source presentation retained only after the
--- complete typed workspace succeeds.
-data VerificationPresentation = VerificationPresentation
- !HtmlExport.HtmlPresentation
-
-instance Show VerificationPresentation where
- show _presentation =
- "VerificationPresentation <HTML presentation>"
-
-data ReportedEscapeKind
- = ReportedSourceAxiom
- | ReportedOmitted
- deriving (Show, Eq)
-
-data ReportedEscape = ReportedEscape
- { reportedEscapeKind :: !ReportedEscapeKind
- , reportedEscapeLocation :: !Location
- }
- deriving (Show, Eq)
-
-data VerificationReport = VerificationReport
- { verificationDirectEscapes :: ![ReportedEscape]
- }
- deriving (Show, Eq)
-
--- | Invocation-local observation of the verification pipeline.
---
--- Durations use the monotonic clock and are never part of fact authority or
--- deterministic verification results.
-data VerificationMeasurements = VerificationMeasurements
- { verificationParseMeasurements :: !Felix.ParseMeasurements
- , verificationSourcePreparationNanoseconds :: !Word64
- , verificationInvocationNanoseconds :: !Word64
- , verificationCheckingNanoseconds :: !Word64
- , verificationModuleCount :: !Int
- , verificationDetectedProcessorCount :: !(Maybe Int)
- , verificationEffectiveJobs :: !Int
- , verificationJobsOverridden :: !Bool
- , verificationMaximumLiveModuleCheckers :: !Int
- , verificationMaximumLiveVampireProcesses :: !Int
- , verificationMaximumReadyModuleCount :: !Int
- , verificationObligationBatchCount :: !Int
- , verificationPreparedObligationCount :: !Int
- , verificationMaximumObligationBatchSize :: !Int
- , verificationPreparedRequestBytes :: !Word64
- , verificationRequestPreparationNanoseconds :: !Word64
- , verificationVampireRunCount :: !Int
- , verificationModuleRootHitCount :: !Int
- , verificationModuleRootMissCount :: !Int
- , verificationFirstVampireStartNanoseconds
- :: !(Maybe Word64)
- , verificationFinalVampireSubmissionNanoseconds
- :: !(Maybe Word64)
- , verificationFinalVampireCompletionNanoseconds
- :: !(Maybe Word64)
- , verificationVampireExecutionNanoseconds :: !Word64
- , verificationLongestVampireExecutionNanoseconds :: !Word64
- }
- deriving (Show, Eq)
-
-data VerificationObservation = VerificationObservation
- { observedModuleCount :: !Int
- , observedDetectedProcessorCount :: !(Maybe Int)
- , observedEffectiveJobs :: !Int
- , observedJobsOverridden :: !Bool
- , observedLiveModuleCheckers :: !Int
- , observedMaximumLiveModuleCheckers :: !Int
- , observedMaximumLiveVampireProcesses :: !Int
- , observedMaximumReadyModuleCount :: !Int
- , observedObligationBatchCount :: !Int
- , observedPreparedObligationCount :: !Int
- , observedMaximumObligationBatchSize :: !Int
- , observedPreparedRequestBytes :: !Word64
- , observedRequestPreparationNanoseconds :: !Word64
- , observedVampireRunCount :: !Int
- , observedModuleRootHitCount :: !Int
- , observedModuleRootMissCount :: !Int
- , observedFirstVampireStart :: !(Maybe Word64)
- , observedFinalVampireSubmission :: !(Maybe Word64)
- , observedFinalVampireCompletion :: !(Maybe Word64)
- , observedVampireExecutionNanoseconds :: !Word64
- , observedLongestVampireExecutionNanoseconds :: !Word64
- }
-
-initialVerificationObservation :: VerificationObservation
-initialVerificationObservation =
- VerificationObservation
- { observedModuleCount = 0
- , observedDetectedProcessorCount = Nothing
- , observedEffectiveJobs = 1
- , observedJobsOverridden = False
- , observedLiveModuleCheckers = 0
- , observedMaximumLiveModuleCheckers = 0
- , observedMaximumLiveVampireProcesses = 0
- , observedMaximumReadyModuleCount = 0
- , observedObligationBatchCount = 0
- , observedPreparedObligationCount = 0
- , observedMaximumObligationBatchSize = 0
- , observedPreparedRequestBytes = 0
- , observedRequestPreparationNanoseconds = 0
- , observedVampireRunCount = 0
- , observedModuleRootHitCount = 0
- , observedModuleRootMissCount = 0
- , observedFirstVampireStart = Nothing
- , observedFinalVampireSubmission = Nothing
- , observedFinalVampireCompletion = Nothing
- , observedVampireExecutionNanoseconds = 0
- , observedLongestVampireExecutionNanoseconds = 0
- }
-
-newtype VerificationRequestObserver = VerificationRequestObserver
- { observeVerificationRequest
- :: WorkPosition
- -> PreparedVerificationRequest
- -> IO ()
- }
-
-verificationRequestObserver
- :: (WorkPosition
- -> PreparedVerificationRequest
- -> IO ())
- -> VerificationRequestObserver
-verificationRequestObserver =
- VerificationRequestObserver
-
-ignoreVerificationRequests :: VerificationRequestObserver
-ignoreVerificationRequests =
- VerificationRequestObserver \_ordinal _request -> pure ()
-
-data FailedVerification = FailedVerification
- { failedVerificationLocation :: !Location
- , failedVerificationReason :: !VerificationFailureReason
- }
- deriving (Show)
-
-data VerificationFailureReason
- = CountermodelFailure !Text
- | ContradictoryInputFailure !Text
- | IndeterminateFailure !Text
- | ProtocolFailure !Text !Text
- | TransportFailure !ProverProcessError
- deriving (Show)
-
-verificationFailureReason
- :: Either ProverProcessError ProverAnswer
- -> Maybe VerificationFailureReason
-verificationFailureReason = \case
- Left processError ->
- Just (TransportFailure processError)
- Right Yes ->
- Nothing
- Right (CounterSatisfiable tptp) ->
- Just (CountermodelFailure tptp)
- Right (ContradictoryAxioms tptp) ->
- Just (ContradictoryInputFailure tptp)
- Right (Uncertain tptp) ->
- Just (IndeterminateFailure tptp)
- Right (Error taskLabel message) ->
- Just (ProtocolFailure taskLabel message)
-
-data VerificationDriverError
- = VerificationWorkspaceError
- !ParseWorkspaceError
- | VerificationFoundationManifestError
- !(NonEmpty Foundation.FoundationManifestError)
- | VerificationMissingImportedModule
- !ResolvedSourceAddress
- | VerificationMissingRootModule
- !ResolvedSourceAddress
- | VerificationFinalPreludeReadinessError
- !Typed.FinalPreludeReadinessError
- | VerificationTypedInputError
- !ResolvedSource
- !Typed.TypedModuleInputError
- | VerificationTypedOpenError
- !ResolvedSource
- !Declaration.DriverOpenError
- | VerificationTypedCachedModuleError
- !ResolvedSource
- !Typed.CachedTypedModuleError
- | VerificationTypedModuleError
- !ResolvedSource
- !Typed.TypedModuleFailure
- !Declaration.PendingModulePrefix
- | VerificationValidationIntegrityError
- !ResolvedSource
- !Declaration.ValidationIntegrityError
- | VerificationAdmittedViewError
- !ResolvedSource
- !AdmittedViewError
- | VerificationParsedArtifactIntegrityError
- !ResolvedSource
- !Felix.ParsedArtifactIntegrityError
- | VerificationStoreFailure !Store.StoreFailure
- | VerificationStorePlanningFailure !Store.StorePlanningError
- | VerificationStoreLifecycleFailure !Store.StoreLifecycleError
- | VerificationModuleArtifactKeyError !Semantic.ModuleArtifactKeyError
- | VerificationModuleSchedulerInvariant !Text
- deriving (Show)
-
-instance Exception VerificationDriverError
-
-data TypedWorkspaceOutcome
- = TypedWorkspaceSucceeded
- !AdmittedTypedWorkspace
- | TypedWorkspaceRejected
- !AdmittedTypedWorkspace
- !TypedWorkspaceFailure
-
-data TypedWorkspaceFailure
- = TypedWorkspaceCheckingRejected !VerificationDriverError
- | TypedWorkspaceProverRejected !FailedVerification
-
-data ModuleTask = ModuleTask
- { moduleTaskOrdinal :: !Natural
- , moduleTaskParsed :: !Felix.ParsedModule
- , moduleTaskDirectAddresses :: ![ResolvedSourceAddress]
- }
-
-data ModuleCheckResult
- = ModuleCheckSucceeded
- !ResolvedSourceAddress
- !Typed.SealedTypedModule
- !AdmittedTypedModule
- | ModuleCheckRejected
- !AdmittedTypedModule
- !TypedWorkspaceFailure
-
-data ModuleFailureCandidate = ModuleFailureCandidate
- !Natural
- !AdmittedTypedModule
- !TypedWorkspaceFailure
-
-data AdmittedTypedDeclaration = AdmittedTypedDeclaration
- !Semantic.DeclarationSlot
- !Typed.TypedSourceDeclaration
-
-newtype AdmittedTypedModule = AdmittedTypedModule
- [AdmittedTypedDeclaration]
-
-newtype AdmittedTypedWorkspace = AdmittedTypedWorkspace
- [AdmittedTypedModule]
-
-data AdmittedViewError
- = AdmittedDeclarationCountMismatch
- !Int
- !Int
- | AdmittedDeclarationSlotMismatch
- ![Semantic.DeclarationSlot]
- ![Semantic.DeclarationSlot]
- deriving (Show, Eq)
-
-completeAdmittedModule
- :: Typed.IdentifiedModuleInput
- -> AdmittedTypedModule
-completeAdmittedModule input =
- AdmittedTypedModule
- (uncurry AdmittedTypedDeclaration <$> expectedDeclarations input)
-
-checkedAdmittedModule
- :: Bool
- -> Typed.IdentifiedModuleInput
- -> Declaration.PendingModulePrefix
- -> Either AdmittedViewError AdmittedTypedModule
-checkedAdmittedModule requireComplete input prefix = do
- let expected = expectedDeclarations input
- expectedSlots = fst <$> expected
- actualSlots =
- Declaration.committedBatchSlot
- <$> Declaration.pendingModulePrefixBatches prefix
- admittedCount = length actualSlots
- if requireComplete
- then unless
- (admittedCount == length expected)
- (Left
- (AdmittedDeclarationCountMismatch
- (length expected)
- admittedCount))
- else unless
- (admittedCount <= length expected)
- (Left
- (AdmittedDeclarationCountMismatch
- (length expected)
- admittedCount))
- unless
- (actualSlots == take admittedCount expectedSlots)
- (Left
- (AdmittedDeclarationSlotMismatch
- (take admittedCount expectedSlots)
- actualSlots))
- pure
- (AdmittedTypedModule
- [ AdmittedTypedDeclaration slot declaration
- | (slot, declaration) <- take admittedCount expected
- ])
-
-expectedDeclarations
- :: Typed.IdentifiedModuleInput
- -> [(Semantic.DeclarationSlot, Typed.TypedSourceDeclaration)]
-expectedDeclarations input =
- zipWith
- (\ordinal declaration ->
- ( Semantic.declarationSlot
- (Typed.identifiedModuleOwner input)
- (localDeclarationOrdinal ordinal)
- , declaration
- ))
- [0..]
- (Typed.typedSourceDeclarations
- (Typed.identifiedModuleParsed input))
-
-data StoreValidationMode
- = FreshStoreValidation
- | WarmStoreValidation
- deriving (Show, Eq)
-
-verifyWithObserverAndStoreMode
- :: (MonadUnliftIO io, MonadLogger io)
- => Store.Store
- -> StoreValidationMode
- -> VerificationRequestObserver
- -> Vampire
- -> FilePath
- -> io (Either VerificationDriverError VerificationResult)
-verifyWithObserverAndStoreMode store validationMode observer prover file =
- verifyWithObserverAndStoreModeAndJobs
- store validationMode sequentialJobs observer prover file
-
-verifyWithObserverAndStoreModeAndJobs
- :: (MonadUnliftIO io, MonadLogger io)
- => Store.Store
- -> StoreValidationMode
- -> JobsSelection
- -> VerificationRequestObserver
- -> Vampire
- -> FilePath
- -> io (Either VerificationDriverError VerificationResult)
-verifyWithObserverAndStoreModeAndJobs
- store validationMode jobs observer prover file =
- fmap (fmap fst)
- (verifyMeasuredWithObserverAndStoreModeAndJobs
- store validationMode jobs observer prover file)
-
-verifyMeasuredWithObserverAndStoreMode
- :: (MonadUnliftIO io, MonadLogger io)
- => Store.Store
- -> StoreValidationMode
- -> VerificationRequestObserver
- -> Vampire
- -> FilePath
- -> io
- (Either
- VerificationDriverError
- (VerificationResult, VerificationMeasurements))
-verifyMeasuredWithObserverAndStoreMode
- store validationMode observer prover file =
- verifyMeasuredWithObserverAndStoreModeAndJobs
- store validationMode sequentialJobs observer prover file
-
-verifyMeasuredWithObserverAndStoreModeAndJobs
- :: (MonadUnliftIO io, MonadLogger io)
- => Store.Store
- -> StoreValidationMode
- -> JobsSelection
- -> VerificationRequestObserver
- -> Vampire
- -> FilePath
- -> io
- (Either
- VerificationDriverError
- (VerificationResult, VerificationMeasurements))
-verifyMeasuredWithObserverAndStoreModeAndJobs
- store validationMode jobs observer prover file =
- try
- (verifyMeasuredThrowingWithStore
- store validationMode jobs observer prover file)
-
-sequentialJobs :: JobsSelection
-sequentialJobs =
- JobsSelection
- { jobsSelectionDetectedProcessors = Nothing
- , jobsSelectionEffectiveJobs =
- fromMaybe
- (impossible "one is not a positive worker count")
- (effectiveJobs 1)
- , jobsSelectionWasOverridden = True
- }
-
-verifyMeasured
- :: (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)
-verifyMeasuredThrowing requestObserver prover file = do
- foundation <-
- either
- (throwIO . VerificationFoundationManifestError)
- pure
- Foundation.checkedFoundation
- planned <- liftIO (Store.planStore Store.FreshTemporaryStore)
- plan <- either
- (throwIO . VerificationStorePlanningFailure)
- pure
- planned
- withRunInIO \runInIO ->
- Store.withStoreLease plan \lease -> do
- opened <- Store.withOpenStore
- lease
- (Identity.theoryId foundation)
- (\_startup store ->
- runInIO
- (verifyMeasuredThrowingWithStore
- store
- FreshStoreValidation
- sequentialJobs
- requestObserver
- prover
- file))
- either
- (throwIO . VerificationStoreLifecycleFailure)
- pure
- opened
-
-verifyMeasuredThrowingWithStore
- :: (MonadUnliftIO io, MonadLogger io)
- => Store.Store
- -> StoreValidationMode
- -> JobsSelection
- -> VerificationRequestObserver
- -> Vampire
- -> FilePath
- -> io (VerificationResult, VerificationMeasurements)
-verifyMeasuredThrowingWithStore
- store validationMode jobsSelection requestObserver prover file = do
- invocationStart <- liftIO getMonotonicTimeNSec
- memo <- liftIO (Store.newStoreMemo store)
- storeCoordinator <- liftIO Store.newStoreCoordinator
- ( admittedResult
- , parseMeasurements
- , sourcePreparation
- , checkingStart
- , checkingEnd
- , observation
- , parsedPresentation
- ) <-
- liftIO
- (withVampireExecutor
- (jobsSelectionEffectiveJobs jobsSelection)
- prover
- (observeVerificationRequest requestObserver)
- \executor -> do
- observationRef <- newIORef
- initialVerificationObservation
- { observedDetectedProcessorCount =
- jobsSelectionDetectedProcessors jobsSelection
- , observedEffectiveJobs =
- effectiveJobsValue
- (jobsSelectionEffectiveJobs jobsSelection)
- , observedJobsOverridden =
- jobsSelectionWasOverridden jobsSelection
- }
- foundation <-
- either
- (throwIO
- . VerificationFoundationManifestError)
- pure
- Foundation.checkedFoundation
- preparationStart <- getMonotonicTimeNSec
- prepared <-
- prepareDefaultSourceRequest file
- >>= either
- (throwIO . VerificationWorkspaceError)
- pure
- let (mounts, request) = prepared
- preparationEnd <- getMonotonicTimeNSec
- prelude <- withVampireRequestOwner executor \owner -> do
- preludeResolver <-
- typedVampireResolver
- owner
- 0
- observationRef
- Typed.acquireFinalPreludeSession
- memo store foundation preludeResolver
- >>= either
- (throwIO
- . VerificationFinalPreludeReadinessError)
- pure
- observeModuleRootAcquisition observationRef
- (Typed.finalPreludeAcquisition prelude)
- let preludeSyntax =
- Typed.sealedTypedModuleSyntax
- (Typed.finalPreludeModule prelude)
- syntaxInputs _source = [preludeSyntax]
- (parsed, measured) <-
- Felix.parseSourceWorkspaceMeasuredWithStoreAndSyntaxInputsAndGraphValidation
- store
- mounts
- request
- syntaxInputs
- (Prelude.rejectOrdinaryPreludeSourceGraph
- (Typed.finalPreludeSource prelude))
- >>= either throwParseExecutionError pure
- checkingStart <- getMonotonicTimeNSec
- outcome <-
- checkTypedWorkspace
- memo
- storeCoordinator
- foundation
- prelude
- executor
- (jobsSelectionEffectiveJobs jobsSelection)
- validationMode
- observationRef
- parsed
- store
- checkingEnd <- getMonotonicTimeNSec
- executorObserved <- vampireExecutorObservation executor
- mergeExecutorObservation observationRef executorObserved
- observed <- readIORef observationRef
- pure
- ( outcome
- , measured
- , preparationEnd - preparationStart
- , checkingStart
- , checkingEnd
- , observed
- , parsed
- ))
- let result =
- case admittedResult of
- TypedWorkspaceRejected admitted failure ->
- let report = admittedWorkspaceReport admitted
- in case failure of
- TypedWorkspaceCheckingRejected checkingFailure ->
- VerificationCheckingFailure
- report checkingFailure
- TypedWorkspaceProverRejected proverFailure ->
- VerificationFailure report proverFailure
- TypedWorkspaceSucceeded admitted ->
- completedResult
- (admittedWorkspaceReport admitted)
- (VerificationPresentation
- (HtmlExport.htmlPresentationFromParsedWorkspace
- parsedPresentation))
- measurements =
- finalizeVerificationMeasurements
- invocationStart
- checkingStart
- checkingEnd
- parseMeasurements
- sourcePreparation
- observation
- logInfoN
- (renderVerificationMeasurements measurements)
- pure (result, measurements)
- where
- throwParseExecutionError = \case
- Felix.ParseExecutionWorkspaceError failure ->
- throwIO (VerificationWorkspaceError failure)
- Felix.ParseExecutionStoreFailure failure ->
- throwIO (VerificationStoreFailure failure)
- Felix.ParseExecutionArtifactIntegrityFailure source failure ->
- throwIO
- (VerificationParsedArtifactIntegrityError source failure)
-
-checkTypedWorkspace
- :: Store.StoreMemo
- -> Store.StoreCoordinator
- -> Foundation.CheckedFoundation
- -> Typed.FinalPreludeSession
- -> VampireExecutor
- -> EffectiveJobs
- -> StoreValidationMode
- -> IORef VerificationObservation
- -> ParsedSourceWorkspace
- -> Store.Store
- -> IO TypedWorkspaceOutcome
-checkTypedWorkspace
- memo
- storeCoordinator
- foundation
- prelude
- executor
- selectedJobs
- validationMode
- observationRef
- workspace
- store = do
- let modules =
- zipWith
- makeTask
- [1..]
- (toList
- (Felix.parsedWorkspaceImportedBeforeImporter workspace))
- rootAddress =
- Felix.parsedModuleAddress
- (Felix.parsedWorkspaceRootModule workspace)
- atomicModifyIORef' observationRef
- (\observation ->
- ( observation
- { observedModuleCount = length modules
- }
- , ()
- ))
- scheduleModules
- rootAddress
- modules
- Map.empty
- Map.empty
- Map.empty
- Nothing
- where
- workerBound = effectiveJobsValue selectedJobs
-
- makeTask ordinal parsed =
- ModuleTask
- { moduleTaskOrdinal = ordinal
- , moduleTaskParsed = parsed
- , moduleTaskDirectAddresses =
- nubOrd
- (Felix.parsedImportedAddress
- <$> Felix.parsedModuleImports parsed)
- }
-
- scheduleModules
- rootAddress
- pending
- running
- sealedByAddress
- admittedByOrdinal
- candidate = do
- let readyCount =
- length
- [ ()
- | task <- pending
- , taskMayStart candidate sealedByAddress task
- ]
- observeReadyModules observationRef readyCount
- (pending', running') <-
- startReadyModules
- pending
- running
- sealedByAddress
- candidate
- Exception.onException
- (if Map.null running'
- then case candidate of
- Just selected
- | any
- (\task ->
- moduleTaskOrdinal task
- < candidateOrdinal selected)
- pending' ->
- throwIO
- (VerificationModuleSchedulerInvariant
- "an earlier module is not terminal")
- | otherwise ->
- pure
- (TypedWorkspaceRejected
- (admittedWorkspaceThrough
- admittedByOrdinal
- selected)
- (candidateFailure selected))
- Nothing
- | null pending' -> do
- unless
- (Map.member rootAddress sealedByAddress)
- (throwIO
- (VerificationMissingRootModule
- rootAddress))
- pure
- (TypedWorkspaceSucceeded
- (completeAdmittedWorkspace
- admittedByOrdinal))
- | otherwise ->
- throwIO
- (VerificationModuleSchedulerInvariant
- "no ready module and no running module")
- else do
- (_completedAsync, (ordinal, completed)) <-
- Async.waitAny (Map.elems running')
- let runningWithoutCompleted =
- Map.delete ordinal running'
- case completed of
- Left fatal -> do
- cancelModuleCheckers runningWithoutCompleted
- Exception.throwIO fatal
- Right (ModuleCheckSucceeded
- address sealed admittedModule) ->
- scheduleModules
- rootAddress
- pending'
- runningWithoutCompleted
- (Map.insert address sealed sealedByAddress)
- (Map.insert
- ordinal
- admittedModule
- admittedByOrdinal)
- candidate
- Right (ModuleCheckRejected
- admittedModule failure) -> do
- let selected =
- chooseEarlierFailure
- candidate
- (ModuleFailureCandidate
- ordinal
- admittedModule
- failure)
- cutoff = candidateOrdinal selected
- (later, retained) =
- Map.partitionWithKey
- (\runningOrdinal _async ->
- runningOrdinal > cutoff)
- runningWithoutCompleted
- cancelModuleCheckers later
- scheduleModules
- rootAddress
- pending'
- retained
- sealedByAddress
- admittedByOrdinal
- (Just selected)
- )
- (cancelModuleCheckers running')
-
- startReadyModules
- pending
- running
- sealedByAddress
- candidate
- | Map.size running >= workerBound =
- pure (pending, running)
- | otherwise =
- case extractFirstReady candidate sealedByAddress pending of
- Nothing ->
- pure (pending, running)
- Just (task, remaining) -> do
- checker <- Async.async do
- completed <-
- (Exception.try
- (observeModuleChecker observationRef
- (checkModule task sealedByAddress))
- :: IO
- (Either
- SomeException
- ModuleCheckResult))
- pure (moduleTaskOrdinal task, completed)
- startReadyModules
- remaining
- (Map.insert
- (moduleTaskOrdinal task)
- checker
- running)
- sealedByAddress
- candidate
-
- checkModule task sealedByAddress =
- withVampireRequestOwner executor \requestOwner -> do
- let parsed = moduleTaskParsed task
- source = Felix.parsedModuleResolved parsed
- address = Felix.parsedModuleAddress parsed
- direct <-
- traverse
- (\directAddress ->
- maybe
- (throwIO
- (VerificationMissingImportedModule
- directAddress))
- pure
- (Map.lookup directAddress sealedByAddress))
- (moduleTaskDirectAddresses task)
- resolver <-
- typedVampireResolver
- requestOwner
- (moduleTaskOrdinal task)
- observationRef
- input <-
- either
- (throwIO . VerificationTypedInputError source)
- pure
- (Typed.typedModuleInput
- foundation
- (Typed.finalPreludeReadiness prelude)
- resolver
- validationRun
- parsed
- direct)
- loadCachedModule parsed direct >>= \case
- Just sealed -> do
- observeModuleRootAcquisition
- observationRef Typed.ModuleRootHit
- pure
- (ModuleCheckSucceeded
- address
- sealed
- (completeAdmittedModule
- (Typed.identifiedPhysicalModule parsed)))
- Nothing -> do
- typedResult <-
- Exception.catch
- (Typed.runTypedModule input)
- (\failure ->
- throwIO
- (VerificationValidationIntegrityError
- source
- failure))
- case typedResult of
- Typed.TypedModuleOpenFailed err ->
- throwIO (VerificationTypedOpenError source err)
- Typed.TypedModuleFailed err prefix -> do
- let driverFailure =
- VerificationTypedModuleError
- source err prefix
- case classifyTypedModuleFailure err of
- TypedIntegrityFailure ->
- throwIO driverFailure
- TypedCheckingRejection ->
- reportFailure
- parsed
- prefix
- (TypedWorkspaceCheckingRejected
- driverFailure)
- TypedVerificationRejection failed ->
- reportFailure
- parsed
- prefix
- (TypedWorkspaceProverRejected failed)
- TypedProverFailure failed ->
- reportFailure
- parsed
- prefix
- (TypedWorkspaceProverRejected failed)
- Typed.TypedModuleSucceeded sealed -> do
- admittedModule <-
- either
- (throwIO
- . VerificationAdmittedViewError source)
- pure
- (checkedAdmittedModule
- True
- (Typed.identifiedPhysicalModule parsed)
- (Typed.sealedTypedModulePrefix sealed))
- persistSealed
- (Typed.identifiedPhysicalModule parsed)
- sealed
- observeModuleRootAcquisition
- observationRef Typed.ModuleRootMiss
- pure
- (ModuleCheckSucceeded
- address sealed admittedModule)
-
- reportFailure parsed prefix failure = do
- let source = Felix.parsedModuleResolved parsed
- admittedModule <-
- either
- (throwIO . VerificationAdmittedViewError source)
- pure
- (checkedAdmittedModule
- False
- (Typed.identifiedPhysicalModule parsed)
- prefix)
- Store.withStoreCoordinator storeCoordinator
- (Store.writePendingModulePrefix store prefix)
- >>= either
- (throwIO . VerificationStoreFailure)
- pure
- pure (ModuleCheckRejected admittedModule failure)
-
- storeValidationLookup lookupStore =
- Declaration.validationLookup
- (\key ->
- Store.withStoreCoordinator storeCoordinator
- (Store.loadProofValidation lookupStore key)
- >>= either
- (throwIO . VerificationStoreFailure)
- pure)
- (\key ->
- Store.withStoreCoordinator storeCoordinator
- (Store.loadDeclarationValidation lookupStore key)
- >>= either
- (throwIO . VerificationStoreFailure)
- pure)
-
- validationRun =
- case validationMode of
- FreshStoreValidation ->
- Declaration.FreshValidation
- WarmStoreValidation ->
- Declaration.WarmValidation
- (storeValidationLookup store)
-
- persistSealed input sealed = do
- artifactKey <-
- either
- (throwIO . VerificationModuleArtifactKeyError)
- pure
- (Semantic.moduleArtifactKey
- (Typed.identifiedModuleOwner input)
- (Felix.identifiedParsedModuleId
- (Typed.identifiedModuleParsed input))
- (Semantic.semanticInterfaceDirectInputs
- (Typed.sealedTypedModuleSemantic sealed))
- (Identity.theoryId foundation))
- let artifact =
- Semantic.moduleArtifactResult
- artifactKey
- (Syntax.moduleSyntaxAssertedId
- (Typed.sealedTypedModuleSyntax sealed))
- (Semantic.semanticInterfaceAssertedId
- (Typed.sealedTypedModuleSemantic sealed))
- acknowledged <-
- Store.withStoreCoordinator storeCoordinator
- (Store.writeSealedModule
- store
- (Typed.sealedTypedModulePrefix sealed)
- [Typed.sealedTypedModuleSyntax sealed]
- [Typed.sealedTypedModuleSemantic sealed]
- artifact)
- >>= either
- (throwIO . VerificationStoreFailure)
- pure
- unless
- (acknowledged == artifact)
- (throwIO
- (VerificationStoreFailure
- Store.StoreModuleArtifactIdMismatch))
-
- loadCachedModule parsed direct =
- case validationMode of
- WarmStoreValidation -> do
- let owner =
- Typed.identifiedModuleOwner
- (Typed.identifiedPhysicalModule parsed)
- directSemantic =
- Semantic.semanticInterfaceAssertedId
- (Typed.sealedTypedModuleSemantic
- (Typed.finalPreludeModule prelude))
- : ( Semantic.semanticInterfaceAssertedId
- . Typed.sealedTypedModuleSemantic
- <$> direct
- )
- artifactKey <-
- either
- (throwIO . VerificationModuleArtifactKeyError)
- pure
- (Semantic.moduleArtifactKey
- owner
- (Felix.identifiedParsedModuleId
- (Typed.identifiedModuleParsed
- (Typed.identifiedPhysicalModule parsed)))
- directSemantic
- (Identity.theoryId foundation))
- loaded <-
- Store.withStoreCoordinator storeCoordinator
- (Store.loadCachedModuleInstallation
- memo
- store
- artifactKey
- (Syntax.moduleSyntaxAssertedId
- (Felix.parsedModuleSyntaxInterface parsed)))
- case loaded of
- Left failure ->
- throwIO (VerificationStoreFailure failure)
- Right Nothing ->
- pure Nothing
- Right (Just installation) ->
- either
- (throwIO
- . VerificationTypedCachedModuleError
- (Felix.parsedModuleResolved parsed))
- (pure . Just)
- (Typed.cachedSealedTypedModule
- foundation
- (Typed.finalPreludeModule prelude : direct)
- installation)
- FreshStoreValidation ->
- pure Nothing
-
- taskMayStart candidate sealedByAddress task =
- maybe True
- (moduleTaskOrdinal task <)
- (candidateOrdinal <$> candidate)
- && all
- (`Map.member` sealedByAddress)
- (moduleTaskDirectAddresses task)
-
- extractFirstReady candidate sealedByAddress = go []
- where
- go _before [] = Nothing
- go before (task : after)
- | taskMayStart candidate sealedByAddress task =
- Just (task, reverse before <> after)
- | otherwise =
- go (task : before) after
-
- chooseEarlierFailure Nothing incoming = incoming
- chooseEarlierFailure (Just current) incoming
- | candidateOrdinal incoming < candidateOrdinal current = incoming
- | otherwise = current
-
- candidateOrdinal (ModuleFailureCandidate ordinal _admitted _failure) =
- ordinal
-
- candidateFailure (ModuleFailureCandidate _ordinal _admitted failure) =
- failure
-
- candidateAdmitted (ModuleFailureCandidate _ordinal admitted _failure) =
- admitted
-
- completeAdmittedWorkspace admittedByOrdinal =
- AdmittedTypedWorkspace
- ( completeAdmittedModule (Typed.finalPreludeInput prelude)
- : fmap snd (Map.toAscList admittedByOrdinal)
- )
-
- admittedWorkspaceThrough admittedByOrdinal selected =
- let cutoff = candidateOrdinal selected
- earlier = Map.filterWithKey
- (\ordinal _admitted -> ordinal < cutoff)
- admittedByOrdinal
- in AdmittedTypedWorkspace
- ( completeAdmittedModule (Typed.finalPreludeInput prelude)
- : ( fmap snd (Map.toAscList earlier)
- <> [candidateAdmitted selected]
- )
- )
-
- cancelModuleCheckers running = do
- traverse_ Async.cancel (Map.elems running)
- traverse_ Async.waitCatch (Map.elems running)
-
-data TypedFailureClassification
- = TypedCheckingRejection
- | TypedVerificationRejection !FailedVerification
- | TypedProverFailure !FailedVerification
- | TypedIntegrityFailure
-
--- | Classify failures at the typed checking boundary conservatively.
---
--- Only source elaboration and recognized prover outcomes may retain an
--- admitted source report. Every declaration/sealing invariant, including a
--- future constructor not explicitly recognized below, remains fatal.
-classifyTypedModuleFailure
- :: Typed.TypedModuleFailure
- -> TypedFailureClassification
-classifyTypedModuleFailure = \case
- Typed.TypedActionFailed{} ->
- TypedCheckingRejection
- Typed.TypedDeclarationFailed
- (Declaration.ProofObligationFailedAt
- location
- (Declaration.VampireProcessFailed processError)) ->
- classifyTypedProverResult location (Left processError)
- Typed.TypedDeclarationFailed
- (Declaration.ProofObligationFailedAt
- location
- (Declaration.VampireObligationRejected answer)) ->
- classifyTypedProverResult location (Right answer)
- _failure ->
- TypedIntegrityFailure
-
-classifyTypedProverResult
- :: Location
- -> Either ProverProcessError ProverAnswer
- -> TypedFailureClassification
-classifyTypedProverResult location result =
- case verificationFailureReason result of
- Nothing ->
- TypedIntegrityFailure
- Just reason ->
- let failed = FailedVerification location reason
- in case reason of
- CountermodelFailure{} ->
- TypedVerificationRejection failed
- ContradictoryInputFailure{} ->
- TypedVerificationRejection failed
- IndeterminateFailure{} ->
- TypedProverFailure failed
- ProtocolFailure{} ->
- TypedProverFailure failed
- TransportFailure{} ->
- TypedProverFailure failed
-
-typedVampireResolver
- :: VampireRequestOwner
- -> Natural
- -> IORef VerificationObservation
- -> IO Declaration.VampireResolver
-typedVampireResolver
- requestOwner moduleOrdinal observationRef = do
- localOrdinalRef <- newIORef 1
- let reserve requests = do
- let batchSize = NonEmpty.length requests
- ordinalCount = fromIntegral batchSize
- firstOrdinal <- atomicModifyIORef' localOrdinalRef
- (\current -> (current + ordinalCount, current))
- let positions =
- NonEmpty.fromList
- [ workPosition moduleOrdinal ordinal
- | ordinal <-
- [firstOrdinal .. firstOrdinal + ordinalCount - 1]
- ]
- preparedBytes =
- foldl'
- (\total request ->
- total
- + fromIntegral
- (preparedVerificationByteCount request))
- 0
- requests
- atomicModifyIORef' observationRef \observation ->
- ( observation
- { observedObligationBatchCount =
- observedObligationBatchCount observation + 1
- , observedPreparedObligationCount =
- observedPreparedObligationCount observation + batchSize
- , observedMaximumObligationBatchSize =
- max batchSize
- (observedMaximumObligationBatchSize observation)
- , observedPreparedRequestBytes =
- observedPreparedRequestBytes observation
- + preparedBytes
- }
- , ()
- )
- pure positions
- submit requests = do
- positions <- reserve requests
- traverse
- (uncurry (submitVampireRequest requestOwner))
- (NonEmpty.zip positions requests)
- observe elapsed =
- atomicModifyIORef' observationRef \observation ->
- ( observation
- { observedRequestPreparationNanoseconds =
- observedRequestPreparationNanoseconds observation
- + elapsed
- }
- , ()
- )
- pure (Declaration.vampireSubmissionResolver submit observe)
-
-observeModuleRootAcquisition
- :: IORef VerificationObservation
- -> Typed.ModuleRootAcquisition
- -> IO ()
-observeModuleRootAcquisition observationRef acquisition =
- atomicModifyIORef' observationRef \observation ->
- ( case acquisition of
- Typed.ModuleRootHit ->
- observation
- { observedModuleRootHitCount =
- observedModuleRootHitCount observation + 1
- }
- Typed.ModuleRootMiss ->
- observation
- { observedModuleRootMissCount =
- observedModuleRootMissCount observation + 1
- }
- , ()
- )
-
-observeReadyModules
- :: IORef VerificationObservation
- -> Int
- -> IO ()
-observeReadyModules observationRef readyCount =
- atomicModifyIORef' observationRef \observation ->
- ( observation
- { observedMaximumReadyModuleCount =
- max readyCount
- (observedMaximumReadyModuleCount observation)
- }
- , ()
- )
-
-observeModuleChecker
- :: IORef VerificationObservation
- -> IO value
- -> IO value
-observeModuleChecker observationRef action = do
- atomicModifyIORef' observationRef \observation ->
- let live = observedLiveModuleCheckers observation + 1
- in
- ( observation
- { observedLiveModuleCheckers = live
- , observedMaximumLiveModuleCheckers =
- max live
- (observedMaximumLiveModuleCheckers observation)
- }
- , ()
- )
- action `Exception.finally`
- atomicModifyIORef' observationRef
- (\observation ->
- ( observation
- { observedLiveModuleCheckers =
- observedLiveModuleCheckers observation - 1
- }
- , ()
- ))
-
-mergeExecutorObservation
- :: IORef VerificationObservation
- -> VampireExecutorObservation
- -> IO ()
-mergeExecutorObservation observationRef executorObserved =
- atomicModifyIORef' observationRef \observation ->
- ( observation
- { observedVampireRunCount =
- vampireExecutorRunCount executorObserved
- , observedMaximumLiveVampireProcesses =
- vampireExecutorMaximumLiveCount executorObserved
- , observedFirstVampireStart =
- vampireExecutorFirstStartNanoseconds executorObserved
- , observedFinalVampireSubmission =
- vampireExecutorFinalSubmissionNanoseconds executorObserved
- , observedFinalVampireCompletion =
- vampireExecutorFinalCompletionNanoseconds executorObserved
- , observedVampireExecutionNanoseconds =
- vampireExecutorExecutionNanoseconds executorObserved
- , observedLongestVampireExecutionNanoseconds =
- vampireExecutorLongestExecutionNanoseconds executorObserved
- }
- , ()
- )
-
-finalizeVerificationMeasurements
- :: Word64
- -> Word64
- -> Word64
- -> Felix.ParseMeasurements
- -> Word64
- -> VerificationObservation
- -> VerificationMeasurements
-finalizeVerificationMeasurements
- invocationStart
- checkingStart
- checkingEnd
- parseMeasurements
- sourcePreparation
- observation =
- VerificationMeasurements
- { verificationParseMeasurements =
- parseMeasurements
- , verificationSourcePreparationNanoseconds =
- sourcePreparation
- , verificationInvocationNanoseconds =
- checkingEnd - invocationStart
- , verificationCheckingNanoseconds =
- checkingEnd - checkingStart
- , verificationModuleCount =
- observedModuleCount observation
- , verificationDetectedProcessorCount =
- observedDetectedProcessorCount observation
- , verificationEffectiveJobs =
- observedEffectiveJobs observation
- , verificationJobsOverridden =
- observedJobsOverridden observation
- , verificationMaximumLiveModuleCheckers =
- observedMaximumLiveModuleCheckers observation
- , verificationMaximumLiveVampireProcesses =
- observedMaximumLiveVampireProcesses observation
- , verificationMaximumReadyModuleCount =
- observedMaximumReadyModuleCount observation
- , verificationObligationBatchCount =
- observedObligationBatchCount observation
- , verificationPreparedObligationCount =
- observedPreparedObligationCount observation
- , verificationMaximumObligationBatchSize =
- observedMaximumObligationBatchSize observation
- , verificationPreparedRequestBytes =
- observedPreparedRequestBytes observation
- , verificationRequestPreparationNanoseconds =
- observedRequestPreparationNanoseconds observation
- , verificationVampireRunCount =
- observedVampireRunCount observation
- , verificationModuleRootHitCount =
- observedModuleRootHitCount observation
- , verificationModuleRootMissCount =
- observedModuleRootMissCount observation
- , verificationFirstVampireStartNanoseconds =
- fmap
- (\started -> started - invocationStart)
- (observedFirstVampireStart observation)
- , verificationFinalVampireSubmissionNanoseconds =
- fmap
- (\submitted -> submitted - invocationStart)
- (observedFinalVampireSubmission observation)
- , verificationFinalVampireCompletionNanoseconds =
- fmap
- (\completed -> completed - invocationStart)
- (observedFinalVampireCompletion observation)
- , verificationVampireExecutionNanoseconds =
- observedVampireExecutionNanoseconds observation
- , verificationLongestVampireExecutionNanoseconds =
- observedLongestVampireExecutionNanoseconds observation
- }
-
-renderVerificationMeasurements
- :: VerificationMeasurements
- -> Text
-renderVerificationMeasurements measurements =
- StrictText.unwords
- [ "M0"
- , "source_setup_ms="
- <> renderNanoseconds
- (verificationSourcePreparationNanoseconds
- measurements)
- , "resolution_ms="
- <> renderNanoseconds
- (Felix.parseMeasurementResolutionNanoseconds
- parseMeasurements)
- , "candidate_probes=" <> renderIntegral
- (Felix.parseMeasurementCandidateProbeCount
- parseMeasurements)
- , "canonicalizations=" <> renderIntegral
- (Felix.parseMeasurementCanonicalizationCount
- parseMeasurements)
- , "target_inspections=" <> renderIntegral
- (Felix.parseMeasurementTargetInspectionCount
- parseMeasurements)
- , "tokenization_ms="
- <> renderNanoseconds
- (Felix.parseMeasurementTokenizationNanoseconds
- parseMeasurements)
- , "scanning_ms="
- <> renderNanoseconds
- (Felix.parseMeasurementScanningNanoseconds
- parseMeasurements)
- , "syntax_interface_ms="
- <> renderNanoseconds
- (Felix.parseMeasurementSyntaxInterfaceNanoseconds
- parseMeasurements)
- , "parsing_ms="
- <> renderNanoseconds
- (Felix.parseMeasurementParsingNanoseconds
- parseMeasurements)
- , "parsed_hits=" <> renderIntegral
- (Felix.parseMeasurementParsedHitCount parseMeasurements)
- , "parsed_misses=" <> renderIntegral
- (Felix.parseMeasurementParsedMissCount parseMeasurements)
- , "parser_tables=" <> renderIntegral
- (Felix.parseMeasurementParserTableMaterializationCount
- parseMeasurements)
- , "modules=" <> renderIntegral
- (verificationModuleCount measurements)
- , "detected_processors="
- <> maybe
- "unavailable"
- renderIntegral
- (verificationDetectedProcessorCount measurements)
- , "effective_jobs=" <> renderIntegral
- (verificationEffectiveJobs measurements)
- , "jobs_overridden="
- <> if verificationJobsOverridden measurements
- then "yes"
- else "no"
- , "max_module_checkers=" <> renderIntegral
- (verificationMaximumLiveModuleCheckers measurements)
- , "max_vampire_processes=" <> renderIntegral
- (verificationMaximumLiveVampireProcesses measurements)
- , "files_read=" <> renderIntegral
- (Felix.parseMeasurementModuleCount
- parseMeasurements)
- , "import_occurrences=" <> renderIntegral
- (Felix.parseMeasurementImportOccurrenceCount
- parseMeasurements)
- , "chunks=" <> renderIntegral
- (Felix.parseMeasurementChunkCount
- parseMeasurements)
- , "source_bytes=" <> renderIntegral
- (Felix.parseMeasurementSourceByteCount
- parseMeasurements)
- , "checking_ms="
- <> renderNanoseconds
- (verificationCheckingNanoseconds
- measurements)
- , "batches=" <> renderIntegral
- (verificationObligationBatchCount measurements)
- , "obligations=" <> renderIntegral
- (verificationPreparedObligationCount measurements)
- , "max_batch=" <> renderIntegral
- (verificationMaximumObligationBatchSize
- measurements)
- , "prepared_bytes=" <> renderIntegral
- (verificationPreparedRequestBytes measurements)
- , "request_preparation_ms="
- <> renderNanoseconds
- (verificationRequestPreparationNanoseconds measurements)
- , "vampire_runs=" <> renderIntegral
- (verificationVampireRunCount measurements)
- , "module_root_hits=" <> renderIntegral
- (verificationModuleRootHitCount measurements)
- , "module_root_misses=" <> renderIntegral
- (verificationModuleRootMissCount measurements)
- , "first_vampire_ms="
- <> maybe
- "none"
- renderNanoseconds
- (verificationFirstVampireStartNanoseconds
- measurements)
- , "vampire_ms="
- <> renderNanoseconds
- (verificationVampireExecutionNanoseconds
- measurements)
- , "final_submission_ms="
- <> maybe
- "none"
- renderNanoseconds
- (verificationFinalVampireSubmissionNanoseconds
- measurements)
- , "final_completion_ms="
- <> maybe
- "none"
- renderNanoseconds
- (verificationFinalVampireCompletionNanoseconds
- measurements)
- , "vampire_span_ms="
- <> maybe
- "none"
- renderNanoseconds
- (vampireExecutionSpan measurements)
- , "longest_vampire_ms="
- <> renderNanoseconds
- (verificationLongestVampireExecutionNanoseconds
- measurements)
- , "max_ready_modules=" <> renderIntegral
- (verificationMaximumReadyModuleCount
- measurements)
- , "total_ms="
- <> renderNanoseconds
- (verificationInvocationNanoseconds
- measurements)
- ]
- where
- parseMeasurements =
- verificationParseMeasurements measurements
-
- vampireExecutionSpan measured = do
- started <- verificationFirstVampireStartNanoseconds measured
- completed <- verificationFinalVampireCompletionNanoseconds measured
- pure (completed - started)
-
-renderNanoseconds :: Word64 -> Text
-renderNanoseconds nanoseconds =
- renderIntegral (nanoseconds `div` 1000000)
-
-renderIntegral :: Show number => number -> Text
-renderIntegral =
- StrictText.pack . show
-
-admittedWorkspaceReport
- :: AdmittedTypedWorkspace
- -> VerificationReport
-admittedWorkspaceReport (AdmittedTypedWorkspace modules) =
- VerificationReport
- { verificationDirectEscapes =
- concatMap admittedModuleEscapes modules
- }
-
-admittedModuleEscapes
- :: AdmittedTypedModule
- -> [ReportedEscape]
-admittedModuleEscapes (AdmittedTypedModule declarations) =
- concatMap admittedDeclarationEscapes declarations
-
-admittedDeclarationEscapes
- :: AdmittedTypedDeclaration
- -> [ReportedEscape]
-admittedDeclarationEscapes
- (AdmittedTypedDeclaration _slot declaration) =
- axiomEscape <> proofEscapes
- where
- axiomEscape =
- case Typed.typedSourceDeclarationHead declaration of
- Raw.BlockAxiom location _title _marker _axiom ->
- [ReportedEscape ReportedSourceAxiom location]
- _ ->
- []
- proofEscapes =
- maybe [] omittedProofEscapes
- (Typed.typedSourceDeclarationProof declaration)
-
-omittedProofEscapes :: Raw.Proof -> [ReportedEscape]
-omittedProofEscapes = \case
- Raw.Omitted location ->
- [ReportedEscape ReportedOmitted location]
- Raw.Qed{} ->
- []
- Raw.Contradiction{} ->
- []
- Raw.ByCase _location cases ->
- concatMap (omittedProofEscapes . Raw.caseProof) cases
- Raw.ByContradiction _location proof ->
- omittedProofEscapes proof
- Raw.BySetInduction _location _term proof ->
- omittedProofEscapes proof
- Raw.ByOrdInduction _location proof ->
- omittedProofEscapes proof
- Raw.Assume _location _statement proof ->
- omittedProofEscapes proof
- Raw.FixSymbolic _location _variables _bound proof ->
- omittedProofEscapes proof
- Raw.FixSuchThat _location _variables _statement proof ->
- omittedProofEscapes proof
- Raw.Calc _location _quantifier _calculation proof ->
- omittedProofEscapes proof
- Raw.TakeVar _location _variables _bound _statement _justification proof ->
- omittedProofEscapes proof
- Raw.TakeNoun _location _noun _justification proof ->
- omittedProofEscapes proof
- Raw.Have _location _condition _statement _justification proof ->
- omittedProofEscapes proof
- Raw.Suffices _location _statement _justification proof ->
- omittedProofEscapes proof
- Raw.Subclaim _location _statement subproof continuation ->
- omittedProofEscapes subproof <> omittedProofEscapes continuation
- Raw.Define _location _variable _expression proof ->
- omittedProofEscapes proof
- Raw.DefineFunction
- _location _function _argument _value _domainVariable _domain
- proof ->
- omittedProofEscapes proof
- Raw.DefineFunctionLocal
- _location _function _argument _domain _target _ruleVariable
- _rules proof ->
- omittedProofEscapes proof
-
-completedResult
- :: VerificationReport
- -> VerificationPresentation
- -> VerificationResult
-completedResult report presentation
- | any ((== ReportedOmitted) . reportedEscapeKind)
- (verificationDirectEscapes report) =
- CompletedWithExplicitGaps report presentation
- | otherwise =
- VerificationCompleted report presentation
-
-verify
- :: (MonadUnliftIO io, MonadLogger io)
- => Vampire
- -> FilePath
- -> io (Either VerificationDriverError VerificationResult)
-verify prover file =
- fmap fst <$> verifyMeasured prover file
-
-prepareVerifiedHtmlExportResult
- :: MonadIO io
- => VerificationPresentation
- -> io (Either HtmlExport.HtmlExportError [PreparedHtmlArtifact])
-prepareVerifiedHtmlExportResult
- (VerificationPresentation workspace) = liftIO do
- hintsResult <- findAndReadRendererFile "lexicon.tsv"
- pure do
- hints <- hintsResult
- HtmlExport.prepareHtmlExport
- defaultHtmlMountPrefixes
- workspace
- hints
-
-defaultHtmlMountPrefixes :: [(SourceMountId, [Text])]
-defaultHtmlMountPrefixes =
- [ (sourceMountId "project", [])
- , (sourceMountId "library", ["library"])
- , (sourceMountId "debug", ["debug"])
- ]
generated by cgit v1.2.3 (git 2.39.1) at 2026-08-06 19:59:10 +0000