diff options
Diffstat (limited to 'source/Test/Unit/Module.hs')
| -rw-r--r-- | source/Test/Unit/Module.hs | 2665 |
1 files changed, 1873 insertions, 792 deletions
diff --git a/source/Test/Unit/Module.hs b/source/Test/Unit/Module.hs index 1cf62e5..fbc6c0d 100644 --- a/source/Test/Unit/Module.hs +++ b/source/Test/Unit/Module.hs @@ -21,7 +21,6 @@ import Checking.Typed.Inductive qualified as TypedInductive import CommandLine qualified import Felix.Module import Felix.Math.Codec -import Felix.Migration qualified as Migration import Felix.Parse qualified as Parse import Felix.Prelude qualified as Prelude import Felix.Source @@ -33,21 +32,45 @@ import Paths_felix qualified as Paths import Syntax.Abstract qualified as Raw import Syntax.Internal qualified as Internal import Syntax.Interface qualified as Syntax - -import Bound.Scope (fromScope) -import Bound.Var (Var(..)) +import Syntax.Pragma qualified as Pragma + +import Control.Concurrent (threadDelay) +import Control.Concurrent.STM + ( atomically + , check + , newEmptyTMVarIO + , newTQueueIO + , newTVarIO + , putTMVar + , readTQueue + , readTVar + , takeTMVar + , tryReadTMVar + , tryReadTQueue + , writeTQueue + , writeTVar + ) import Control.Exception (bracket) -import Control.Monad (foldM) +import Control.Monad (foldM, when) import Data.ByteString qualified as ByteString import Data.Text qualified as StrictText import Data.Text.Encoding qualified as Text import Control.Monad.Logger (runNoLoggingT) -import Data.IORef (IORef, modifyIORef', newIORef, readIORef) +import Data.IORef + ( IORef + , atomicModifyIORef' + , modifyIORef' + , newIORef + , readIORef + ) +import Data.List (sort) +import Data.List.NonEmpty qualified as NonEmpty import Data.Map.Strict qualified as Map import Data.Set qualified as Set import Data.Vector qualified as Vector import System.Directory ( createDirectoryIfMissing + , doesFileExist , getCurrentDirectory , getPermissions , setOwnerExecutable @@ -55,8 +78,10 @@ import System.Directory ) import System.FilePath.Posix qualified as Posix import System.IO.Temp qualified as Temp +import System.Timeout qualified as Timeout import Test.Tasty import Test.Tasty.HUnit +import UnliftIO.Async (withAsync, wait) unitTests :: TestTree @@ -68,26 +93,28 @@ unitTests = identifiesCommentOnlyInput , testCase "loads and parses the packaged final prelude" parsesPackagedFinalPrelude + , testCase "renders packaged final-prelude failures" + rendersPackagedPreludeFailures , testCase "confines exact foundation-leaf completion" confinesFoundationLeafCompletion , testCase "builds the confined final prelude" buildsConfinedFinalPrelude , testCase "publishes the final prelude as an ordinary sealed root" publishesFinalPreludeRoot - , testCase "checks the protected nat closure with the final prelude" - checksProtectedNatClosure - , testCase "checks Phase 5.3 library closures with the final prelude" - checksPhase53LibraryClosures , testCase "retains exact omitted-proof locations" retainsExactOmittedProofLocation , testCase "coalesces syntax without collapsing semantic imports" coalescesSharedDirectSyntax - , testCase "resets gloss state between modules" - resetsGlossStatePerModule , testCase "makes selected source errors terminal" rejectsUnsupportedTypedSource , testCase "compiles exact declarations across an import" compilesExactDeclarationGraph + , testCase "compiles and imports exact structures" + compilesExactStructures + , testCase "compiles and caches contextual abbreviations" + compilesContextualAbbreviations + , testCase "rejects an unknown exact structure parent atomically" + rejectsUnknownExactStructureParent , testCase "compiles exact relation expressions" compilesExactRelationExpressions , testCase "resolves source-owned set application" @@ -98,6 +125,8 @@ unitTests = compilesExactOrdinaryProofs , testCase "compiles and reuses proof-local set definitions" compilesAndReusesProofLocalSetDefinitions + , testCase "compiles and reuses proof-local function graphs" + compilesAndReusesProofLocalFunctionGraphs , testCase "confines terminal exact contradiction" confinesTerminalExactContradiction , testCase "compiles exact separation comprehensions" @@ -146,9 +175,21 @@ unitTests = keepsExactSemanticsIndependentOfFixity , testCase "loads a cached exact producer for a fresh importer" loadsCachedExactProducerForFreshImporter + , testCase "reports admitted source escapes on fresh, warm, and failure paths" + reportsAdmittedSourceEscapes + , testCase "selects concurrent module failures by source order" + selectsConcurrentModuleFailureDeterministically + , testCase "batches independent structure obligations atomically" + batchesStructureObligationsAtomically + , testCase "keeps dependent proof obligations sequential" + keepsDependentProofObligationsSequential + , testCase "starts diamond consumers after sealed acknowledgements" + schedulesDiamondAfterSealedImports + , testCase "classifies typed Vampire failures conservatively" + classifiesTypedVampireFailures , testCase "retains the exact prefix before a later failure" retainsExactPrefixBeforeFailure - , testCase "routes production verification by complete graph" + , testCase "routes every production root through exact checking" routesProductionVerification , testCase "installs nonempty implicit prelude evidence" installsNonemptyImplicitPreludeEvidence @@ -285,6 +326,30 @@ parsesPackagedFinalPrelude = do (Syntax.moduleSyntaxAssertedId (Parse.identifiedParsedModuleSyntaxInterface secondParsed)) +rendersPackagedPreludeFailures :: Assertion +rendersPackagedPreludeFailures = do + assertEqual "load failure" + "/missing/felix-prelude.tex: unable to read packaged final prelude: not found" + (Prelude.renderPreludeLoadError + (Prelude.PreludeSourceReadFailed + "/missing/felix-prelude.tex" + "not found")) + assertEqual "located syntax failure" + "<felix-prelude>: syntax pragma location is out of range at 7:3" + (Prelude.renderPreludeParseError parseFailure) + assertEqual "authority-free API presentation" + ("packaged final prelude parsing failed: " + <> "<felix-prelude>: syntax pragma location is out of range at 7:3") + (Api.renderAuthorityFreeParseError + (Api.AuthorityFreePreludeParseFailed parseFailure)) + where + parseFailure = + Prelude.PreludeSyntaxPragmaFailed + (Pragma.SyntaxPragmaLocationOutOfRange + Prelude.preludeDiagnosticLabel + 7 + 3) + confinesFoundationLeafCompletion :: Assertion confinesFoundationLeafCompletion = do foundation <- expectRight Foundation.checkedFoundation @@ -387,6 +452,54 @@ buildsConfinedFinalPrelude = do [] (Semantic.semanticInterfaceDirectInputs (FinalPrelude.finalPreludeSemantic candidate)) + let baseDeltas = + [ delta + | delta <- Semantic.semanticInterfaceDeclarations + (FinalPrelude.finalPreludeSemantic candidate) + , not + (null + (Semantic.semanticEnvironmentStructures + (Semantic.declarationDeltaEnvironment delta))) + ] + case baseDeltas of + [delta] -> do + assertEqual "base structure has no facts" + [] + (Semantic.declarationDeltaFacts delta) + assertEqual "base structure has no propositions" + [] + (Semantic.declarationDeltaPropositions delta) + case Semantic.semanticEnvironmentStructures + (Semantic.declarationDeltaEnvironment delta) of + [descriptor] -> do + assertEqual "base structure is metadata-only" + Nothing + (Semantic.semanticStructureDescriptorPredicate + descriptor) + case Semantic.semanticStructureDescriptorOperations + descriptor of + [operation] -> + case Identity.lookupCheckedObjectContent + (Semantic.semanticStructureOperationObject + operation) + (FinalPrelude.finalPreludeObjects candidate) of + Just Identity.OpaqueObjectContent{} -> pure () + content -> + assertFailure + ("expected opaque carrier, got " + <> show content) + operations -> + assertFailure + ("expected one base operation, got " + <> show operations) + descriptors -> + assertFailure + ("expected one base descriptor, got " + <> show descriptors) + deltas -> + assertFailure + ("expected one base structure delta, got " + <> show (length deltas)) let role roleName = maybe (assertFailure @@ -395,13 +508,13 @@ buildsConfinedFinalPrelude = do pure (FinalPrelude.finalPreludePublicRole candidate roleName) - omega <- role Migration.PreludeOmegaObject - naturals <- role Migration.PreludeNaturalsAlias + omega <- role FinalPrelude.PreludeOmegaObject + naturals <- role FinalPrelude.PreludeNaturalsAlias assertEqual "naturals expands to Omega" omega naturals traverse_ (void . role) - (Set.toList Migration.expectedFinalPreludePublicRoles) + (Set.toList FinalPrelude.expectedFinalPreludePublicRoles) let foundationTags = Set.fromList [ tag | batch <- @@ -459,518 +572,61 @@ publishesFinalPreludeRoot = do Store.openStore path theory >>= expectRight pure store bracket open Store.closeStore \store -> do + freshMemo <- Store.newStoreMemo store session <- expectRight - =<< Module.buildFinalPreludeSession - store foundation finalPreludeResolver - let input = Module.migrationPreludeInput session - sealed = Module.migrationPreludeModule session + =<< Module.acquireFinalPreludeSession + freshMemo store foundation finalPreludeResolver + let input = Module.finalPreludeInput session + sealed = Module.finalPreludeModule session syntax = Module.sealedTypedModuleSyntax sealed semantic = Module.sealedTypedModuleSemantic sealed + assertEqual "empty store constructs the final-prelude root" + Module.ModuleRootMiss + (Module.finalPreludeAcquisition session) assertEqual "final prelude owner" preludeModuleName (Module.identifiedModuleOwner input) assertEqual "final prelude has no semantic parents" [] (Semantic.semanticInterfaceDirectInputs semantic) - key <- expectRight - (Semantic.moduleArtifactKey - preludeModuleName - (Parse.identifiedParsedModuleId - (Module.identifiedModuleParsed input)) - [] - theory) - memo <- Store.newStoreMemo store - loaded <- expectRight - =<< Store.loadCachedModuleInstallation - memo - store - key - (Syntax.moduleSyntaxAssertedId syntax) - installation <- maybe - (assertFailure "final prelude root was not installed" - >> fail "unreachable") - pure - loaded - cached <- expectRight - (Module.cachedSealedTypedModule - foundation [] installation) + warmMemo <- Store.newStoreMemo store + warmSession <- expectRight + =<< Module.acquireFinalPreludeSession + warmMemo store foundation unusedResolver + let cached = Module.finalPreludeModule warmSession + assertEqual "persisted final-prelude root is a cache hit" + Module.ModuleRootHit + (Module.finalPreludeAcquisition warmSession) assertEqual "generic root syntax" syntax (Module.sealedTypedModuleSyntax cached) assertEqual "generic root semantics" semantic (Module.sealedTypedModuleSemantic cached) + assertEqual "cached base structure descriptor" + (semanticStructureDescriptors semantic) + (semanticStructureDescriptors + (Module.sealedTypedModuleSemantic cached)) assertEqual "generic root final prefix" (Declaration.pendingModulePrefixCurrent (Module.sealedTypedModulePrefix sealed)) (Declaration.pendingModulePrefixCurrent (Module.sealedTypedModulePrefix cached)) - -checksProtectedNatClosure :: Assertion -checksProtectedNatClosure = do - foundation <- expectRight Foundation.checkedFoundation - repository <- getCurrentDirectory - Temp.withSystemTempDirectory "felix-protected-nat" \directory -> do - let storePath = directory Posix.</> "store.sqlite" - executable = directory Posix.</> "vampire" - writeFile executable - (unlines - [ "#!/bin/sh" - , "cat >/dev/null" - , "printf '%s\\n' '% SZS status Theorem for protected-core'" - ]) - permissions <- getPermissions executable - setPermissions executable - (setOwnerExecutable True permissions) - runs <- newIORef (0 :: Int) - let resolver = countingAcceptedResolver executable runs - open = do - (_startup, store) <- - Store.openStore - storePath - (Identity.theoryId foundation) - >>= expectRight - pure store - bracket open Store.closeStore \store -> do - prelude <- - expectRight - =<< Module.buildFinalPreludeSession - store foundation resolver - mounts <- exactFixtureMounts repository - workspace <- parseFinalExactWorkspace prelude mounts "nat.tex" - sealed <- compileFinalParsedWorkspaceWithResolver - foundation prelude resolver workspace - let parsed = toList - (Parse.parsedWorkspaceImportedBeforeImporter workspace) - modules = Map.fromList - [ ( safeRelativePathFilePath - (resolvedSourceRelativePath - (Parse.parsedModuleResolved source)) - , checked - ) - | (source, checked) <- zip parsed sealed - ] - moduleAt path = maybe - (assertFailure ("missing typed module " <> path) - >> fail "unreachable") - pure - (Map.lookup path modules) - assertEqual "protected module count" - 5 - (length sealed) - let preludeSyntaxId = - Syntax.moduleSyntaxAssertedId - (Module.sealedTypedModuleSyntax - (Module.migrationPreludeModule prelude)) - preludeSemanticId = - Semantic.semanticInterfaceAssertedId - (Module.sealedTypedModuleSemantic - (Module.migrationPreludeModule prelude)) - forM_ - (toList - (Parse.parsedWorkspaceImportedBeforeImporter workspace)) - \parsedModule -> - assertEqual "final prelude is the first syntax input" - (Just preludeSyntaxId) - (listToMaybe - (Syntax.moduleSyntaxDirectInputs - (Parse.parsedModuleSyntaxInterface - parsedModule))) - forM_ sealed \sealedModule -> - assertEqual "final prelude is the first semantic input" - (Just preludeSemanticId) - (listToMaybe - (Semantic.semanticInterfaceDirectInputs - (Module.sealedTypedModuleSemantic sealedModule))) - setModule <- moduleAt "set.tex" - sucModule <- moduleAt "set/suc.tex" - natModule <- moduleAt "nat.tex" - assertLocalAliasesAbsent - setModule - [ "setext" - , "emptyset" - , "unions" - , "unions_iff" - ] - assertLocalAliasesAbsent - natModule - [ "num_naturals_inductive_set" - , "num_naturals_smallest_inductive_set" - ] - assertTransparentObjectAlias setModule "cons" - assertTransparentObjectAlias setModule "union" - pairIdentity <- localObjectKeyTarget - setModule - (Semantic.SemanticExpressionFunction - (Raw.mixfixPattern Raw.PairSymbol)) - consBody <- localTransparentObjectBody setModule "cons" - let expectedConsBody = - Core.CLam Core.TySet - (Core.CLam Core.TySet - (Core.canonicalSetInsert - (Core.CBound 1) - (Core.CBound 0))) - assertEqual "cons uses canonical set insertion" - expectedConsBody consBody - assertBool "cons does not use ordered pairing" - ( pairIdentity - `Set.notMember` Core.canonicalTermGlobals consBody - ) - let preludeModule = Module.migrationPreludeModule prelude - preludeSuccessor <- - localObjectAliasTarget preludeModule "prelude_successor" - sourceSuccessor <- localObjectAliasTarget sucModule "suc" - assertEqual "source successor reuses packaged successor content" - preludeSuccessor sourceSuccessor - preludeSuccessorBody <- - localTransparentObjectBody preludeModule "prelude_successor" - assertEqual "packaged successor uses canonical set insertion" - (Core.CLam Core.TySet - (Core.canonicalSetInsert - (Core.CBound 0) - (Core.CBound 0))) - preludeSuccessorBody - assertBool "successor does not use ordered pairing" - ( pairIdentity - `Set.notMember` - Core.canonicalTermGlobals preludeSuccessorBody - ) - assertOpaqueObjectKey - setModule - "pair" - (Semantic.SemanticExpressionFunction - (Raw.mixfixPattern Raw.PairSymbol)) - assertCleanFactAlias setModule "cons_iff" - assertCleanFactAlias setModule "union_iff" - traverse_ - (assertSourceAxiomAlias setModule) - [ "pair_eq_iff" - , "fst_eq" - , "snd_eq" - ] - assertBool "protected checking exercised Vampire" - . (> 0) - =<< readIORef runs - -checksPhase53LibraryClosures :: Assertion -checksPhase53LibraryClosures = do - foundation <- expectRight Foundation.checkedFoundation - repository <- getCurrentDirectory - Temp.withSystemTempDirectory "felix-phase53-library" \directory -> do - let storePath = directory Posix.</> "store.sqlite" - executable = directory Posix.</> "vampire" - writeFile executable - (unlines - [ "#!/bin/sh" - , "cat >/dev/null" - , "printf '%s\\n' '% SZS status Theorem for phase53-library'" - ]) - permissions <- getPermissions executable - setPermissions executable - (setOwnerExecutable True permissions) - runs <- newIORef (0 :: Int) - let resolver = countingAcceptedResolver executable runs - bracket - (snd <$> (Store.openStore storePath - (Identity.theoryId foundation) >>= expectRight)) - Store.closeStore - \store -> do - prelude <- - expectRight - =<< Module.buildFinalPreludeSession - store foundation resolver - mounts <- exactFixtureMounts repository - selection <- expectRight - (Migration.resolveMigrationSelection - mounts Migration.typedMigrationModules) - let preludeSyntaxId = Syntax.moduleSyntaxAssertedId - (Module.sealedTypedModuleSyntax - (Module.migrationPreludeModule prelude)) - preludeSemanticId = - Semantic.semanticInterfaceAssertedId - (Module.sealedTypedModuleSemantic - (Module.migrationPreludeModule prelude)) - checkRoot path inspect = do - workspace <- parseFinalExactWorkspace - prelude mounts path - assertEqual (path <> " graph route") - Migration.TypedMigrationGraph - (Migration.classifyMigrationGraph - selection workspace) - sealed <- compileFinalParsedWorkspaceWithResolver - foundation prelude resolver workspace - let parsed = toList - (Parse.parsedWorkspaceImportedBeforeImporter - workspace) - modules = Map.fromList - [ ( safeRelativePathFilePath - (resolvedSourceRelativePath - (Parse.parsedModuleResolved source)) - , (source, checked) - ) - | (source, checked) <- zip parsed sealed - ] - moduleAt modulePath = maybe - (assertFailure - ("missing typed module " <> modulePath) - >> fail "unreachable") - pure - (Map.lookup modulePath modules) - assertEqual (path <> " module count") - (length parsed) - (length sealed) - forM_ parsed \source -> - assertEqual - (path <> " final-prelude syntax input") - (Just preludeSyntaxId) - (listToMaybe - (Syntax.moduleSyntaxDirectInputs - (Parse.parsedModuleSyntaxInterface - source))) - forM_ sealed \checked -> - assertEqual - (path <> " final-prelude semantic input") - (Just preludeSemanticId) - (listToMaybe - (Semantic.semanticInterfaceDirectInputs - (Module.sealedTypedModuleSemantic - checked))) - inspect moduleAt - unselectedImporter <- parseFinalExactWorkspace - prelude mounts "set/equinumerosity.tex" - assertEqual "unselected function importer graph route" - Migration.LegacyMigrationGraph - (Migration.classifyMigrationGraph - selection unselectedImporter) - checkRoot "set/bipartition.tex" - \moduleAt -> do - (_setParsed, setModule) <- moduleAt "set.tex" - (_consParsed, consModule) <- - moduleAt "set/cons.tex" - (_powersetParsed, powersetModule) <- - moduleAt "set/powerset.tex" - (_bipartitionParsed, bipartitionModule) <- - moduleAt "set/bipartition.tex" - assertLocalAliasesAbsent powersetModule ["pow_iff"] - assertEqual "bipartition semantic imports" - [ preludeSemanticId - , semanticId setModule - , semanticId consModule - , semanticId powersetModule - ] - (Semantic.semanticInterfaceDirectInputs - (Module.sealedTypedModuleSemantic - bipartitionModule)) - assertFactAliasEscapeKind - bipartitionModule - "bipartition_elim" - Authority.SourceAxiom - checkRoot "set/product.tex" - \moduleAt -> do - (_setParsed, setModule) <- moduleAt "set.tex" - (_productParsed, productModule) <- - moduleAt "set/product.tex" - assertEqual "product semantic imports" - [preludeSemanticId, semanticId setModule] - (Semantic.semanticInterfaceDirectInputs - (Module.sealedTypedModuleSemantic - productModule)) - assertFactAliasEscapeKind - productModule - "inter_times_intro" - Authority.SourceAxiom - checkRoot "set/filter.tex" - \moduleAt -> do - (_setParsed, setModule) <- moduleAt "set.tex" - (_powersetParsed, powersetModule) <- - moduleAt "set/powerset.tex" - (_filterParsed, filterModule) <- - moduleAt "set/filter.tex" - assertEqual "filter semantic imports" - [ preludeSemanticId - , semanticId setModule - , semanticId powersetModule - ] - (Semantic.semanticInterfaceDirectInputs - (Module.sealedTypedModuleSemantic filterModule)) - assertAllLocalFactsClean filterModule - checkRoot "relation.tex" - \moduleAt -> do - (_setParsed, setModule) <- moduleAt "set.tex" - (_powersetParsed, powersetModule) <- - moduleAt "set/powerset.tex" - (_productParsed, productModule) <- - moduleAt "set/product.tex" - (_relationParsed, relationModule) <- - moduleAt "relation.tex" - assertEqual "relation semantic imports" - [ preludeSemanticId - , semanticId setModule - , semanticId powersetModule - , semanticId productModule - ] - (Semantic.semanticInterfaceDirectInputs - (Module.sealedTypedModuleSemantic - relationModule)) - assertCleanFactAlias - relationModule - "union_relations_is_relation" - assertFactAliasEscapeKind - relationModule - "id_iff" - Authority.SourceAxiom - assertNoLocalFactEscapeKind - relationModule - Authority.Omitted - checkRoot "relation/properties.tex" - \moduleAt -> do - (_setParsed, setModule) <- moduleAt "set.tex" - (_relationParsed, relationModule) <- - moduleAt "relation.tex" - (_propertiesParsed, propertiesModule) <- - moduleAt "relation/properties.tex" - assertEqual "relation properties semantic imports" - [ preludeSemanticId - , semanticId setModule - , semanticId relationModule - ] - (Semantic.semanticInterfaceDirectInputs - (Module.sealedTypedModuleSemantic - propertiesModule)) - assertCleanFactAlias - propertiesModule - "asymmetric_implies_irreflexive" - assertNoLocalFactEscapeKind - propertiesModule - Authority.Omitted - assertNoLocalSourceAxiom propertiesModule - checkRoot "relation/uniqueness.tex" - \moduleAt -> do - (_setParsed, setModule) <- moduleAt "set.tex" - (_relationParsed, relationModule) <- - moduleAt "relation.tex" - (_uniquenessParsed, uniquenessModule) <- - moduleAt "relation/uniqueness.tex" - assertEqual "relation uniqueness semantic imports" - [ preludeSemanticId - , semanticId setModule - , semanticId relationModule - ] - (Semantic.semanticInterfaceDirectInputs - (Module.sealedTypedModuleSemantic - uniquenessModule)) - assertCleanFactAlias - uniquenessModule - "subseteq_of_injective_is_injective" - assertFactAliasEscapeKind - uniquenessModule - "identity_injective" - Authority.SourceAxiom - assertNoLocalFactEscapeKind - uniquenessModule - Authority.Omitted - assertNoLocalSourceAxiom uniquenessModule - checkRoot "function.tex" - \moduleAt -> do - (_setParsed, setModule) <- moduleAt "set.tex" - (_relationParsed, relationModule) <- - moduleAt "relation.tex" - (_uniquenessParsed, uniquenessModule) <- - moduleAt "relation/uniqueness.tex" - (_functionParsed, functionModule) <- - moduleAt "function.tex" - assertEqual "function semantic imports" - [ preludeSemanticId - , semanticId setModule - , semanticId relationModule - , semanticId uniquenessModule - ] - (Semantic.semanticInterfaceDirectInputs - (Module.sealedTypedModuleSemantic - functionModule)) - assertCleanFactAlias - functionModule - "function_on_weaken_codom" - assertFactAliasEscapeKind - functionModule - "function_apply_intro" - Authority.SourceAxiom - assertFactAliasEscapeKind - functionModule - "funs_circ" - Authority.Omitted - assertLocalDirectAuthorizationCount - functionModule - Authority.OmittedAuthorization - 6 - assertNoLocalSourceAxiom functionModule - checkRoot "set/cantor.tex" - \moduleAt -> do - (_powersetParsed, powersetModule) <- - moduleAt "set/powerset.tex" - (_functionParsed, functionModule) <- - moduleAt "function.tex" - (_cantorParsed, cantorModule) <- - moduleAt "set/cantor.tex" - assertEqual "Cantor semantic imports" - [ preludeSemanticId - , semanticId powersetModule - , semanticId functionModule - ] - (Semantic.semanticInterfaceDirectInputs - (Module.sealedTypedModuleSemantic - cantorModule)) - assertCleanFactAlias cantorModule "cantor" - assertNoLocalFactEscapeKind - cantorModule Authority.Omitted - assertNoLocalSourceAxiom cantorModule - checkRoot "set/fixpoint.tex" - \moduleAt -> do - (_powersetParsed, powersetModule) <- - moduleAt "set/powerset.tex" - (_functionParsed, functionModule) <- - moduleAt "function.tex" - (_fixpointParsed, fixpointModule) <- - moduleAt "set/fixpoint.tex" - assertEqual "fixpoint semantic imports" - [ preludeSemanticId - , semanticId powersetModule - , semanticId functionModule - ] - (Semantic.semanticInterfaceDirectInputs - (Module.sealedTypedModuleSemantic - fixpointModule)) - assertCleanFactAlias fixpointModule "fixpoint" - assertCleanFactAlias - fixpointModule "subseteqpreserving" - assertFactAliasEscapeKind - fixpointModule - "knastertarski" - Authority.SourceAxiom - assertNoLocalFactEscapeKind - fixpointModule Authority.Omitted - assertNoLocalSourceAxiom fixpointModule - where - semanticId = - Semantic.semanticInterfaceAssertedId - . Module.sealedTypedModuleSemantic - -assertLocalAliasesAbsent - :: Module.SealedTypedModule - -> [Text] - -> Assertion -assertLocalAliasesAbsent sealed names = - forM_ names \name -> - assertBool - ("protected module still publishes " <> show name) - (Semantic.semanticName name `notElem` aliases) - where - aliases = - [ Semantic.semanticAliasName alias - | delta <- localSemanticDeltas sealed - , alias <- Semantic.declarationDeltaAliases delta - ] + visits <- Store.storeMemoVisits warmMemo + assertEqual "cached prelude validates one artifact root" + 1 + (Store.storeArtifactsValidated visits) + +semanticStructureDescriptors + :: Semantic.SemanticInterface + -> [Semantic.SemanticStructureDescriptor] +semanticStructureDescriptors semantic = + [ descriptor + | delta <- Semantic.semanticInterfaceDeclarations semantic + , descriptor <- Semantic.semanticEnvironmentStructures + (Semantic.declarationDeltaEnvironment delta) + ] assertTransparentObjectAlias :: Module.SealedTypedModule @@ -983,18 +639,6 @@ assertTransparentObjectAlias sealed name = do Identity.TransparentObject (Identity.objectIdFamily target) -assertOpaqueObjectKey - :: Module.SealedTypedModule - -> Text - -> Semantic.SemanticGlobalKey - -> Assertion -assertOpaqueObjectKey sealed name key = do - target <- localObjectKeyTarget sealed key - assertEqual - ("opaque object for " <> StrictText.unpack name) - Identity.OpaqueObject - (Identity.objectIdFamily target) - localObjectKeyTarget :: Module.SealedTypedModule -> Semantic.SemanticGlobalKey @@ -1026,29 +670,6 @@ localObjectAliasTarget sealed name = do (Semantic.semanticGlobalTargetObject (Semantic.semanticGlobalBindingTarget binding)) -localTransparentObjectBody - :: Module.SealedTypedModule - -> Text - -> IO (Core.CanonicalTerm Identity.ObjectId) -localTransparentObjectBody sealed name = do - identity <- localObjectAliasTarget sealed name - object <- sole - ("asserted object for " <> StrictText.unpack name) - [ candidate - | batch <- Declaration.pendingModulePrefixBatches - (Module.sealedTypedModulePrefix sealed) - , candidate <- Declaration.committedBatchObjects batch - , Identity.assertedObjectId candidate == identity - ] - case Identity.assertedObjectContent object of - Identity.TransparentObjectContent _theory _coreType body -> - pure body - content -> - assertFailure - ("object for " <> StrictText.unpack name - <> " is not transparent: " <> show content) - >> fail "unreachable" - checkedPropositionTermByAlias :: Module.SealedTypedModule -> Text @@ -1057,30 +678,31 @@ checkedPropositionTermByAlias sealed name = do batch <- batchByAlias (Module.sealedTypedModulePrefix sealed) name + alias <- sole + ("semantic alias for " <> StrictText.unpack name) + [ candidate + | candidate <- Semantic.declarationDeltaAliases + (Declaration.committedBatchDelta batch) + , Semantic.semanticAliasName candidate + == Semantic.semanticName name + ] + occurrence <- sole + ("semantic fact for " <> StrictText.unpack name) + [ candidate + | candidate <- Semantic.declarationDeltaFacts + (Declaration.committedBatchDelta batch) + , Semantic.semanticFactFingerprint candidate + == Semantic.semanticAliasTarget alias + ] proposition <- sole ("checked proposition for " <> StrictText.unpack name) - (Declaration.committedBatchPropositions batch) + [ candidate + | candidate <- Declaration.committedBatchPropositions batch + , Identity.checkedPropositionId candidate + == Semantic.semanticFactProposition occurrence + ] pure (Identity.checkedPropositionTerm proposition) -assertFactAliasEscapeKind - :: Module.SealedTypedModule - -> Text - -> Authority.EscapeKind - -> Assertion -assertFactAliasEscapeKind sealed name expected = do - delta <- localDeltaByAlias sealed name - fact <- sole - ("semantic fact for " <> StrictText.unpack name) - (Semantic.declarationDeltaFacts delta) - assertBool - ("escape authority for " <> StrictText.unpack name) - ( expected - `elem` Authority.escapeKindsToList - (Authority.authoritySafetyEscapeKinds - (Authority.factAuthoritySafety - (Semantic.semanticFactAuthority fact))) - ) - assertCleanFactAlias :: Module.SealedTypedModule -> Text @@ -1107,114 +729,6 @@ assertCleanFactAlias sealed name = do (Authority.factAuthoritySafety (Semantic.semanticFactAuthority fact)) -assertAllLocalFactsClean - :: Module.SealedTypedModule - -> Assertion -assertAllLocalFactsClean sealed = - assertBool - "all locally published facts have clean authority" - (all hasCleanAuthority localFacts) - where - localFacts = - [ fact - | delta <- localSemanticDeltas sealed - , fact <- Semantic.declarationDeltaFacts delta - ] - hasCleanAuthority fact = - Authority.factAuthoritySafety - (Semantic.semanticFactAuthority fact) - == Authority.cleanAuthoritySafety - -assertNoLocalFactEscapeKind - :: Module.SealedTypedModule - -> Authority.EscapeKind - -> Assertion -assertNoLocalFactEscapeKind sealed unexpected = - assertBool - ("no local fact has " <> show unexpected <> " authority") - (all lacksEscapeKind localFacts) - where - localFacts = - [ fact - | delta <- localSemanticDeltas sealed - , fact <- Semantic.declarationDeltaFacts delta - ] - lacksEscapeKind fact = - unexpected - `notElem` Authority.escapeKindsToList - (Authority.authoritySafetyEscapeKinds - (Authority.factAuthoritySafety - (Semantic.semanticFactAuthority fact))) - -assertNoLocalSourceAxiom - :: Module.SealedTypedModule - -> Assertion -assertNoLocalSourceAxiom sealed = - assertBool - "module introduces no source axiom" - (all (/= Authority.SourceAxiomAuthorization) directAuthorizations) - where - directAuthorizations = - [ Authority.validationDirectAuthorization certificate - | batch <- Declaration.pendingModulePrefixBatches - (Module.sealedTypedModulePrefix sealed) - , validation <- maybeToList - (Declaration.committedBatchDeclarationValidation batch) - , certificate <- - Semantic.declarationValidationRecordCertificates validation - ] - -assertLocalDirectAuthorizationCount - :: Module.SealedTypedModule - -> Authority.DirectAuthorization - -> Int - -> Assertion -assertLocalDirectAuthorizationCount sealed expected expectedCount = - assertEqual - ("local " <> show expected <> " authorization count") - expectedCount - (length - [ () - | batch <- Declaration.pendingModulePrefixBatches - (Module.sealedTypedModulePrefix sealed) - , validation <- Declaration.committedBatchProofValidations batch - , Authority.validationDirectAuthorization - (Semantic.proofValidationRecordCertificate validation) - == expected - ]) - -assertSourceAxiomAlias - :: Module.SealedTypedModule - -> Text - -> Assertion -assertSourceAxiomAlias sealed name = do - batch <- batchByAlias - (Module.sealedTypedModulePrefix sealed) - name - fact <- sole - ("source axiom fact " <> StrictText.unpack name) - (Semantic.declarationDeltaFacts - (Declaration.committedBatchDelta batch)) - assertEqual - ("source axiom safety for " <> StrictText.unpack name) - (Authority.authoritySafety - (Authority.singletonEscapeKind Authority.SourceAxiom)) - (Authority.factAuthoritySafety - (Semantic.semanticFactAuthority fact)) - validation <- maybe - (assertFailure - ("source axiom validation for " <> StrictText.unpack name) - >> fail "unreachable") - pure - (Declaration.committedBatchDeclarationValidation batch) - certificate <- sole - ("source axiom certificate for " <> StrictText.unpack name) - (Semantic.declarationValidationRecordCertificates validation) - assertEqual - ("source axiom authority for " <> StrictText.unpack name) - Authority.SourceAxiomAuthorization - (Authority.validationDirectAuthorization certificate) - batchByAlias :: Declaration.PendingModulePrefix -> Text @@ -1350,18 +864,10 @@ coalescesSharedDirectSyntax = do , (sourceMountId "library", root Posix.</> "library") , (sourceMountId "debug", root Posix.</> "debug") ] - selection <- - expectRight - (Migration.resolveMigrationSelection - mounts - Migration.typedMigrationModules) let bootstrapSyntax = Module.sealedTypedModuleSyntax (Module.bootstrapPreludeModule session) - syntaxInputs source - | Migration.migrationSelectionContains selection source = - [bootstrapSyntax] - | otherwise = [] + syntaxInputs _source = [bootstrapSyntax] request <- expectRight (searchedRoot "test/phase3/typed-shared-root.tex") @@ -1371,9 +877,6 @@ coalescesSharedDirectSyntax = do mounts request syntaxInputs - assertEqual "selected shared-syntax graph" - Migration.TypedMigrationGraph - (Migration.classifyMigrationGraph selection workspace) case Parse.parsedWorkspaceModules workspace of [firstParsed, secondParsed, rootParsed] -> do first <- seal foundation session firstParsed [] @@ -1436,31 +939,6 @@ coalescesSharedDirectSyntax = do assertFailure "empty typed module did not seal" >> fail "unreachable" -resetsGlossStatePerModule :: Assertion -resetsGlossStatePerModule = do - blocks <- Api.gloss "test/phase3/gloss-root.tex" - binders <- traverse signatureBinder blocks - assertEqual "fresh variables restart at each module boundary" - [Internal.FreshVar 0, Internal.FreshVar 0, Internal.FreshVar 1] - binders - where - signatureBinder = \case - Internal.BlockSig - _location - _marker - _assumptions - (Internal.SignatureFormula - (Internal.Quantified Internal.Universally scope)) -> - case nubOrd [binder | B binder <- toList (fromScope scope)] of - [binder] -> pure binder - binders -> - assertFailure - ("unexpected signature binders: " <> show binders) - >> fail "unreachable" - block -> - assertFailure ("unexpected glossed block: " <> show block) - >> fail "unreachable" - rejectsUnsupportedTypedSource :: Assertion rejectsUnsupportedTypedSource = do result <- @@ -1472,13 +950,16 @@ rejectsUnsupportedTypedSource = do Provers.defaultMemoryLimit) "test/phase3/typed-unsupported.tex") case result of - Left - (failure@(Api.VerificationTypedModuleError + Right + ( Api.VerificationCheckingFailure _report + (failure@(Api.VerificationTypedModuleError source (Module.TypedActionFailed (Module.TypedExactCompileFailed (Exact.ExactUnsupportedDeclarationBody location))) - prefix)) -> do + prefix)) + , _measurements + ) -> do assertEqual "failed source" "test/phase3/typed-unsupported.tex" (safeRelativePathFilePath @@ -1670,6 +1151,566 @@ compilesExactDeclarationGraph = do Identity.TransparentObjectContent{} -> "transparent" Identity.IntrinsicObjectContent{} -> "intrinsic" +compilesExactStructures :: Assertion +compilesExactStructures = do + foundation <- expectRight Foundation.checkedFoundation + repository <- getCurrentDirectory + Temp.withSystemTempDirectory "felix-exact-structures" \directory -> do + let path = directory Posix.</> "store.sqlite" + executable = directory Posix.</> "vampire" + writeAcceptedFixtureVampire executable + runs <- newIORef (0 :: Int) + let resolver = countingAcceptedResolver executable runs + (_startup, store) <- + Store.openStore path (Identity.theoryId foundation) + >>= expectRight + bracket (pure store) Store.closeStore \opened -> do + prelude <- + expectRight + =<< acquireFinalPreludeSession + opened foundation resolver + carrierOperation <- sole "base carrier operation" + [ operation + | descriptor <- semanticStructureDescriptors + (Module.sealedTypedModuleSemantic + (Module.finalPreludeModule prelude)) + , operation <- + Semantic.semanticStructureDescriptorOperations descriptor + ] + mounts <- exactFixtureMounts repository + workspace <- parseFinalExactWorkspace + prelude mounts "test/phase5/exact-structure-child.tex" + sealed <- compileFinalParsedWorkspaceWithResolver + foundation prelude resolver workspace + freshRuns <- readIORef runs + warm <- installAndLoadStructures + opened foundation prelude workspace sealed + warmRuns <- readIORef runs + assertEqual "warm structures preserve descriptors" + (structureDescriptors <$> sealed) + (structureDescriptors <$> warm) + assertEqual "warm structures make no prover calls" + freshRuns warmRuns + case sealed of + [parent, child] -> do + let parentBatches = + Declaration.pendingModulePrefixBatches + (Module.sealedTypedModulePrefix parent) + parentDeltas = + Semantic.semanticInterfaceDeclarations + (Module.sealedTypedModuleSemantic parent) + childBatches = + Declaration.pendingModulePrefixBatches + (Module.sealedTypedModulePrefix child) + childDeltas = + Semantic.semanticInterfaceDeclarations + (Module.sealedTypedModuleSemantic child) + parentBatch <- sole "parent structure batch" + (take 1 parentBatches) + parentDelta <- sole "parent structure delta" + (take 1 parentDeltas) + parentDescriptor <- sole "parent structure descriptor" + (Semantic.semanticEnvironmentStructures + (Semantic.declarationDeltaEnvironment parentDelta)) + parentOperation <- sole "parent structure operation" + (Semantic.semanticStructureDescriptorOperations + parentDescriptor) + parentPredicate <- + maybe + (assertFailure "parent structure has no predicate" + >> fail "unreachable") + pure + (Semantic.semanticStructureDescriptorPredicate + parentDescriptor) + assertEqual "structure object family order" + ["opaque", "transparent"] + [ objectFamilyName + (Identity.assertedObjectContent object) + | object <- Declaration.committedBatchObjects parentBatch + ] + assertEqual "structure fact aliases" + [ Semantic.semanticName "pointed_set" + , Semantic.semanticName "pointed_refl" + ] + (Semantic.semanticAliasName + <$> Semantic.declarationDeltaAliases parentDelta) + definitionFact <- sole "structure definition fact" + (take 1 (Semantic.declarationDeltaFacts parentDelta)) + definitionTarget <- + targetForOccurrence parentBatch definitionFact + assertEqual "pointwise structure definition" + (Core.CForall Core.TySet + (Core.CEq Core.TyProp + (Core.CApp + (Core.CGlobal parentPredicate) + (Core.CBound 0)) + (Core.CEq Core.TySet + (Core.CBound 0) + (Core.CBound 0)))) + definitionTarget + validations <- + maybe + (assertFailure "structure validation is absent" + >> fail "unreachable") + (pure + . Semantic.declarationValidationRecordCertificates) + (Declaration.committedBatchDeclarationValidation + parentBatch) + case validations of + definitionValidation : projectionValidation : [] -> do + assertEqual "structure definition authority" + (Authority.CheckedKernelConstruction + (Authority.CheckedDefinitionEquation + parentPredicate)) + (Authority.validationDirectAuthorization + definitionValidation) + projectionFact <- sole + "structure projection fact" + (drop 1 + (Semantic.declarationDeltaFacts + parentDelta)) + assertEqual + "projection has independent authority" + (Semantic.semanticFactAuthority projectionFact) + (Authority.validationTarget + projectionValidation) + assertEqual "projection authority is clean" + Authority.cleanAuthoritySafety + (Authority.factAuthoritySafety + (Authority.validationTarget + projectionValidation)) + records -> + assertFailure + ("expected two structure validations, got " + <> show records) + assertBool "all parent structure facts are clean" + (all + ((== Authority.cleanAuthoritySafety) + . Authority.factAuthoritySafety + . Semantic.semanticFactAuthority) + (Semantic.declarationDeltaFacts parentDelta)) + + let claimGlobals marker = do + batch <- batchWithAlias marker parentBatches + occurrence <- sole (marker <> " occurrence") + (Semantic.declarationDeltaFacts + (Declaration.committedBatchDelta batch)) + Core.canonicalTermGlobals + <$> targetForOccurrence batch occurrence + carrierGlobals <- claimGlobals "pointed_carrier" + operationGlobals <- claimGlobals "pointed_operation" + assertBool "membership uses inherited carrier" + (Semantic.semanticStructureOperationObject carrierOperation + `Set.member` carrierGlobals) + assertBool "implicit and explicit operation share one object" + (Semantic.semanticStructureOperationObject parentOperation + `Set.member` operationGlobals) + + childBatch <- sole "child structure batch" childBatches + childDelta <- sole "child structure delta" childDeltas + childDescriptor <- sole "child structure descriptor" + (Semantic.semanticEnvironmentStructures + (Semantic.declarationDeltaEnvironment childDelta)) + assertEqual "child allocates no replacement operation" + [] + (Semantic.semanticStructureDescriptorOperations + childDescriptor) + assertEqual "child owns only its transparent predicate" + ["transparent"] + [ objectFamilyName + (Identity.assertedObjectContent object) + | object <- Declaration.committedBatchObjects childBatch + ] + modules -> + assertFailure + ("expected parent and child structures, got " + <> show (length modules)) + where + installAndLoadStructures store foundation prelude workspace sealed = do + memo <- Store.newStoreMemo store + case + ( toList + (Parse.parsedWorkspaceImportedBeforeImporter workspace) + , sealed + ) of + ([parentParsed, childParsed], [parent, child]) -> do + cachedParent <- persistAndLoad memo [] parentParsed parent + cachedChild <- persistAndLoad + memo [cachedParent] childParsed child + pure [cachedParent, cachedChild] + (parsed, modules) -> + assertFailure + ("expected two structure installations, got " + <> show (length parsed) + <> " parsed and " + <> show (length modules) + <> " checked modules") + >> fail "unreachable" + where + preludeModule = Module.finalPreludeModule prelude + + persistAndLoad memo parents parsed sealedModule = do + let input = Module.identifiedPhysicalModule parsed + syntax = Module.sealedTypedModuleSyntax sealedModule + semantic = Module.sealedTypedModuleSemantic sealedModule + key <- expectRight + (Semantic.moduleArtifactKey + (Module.identifiedModuleOwner input) + (Parse.identifiedParsedModuleId + (Module.identifiedModuleParsed input)) + (Semantic.semanticInterfaceDirectInputs semantic) + (Identity.theoryId foundation)) + let artifact = Semantic.moduleArtifactResult + key + (Syntax.moduleSyntaxAssertedId syntax) + (Semantic.semanticInterfaceAssertedId semantic) + acknowledged <- expectRight + =<< Store.writeSealedModule + store + (Module.sealedTypedModulePrefix sealedModule) + [syntax] + [semantic] + artifact + assertEqual "cached structure artifact acknowledgement" + artifact acknowledged + loaded <- expectRight + =<< Store.loadCachedModuleInstallation + memo + store + key + (Syntax.moduleSyntaxAssertedId + (Parse.parsedModuleSyntaxInterface parsed)) + installation <- maybe + (assertFailure "cached structure installation is absent" + >> fail "unreachable") + pure + loaded + expectRight + (Module.cachedSealedTypedModule + foundation + (preludeModule : parents) + installation) + + structureDescriptors = + semanticStructureDescriptors + . Module.sealedTypedModuleSemantic + + objectFamilyName :: Identity.ObjectContent -> String + objectFamilyName = \case + Identity.OpaqueObjectContent{} -> "opaque" + Identity.TransparentObjectContent{} -> "transparent" + Identity.IntrinsicObjectContent{} -> "intrinsic" + + targetForOccurrence batch occurrence = + maybe + (assertFailure "structure proposition is absent" + >> fail "unreachable") + (pure . Core.frozenCoreTerm . Identity.checkedPropositionTerm) + (find + ((== Semantic.semanticFactProposition occurrence) + . Identity.checkedPropositionId) + (Declaration.committedBatchPropositions batch)) + + batchWithAlias marker batches = + maybe + (assertFailure ("missing batch alias " <> marker) + >> fail "unreachable") + pure + (find + (elem (Semantic.semanticName (StrictText.pack marker)) + . fmap Semantic.semanticAliasName + . Semantic.declarationDeltaAliases + . Declaration.committedBatchDelta) + batches) + +compilesContextualAbbreviations :: Assertion +compilesContextualAbbreviations = do + foundation <- expectRight Foundation.checkedFoundation + repository <- getCurrentDirectory + Temp.withSystemTempDirectory "felix-contextual-abbreviation" \directory -> do + let storePath = directory Posix.</> "store.sqlite" + executable = directory Posix.</> "vampire" + relative = "test/phase5/exact-contextual-abbreviation.tex" + writeAcceptedFixtureVampire executable + runs <- newIORef (0 :: Int) + let resolver = countingAcceptedResolver executable runs + (_startup, store) <- + Store.openStore storePath (Identity.theoryId foundation) + >>= expectRight + bracket (pure store) Store.closeStore \opened -> do + prelude <- + expectRight + =<< acquireFinalPreludeSession + opened foundation resolver + mounts <- exactFixtureMounts repository + workspace <- parseFinalExactWorkspace prelude mounts relative + sealed <- sole "contextual abbreviation module" + =<< compileFinalParsedWorkspaceWithResolver + foundation prelude resolver workspace + let deltas = + Semantic.semanticInterfaceDeclarations + (Module.sealedTypedModuleSemantic sealed) + contextualTargets = + [ (identity, requirements) + | delta <- deltas + , binding <- Semantic.semanticEnvironmentBindings + (Semantic.declarationDeltaEnvironment delta) + , Semantic.ContextualTransparentExpansion + identity requirements <- + [Semantic.semanticGlobalBindingTarget binding] + ] + assertEqual "contextual target count" 2 + (length contextualTargets) + requirements <- + sole "canonical contextual requirement set" + (nubOrd (snd <$> contextualTargets)) + assertEqual "one structure operation requirement" 1 + (Map.size requirements) + let batches = + Declaration.pendingModulePrefixBatches + (Module.sealedTypedModulePrefix sealed) + traverse_ + (assertReflexiveFact batches) + [ "phase5_context_dot_explicit" + , "phase5_context_inherited" + , "phase5_context_nested" + , "phase5_context_explicit_unique" + ] + + parsed <- pure (Parse.parsedWorkspaceRootModule workspace) + let syntax = Module.sealedTypedModuleSyntax sealed + semantic = Module.sealedTypedModuleSemantic sealed + key <- expectRight + (Semantic.moduleArtifactKey + (moduleName (Parse.parsedModuleAddress parsed)) + (Parse.parsedModuleId parsed) + (Semantic.semanticInterfaceDirectInputs semantic) + (Identity.theoryId foundation)) + let artifact = + Semantic.moduleArtifactResult + key + (Syntax.moduleSyntaxAssertedId syntax) + (Semantic.semanticInterfaceAssertedId semantic) + void + (expectRight + =<< Store.writeSealedModule + opened + (Module.sealedTypedModulePrefix sealed) + [syntax] + [semantic] + artifact) + memo <- Store.newStoreMemo opened + loaded <- expectRight + =<< Store.loadCachedModuleInstallation + memo opened key + (Syntax.moduleSyntaxAssertedId + (Parse.parsedModuleSyntaxInterface parsed)) + installation <- maybe + (assertFailure "contextual cached installation is absent" + >> fail "unreachable") + pure + loaded + cached <- expectRight + (Module.cachedSealedTypedModule + foundation + [Module.finalPreludeModule prelude] + installation) + assertEqual "cached contextual semantic target" + semantic + (Module.sealedTypedModuleSemantic cached) + + runsBeforeConsumer <- readIORef runs + consumerWorkspace <- + parseFinalExactWorkspace prelude mounts + "test/phase5/exact-contextual-abbreviation-consumer.tex" + let consumerParsed = + Parse.parsedWorkspaceRootModule consumerWorkspace + consumerInput <- expectRight + (Module.typedModuleInput + foundation + (Module.finalPreludeReadiness prelude) + resolver + Declaration.FreshValidation + consumerParsed + [cached]) + consumer <- Module.runTypedModule consumerInput >>= \case + Module.TypedModuleSucceeded sealedConsumer -> + pure sealedConsumer + Module.TypedModuleOpenFailed failure -> + assertFailure + ("contextual consumer did not open: " <> show failure) + >> fail "unreachable" + Module.TypedModuleFailed failure _prefix -> + assertFailure + ("contextual consumer did not seal: " <> show failure) + >> fail "unreachable" + let consumerTargets = + [ Semantic.semanticGlobalTargetObject + (Semantic.semanticGlobalBindingTarget binding) + | delta <- localSemanticDeltas consumer + , binding <- Semantic.semanticEnvironmentBindings + (Semantic.declarationDeltaEnvironment delta) + ] + assertEqual "two contextual consumer declarations" 2 + (length consumerTargets) + void + (sole + "quantified contextual binder matches its explicit parameter" + (nubOrd consumerTargets)) + runsAfterConsumer <- readIORef runs + assertEqual "contextual abbreviations require no prover call" + runsBeforeConsumer runsAfterConsumer + + verifyFailure foundation resolver prelude mounts sealed + "test/phase5/exact-contextual-abbreviation-missing.tex" + (\case + Exact.ExactContextualExpansionNotAvailable location _key -> + assertEqual "missing context line" 5 (locLine location) + failure -> + assertFailure + ("unexpected missing-context failure: " + <> show failure)) + verifyFailure foundation resolver prelude mounts sealed + "test/phase5/exact-contextual-abbreviation-ambiguous.tex" + (\case + Exact.ExactStructureOperationAmbiguous + location _symbol objects -> do + assertEqual "ambiguous operation line" 16 + (locLine location) + assertEqual "two distinct operation objects" 2 + (length objects) + failure -> + assertFailure + ("unexpected operation ambiguity failure: " + <> show failure)) + where + assertReflexiveFact batches marker = do + batch <- maybe + (assertFailure ("missing contextual fact " <> marker) + >> fail "unreachable") + pure + (find + (elem (Semantic.semanticName (StrictText.pack marker)) + . fmap Semantic.semanticAliasName + . Semantic.declarationDeltaAliases + . Declaration.committedBatchDelta) + batches) + proposition <- sole (marker <> " proposition") + (Declaration.committedBatchPropositions batch) + let body = stripClaimEnvelope + (Core.frozenCoreTerm + (Identity.checkedPropositionTerm proposition)) + case body of + Core.CEq _ left right -> + assertEqual (marker <> " canonical sides") left right + _ -> + assertFailure + (marker <> " did not elaborate to reflexive equality: " + <> show body) + + stripClaimEnvelope = \case + Core.CForall _ body -> stripClaimEnvelope body + Core.CImp _ body -> stripClaimEnvelope body + term -> term + + verifyFailure foundation resolver prelude mounts imported relative checkFailure = do + workspace <- parseFinalExactWorkspace prelude mounts relative + let parsed = Parse.parsedWorkspaceRootModule workspace + input <- expectRight + (Module.typedModuleInput + foundation + (Module.finalPreludeReadiness prelude) + resolver + Declaration.FreshValidation + parsed + [imported]) + Module.runTypedModule input >>= \case + Module.TypedModuleFailed + (Module.TypedActionFailed + (Module.TypedExactCompileFailed failure)) + _prefix -> + checkFailure failure + Module.TypedModuleFailed + (Module.TypedActionFailed + (Module.TypedExactProofFailed + (ExactProof.ExactProofElaborationFailed failure))) + _prefix -> + checkFailure failure + Module.TypedModuleSucceeded{} -> + assertFailure (relative <> " was unexpectedly accepted") + Module.TypedModuleOpenFailed failure -> + assertFailure + (relative <> " did not open: " <> show failure) + Module.TypedModuleFailed failure _prefix -> + assertFailure + (relative <> " failed unexpectedly: " <> show failure) + +rejectsUnknownExactStructureParent :: Assertion +rejectsUnknownExactStructureParent = + Temp.withSystemTempDirectory "felix-exact-structure-parent" \root -> do + let relative = "entry.tex" + path = root Posix.</> relative + source = + "\\begin{struct}\\label{known_structure}\n" + <> " A known structure $X$ is a onesorted structure.\n" + <> "\\end{struct}\n\n" + <> "\\begin{struct}\\label{invalid_structure}\n" + <> " An invalid structure $X$ is a future structure.\n" + <> "\\end{struct}\n\n" + <> "\\begin{struct}\\label{future_structure}\n" + <> " A future structure $X$ is a onesorted structure.\n" + <> "\\end{struct}\n" + ByteString.writeFile path + (Text.encodeUtf8 (StrictText.pack source)) + foundation <- expectRight Foundation.checkedFoundation + Temp.withSystemTempDirectory "felix-exact-structure-store" \directory -> do + let storePath = directory Posix.</> "store.sqlite" + executable = directory Posix.</> "vampire" + writeAcceptedFixtureVampire executable + runs <- newIORef (0 :: Int) + let resolver = countingAcceptedResolver executable runs + (_startup, store) <- + Store.openStore storePath (Identity.theoryId foundation) + >>= expectRight + bracket (pure store) Store.closeStore \opened -> do + prelude <- + expectRight + =<< acquireFinalPreludeSession + opened foundation resolver + mounts <- exactFixtureMounts root + workspace <- parseFinalExactWorkspace prelude mounts relative + let parsed = Parse.parsedWorkspaceRootModule workspace + input <- expectRight + (Module.typedModuleInput + foundation + (Module.finalPreludeReadiness prelude) + resolver + Declaration.FreshValidation + parsed + []) + Module.runTypedModule input >>= \case + Module.TypedModuleFailed + (Module.TypedActionFailed + (Module.TypedExactCompileFailed + (Exact.ExactStructureNotVisible + location _phrase))) + prefix -> do + assertEqual "unknown parent line" 5 (locLine location) + assertEqual "only the valid structure was published" + 1 + (length + (Declaration.pendingModulePrefixBatches prefix)) + Module.TypedModuleSucceeded{} -> + assertFailure "unknown structure parent was accepted" + Module.TypedModuleOpenFailed failure -> + assertFailure + ("invalid structure module did not open: " + <> show failure) + Module.TypedModuleFailed failure _prefix -> + assertFailure + ("unexpected invalid structure failure: " + <> show failure) + compilesExactRelationExpressions :: Assertion compilesExactRelationExpressions = do foundation <- expectRight Foundation.checkedFoundation @@ -1712,14 +1753,17 @@ compilesExactRelationExpressions = do prover "test/phase5/exact-relation-expression-missing-pair.tex") case missingPair of - Left - (Api.VerificationTypedModuleError + Right + ( Api.VerificationCheckingFailure _report + (Api.VerificationTypedModuleError _source (Module.TypedActionFailed (Module.TypedExactProofFailed (ExactProof.ExactProofElaborationFailed (Exact.ExactGlobalNotVisible location key)))) - prefix) -> do + prefix) + , _measurements + ) -> do assertEqual "missing ordered-pair provider line" 2 (locLine location) @@ -1752,7 +1796,7 @@ resolvesSourceOwnedApplication = do \store -> do prelude <- expectRight - =<< Module.buildFinalPreludeSession + =<< acquireFinalPreludeSession store foundation resolver mounts <- exactFixtureMounts repository workspace <- parseFinalExactWorkspace @@ -1788,14 +1832,17 @@ resolvesSourceOwnedApplication = do prover "test/phase5/exact-application-missing.tex") case missing of - Left - (Api.VerificationTypedModuleError + Right + ( Api.VerificationCheckingFailure _report + (Api.VerificationTypedModuleError _source (Module.TypedActionFailed (Module.TypedExactProofFailed (ExactProof.ExactProofElaborationFailed (Exact.ExactGlobalNotVisible location key)))) - prefix) -> do + prefix) + , _measurements + ) -> do assertEqual "unresolved application line" 2 (locLine location) assertEqual "unresolved application key" (Semantic.SemanticExpressionFunction @@ -1826,7 +1873,7 @@ confinesExactQuantifiedTerms = do \store -> do prelude <- expectRight - =<< Module.buildFinalPreludeSession + =<< acquireFinalPreludeSession store foundation resolver mounts <- exactFixtureMounts repository workspace <- parseFinalExactWorkspace @@ -1856,15 +1903,18 @@ confinesExactQuantifiedTerms = do prover "test/phase5/exact-quantified-subject-nested.tex") case negative of - Left - (Api.VerificationTypedModuleError + Right + ( Api.VerificationCheckingFailure _report + (Api.VerificationTypedModuleError _source (Module.TypedActionFailed (Module.TypedExactProofFailed (ExactProof.ExactProofElaborationFailed (Exact.ExactQuantifiedTermRequiresStatementSubject location)))) - prefix) -> do + prefix) + , _measurements + ) -> do assertEqual "nested quantified term line" 8 (locLine location) assertEqual "earlier exact definition remains committed" 1 @@ -2307,6 +2357,209 @@ compilesAndReusesProofLocalSetDefinitions = (Core.CImp left (Core.CImp right Core.CFalsum)) Core.CFalsum +compilesAndReusesProofLocalFunctionGraphs :: Assertion +compilesAndReusesProofLocalFunctionGraphs = + Temp.withSystemTempDirectory "felix-exact-local-function" \root -> do + let relative = "test/phase5/exact-local-function.tex" + failedRelative = + "test/phase5/exact-local-function-failure.tex" + executable = root Posix.</> "vampire" + storePath = root Posix.</> "store.sqlite" + writeAcceptedFixtureVampire executable + foundation <- expectRight Foundation.checkedFoundation + bootstrap <- + expectRight + =<< Module.buildBootstrapPreludeFixture + foundation unusedResolver + mounts <- exactFixtureMounts =<< getCurrentDirectory + workspace <- parseExactWorkspace bootstrap mounts relative + observations <- newIORef [] + let resolver = Declaration.vampireResolver \prepared -> do + let problem = + Provers.preparedTypedProverLogicalProblem prepared + premises = + [ ( Backend.typedProblemRoute problem + , fmap snd + (Vector.toList + (Backend.supportedPropositionSupport + proposition)) + , Backend.supportedPropositionTerm proposition + ) + | premise <- + Vector.toList + (Backend.typedProblemLocalPremises problem) + , let proposition = + Backend.typedLocalPremiseProposition premise + ] + modifyIORef' observations (<> premises) + runNoLoggingT + (Provers.runPreparedTypedProver + (Provers.vampire + executable + Provers.defaultTimeLimit + Provers.defaultMemoryLimit) + prepared) + freshModules <- + compileParsedWorkspaceWithValidation + foundation bootstrap resolver + Declaration.FreshValidation workspace + allObserved <- readIORef observations + let observed = + [ (route, proposition) + | (route, support, proposition) <- allObserved + , support == [Core.TySet, Core.TySet] + , isJust (localFunctionPair proposition) + ] + assertBool + ("the local graph characteristic reaches a discharge: " + <> show allObserved) + (not (null observed)) + for_ observed \(route, proposition) -> do + assertEqual "local function characteristic stays on FOF" + Backend.RouteFof route + assertExactLocalFunctionCharacteristic proposition + freshRoot <- sole "fresh local-function root" + (take 1 (reverse freshModules)) + rootBatch <- sole "local function publishes only its theorem" + (drop 1 + (Declaration.pendingModulePrefixBatches + (Module.sealedTypedModulePrefix freshRoot))) + assertEqual "local function publishes no object" + [] (Declaration.committedBatchObjects rootBatch) + assertEqual "local function publishes only its theorem" + 1 + (length + (Declaration.committedBatchPropositions rootBatch)) + assertEqual "local function publishes no semantic binding" + [] + (Semantic.semanticEnvironmentBindings + (Semantic.declarationDeltaEnvironment + (Declaration.committedBatchDelta rootBatch))) + rootFact <- sole "local-function theorem" + (Semantic.declarationDeltaFacts + (Declaration.committedBatchDelta rootBatch)) + assertEqual "local-function theorem remains clean" + Authority.cleanAuthoritySafety + (Authority.factAuthoritySafety + (Semantic.semanticFactAuthority rootFact)) + + bracket + (snd <$> (Store.openStore storePath + (Identity.theoryId foundation) >>= expectRight)) + Store.closeStore + \store -> do + traverse_ + (expectRightIO + . Store.writePendingModulePrefix store + . Module.sealedTypedModulePrefix) + freshModules + let validation = + Declaration.WarmValidation + (Declaration.validationLookup + (expectRightIO + . Store.loadProofValidation store) + (expectRightIO + . Store.loadDeclarationValidation store)) + warmRuns <- newIORef (0 :: Int) + warmModules <- + compileParsedWorkspaceWithValidation + foundation bootstrap + (countingAcceptedResolver executable warmRuns) + validation workspace + assertEqual "warm local-function graph skips Vampire" + 0 =<< readIORef warmRuns + warmRoot <- sole "warm local-function root" + (take 1 (reverse warmModules)) + assertEqual "warm local-function semantic interface" + (Module.sealedTypedModuleSemantic freshRoot) + (Module.sealedTypedModuleSemantic warmRoot) + assertEqual "warm local-function prefix" + (Declaration.pendingModulePrefixCurrent + (Module.sealedTypedModulePrefix freshRoot)) + (Declaration.pendingModulePrefixCurrent + (Module.sealedTypedModulePrefix warmRoot)) + + failedWorkspace <- + parseExactWorkspace bootstrap mounts failedRelative + failedInput <- expectRight + (Module.typedModuleInput + foundation + (Module.bootstrapPreludeReadiness bootstrap) + unusedResolver + Declaration.FreshValidation + (Parse.parsedWorkspaceRootModule failedWorkspace) + []) + Module.runTypedModule failedInput >>= \case + Module.TypedModuleFailed + (Module.TypedActionFailed + (Module.TypedExactProofFailed + (ExactProof.ExactProofElaborationFailed + (Exact.ExactFreeVariable location + (Raw.NamedVar "f"))))) + prefix -> do + assertEqual "self-reference rejection line" + 6 (locLine location) + assertBool "failed local function publishes no theorem" + (null + (Declaration.pendingModulePrefixBatches prefix)) + Module.TypedModuleSucceeded{} -> + assertFailure "self-referential local function was accepted" + Module.TypedModuleOpenFailed failure -> + assertFailure + ("local-function failure fixture did not open: " + <> show failure) + Module.TypedModuleFailed failure _prefix -> + assertFailure + ("unexpected local-function failure: " + <> show failure) + where + assertExactLocalFunctionCharacteristic proposition = do + pair <- + maybe + (assertFailure "local function characteristic has wrong shape") + pure + (localFunctionPair proposition) + assertEqual "local function uses the exact replacement characteristic" + (expectedLocalFunctionCharacteristic pair) + proposition + + localFunctionPair proposition = + case Set.toList (Core.canonicalTermGlobals proposition) of + [pair] + | proposition == expectedLocalFunctionCharacteristic pair -> + Just pair + _ -> + Nothing + + expectedLocalFunctionCharacteristic pair = + Core.CForall Core.TySet + (Core.CEq Core.TyProp + (member (Core.CBound 0) (Core.CBound 1)) + (existsP + (andP + (member (Core.CBound 0) (Core.CBound 3)) + (Core.CEq Core.TySet + (Core.CBound 1) + (Core.CApp + (Core.CApp + (Core.CGlobal pair) + (Core.CBound 0)) + (Core.CBound 0)))))) + + member element set = + Core.CApp + (Core.CApp (Core.CIntrinsic Core.Member) element) + set + + andP left right = + notP (Core.CImp left (notP right)) + + existsP proposition = + notP (Core.CForall Core.TySet (notP proposition)) + + notP proposition = + Core.CImp proposition Core.CFalsum + confinesTerminalExactContradiction :: Assertion confinesTerminalExactContradiction = Temp.withSystemTempDirectory "felix-exact-contradiction" \directory -> do @@ -3210,7 +3463,8 @@ assertExactDatatypeModule label sealed = do (\binding -> case Semantic.semanticGlobalBindingTarget binding of Semantic.GlobalReference{} -> True - Semantic.TransparentExpansion{} -> False) + Semantic.TransparentExpansion{} -> False + Semantic.ContextualTransparentExpansion{} -> False) bindings) assertEqual (label <> " datatype global targets") (Set.fromList objectIds) @@ -4537,9 +4791,6 @@ loadsCachedExactProducerForFreshImporter = do executable Provers.defaultTimeLimit Provers.defaultMemoryLimit - resolver = Declaration.vampireResolver \prepared -> - runNoLoggingT - (Provers.runPreparedTypedProver prover prepared) verify mode source = runNoLoggingT (Api.verifyWithObserverAndStoreMode @@ -4553,10 +4804,12 @@ loadsCachedExactProducerForFreshImporter = do "test/phase5/exact-importer.tex" assertTypedSuccess "fresh producer" producer assertTypedSuccess "warm producer/fresh importer" importer + memo <- Store.newStoreMemo store prelude <- expectRight - =<< Module.buildFinalPreludeSession - store foundation resolver + =<< Module.acquireFinalPreludeSession + memo store foundation unusedResolver + preludeVisits <- Store.storeMemoVisits memo repository <- getCurrentDirectory mounts <- exactFixtureMounts repository workspace <- parseFinalExactWorkspace @@ -4566,11 +4819,11 @@ loadsCachedExactProducerForFreshImporter = do (Parse.parsedWorkspaceImportedBeforeImporter workspace) preludeSemantic = Module.sealedTypedModuleSemantic - (Module.migrationPreludeModule prelude) + (Module.finalPreludeModule prelude) preludeId = Semantic.semanticInterfaceAssertedId preludeSemantic theory = Identity.theoryId foundation - loadInstallation memo parsed direct = do + loadInstallation parsed direct = do key <- expectRight (Semantic.moduleArtifactKey (moduleName (Parse.parsedModuleAddress parsed)) @@ -4598,16 +4851,25 @@ loadsCachedExactProducerForFreshImporter = do ] case parsedModules of [producerParsed, importerParsed] -> do - memo <- Store.newStoreMemo store producerInstallation <- - loadInstallation memo producerParsed [preludeId] + loadInstallation producerParsed [preludeId] + producerVisits <- Store.storeMemoVisits memo + assertEqual "ordinary root adds one artifact validation" + (Store.storeArtifactsValidated preludeVisits + 1) + (Store.storeArtifactsValidated producerVisits) + assertEqual "ordinary root reuses prelude syntax validation" + (Store.storeSyntaxRowsValidated preludeVisits + 1) + (Store.storeSyntaxRowsValidated producerVisits) + assertEqual "ordinary root reuses prelude semantic validation" + (Store.storeSemanticRowsValidated preludeVisits + 1) + (Store.storeSemanticRowsValidated producerVisits) let producerSemanticId = Semantic.semanticInterfaceAssertedId (Store.cachedInstallationSemantic producerInstallation) importerInstallation <- loadInstallation - memo importerParsed [preludeId, producerSemanticId] + importerParsed [preludeId, producerSemanticId] case ( environmentBindings producerInstallation , environmentBindings importerInstallation ) of @@ -4666,6 +4928,832 @@ loadsCachedExactProducerForFreshImporter = do <> show (length modules)) Store.closeStore store +selectsConcurrentModuleFailureDeterministically :: Assertion +selectsConcurrentModuleFailureDeterministically = do + foundation <- expectRight Foundation.checkedFoundation + Temp.withSystemTempDirectory "felix-concurrent-module-failure" \root -> do + let executable = root Posix.</> "vampire" + source = "test/phase7/concurrent-failure-root.tex" + prover = + Provers.vampire + executable + Provers.defaultTimeLimit + Provers.defaultMemoryLimit + ignored = + Api.verificationRequestObserver + (\_position _request -> pure ()) + select amount = + Provers.selectEffectiveJobs + (Provers.effectiveJobs amount) + (fail "explicit jobs unexpectedly detected processors") + reportEntry escape = + ( Api.reportedEscapeKind escape + , locFile (Api.reportedEscapeLocation escape) + , locLine (Api.reportedEscapeLocation escape) + ) + inspect label expectedPositions + (result, measurements, positions) = do + case result of + Api.VerificationFailure report failed -> do + assertEqual (label <> " selected earlier failure") + "test/phase7/concurrent-earlier.tex" + (locFile (Api.failedVerificationLocation failed)) + assertEqual (label <> " admitted source prefix") + [ ( Api.ReportedSourceAxiom + , "test/phase7/concurrent-earlier.tex" + , 1 + ) + ] + (reportEntry + <$> Api.verificationDirectEscapes report) + other -> + assertFailure + (label <> " did not reject deterministically: " + <> show other) + assertEqual (label <> " executed only sibling obligations") + expectedPositions + (sort + [ ( Provers.workPositionModuleOrdinal position + , Provers.workPositionLocalRequestOrdinal position + ) + | position <- positions + ]) + pure measurements + runCase label jobsAmount = do + let storePath = root Posix.</> (label <> ".sqlite") + processLock = root Posix.</> (label <> ".process-lock") + processStarted = + root Posix.</> (label <> ".process-started") + writeAcceptedFixtureVampire executable + (_startup, store) <- + Store.openStore storePath (Identity.theoryId foundation) + >>= expectRight + bracket (pure store) Store.closeStore \openStore -> do + -- Seed only the final prelude. The unsupported ordinary + -- module cannot publish a root. + void + (runNoLoggingT + (Api.verifyMeasuredWithObserverAndStoreMode + openStore + Api.WarmStoreValidation + ignored + prover + "test/phase3/typed-unsupported.tex") + >>= expectRight) + writeFile executable + (unlines + [ "#!/bin/sh" + , "while ! mkdir \"" <> processLock + <> "\" 2>/dev/null; do sleep 0.01; done" + , "trap 'rmdir \"" <> processLock + <> "\"' EXIT" + , ": > \"" <> processStarted <> "\"" + , "cat >/dev/null" + , "printf '%s\\n' '% SZS status CounterSatisfiable for concurrent-fixture'" + ]) + permissions <- getPermissions executable + setPermissions executable + (setOwnerExecutable True permissions) + positionsRef <- newIORef [] + let observer = + Api.verificationRequestObserver + (\position _request -> do + atomicModifyIORef' positionsRef + (\positions -> + (position : positions, ())) + when + (jobsAmount > 1 + && Provers.workPositionModuleOrdinal + position == 1) + (waitForFileSignal + "later module process" + processStarted)) + jobs <- select jobsAmount + (result, measurements) <- + runNoLoggingT + (Api.verifyMeasuredWithObserverAndStoreModeAndJobs + openStore + Api.WarmStoreValidation + jobs + observer + prover + source) + >>= expectRight + positions <- readIORef positionsRef + pure (result, measurements, positions) + parallel <- + runCase "parallel" 2 + >>= inspect "parallel" [(1, 1), (2, 1)] + sequential <- + runCase "sequential" 1 + >>= inspect "sequential" [(1, 1)] + assertEqual "parallel module checker bound" + 2 + (Api.verificationMaximumLiveModuleCheckers parallel) + assertEqual "parallel Vampire bound" + 2 + (Api.verificationMaximumLiveVampireProcesses parallel) + assertEqual "sequential module checker reference" + 1 + (Api.verificationMaximumLiveModuleCheckers sequential) + assertEqual "sequential Vampire reference" + 1 + (Api.verificationMaximumLiveVampireProcesses sequential) + +waitForFileSignal :: String -> FilePath -> Assertion +waitForFileSignal label path = do + guarded <- Timeout.timeout 10000000 loop + case guarded of + Just () -> + pure () + Nothing -> + assertFailure (label <> " was not observed") + where + loop = do + exists <- doesFileExist path + if exists + then pure () + else do + threadDelay 10000 + loop + +batchesStructureObligationsAtomically :: Assertion +batchesStructureObligationsAtomically = do + foundation <- expectRight Foundation.checkedFoundation + Temp.withSystemTempDirectory "felix-structure-obligation-batch" \root -> do + let storePath = root Posix.</> "store.sqlite" + executable = root Posix.</> "vampire" + unavailable = root Posix.</> "must-not-run-vampire" + source = "test/phase7/structure-obligation-batch.tex" + prover path = + Provers.vampire + path + Provers.defaultTimeLimit + Provers.defaultMemoryLimit + select amount = + Provers.selectEffectiveJobs + (Provers.effectiveJobs amount) + (fail "explicit jobs unexpectedly detected processors") + run openStore jobs observer vampireCommand = + runNoLoggingT + (Api.verifyMeasuredWithObserverAndStoreModeAndJobs + openStore + Api.WarmStoreValidation + jobs + observer + vampireCommand + source) + >>= expectRight + inspectFailure label positions (result, measurements) = do + case result of + Api.VerificationFailure report failed -> do + assertEqual (label <> " selects first consequence") + (source, 12) + ( locFile (Api.failedVerificationLocation failed) + , locLine (Api.failedVerificationLocation failed) + ) + assertEqual (label <> " retains preceding prefix") + [(Api.ReportedSourceAxiom, source, 1)] + [ ( Api.reportedEscapeKind escape + , locFile (Api.reportedEscapeLocation escape) + , locLine (Api.reportedEscapeLocation escape) + ) + | escape <- Api.verificationDirectEscapes report + ] + other -> + assertFailure + (label <> " did not reject its structure batch: " + <> show other) + assertEqual (label <> " assigns consecutive positions") + [(1, 1), (1, 2)] + (sort positions) + assertEqual (label <> " observes one two-member batch") + (1, 2, 2) + ( Api.verificationObligationBatchCount measurements + , Api.verificationPreparedObligationCount measurements + , Api.verificationMaximumObligationBatchSize measurements + ) + pure measurements + writeAcceptedFixtureVampire executable + (_startup, store) <- + Store.openStore storePath (Identity.theoryId foundation) + >>= expectRight + bracket (pure store) Store.closeStore \openStore -> do + let ignored = + Api.verificationRequestObserver + (\_position _request -> pure ()) + -- Seed only the confined prelude so this fixture observes exactly + -- the ordinary structure module's ready batch. + void + (runNoLoggingT + (Api.verifyMeasuredWithObserverAndStoreMode + openStore + Api.WarmStoreValidation + ignored + (prover executable) + "test/phase3/typed-unsupported.tex") + >>= expectRight) + parallelJobs <- select 2 + parallelPositions <- newIORef [] + firstStarted <- newEmptyTMVarIO + secondStarted <- newEmptyTMVarIO + releaseFirst <- newEmptyTMVarIO + let laterCompleted = root Posix.</> "later-completed" + writeRejectingVampire executable laterCompleted + let parallelObserver = + Api.verificationRequestObserver \position _request -> do + let ordinal = + Provers.workPositionLocalRequestOrdinal position + atomicModifyIORef' parallelPositions + (\positions -> + ( ( Provers.workPositionModuleOrdinal position + , ordinal + ) : positions + , () + )) + case ordinal of + 1 -> do + atomically (putTMVar firstStarted ()) + atomically (takeTMVar releaseFirst) + 2 -> + atomically (putTMVar secondStarted ()) + _ -> + assertFailure + ("unexpected structure request ordinal: " + <> show ordinal) + withAsync + (run openStore parallelJobs parallelObserver + (prover executable)) + \verification -> do + void + (awaitSignal "first structure request" + (atomically (takeTMVar firstStarted))) + void + (awaitSignal "second structure request" + (atomically (takeTMVar secondStarted))) + -- Only the later member can reach the subprocess while + -- the first observer is gated. Its completed signal + -- therefore establishes reversed wall-clock completion. + waitForFileSignal + "later structure consequence" + laterCompleted + atomically (putTMVar releaseFirst ()) + parallelResult <- wait verification + positions <- readIORef parallelPositions + parallelMeasurements <- + inspectFailure "parallel" + positions parallelResult + assertEqual "parallel obligations overlap" + 2 + (Api.verificationMaximumLiveVampireProcesses + parallelMeasurements) + + sequentialJobs <- select 1 + sequentialPositions <- newIORef [] + let sequentialCompleted = root Posix.</> "sequential-completed" + writeRejectingVampire executable sequentialCompleted + let sequentialObserver = + Api.verificationRequestObserver \position _request -> + atomicModifyIORef' sequentialPositions + (\positions -> + ( ( Provers.workPositionModuleOrdinal position + , Provers.workPositionLocalRequestOrdinal + position + ) : positions + , () + )) + sequentialResult <- + run openStore sequentialJobs sequentialObserver + (prover executable) + sequentialObserved <- readIORef sequentialPositions + sequentialMeasurements <- + inspectFailure "sequential" + sequentialObserved sequentialResult + assertEqual "sequential batch is the semantic reference" + 1 + (Api.verificationMaximumLiveVampireProcesses + sequentialMeasurements) + + -- A rejected sibling wrote neither validation nor a module root: + -- the complete batch executes again, while the earlier source + -- axiom remains the admitted prefix. A subsequent hit executes + -- no request at all. + writeAcceptedFixtureVampire executable + acceptedPositions <- newIORef [] + let acceptedObserver = + Api.verificationRequestObserver \position _request -> + modifyIORef' acceptedPositions + (position :) + (accepted, acceptedMeasurements) <- + run openStore parallelJobs acceptedObserver + (prover executable) + case accepted of + Api.VerificationCompleted report _presentation -> + assertEqual "successful retry retains only source axiom" + [Api.ReportedSourceAxiom] + (Api.reportedEscapeKind + <$> Api.verificationDirectEscapes report) + other -> + assertFailure + ("successful structure retry failed: " <> show other) + acceptedObserved <- readIORef acceptedPositions + assertEqual "successful retry executes the complete batch" + 2 + (length acceptedObserved) + assertEqual "failed declaration published no root" + (1, 1) + ( Api.verificationModuleRootHitCount acceptedMeasurements + , Api.verificationModuleRootMissCount acceptedMeasurements + ) + let forbiddenObserver = + Api.verificationRequestObserver \position _request -> + assertFailure + ("warm structure batch invoked Vampire at " + <> show position) + (warm, warmMeasurements) <- + run openStore parallelJobs forbiddenObserver + (prover unavailable) + case warm of + Api.VerificationCompleted{} -> pure () + other -> + assertFailure + ("warm structure batch did not install: " <> show other) + assertEqual "warm module hit executes no batch" + (2, 0, 0) + ( Api.verificationModuleRootHitCount warmMeasurements + , Api.verificationModuleRootMissCount warmMeasurements + , Api.verificationVampireRunCount warmMeasurements + ) + where + awaitSignal label action = do + result <- Timeout.timeout 10000000 action + maybe + (assertFailure (label <> " was not observed") + >> fail "unreachable") + pure + result + + writeRejectingVampire executable completed = do + writeFile executable + (unlines + [ "#!/bin/sh" + , "cat >/dev/null" + , ": > \"" <> completed <> "\"" + , "printf '%s\\n' '% SZS status CounterSatisfiable for structure-batch-fixture'" + ]) + permissions <- getPermissions executable + setPermissions executable + (setOwnerExecutable True permissions) + +keepsDependentProofObligationsSequential :: Assertion +keepsDependentProofObligationsSequential = + Temp.withSystemTempDirectory "felix-dependent-proof-chain" \root -> do + repository <- getCurrentDirectory + foundation <- expectRight Foundation.checkedFoundation + bootstrap <- + expectRight + =<< Module.buildBootstrapPreludeFixture + foundation + unusedResolver + mounts <- exactFixtureMounts repository + workspace <- parseExactWorkspace + bootstrap mounts "test/phase7/dependent-proof-chain.tex" + let executable = root Posix.</> "vampire" + writeAcceptedFixtureVampire executable + firstSubmitted <- newEmptyTMVarIO + secondSubmitted <- newEmptyTMVarIO + releaseFirst <- newEmptyTMVarIO + calls <- newIORef (0 :: Int) + let resolver = + Declaration.vampireBatchResolver \tasks -> do + assertEqual "dependent proof resolver batch is singleton" + 1 + (NonEmpty.length tasks) + ordinal <- atomicModifyIORef' calls + (\current -> (current + 1, current + 1)) + case ordinal of + 1 -> do + atomically (putTMVar firstSubmitted ()) + atomically (takeTMVar releaseFirst) + 2 -> + atomically (putTMVar secondSubmitted ()) + _ -> + assertFailure + ("unexpected dependent proof request: " + <> show ordinal) + traverse + (\prepared -> + runNoLoggingT + (Provers.runPreparedTypedProver + (Provers.vampire + executable + Provers.defaultTimeLimit + Provers.defaultMemoryLimit) + prepared)) + tasks + withAsync + (compileParsedWorkspaceWithResolver + foundation bootstrap resolver workspace) + \checking -> do + void + (awaitSignal "local subclaim request" + (atomically (takeTMVar firstSubmitted))) + atomically (tryReadTMVar secondSubmitted) >>= \case + Nothing -> pure () + Just () -> + assertFailure + "proof continuation was submitted before its local claim" + atomically (putTMVar releaseFirst ()) + void + (awaitSignal "dependent continuation request" + (atomically (takeTMVar secondSubmitted))) + sealed <- wait checking + assertEqual "dependent proof module sealed" 1 (length sealed) + readIORef calls + >>= assertEqual "dependent proof executed two ordered requests" 2 + where + awaitSignal label action = do + result <- Timeout.timeout 10000000 action + maybe + (assertFailure (label <> " was not observed") + >> fail "unreachable") + pure + result + +schedulesDiamondAfterSealedImports :: Assertion +schedulesDiamondAfterSealedImports = do + foundation <- expectRight Foundation.checkedFoundation + Temp.withSystemTempDirectory "felix-concurrent-diamond" \root -> do + let storePath = root Posix.</> "store.sqlite" + executable = root Posix.</> "vampire" + unavailable = root Posix.</> "must-not-run-vampire" + source = "test/phase7/diamond-root.tex" + prover path = + Provers.vampire + path + Provers.defaultTimeLimit + Provers.defaultMemoryLimit + ignored = + Api.verificationRequestObserver + (\_position _request -> pure ()) + writeAcceptedFixtureVampire executable + (_startup, store) <- + Store.openStore storePath (Identity.theoryId foundation) + >>= expectRight + bracket (pure store) Store.closeStore \openStore -> do + -- Acquire the final prelude before introducing scheduler gates. + void + (runNoLoggingT + (Api.verifyMeasuredWithObserverAndStoreMode + openStore + Api.WarmStoreValidation + ignored + (prover executable) + "test/phase3/typed-unsupported.tex") + >>= expectRight) + jobs <- Provers.selectEffectiveJobs + (Provers.effectiveJobs 2) + (fail "explicit jobs unexpectedly detected processors") + baseStarted <- newEmptyTMVarIO + branchStarted <- newTQueueIO + rootStarted <- newEmptyTMVarIO + releaseBase <- newTVarIO False + releaseBranches <- newTVarIO False + let awaitRelease released = + atomically (readTVar released >>= check) + observer = + Api.verificationRequestObserver + (\position _request -> + case Provers.workPositionModuleOrdinal position of + 1 -> do + atomically (putTMVar baseStarted ()) + awaitRelease releaseBase + ordinal@2 -> do + atomically + (writeTQueue branchStarted ordinal) + awaitRelease releaseBranches + ordinal@3 -> do + atomically + (writeTQueue branchStarted ordinal) + awaitRelease releaseBranches + 4 -> + atomically (putTMVar rootStarted ()) + _ -> + pure ()) + verify vampireCommand requestObserver = + runNoLoggingT + (Api.verifyMeasuredWithObserverAndStoreModeAndJobs + openStore + Api.WarmStoreValidation + jobs + requestObserver + vampireCommand + source) + >>= expectRight + await label action = do + result <- Timeout.timeout 10000000 action + maybe + (assertFailure (label <> " was not observed") + >> fail "unreachable") + pure + result + withAsync (verify (prover executable) observer) \verification -> do + void (await "base request" (atomically (takeTMVar baseStarted))) + threadDelay 50000 + atomically (tryReadTQueue branchStarted) >>= \case + Nothing -> pure () + Just ordinal -> + assertFailure + ("dependent module started before base seal: " + <> show ordinal) + atomically (writeTVar releaseBase True) + firstBranch <- await "first branch" + (atomically (readTQueue branchStarted)) + secondBranch <- await "second branch" + (atomically (readTQueue branchStarted)) + assertEqual "both diamond branches became ready together" + [2, 3] + (sort [firstBranch, secondBranch]) + atomically (tryReadTMVar rootStarted) >>= \case + Nothing -> pure () + Just () -> + assertFailure + "diamond root started before both branch seals" + atomically (writeTVar releaseBranches True) + void (await "diamond root" (atomically (takeTMVar rootStarted))) + (coldResult, coldMeasurements) <- wait verification + case coldResult of + Api.VerificationCompleted{} -> pure () + other -> + assertFailure + ("cold diamond did not complete: " <> show other) + assertEqual "cold diamond module misses plus prelude hit" + (1, 4) + ( Api.verificationModuleRootHitCount coldMeasurements + , Api.verificationModuleRootMissCount coldMeasurements + ) + let forbiddenObserver = + Api.verificationRequestObserver + (\position _request -> + assertFailure + ("warm diamond invoked Vampire at " + <> show position)) + (warmResult, warmMeasurements) <- + verify (prover unavailable) forbiddenObserver + case warmResult of + Api.VerificationCompleted{} -> pure () + other -> + assertFailure + ("warm diamond did not install: " <> show other) + assertEqual "warm diamond installs each distinct root" + (5, 0) + ( Api.verificationModuleRootHitCount warmMeasurements + , Api.verificationModuleRootMissCount warmMeasurements + ) + assertEqual "warm diamond runs no prover" + 0 + (Api.verificationVampireRunCount warmMeasurements) + +reportsAdmittedSourceEscapes :: Assertion +reportsAdmittedSourceEscapes = do + foundation <- expectRight Foundation.checkedFoundation + Temp.withSystemTempDirectory "felix-admitted-source-report" \root -> do + let storePath = root Posix.</> "store.sqlite" + executable = root Posix.</> "vampire" + unavailable = root Posix.</> "must-not-run-vampire" + observer = + Api.verificationRequestObserver \_ordinal _request -> pure () + prover path = + Provers.vampire + path + Provers.defaultTimeLimit + Provers.defaultMemoryLimit + writeAcceptedFixtureVampire executable + (_startup, store) <- + Store.openStore storePath (Identity.theoryId foundation) + >>= expectRight + bracket (pure store) Store.closeStore \openStore -> do + let verify mode vampirePath source = + runNoLoggingT + (Api.verifyMeasuredWithObserverAndStoreMode + openStore + mode + observer + (prover vampirePath) + source) + >>= expectRight + reportEntries = + fmap + (\escape -> + ( Api.reportedEscapeKind escape + , locFile (Api.reportedEscapeLocation escape) + , locLine (Api.reportedEscapeLocation escape) + )) + . Api.verificationDirectEscapes + expectedConsumer = + [ ( Api.ReportedSourceAxiom + , "test/phase5/exact-escape-producer.tex" + , 1 + ) + , ( Api.ReportedOmitted + , "test/phase5/exact-escape-producer.tex" + , 9 + ) + , ( Api.ReportedOmitted + , "test/phase5/exact-escape-consumer.tex" + , 35 + ) + ] + (freshResult, freshMeasurements) <- + verify + Api.FreshStoreValidation + executable + "test/phase5/exact-escape-consumer.tex" + freshReport <- case freshResult of + Api.CompletedWithExplicitGaps report _presentation -> pure report + other -> + assertFailure + ("fresh escape report did not complete with gaps: " + <> show other) + >> fail "unreachable" + assertEqual "fresh direct escapes" + expectedConsumer + (reportEntries freshReport) + assertEqual "cold acquisition includes prelude and two modules" + (0, 3) + ( Api.verificationModuleRootHitCount freshMeasurements + , Api.verificationModuleRootMissCount freshMeasurements + ) + + (warmResult, warmMeasurements) <- + verify + Api.WarmStoreValidation + unavailable + "test/phase5/exact-escape-consumer.tex" + warmReport <- case warmResult of + Api.CompletedWithExplicitGaps report _presentation -> pure report + other -> + assertFailure + ("warm escape report did not complete with gaps: " + <> show other) + >> fail "unreachable" + assertEqual "warm report uses rebound current locations" + freshReport warmReport + assertEqual "warm acquisition includes prelude and two modules" + (3, 0) + ( Api.verificationModuleRootHitCount warmMeasurements + , Api.verificationModuleRootMissCount warmMeasurements + ) + assertEqual "warm root hit invokes no Vampire process" + 0 + (Api.verificationVampireRunCount warmMeasurements) + + void + (verify + Api.FreshStoreValidation + executable + "test/phase5/exact-source-axiom.tex") + (failedResult, failedMeasurements) <- + verify + Api.WarmStoreValidation + unavailable + "test/phase6/admitted-prefix-failure.tex" + failedReport <- case failedResult of + Api.VerificationCheckingFailure report _failure -> pure report + other -> + assertFailure + ("typed suffix failure was not report-bearing: " + <> show other) + >> fail "unreachable" + assertEqual "failure report retains only admitted source prefix" + (take 2 expectedConsumer + <> [ ( Api.ReportedOmitted + , "test/phase6/admitted-prefix-failure.tex" + , 7 + ) + ]) + (reportEntries failedReport) + assertEqual "failed root is not counted as acquired" + (2, 0) + ( Api.verificationModuleRootHitCount failedMeasurements + , Api.verificationModuleRootMissCount failedMeasurements + ) + assertEqual "cached prefix failure invokes no Vampire process" + 0 + (Api.verificationVampireRunCount failedMeasurements) + +classifiesTypedVampireFailures :: Assertion +classifiesTypedVampireFailures = do + foundation <- expectRight Foundation.checkedFoundation + Temp.withSystemTempDirectory "felix-typed-failure-classification" \root -> do + let storePath = root Posix.</> "store.sqlite" + executable = root Posix.</> "vampire" + observer = + Api.verificationRequestObserver \_ordinal _request -> pure () + prover = + Provers.vampire + executable + Provers.defaultTimeLimit + Provers.defaultMemoryLimit + writeAcceptedFixtureVampire executable + (_startup, store) <- + Store.openStore storePath (Identity.theoryId foundation) + >>= expectRight + bracket (pure store) Store.closeStore \openStore -> do + let verify source = + runNoLoggingT + (Api.verifyMeasuredWithObserverAndStoreMode + openStore + Api.WarmStoreValidation + observer + prover + source) + >>= expectRight + writeProtocol lines = do + writeFile executable + (unlines (["#!/bin/sh", "cat >/dev/null"] <> lines)) + permissions <- getPermissions executable + setPermissions executable + (setOwnerExecutable True permissions) + expectTypedFailure classify = do + (result, _measurements) <- + verify "test/phase5/exact-runtime-failure.tex" + case result of + Api.VerificationFailure report failed -> do + assertEqual "typed failure has no direct escapes" + [] + (Api.verificationDirectEscapes report) + assertEqual "typed failure retains source location" + "test/phase5/exact-runtime-failure.tex" + (locFile + (Api.failedVerificationLocation failed)) + classify + (Api.failedVerificationReason failed) + (CommandLine.verificationCommandOutcome result) + other -> + assertFailure + ("typed prover outcome was misclassified: " + <> show other) + + -- Populate only the confined prelude. The selected ordinary + -- module then remains a miss for each classified live failure. + (_preludeResult, _preludeMeasurements) <- + verify "test/phase3/typed-unsupported.tex" + + writeProtocol + [ "printf '%s\\n' '% SZS status CounterSatisfiable for typed-failure'" + , "exit 0" + ] + expectTypedFailure \reason outcome -> do + case reason of + Api.CountermodelFailure{} -> pure () + other -> assertFailure ("expected countermodel: " <> show other) + case outcome of + CommandLine.VerificationRejected{} -> pure () + other -> assertFailure ("expected rejection: " <> show other) + + writeProtocol + [ "printf '%s\\n' '% SZS status Timeout for typed-failure'" + , "exit 0" + ] + expectTypedFailure \reason outcome -> do + case reason of + Api.IndeterminateFailure{} -> pure () + other -> assertFailure ("expected indeterminate result: " <> show other) + case outcome of + CommandLine.ProverFailed + _report _location CommandLine.ProverIndeterminate{} -> + pure () + other -> assertFailure ("expected prover failure: " <> show other) + + writeProtocol + [ "printf '%s\\n' '% SZS status Theorem for typed-failure'" + , "exit 7" + ] + expectTypedFailure \reason outcome -> do + case reason of + Api.ProtocolFailure{} -> pure () + other -> assertFailure ("expected protocol failure: " <> show other) + case outcome of + CommandLine.ProverFailed + _report _location CommandLine.ProverProtocolFailure{} -> + pure () + other -> assertFailure ("expected prover failure: " <> show other) + + writeFile executable "not executable" + permissions <- getPermissions executable + setPermissions executable + (setOwnerExecutable False permissions) + expectTypedFailure \reason outcome -> do + case reason of + Api.TransportFailure{} -> pure () + other -> assertFailure ("expected transport failure: " <> show other) + case outcome of + CommandLine.ProverFailed + _report _location CommandLine.ProverTransportFailure{} -> + pure () + other -> assertFailure ("expected prover failure: " <> show other) + retainsExactPrefixBeforeFailure :: Assertion retainsExactPrefixBeforeFailure = do result <- @@ -4675,13 +5763,16 @@ retainsExactPrefixBeforeFailure = do prover "test/phase5/exact-failure.tex") case result of - Left - (Api.VerificationTypedModuleError + Right + ( Api.VerificationCheckingFailure _report + (Api.VerificationTypedModuleError source (Module.TypedActionFailed (Module.TypedExactCompileFailed (Exact.ExactUnsupportedDeclarationBody location))) - prefix) -> do + prefix) + , _measurements + ) -> do assertEqual "failed exact source" "test/phase5/exact-failure.tex" (safeRelativePathFilePath @@ -4702,14 +5793,17 @@ retainsExactPrefixBeforeFailure = do prover "test/phase5/exact-proof-failure.tex") case proofFailure of - Left - (Api.VerificationTypedModuleError + Right + ( Api.VerificationCheckingFailure _report + (Api.VerificationTypedModuleError _source (Module.TypedActionFailed (Module.TypedExactProofFailed (ExactProof.ExactProofGoalStatementMismatch location))) - prefix) -> do + prefix) + , _measurements + ) -> do assertEqual "mismatched assumption line" 10 (locLine location) assertEqual "failed proof publishes no theorem" 1 @@ -4727,12 +5821,15 @@ retainsExactPrefixBeforeFailure = do prover "test/phase5/unmatched-proof.tex") case unmatched of - Left - (Api.VerificationTypedModuleError + Right + ( Api.VerificationCheckingFailure _report + (Api.VerificationTypedModuleError _source (Module.TypedActionFailed (Module.TypedUnmatchedProof location)) - prefix) -> do + prefix) + , _measurements + ) -> do assertEqual "unmatched proof line" 1 (locLine location) assertEqual "unmatched proof publishes no declaration" 0 @@ -4821,14 +5918,17 @@ rejectsNestedExactSetInduction = do prover "test/phase5/exact-induction-nested.tex") case result of - Left - (Api.VerificationTypedModuleError + Right + ( Api.VerificationCheckingFailure _report + (Api.VerificationTypedModuleError _source (Module.TypedActionFailed (Module.TypedExactProofFailed (ExactProof.ExactProofSetInductionNotOutermost location))) - prefix) -> do + prefix) + , _measurements + ) -> do assertEqual "nested induction line" 7 (locLine location) assertBool "failed proof publishes no theorem" (null (Declaration.pendingModulePrefixBatches prefix)) @@ -4854,35 +5954,14 @@ routesProductionVerification = setPermissions executable (setOwnerExecutable True permissions) producer <- verifyFixture executable "test/phase3/typed-producer.tex" - assertRoute "selected producer" - Api.TypedVerificationRoute - producer - setRoot <- verifyFixture executable "set.tex" - assertRoute "protected set root" - Api.TypedVerificationRoute - setRoot - natRoot <- verifyFixture executable "nat.tex" - assertRoute "protected naturals root" - Api.TypedVerificationRoute - natRoot - forM_ - [ ("bipartition", "set/bipartition.tex") - , ("function", "function.tex") - , ("Cantor", "set/cantor.tex") - ] - \(label, path) -> - assertRoute ("typed " <> label) - Api.TypedVerificationRoute - =<< verifyFixture executable path + assertTypedSuccess "exact producer" producer selectedRuns <- runCount counter - assertBool "selected roots constructed the final prelude" + assertBool "ordinary roots construct the final prelude" (selectedRuns > 0) - importer <- verifyFixture executable "test/phase3/legacy-importer.tex" - assertRoute "unselected importer" - Api.LegacyVerificationRoute - importer - assertEqual "legacy root did not construct the final prelude" - selectedRuns + importer <- verifyFixture executable "test/phase3/typed-importer.tex" + assertTypedSuccess "ordinary importer" importer + assertBool "every root constructs the final prelude" + . (> selectedRuns) =<< runCount counter where verifyFixture executable path = @@ -4899,16 +5978,6 @@ routesProductionVerification = runCount path = length . StrictText.lines . StrictText.pack <$> readFile path - assertRoute label expected = \case - Api.VerifiedWithTrustedVampire report -> - assertEqual label expected (Api.verificationRoute report) - Api.CompletedWithExplicitGaps report -> - assertFailure - (label <> " completed with gaps via " - <> show (Api.verificationRoute report)) - Api.VerificationFailure failure -> - assertFailure (label <> " failed: " <> show failure) - installsNonemptyImplicitPreludeEvidence :: Assertion installsNonemptyImplicitPreludeEvidence = do foundation <- expectRight Foundation.checkedFoundation @@ -5330,13 +6399,13 @@ parseExactWorkspace bootstrap mounts relative = relative parseFinalExactWorkspace - :: Module.MigrationPreludeSession + :: Module.FinalPreludeSession -> SourceMounts -> FilePath -> IO Parse.ParsedSourceWorkspace parseFinalExactWorkspace prelude mounts relative = parseExactWorkspaceWithPrelude - (Module.migrationPreludeModule prelude) + (Module.finalPreludeModule prelude) mounts relative @@ -5401,7 +6470,7 @@ compileParsedWorkspaceWithValidation compileFinalParsedWorkspaceWithResolver :: Foundation.CheckedFoundation - -> Module.MigrationPreludeSession + -> Module.FinalPreludeSession -> Declaration.VampireResolver -> Parse.ParsedSourceWorkspace -> IO [Module.SealedTypedModule] @@ -5468,14 +6537,13 @@ compileParsedWorkspaceWithReadiness assertTypedSuccess :: String -> Api.VerificationResult -> Assertion assertTypedSuccess label = \case - Api.VerifiedWithTrustedVampire report -> - assertEqual label Api.TypedVerificationRoute - (Api.verificationRoute report) - Api.CompletedWithExplicitGaps report -> - assertFailure - (label <> " completed with gaps via " - <> show (Api.verificationRoute report)) - Api.VerificationFailure failure -> + Api.VerificationCompleted _report _presentation -> + pure () + Api.CompletedWithExplicitGaps _report _presentation -> + assertFailure (label <> " completed with gaps") + Api.VerificationFailure _report failure -> + assertFailure (label <> " failed: " <> show failure) + Api.VerificationCheckingFailure _report failure -> assertFailure (label <> " failed: " <> show failure) sole :: String -> [value] -> IO value @@ -5494,3 +6562,16 @@ expectRight = \case expectRightIO :: Show error => IO (Either error value) -> IO value expectRightIO action = action >>= expectRight + +acquireFinalPreludeSession + :: Store.Store + -> Foundation.CheckedFoundation + -> Declaration.VampireResolver + -> IO + (Either + Module.FinalPreludeReadinessError + Module.FinalPreludeSession) +acquireFinalPreludeSession store foundation resolver = do + memo <- Store.newStoreMemo store + Module.acquireFinalPreludeSession + memo store foundation resolver |