{-# LANGUAGE NoImplicitPrelude #-} module Felix.Test.Unit.Store (unitTests) where import Base import Felix.Checking.Authority qualified as Authority import Felix.Checking.Core qualified as Core import Felix.Checking.Declaration qualified as Declaration import Felix.Checking.Foundation qualified as Foundation import Felix.Checking.Identity qualified as Identity import Felix.Checking.Module qualified as Typed import Felix.Checking.Semantic qualified as Semantic import Felix.Cache.Codec qualified as Cache import Felix.Math.Codec import Felix.Module import Felix.Parsed.Identity qualified as Parsed import Felix.Parsed.Payload qualified as ParsedPayload import Felix.Source.Content qualified as Content import Felix.Source import Felix.Store qualified as Store import Felix.Provers qualified as Provers import Felix.Syntax.Interface qualified as Syntax import Control.Concurrent (threadDelay) import Control.Exception qualified as Exception import Data.ByteString qualified as ByteString import Data.ByteString.Char8 qualified as ByteString.Char8 import Data.IORef qualified as IORef import Database.SQLite.Simple qualified as SQLite import Database.SQLite.Simple.Types (Only(..)) import System.Directory qualified as Directory import System.Environment qualified as Environment import System.FilePath.Posix qualified as Posix import System.IO.Temp qualified as Temp import Test.Tasty import Test.Tasty.HUnit import UnliftIO.Async (concurrently) unitTests :: TestTree unitTests = testGroup "SQLite store" [ testCase "initializes and reopens the current schema" initializesAndReopensCurrentSchema , testCase "serializes invocation-local coordinator access" serializesCoordinatorAccess , testCase "rejects incompatibility without configuring the store" rejectsIncompatibilityWithoutConfiguration , testCase "rejects malformed compatibility metadata" rejectsMalformedCompatibilityMetadata , testCase "rejects a compatible incomplete schema" rejectsCompatibleIncompleteSchema , testCase "round-trips exact parsed artifacts" roundTripsExactParsedArtifacts , testCase "rejects malformed parsed payloads" rejectsMalformedParsedPayloads , testCase "rejects disagreeing parsed artifact identities" rejectsDisagreeingParsedArtifactIdentities , testCase "rejects malformed typed validation rows" rejectsMalformedTypedValidationRows , testCase "publishes a completed prefix before readiness" publishesCompletedPrefixBeforeReadiness , testCase "installs a sealed producer for a cached importer" installsSealedProducerForCachedImporter , testCase "validates exact cached installation inputs" validatesExactCachedInstallationInputs , testCase "rejects invalid cached root authority and closure" rejectsInvalidCachedRootAuthorityAndClosure , testCase "rejects disagreeing module artifact columns" rejectsDisagreeingModuleArtifactColumns , testCase "validates shared closures once per invocation" validatesSharedClosuresOncePerInvocation , testCase "rolls back a failed readiness transaction" rollsBackFailedReadiness , testCase "rolls back an unequal duplicate batch" rollsBackUnequalDuplicateBatch , testCase "rejects malformed canonical payloads" rejectsMalformedCanonicalPayloads , testCase "plans default and explicit persistent stores" plansPersistentStores , testCase "cleans fresh stores on return and exceptions" cleansFreshStores , testCase "does not fall back after fatal startup" doesNotFallBackAfterFatalStartup ] serializesCoordinatorAccess :: Assertion serializesCoordinatorAccess = do coordinator <- Store.newStoreCoordinator active <- IORef.newIORef (0 :: Int) maximumActive <- IORef.newIORef (0 :: Int) let operation = Store.withStoreCoordinator coordinator (Exception.bracket_ (IORef.atomicModifyIORef' active (\current -> let next = current + 1 in (next, ()))) (IORef.atomicModifyIORef' active (\current -> (current - 1, ()))) (do current <- IORef.readIORef active IORef.atomicModifyIORef' maximumActive (\observed -> (max current observed, ())) threadDelay 50000)) void (concurrently operation operation) IORef.readIORef maximumActive >>= assertEqual "maximum owner count" 1 roundTripsExactParsedArtifacts :: Assertion roundTripsExactParsedArtifacts = withStoreFixture "felix-store-parsed" \path theory _fixture -> do (_startup, store) <- expectOpen path theory (key, artifact, unequal) <- makeParsedArtifacts assertEqual "initial exact lookup misses" (Right Nothing) =<< Store.loadParsedArtifact store key assertEqual "published parsed artifact" (Right artifact) =<< Store.writeParsedArtifact store key artifact assertEqual "exact parsed round trip" (Right (Just artifact)) =<< Store.loadParsedArtifact store key assertEqual "equal publication is idempotent" (Right artifact) =<< Store.writeParsedArtifact store key artifact Store.writeParsedArtifact store key unequal >>= \case Left Store.StoreRowPayloadMismatch{} -> pure () other -> assertFailure ("unexpected unequal parsed publication: " <> show other) Store.closeStore store rejectsMalformedParsedPayloads :: Assertion rejectsMalformedParsedPayloads = do check "malformed" (ByteString.singleton 0xff) check "noncanonical" . (<> ByteString.singleton 0x00) =<< parsedPayloadBytes where check label corrupted = withStoreFixture ("felix-store-parsed-" <> label) \path theory _fixture -> do (_startup, store) <- expectOpen path theory (key, artifact, _unequal) <- makeParsedArtifacts _ <- expectRightIO (Store.writeParsedArtifact store key artifact) Store.closeStore store updateParsedPayload path key corrupted (_reopened, current) <- expectOpen path theory Store.loadParsedArtifact current key >>= \case Left Store.StoreRowDecodeFailure{} -> pure () other -> assertFailure ("unexpected " <> label <> " parsed row result: " <> show other) Store.closeStore current parsedPayloadBytes = do (_key, artifact, _unequal) <- makeParsedArtifacts pure (ParsedPayload.canonicalParsedPayloadBytes (ParsedPayload.parsedArtifactPayload artifact)) rejectsDisagreeingParsedArtifactIdentities :: Assertion rejectsDisagreeingParsedArtifactIdentities = withStoreFixture "felix-store-parsed-id" \path theory _fixture -> do (_startup, store) <- expectOpen path theory (key, artifact, _unequal) <- makeParsedArtifacts _ <- expectRightIO (Store.writeParsedArtifact store key artifact) Store.closeStore store connection <- SQLite.open path SQLite.execute connection "UPDATE parsed_artifacts SET parsed_module_id = ? \ \WHERE parsed_module_key = ?" ( ByteString.replicate 32 0 , Cache.cacheDigestBytes (Parsed.parsedModuleKeyDigest key) ) SQLite.close connection (_reopened, current) <- expectOpen path theory Store.loadParsedArtifact current key >>= \case Left Store.StoreParsedArtifactIdMismatch -> pure () other -> assertFailure ("unexpected parsed identity result: " <> show other) Store.closeStore current makeParsedArtifacts :: IO ( Parsed.ParsedModuleKey , ParsedPayload.ParsedArtifact , ParsedPayload.ParsedArtifact ) makeParsedArtifacts = do key <- expectRight (Parsed.parsedModuleKey (Content.sourceContentIdBytes "parsed-source") Syntax.baseSyntaxInterfaceId []) emptyDelta <- expectRight (Syntax.canonicalSyntaxDelta []) emptySyntax <- expectRight (Syntax.moduleSyntaxInterface [] emptyDelta) otherDelta <- expectRight (Syntax.canonicalSyntaxDelta [Syntax.CanonicalStructureOperation "other"]) otherSyntax <- expectRight (Syntax.moduleSyntaxInterface [] otherDelta) let payload syntax = ParsedPayload.canonicalParsedPayload [] [] [] (Syntax.moduleSyntaxAssertedId syntax) pure ( key , ParsedPayload.parsedArtifact key (payload emptySyntax) , ParsedPayload.parsedArtifact key (payload otherSyntax) ) updateParsedPayload :: FilePath -> Parsed.ParsedModuleKey -> ByteString.ByteString -> IO () updateParsedPayload path key payload = do connection <- SQLite.open path SQLite.execute connection "UPDATE parsed_artifacts SET payload = ? \ \WHERE parsed_module_key = ?" ( payload , Cache.cacheDigestBytes (Parsed.parsedModuleKeyDigest key) ) SQLite.close connection rejectsMalformedTypedValidationRows :: Assertion rejectsMalformedTypedValidationRows = withStoreFixture "felix-store-malformed-typed" \path theory fixture -> do (_startup, store) <- expectOpen path theory (_owner, prefix, _syntax, _semantic, _key, _artifact, _proposition) <- makeCommittedModule theory fixture batch <- case Declaration.pendingModulePrefixBatches prefix of [one] -> pure one batches -> assertFailure ("unexpected prefix batch count: " <> show (length batches)) >> fail "unreachable" proof <- case Declaration.committedBatchProofValidations batch of [one] -> pure one proofs -> assertFailure ("unexpected proof validation count: " <> show (length proofs)) >> fail "unreachable" let key = Semantic.proofValidationRecordKey proof certificate = Semantic.proofValidationRecordCertificate proof theorem = Identity.theoremId (Authority.factAuthorityTheorem (Authority.validationTarget certificate)) wrongKey = Semantic.proofValidationKey theorem (Semantic.proofSyntaxId "other-row") (Declaration.committedBatchPreviousPrefix batch) wrongProof = Semantic.proofValidationRecord wrongKey certificate expectRightIO (Store.writePendingModulePrefix store prefix) Store.closeStore store connection <- SQLite.open path SQLite.execute connection "UPDATE proof_validations SET payload = ? \ \WHERE validation_key = ?" ( Cache.encodeCache (Semantic.putProofValidationRecordCache wrongProof) , Cache.cacheDigestBytes (Semantic.proofValidationKeyDigest key) ) SQLite.close connection (_reopened, current) <- expectOpen path theory Store.loadProofValidation current key >>= \case Left Store.StoreValidationRecordKeyMismatch{} -> pure () Left other -> assertFailure ("unexpected typed key mismatch: " <> show other) Right _ -> assertFailure "typed key mismatch was accepted" Store.closeStore current connection' <- SQLite.open path SQLite.execute connection' "UPDATE proof_validations SET payload = ? \ \WHERE validation_key = ?" ( ByteString.singleton 0xff , Cache.cacheDigestBytes (Semantic.proofValidationKeyDigest key) ) SQLite.close connection' (_reopenedMalformed, malformed) <- expectOpen path theory Store.loadProofValidation malformed key >>= \case Left Store.StoreRowDecodeFailure{} -> pure () Left other -> assertFailure ("unexpected malformed typed row: " <> show other) Right _ -> assertFailure "malformed typed row was accepted" Store.closeStore malformed publishesCompletedPrefixBeforeReadiness :: Assertion publishesCompletedPrefixBeforeReadiness = withStoreFixture "felix-store-prefix" \path theory fixture -> do (_startup, store) <- expectOpen path theory (_owner, prefix, syntax, semantic, artifactKey, artifact, proposition) <- makeCommittedModule theory fixture expectRightIO (Store.writePendingModulePrefix store prefix) connection <- SQLite.open path [Only propositionRows] <- SQLite.query connection "SELECT COUNT(*) FROM canonical_propositions \ \WHERE proposition_id = ?" (Only (Cache.encodeCache (Identity.putPropositionIdCache (Identity.checkedPropositionId proposition)))) :: IO [Only Int] [Only artifactRowsBefore] <- SQLite.query_ connection "SELECT COUNT(*) FROM module_artifacts" :: IO [Only Int] SQLite.close connection assertEqual "completed prefix proposition is visible" 1 propositionRows assertEqual "prefix publication does not publish readiness" 0 artifactRowsBefore expectRightIO (Store.writeSealedModule store prefix [syntax] [semantic] artifact) memo <- Store.newStoreMemo store installation <- expectRightIO (Store.loadCachedModuleInstallation memo store artifactKey (Syntax.moduleSyntaxAssertedId syntax)) case installation of Just loaded -> do assertEqual "validated semantic interface" semantic (Store.cachedInstallationSemantic loaded) assertEqual "validated imported proposition count" 1 (length (Store.cachedInstallationPropositions loaded)) Nothing -> assertFailure "validated module installation was absent" Store.closeStore store installsSealedProducerForCachedImporter :: Assertion installsSealedProducerForCachedImporter = withStoreFixture "felix-store-cached-import" \path theory fixture -> do (_startup, store) <- expectOpen path theory foundation <- expectRight Foundation.checkedFoundation (_owner, prefix, syntax, semantic, artifactKey, artifact, proposition) <- makeCommittedModule theory fixture expectRightIO (Store.writeSealedModule store prefix [syntax] [semantic] artifact) memo <- Store.newStoreMemo store installation <- expectRightIO (Store.loadCachedModuleInstallation memo store artifactKey (Syntax.moduleSyntaxAssertedId syntax)) >>= \case Nothing -> assertFailure "sealed producer was not loadable" >> fail "unreachable" Just loaded -> pure loaded cached <- expectRight (Typed.cachedSealedTypedModule foundation [] installation) let loadedSemantic = Store.cachedInstallationSemantic installation fingerprint <- case concatMap Semantic.declarationDeltaFacts (Semantic.semanticInterfaceDeclarations loadedSemantic) of [occurrence] -> pure (Semantic.semanticFactFingerprint occurrence) occurrences -> assertFailure ("unexpected cached producer facts: " <> show (length occurrences)) >> fail "unreachable" namespaceDigest <- expectRight (hashCanonicalFields "store-cached-import-consumer" ["consumer"]) relative <- expectRight (safeRelativePath "consumer.tex") let consumerOwner = moduleNameFromParts (sourceNamespaceIdFromDigest namespaceDigest) relative resolver = Declaration.vampireResolver \_ -> pure (Left (Provers.ProverLaunchFailed "unused" "cached importer does not run Vampire")) result <- (Declaration.runModuleDriver foundation consumerOwner [Semantic.semanticInterfaceAssertedId loadedSemantic] resolver Declaration.FreshValidation do Declaration.importSealedModuleDriver (Typed.sealedTypedModuleEvidence cached) (_value, batch) <- Declaration.commitProofDeclaration (Semantic.proofSyntaxId "cached-import-consumer") do candidate <- Declaration.reserveCandidate (Declaration.candidateSpec proposition Semantic.SearchIneligible []) Declaration.authorizeOmittedCandidate candidate do _ <- Declaration.useAuthorizedFact fingerprint Declaration.recordOmittedUse pure batch :: IO (Either Declaration.DriverOpenError (Declaration.DriverResult Text Declaration.CommittedDeclarationBatch))) case result of Left failure -> assertFailure ("cached importer could not open: " <> show failure) Right (Declaration.DriverSucceeded _ _ _ _closure) -> pure () Right (Declaration.DriverFailed failure _prefix) -> assertFailure ("cached importer failed: " <> show failure) Right (Declaration.DriverSealFailed failure _prefix) -> assertFailure ("cached importer did not seal: " <> show failure) Store.closeStore store validatesExactCachedInstallationInputs :: Assertion validatesExactCachedInstallationInputs = withStoreFixture "felix-store-exact-install" \path theory fixture -> do (_startup, store) <- expectOpen path theory (owner, prefix, syntax, semantic, artifactKey, artifact, proposition) <- makeCommittedModule theory fixture _ <- expectRightIO (Store.writeSealedModule store prefix [syntax] [semantic] artifact) otherDelta <- expectRight (Syntax.canonicalSyntaxDelta [Syntax.CanonicalStructureOperation "other-syntax"]) otherSyntax <- expectRight (Syntax.moduleSyntaxInterface [] otherDelta) wrongSyntaxMemo <- Store.newStoreMemo store Store.loadCachedModuleInstallation wrongSyntaxMemo store artifactKey (Syntax.moduleSyntaxAssertedId otherSyntax) >>= \case Left Store.StoreModuleArtifactSyntaxMismatch{} -> pure () _ -> assertFailure "unexpected syntax-input result" parent <- expectRight (Semantic.semanticInterface preludeModuleName [] []) mismatched <- expectRight (Semantic.semanticInterface owner [Semantic.semanticInterfaceAssertedId parent] (Semantic.semanticInterfaceDeclarations semantic)) mismatchKey <- makeArtifactKey owner theory "direct-mismatch" let mismatchArtifact = Semantic.moduleArtifactResult mismatchKey (Syntax.moduleSyntaxAssertedId syntax) (Semantic.semanticInterfaceAssertedId mismatched) writeRawModuleRows path [fixtureFirstObject fixture] [proposition] syntax [parent, mismatched] mismatchArtifact directMemo <- Store.newStoreMemo store Store.loadCachedModuleInstallation directMemo store mismatchKey (Syntax.moduleSyntaxAssertedId syntax) >>= \case Left Store.StoreModuleArtifactDirectMismatch{} -> pure () _ -> assertFailure "unexpected direct-input result" Store.closeStore store rejectsInvalidCachedRootAuthorityAndClosure :: Assertion rejectsInvalidCachedRootAuthorityAndClosure = withStoreFixture "felix-store-invalid-install" \path theory fixture -> do (_startup, store) <- expectOpen path theory (owner, _prefix, syntax, semantic, _artifactKey, _artifact, proposition) <- makeCommittedModule theory fixture otherTheory <- expectRight (Cache.decodeCache Identity.getTheoryIdCache (ByteString.replicate 32 0x5a)) original <- case Semantic.semanticInterfaceDeclarations semantic of [delta] -> pure delta deltas -> assertFailure ("unexpected declaration count: " <> show (length deltas)) >> fail "unreachable" occurrence <- case Semantic.declarationDeltaFacts original of [fact] -> pure fact facts -> assertFailure ("unexpected fact count: " <> show (length facts)) >> fail "unreachable" let badAuthority = Authority.factAuthority (Identity.theoremRef otherTheory (Semantic.semanticFactProposition occurrence)) (Authority.factAuthoritySafety (Semantic.semanticFactAuthority occurrence)) badOccurrence = Semantic.semanticFactOccurrence (Semantic.semanticFactSlot occurrence) badAuthority (Semantic.semanticFactSearchEligibility occurrence) badDelta <- expectRight (Semantic.declarationInterfaceDelta (Semantic.declarationDeltaSlot original) [badOccurrence] (Semantic.declarationDeltaAliases original) (Semantic.declarationDeltaObjects original) (Semantic.declarationDeltaPropositions original) (Semantic.declarationDeltaEnvironment original)) badSemantic <- expectRight (Semantic.semanticInterface owner [] [badDelta]) badKey <- makeArtifactKey owner theory "bad-authority" let badArtifact = Semantic.moduleArtifactResult badKey (Syntax.moduleSyntaxAssertedId syntax) (Semantic.semanticInterfaceAssertedId badSemantic) writeRawModuleRows path [fixtureFirstObject fixture] [proposition] syntax [badSemantic] badArtifact badMemo <- Store.newStoreMemo store Store.loadCachedModuleInstallation badMemo store badKey (Syntax.moduleSyntaxAssertedId syntax) >>= \case Left Store.StoreImportedOccurrenceValidationFailure{} -> pure () _ -> assertFailure "unexpected root-authority result" childKey <- makeArtifactKey owner theory "missing-late-child" let childArtifact = Semantic.moduleArtifactResult childKey (Syntax.moduleSyntaxAssertedId syntax) (Semantic.semanticInterfaceAssertedId semantic) writeRawModuleRows path [fixtureFirstObject fixture] [proposition] syntax [semantic] childArtifact connection <- SQLite.open path SQLite.execute connection "DELETE FROM canonical_objects WHERE object_id = ?" (Only (Cache.encodeCache (Identity.putObjectIdCache (Identity.assertedObjectId (fixtureFirstObject fixture))))) SQLite.close connection childMemo <- Store.newStoreMemo store Store.loadCachedModuleInstallation childMemo store childKey (Syntax.moduleSyntaxAssertedId syntax) >>= \case Left Store.StoreAssertedChildMissing{} -> pure () _ -> assertFailure "unexpected missing-child result" Store.closeStore store rejectsDisagreeingModuleArtifactColumns :: Assertion rejectsDisagreeingModuleArtifactColumns = withStoreFixture "felix-store-artifact-columns" \path theory fixture -> do (_startup, store) <- expectOpen path theory (_owner, prefix, syntax, semantic, key, artifact, _proposition) <- makeCommittedModule theory fixture _ <- expectRightIO (Store.writeSealedModule store prefix [syntax] [semantic] artifact) connection <- SQLite.open path SQLite.execute_ connection "PRAGMA foreign_keys = OFF" SQLite.execute connection "UPDATE module_artifacts SET syntax_interface_id = ? \ \WHERE module_artifact_id = ?" ( ByteString.replicate 32 0x3c , Cache.cacheDigestBytes (Semantic.moduleArtifactIdDigest (Semantic.moduleArtifactResultId artifact)) ) SQLite.close connection memo <- Store.newStoreMemo store Store.loadCachedModuleInstallation memo store key (Syntax.moduleSyntaxAssertedId syntax) >>= \case Left Store.StoreModuleArtifactColumnsMismatch -> pure () Left other -> assertFailure ("unexpected artifact-column load: " <> show other) Right _ -> assertFailure "disagreeing artifact columns were accepted" Store.writeSealedModule store prefix [syntax] [semantic] artifact >>= \case Left Store.StoreRowPayloadMismatch{} -> pure () other -> assertFailure ("unexpected artifact-column rewrite: " <> show other) Store.closeStore store validatesSharedClosuresOncePerInvocation :: Assertion validatesSharedClosuresOncePerInvocation = withStoreFixture "felix-store-linear-closure" \path theory fixture -> do (_startup, store) <- expectOpen path theory let baseObject = fixtureFirstObject fixture first = transparentSetObject theory baseObject second = transparentSetObject theory first third = transparentSetObject theory second objects = [baseObject, first, second, third] closure <- expectRight (Identity.validateObjectClosure theory objects) proposition <- expectRight (Identity.validatePropositionContent closure (Core.CEq Core.TySet (Core.CGlobal (Identity.assertedObjectId third)) (Core.CGlobal (Identity.assertedObjectId third)))) baseOwner <- testModuleName "linear-base.tex" leftOwner <- testModuleName "linear-left.tex" rightOwner <- testModuleName "linear-right.tex" rootOwner <- testModuleName "linear-root.tex" let theorem = Identity.theoremRef theory (Identity.checkedPropositionId proposition) occurrence = Semantic.semanticFactOccurrence (Semantic.factSlot baseOwner (localFactOrdinal 0)) (Authority.factAuthority theorem Authority.cleanAuthoritySafety) Semantic.SearchEligible baseDelta <- expectRight (Semantic.declarationInterfaceDelta (Semantic.declarationSlot baseOwner (localDeclarationOrdinal 0)) [occurrence] [] (Identity.assertedObjectId <$> objects) [Identity.checkedPropositionId proposition] Semantic.emptySemanticEnvironmentDelta) baseSemantic <- expectRight (Semantic.semanticInterface baseOwner [] [baseDelta]) leftSemantic <- expectRight (Semantic.semanticInterface leftOwner [Semantic.semanticInterfaceAssertedId baseSemantic] []) rightSemantic <- expectRight (Semantic.semanticInterface rightOwner [Semantic.semanticInterfaceAssertedId baseSemantic] []) rootSemantic <- expectRight (Semantic.semanticInterface rootOwner [ Semantic.semanticInterfaceAssertedId leftSemantic , Semantic.semanticInterfaceAssertedId rightSemantic ] []) emptyDelta <- expectRight (Syntax.canonicalSyntaxDelta []) leftDelta <- expectRight (Syntax.canonicalSyntaxDelta [Syntax.CanonicalStructureOperation "linear-left"]) rightDelta <- expectRight (Syntax.canonicalSyntaxDelta [Syntax.CanonicalStructureOperation "linear-right"]) baseSyntax <- expectRight (Syntax.moduleSyntaxInterface [] emptyDelta) leftSyntax <- expectRight (Syntax.moduleSyntaxInterface [Syntax.moduleSyntaxAssertedId baseSyntax] leftDelta) rightSyntax <- expectRight (Syntax.moduleSyntaxInterface [Syntax.moduleSyntaxAssertedId baseSyntax] rightDelta) rootSyntax <- expectRight (Syntax.moduleSyntaxInterface [ Syntax.moduleSyntaxAssertedId leftSyntax , Syntax.moduleSyntaxAssertedId rightSyntax ] emptyDelta) rootKey <- makeArtifactKeyWithDirect rootOwner theory [ Semantic.semanticInterfaceAssertedId leftSemantic , Semantic.semanticInterfaceAssertedId rightSemantic ] "linear-root" leftKey <- makeArtifactKeyWithDirect leftOwner theory [Semantic.semanticInterfaceAssertedId baseSemantic] "linear-left" let rootArtifact = Semantic.moduleArtifactResult rootKey (Syntax.moduleSyntaxAssertedId rootSyntax) (Semantic.semanticInterfaceAssertedId rootSemantic) leftArtifact = Semantic.moduleArtifactResult leftKey (Syntax.moduleSyntaxAssertedId leftSyntax) (Semantic.semanticInterfaceAssertedId leftSemantic) connection <- SQLite.open path SQLite.withTransaction connection do traverse_ (insertRawObject connection) objects insertRawProposition connection proposition traverse_ (insertRawSyntaxInterface connection) [baseSyntax, leftSyntax, rightSyntax, rootSyntax] traverse_ (insertRawSemanticInterface connection) [baseSemantic, leftSemantic, rightSemantic, rootSemantic] insertRawModuleArtifact connection rootArtifact insertRawModuleArtifact connection leftArtifact SQLite.close connection memo <- Store.newStoreMemo store expectInstallation memo store rootKey rootSyntax expectInstallation memo store leftKey leftSyntax expectInstallation memo store rootKey rootSyntax visits <- Store.storeMemoVisits memo assertEqual "unique artifact rows" 2 (Store.storeArtifactRowsDecoded visits) assertEqual "unique artifact validations" 2 (Store.storeArtifactsValidated visits) assertEqual "syntax diamond rows" 4 (Store.storeSyntaxRowsDecoded visits) assertEqual "syntax diamond validations" 4 (Store.storeSyntaxRowsValidated visits) assertEqual "semantic diamond rows" 4 (Store.storeSemanticRowsDecoded visits) assertEqual "semantic diamond validations" 4 (Store.storeSemanticRowsValidated visits) assertEqual "transparent-chain rows" 4 (Store.storeObjectRowsDecoded visits) assertEqual "transparent-chain validations" 4 (Store.storeObjectRowsValidated visits) assertEqual "proposition rows" 1 (Store.storePropositionRowsDecoded visits) assertEqual "proposition validations" 1 (Store.storePropositionRowsValidated visits) Store.closeStore store where expectInstallation memo store key syntax = Store.loadCachedModuleInstallation memo store key (Syntax.moduleSyntaxAssertedId syntax) >>= \case Right (Just _installation) -> pure () _ -> assertFailure "cached closure installation failed" transparentSetObject :: Identity.TheoryId -> Identity.AssertedObject -> Identity.AssertedObject transparentSetObject theory dependency = Identity.assertedObject identity content where content = Identity.TransparentObjectContent theory Core.TySet (Core.CGlobal (Identity.assertedObjectId dependency)) identity = Identity.transparentObjectId theory Core.TySet (Core.CGlobal (Identity.assertedObjectId dependency)) testModuleName :: FilePath -> IO ModuleName testModuleName path = do digest <- expectRight (hashCanonicalFields "store-linear-module" [ByteString.Char8.pack path]) relative <- expectRight (safeRelativePath path) pure (moduleNameFromParts (sourceNamespaceIdFromDigest digest) relative) makeArtifactKey :: ModuleName -> Identity.TheoryId -> ByteString.ByteString -> IO Semantic.ModuleArtifactKey makeArtifactKey owner theory label = do makeArtifactKeyWithDirect owner theory [] label makeArtifactKeyWithDirect :: ModuleName -> Identity.TheoryId -> [Semantic.SemanticInterfaceId] -> ByteString.ByteString -> IO Semantic.ModuleArtifactKey makeArtifactKeyWithDirect owner theory direct label = do parsedKey <- expectRight (Parsed.parsedModuleKey (Content.sourceContentIdBytes label) Syntax.baseSyntaxInterfaceId []) expectRight (Semantic.moduleArtifactKey owner (Parsed.parsedModuleId parsedKey label) direct theory) writeRawModuleRows :: FilePath -> [Identity.AssertedObject] -> [Identity.CheckedPropositionContent] -> Syntax.ModuleSyntaxInterface -> [Semantic.SemanticInterface] -> Semantic.ModuleArtifactResult -> IO () writeRawModuleRows path objects propositions syntax semantics artifact = do connection <- SQLite.open path SQLite.withTransaction connection do traverse_ (insertRawObject connection) objects traverse_ (insertRawProposition connection) propositions insertRawSyntaxInterface connection syntax traverse_ (insertRawSemanticInterface connection) semantics insertRawModuleArtifact connection artifact SQLite.close connection insertRawObject :: SQLite.Connection -> Identity.AssertedObject -> IO () insertRawObject connection object = SQLite.execute connection "INSERT OR IGNORE INTO canonical_objects (object_id, payload) \ \VALUES (?, ?)" ( Cache.encodeCache (Identity.putObjectIdCache (Identity.assertedObjectId object)) , Cache.encodeCache (Identity.putObjectContentCache (Identity.assertedObjectContent object)) ) insertRawProposition :: SQLite.Connection -> Identity.CheckedPropositionContent -> IO () insertRawProposition connection proposition = SQLite.execute connection "INSERT OR IGNORE INTO canonical_propositions \ \(proposition_id, payload) VALUES (?, ?)" ( Cache.encodeCache (Identity.putPropositionIdCache (Identity.checkedPropositionId proposition)) , Cache.encodeCache (Cache.putCanonicalTermCache Identity.putObjectIdCache (Core.frozenCoreTerm (Identity.checkedPropositionTerm proposition))) ) insertRawSyntaxInterface :: SQLite.Connection -> Syntax.ModuleSyntaxInterface -> IO () insertRawSyntaxInterface connection interface = SQLite.execute connection "INSERT OR IGNORE INTO syntax_interfaces \ \(syntax_interface_id, payload) VALUES (?, ?)" ( Cache.cacheDigestBytes (Syntax.syntaxInterfaceIdDigest (Syntax.moduleSyntaxAssertedId interface)) , Cache.encodeCache (Syntax.putModuleSyntaxInterfaceCache interface) ) insertRawSemanticInterface :: SQLite.Connection -> Semantic.SemanticInterface -> IO () insertRawSemanticInterface connection interface = SQLite.execute connection "INSERT OR IGNORE INTO semantic_interfaces \ \(semantic_interface_id, payload) VALUES (?, ?)" ( Cache.cacheDigestBytes (Semantic.semanticInterfaceIdDigest (Semantic.semanticInterfaceAssertedId interface)) , Cache.encodeCache (Semantic.putSemanticInterfaceCache interface) ) insertRawModuleArtifact :: SQLite.Connection -> Semantic.ModuleArtifactResult -> IO () insertRawModuleArtifact connection artifact = SQLite.execute connection "INSERT OR IGNORE INTO module_artifacts \ \(module_artifact_id, syntax_interface_id, \ \semantic_interface_id, payload) VALUES (?, ?, ?, ?)" ( Cache.cacheDigestBytes (Semantic.moduleArtifactIdDigest (Semantic.moduleArtifactResultId artifact)) , Cache.cacheDigestBytes (Syntax.syntaxInterfaceIdDigest (Semantic.moduleArtifactResultSyntax artifact)) , Cache.cacheDigestBytes (Semantic.semanticInterfaceIdDigest (Semantic.moduleArtifactResultSemantic artifact)) , Cache.encodeCache (Semantic.putModuleArtifactResultCache artifact) ) storedPropositionCount :: FilePath -> Identity.PropositionId -> IO Int storedPropositionCount path identity = do connection <- SQLite.open path [Only rowCount] <- SQLite.query connection "SELECT COUNT(*) FROM canonical_propositions \ \WHERE proposition_id = ?" (Only (Cache.encodeCache (Identity.putPropositionIdCache identity))) SQLite.close connection pure rowCount storedObjectCount :: FilePath -> Identity.ObjectId -> IO Int storedObjectCount path identity = do connection <- SQLite.open path [Only rowCount] <- SQLite.query connection "SELECT COUNT(*) FROM canonical_objects WHERE object_id = ?" (Only (Cache.encodeCache (Identity.putObjectIdCache identity))) SQLite.close connection pure rowCount storedArtifactCount :: FilePath -> Semantic.ModuleArtifactId -> IO Int storedArtifactCount path identity = do connection <- SQLite.open path [Only rowCount] <- SQLite.query connection "SELECT COUNT(*) FROM module_artifacts \ \WHERE module_artifact_id = ?" (Only (Cache.cacheDigestBytes (Semantic.moduleArtifactIdDigest identity))) SQLite.close connection pure rowCount rollsBackFailedReadiness :: Assertion rollsBackFailedReadiness = withStoreFixture "felix-store-readiness-rollback" \path theory fixture -> do (_startup, store) <- expectOpen path theory (owner, prefix, _syntax, semantic, _artifactKey, artifact, proposition) <- makeCommittedModule theory fixture missingDelta <- expectRight (Syntax.canonicalSyntaxDelta [Syntax.CanonicalStructureOperation "missing-child"]) missingInterface <- expectRight (Syntax.moduleSyntaxInterface [] missingDelta) syntaxDelta <- expectRight (Syntax.canonicalSyntaxDelta []) brokenSyntax <- expectRight (Syntax.moduleSyntaxInterface [Syntax.moduleSyntaxAssertedId missingInterface] syntaxDelta) brokenParsedKey <- expectRight (Parsed.parsedModuleKey (Content.sourceContentIdBytes "rollback-source") Syntax.baseSyntaxInterfaceId []) brokenArtifactKey <- expectRight (Semantic.moduleArtifactKey owner (Parsed.parsedModuleId brokenParsedKey "rollback-parsed") [] theory) let brokenArtifact = Semantic.moduleArtifactResult brokenArtifactKey (Syntax.moduleSyntaxAssertedId brokenSyntax) (Semantic.semanticInterfaceAssertedId semantic) result <- Store.writeSealedModule store prefix [brokenSyntax] [semantic] brokenArtifact case result of Left Store.StoreAssertedChildMissing{} -> pure () Left other -> assertFailure ("unexpected readiness failure: " <> show other) Right _ -> assertFailure "broken readiness transaction was accepted" assertEqual "failed readiness did not publish the prefix" 0 =<< storedPropositionCount path (Identity.checkedPropositionId proposition) assertEqual "failed readiness leaves no module root" 0 =<< storedArtifactCount path (Semantic.moduleArtifactResultId artifact) -- A later failed seal must not erase a prefix published by an -- earlier successful source prefix flush. expectRightIO (Store.writePendingModulePrefix store prefix) assertEqual "successful prefix is visible before retry" 1 =<< storedPropositionCount path (Identity.checkedPropositionId proposition) retry <- Store.writeSealedModule store prefix [brokenSyntax] [semantic] brokenArtifact case retry of Left Store.StoreAssertedChildMissing{} -> pure () Left other -> assertFailure ("unexpected retry readiness failure: " <> show other) Right _ -> assertFailure "broken readiness retry was accepted" assertEqual "failed retry retains successful prefix" 1 =<< storedPropositionCount path (Identity.checkedPropositionId proposition) assertEqual "failed retry still leaves no module root" 0 =<< storedArtifactCount path (Semantic.moduleArtifactResultId artifact) Store.closeStore store makeCommittedModule :: Identity.TheoryId -> StoreFixture -> IO ( ModuleName , Declaration.PendingModulePrefix , Syntax.ModuleSyntaxInterface , Semantic.SemanticInterface , Semantic.ModuleArtifactKey , Semantic.ModuleArtifactResult , Identity.CheckedPropositionContent ) makeCommittedModule theory fixture = do foundation <- expectRight Foundation.checkedFoundation namespaceDigest <- expectRight (hashCanonicalFields "store-module-test" ["prefix"]) relative <- expectRight (safeRelativePath "module.tex") let owner = moduleNameFromParts (sourceNamespaceIdFromDigest namespaceDigest) relative proposition = fixtureProposition fixture resolver = Declaration.vampireResolver \_ -> pure (Left (Provers.ProverLaunchFailed "unused" "store fixture does not run Vampire")) driver <- Declaration.runModuleDriver foundation owner [] resolver Declaration.FreshValidation do (_value, _batch) <- Declaration.commitProofDeclaration (Semantic.proofSyntaxId "store-prefix") do Declaration.addDeclarationObject (fixtureFirstObject fixture) candidate <- Declaration.reserveCandidate (Declaration.candidateSpec proposition Semantic.SearchIneligible []) Declaration.authorizeOmittedCandidate candidate Declaration.recordOmittedUse pure () (_value, prefix, semantic) <- case driver of Right (Declaration.DriverSucceeded value interface pending _closure) -> pure (value, pending, interface) Right (Declaration.DriverFailed failure _prefix) -> assertFailure ("unexpected declaration failure: " <> show (failure :: Declaration.DriverFailure Declaration.DeclarationError)) >> fail "unreachable" Right (Declaration.DriverSealFailed failure _prefix) -> assertFailure ("unexpected seal failure: " <> show failure) >> fail "unreachable" Left failure -> assertFailure ("unexpected driver-open failure: " <> show failure) >> fail "unreachable" delta <- expectRight (Syntax.canonicalSyntaxDelta []) syntax <- expectRight (Syntax.moduleSyntaxInterface [] delta) parsedKey <- expectRight (Parsed.parsedModuleKey (Content.sourceContentIdBytes "store-module-source") Syntax.baseSyntaxInterfaceId []) artifactKey <- expectRight (Semantic.moduleArtifactKey owner (Parsed.parsedModuleId parsedKey "store-module-parsed") [] theory) let artifact = Semantic.moduleArtifactResult artifactKey (Syntax.moduleSyntaxAssertedId syntax) (Semantic.semanticInterfaceAssertedId semantic) pure ( owner , prefix , syntax , semantic , artifactKey , artifact , proposition ) makePendingPrefix :: StoreFixture -> [Identity.AssertedObject] -> IO Declaration.PendingModulePrefix makePendingPrefix fixture objects = do foundation <- expectRight Foundation.checkedFoundation owner <- testModuleName "rollback-prefix.tex" let proposition = fixtureProposition fixture resolver = Declaration.vampireResolver \_ -> pure (Left (Provers.ProverLaunchFailed "unused" "store fixture does not run Vampire")) driver <- Declaration.runModuleDriver foundation owner [] resolver Declaration.FreshValidation do (_value, _batch) <- Declaration.commitProofDeclaration (Semantic.proofSyntaxId "store-rollback") do traverse_ Declaration.addDeclarationObject objects candidate <- Declaration.reserveCandidate (Declaration.candidateSpec proposition Semantic.SearchIneligible []) Declaration.authorizeOmittedCandidate candidate Declaration.recordOmittedUse pure () case driver of Right (Declaration.DriverSucceeded _value _interface prefix _closure) -> pure prefix Right (Declaration.DriverFailed failure _prefix) -> assertFailure ("unexpected declaration failure: " <> show (failure :: Declaration.DriverFailure Declaration.DeclarationError)) >> fail "unreachable" Right (Declaration.DriverSealFailed failure _prefix) -> assertFailure ("unexpected seal failure: " <> show failure) >> fail "unreachable" Left failure -> assertFailure ("unexpected driver-open failure: " <> show failure) >> fail "unreachable" initializesAndReopensCurrentSchema :: Assertion initializesAndReopensCurrentSchema = withStoreFixture "felix-store-startup" \path theory _fixture -> do (startup, store) <- expectOpen path theory assertEqual "new store status" Store.InitializedNewStore startup Store.closeStore store (reopened, current) <- expectOpen path theory assertEqual "current store status" Store.OpenedCurrentStore reopened Store.closeStore current connection <- SQLite.open path names <- SQLite.query_ connection "SELECT name FROM sqlite_master \ \WHERE type = 'table' AND name NOT LIKE 'sqlite_%' \ \ORDER BY name" :: IO [Only Text] journal <- SQLite.query_ connection "PRAGMA journal_mode" :: IO [Only Text] SQLite.close connection assertEqual "complete schema table count" 9 (length names) assertEqual "rollback journal persists" [Only "delete"] journal rejectsIncompatibilityWithoutConfiguration :: Assertion rejectsIncompatibilityWithoutConfiguration = withStoreFixture "felix-store-incompatible" \path theory _fixture -> do connection <- SQLite.open path _ <- SQLite.query_ connection "PRAGMA journal_mode = WAL" :: IO [Only Text] SQLite.execute_ connection "CREATE TABLE store_compatibility ( \ \singleton INTEGER, cache_epoch INTEGER, theory_id BLOB )" SQLite.execute connection "INSERT INTO store_compatibility VALUES (1, ?, ?)" ( 999 :: Int , Cache.encodeCache (Identity.putTheoryIdCache theory) ) SQLite.execute_ connection "CREATE TABLE untouched (value INTEGER)" SQLite.close connection result <- Store.openStore path theory case result of Left (Store.IncompatibleStore Store.StoreCompatibilityMismatch{}) -> pure () Left other -> assertFailure ("unexpected incompatibility result: " <> show other) Right (_startup, store) -> do Store.closeStore store assertFailure "incompatible store was accepted" inspected <- SQLite.open path names <- SQLite.query_ inspected "SELECT name FROM sqlite_master \ \WHERE type = 'table' AND name NOT LIKE 'sqlite_%' \ \ORDER BY name" :: IO [Only Text] journal <- SQLite.query_ inspected "PRAGMA journal_mode" :: IO [Only Text] SQLite.close inspected assertEqual "startup creates no schema" [Only "store_compatibility", Only "untouched"] names assertEqual "startup applies no journal configuration" [Only "wal"] journal rejectsMalformedCompatibilityMetadata :: Assertion rejectsMalformedCompatibilityMetadata = withStoreFixture "felix-store-malformed" \path theory _fixture -> do connection <- SQLite.open path SQLite.execute_ connection "CREATE TABLE store_compatibility ( \ \singleton INTEGER, cache_epoch, theory_id )" SQLite.execute connection "INSERT INTO store_compatibility VALUES (1, ?, ?)" ( "not-an-epoch" :: Text , Cache.encodeCache (Identity.putTheoryIdCache theory) ) SQLite.close connection result <- Store.openStore path theory case result of Left (Store.IncompatibleStore Store.StoreCompatibilityMalformed{}) -> pure () Left other -> assertFailure ("unexpected malformed result: " <> show other) Right (_startup, store) -> do Store.closeStore store assertFailure "malformed metadata was accepted" rejectsCompatibleIncompleteSchema :: Assertion rejectsCompatibleIncompleteSchema = withStoreFixture "felix-store-incomplete" \path theory _fixture -> do (_startup, store) <- expectOpen path theory Store.closeStore store connection <- SQLite.open path SQLite.execute_ connection "DROP TABLE canonical_propositions" SQLite.close connection result <- Store.openStore path theory case result of Left (Store.FatalStoreStartup Store.StoreSchemaIntegrityFailure{}) -> pure () Left other -> assertFailure ("unexpected incomplete-schema result: " <> show other) Right (_startup, current) -> do Store.closeStore current assertFailure "incomplete current schema was accepted" rollsBackUnequalDuplicateBatch :: Assertion rollsBackUnequalDuplicateBatch = withStoreFixture "felix-store-rollback" \path theory fixture -> do (_startup, store) <- expectOpen path theory let first = fixtureFirstObject fixture second = fixtureSecondObject fixture prefix <- makePendingPrefix fixture [first, second] Store.closeStore store connection <- SQLite.open path SQLite.execute connection "INSERT INTO canonical_objects (object_id, payload) VALUES (?, ?)" ( Cache.encodeCache (Identity.putObjectIdCache (Identity.assertedObjectId second)) , Cache.encodeCache (Identity.putObjectContentCache (Identity.assertedObjectContent first)) ) SQLite.close connection (_reopened, current) <- expectOpen path theory result <- Store.writePendingModulePrefix current prefix case result of Left Store.StoreRowPayloadMismatch{} -> pure () Left other -> assertFailure ("unexpected duplicate result: " <> show other) Right () -> assertFailure "unequal duplicate was accepted" assertEqual "earlier insertion was rolled back" 0 =<< storedObjectCount path (Identity.assertedObjectId first) Store.closeStore current rejectsMalformedCanonicalPayloads :: Assertion rejectsMalformedCanonicalPayloads = withStoreFixture "felix-store-decode" \path theory fixture -> do (_startup, store) <- expectOpen path theory let object = fixtureFirstObject fixture (_owner, prefix, syntax, semantic, key, artifact, _proposition) <- makeCommittedModule theory fixture expectRightIO (Store.writeSealedModule store prefix [syntax] [semantic] artifact) Store.closeStore store connection <- SQLite.open path SQLite.execute connection "UPDATE canonical_objects SET payload = ? \ \WHERE object_id = ?" ( ByteString.singleton 0xff , Cache.encodeCache (Identity.putObjectIdCache (Identity.assertedObjectId object)) ) SQLite.close connection (_reopened, current) <- expectOpen path theory memo <- Store.newStoreMemo current result <- Store.loadCachedModuleInstallation memo current key (Syntax.moduleSyntaxAssertedId syntax) case result of Left Store.StoreRowDecodeFailure{} -> pure () Left other -> assertFailure ("unexpected malformed-row result: " <> show other) Right _ -> assertFailure "malformed canonical payload was accepted" Store.closeStore current plansPersistentStores :: Assertion plansPersistentStores = Temp.withSystemTempDirectory "felix-store-planning" \root -> do (theory, _fixture) <- makeStoreFixture let cacheRoot = root Posix. "cache" expectedDefault = cacheRoot Posix. "felix" Posix. "store.sqlite" explicitParent = root Posix. "explicit" explicitPath = explicitParent Posix. "selected.sqlite" Directory.createDirectory cacheRoot Directory.createDirectory explicitParent withEnvironment "XDG_CACHE_HOME" cacheRoot do defaultPlan <- expectRightIO (Store.planStore Store.DefaultStore) defaultResult <- Store.withStoreLease defaultPlan \lease -> do assertEqual "default store path" expectedDefault (Store.storePathFilePath (Store.storeLeasePath lease)) assertBool "planning does not create the default parent" . not =<< Directory.doesPathExist (cacheRoot Posix. "felix") Store.withOpenStore lease theory \_startup _store -> Directory.doesFileExist expectedDefault assertEqual "default store opens at the XDG path" (Right True) defaultResult explicitPlan <- expectRightIO (Store.planStore (Store.ExplicitStore explicitPath)) explicitResult <- Store.withStoreLease explicitPlan \lease -> do assertEqual "explicit store path" explicitPath (Store.storePathFilePath (Store.storeLeasePath lease)) Store.withOpenStore lease theory \_startup _store -> Directory.doesFileExist explicitPath assertEqual "explicit store opens without creating its parent" (Right True) explicitResult missing <- Store.planStore (Store.ExplicitStore (root Posix. "missing" Posix. "store.sqlite")) case missing of Left Store.ExplicitStoreParentMissing{} -> pure () Left other -> assertFailure ("unexpected missing-parent result: " <> show other) Right _ -> assertFailure "missing explicit parent was accepted" cleansFreshStores :: Assertion cleansFreshStores = do (theory, _fixture) <- makeStoreFixture plan <- expectRightIO (Store.planStore Store.FreshTemporaryStore) successPath <- IORef.newIORef Nothing success <- Store.withStoreLease plan \lease -> do let path = Store.storePathFilePath (Store.storeLeasePath lease) IORef.writeIORef successPath (Just path) Store.withOpenStore lease theory \_startup _store -> Directory.doesFileExist path assertEqual "fresh store opened" (Right True) success assertFreshRemoved successPath failurePath <- IORef.newIORef Nothing failed <- Exception.try (Store.withStoreLease plan \lease -> do let path = Store.storePathFilePath (Store.storeLeasePath lease) IORef.writeIORef failurePath (Just path) void (Store.withOpenStore lease theory \_startup _store -> ioError (userError "fresh action failed"))) :: IO (Either IOError ()) case failed of Left _ -> pure () Right () -> assertFailure "fresh-store action exception did not escape" assertFreshRemoved failurePath doesNotFallBackAfterFatalStartup :: Assertion doesNotFallBackAfterFatalStartup = Temp.withSystemTempDirectory "felix-store-no-fallback" \root -> do (theory, _fixture) <- makeStoreFixture let persistentParent = root Posix. "persistent" persistentPath = persistentParent Posix. "store.sqlite" cacheRoot = root Posix. "cache" Directory.createDirectory persistentParent Directory.createDirectory cacheRoot plan <- expectRightIO (Store.planStore (Store.ExplicitStore persistentPath)) initialized <- Store.withStoreLease plan \lease -> Store.withOpenStore lease theory \_startup _store -> pure () assertEqual "fixture store initialized" (Right ()) initialized connection <- SQLite.open persistentPath SQLite.execute_ connection "DROP TABLE canonical_objects" SQLite.close connection withEnvironment "XDG_CACHE_HOME" cacheRoot do result <- Store.withStoreLease plan \lease -> Store.withOpenStore lease theory \_startup _store -> pure () case result of Left (Store.StoreLifecycleOpenFailed (Store.FatalStoreStartup Store.StoreSchemaIntegrityFailure{})) -> pure () Left other -> assertFailure ("unexpected fatal-startup result: " <> show other) Right () -> assertFailure "corrupt persistent store was accepted" assertBool "fatal startup creates no default fallback" . not =<< Directory.doesPathExist (cacheRoot Posix. "felix") data StoreFixture = StoreFixture !Identity.AssertedObject !Identity.AssertedObject !Identity.CheckedPropositionContent fixtureFirstObject :: StoreFixture -> Identity.AssertedObject fixtureFirstObject (StoreFixture object _second _proposition) = object fixtureSecondObject :: StoreFixture -> Identity.AssertedObject fixtureSecondObject (StoreFixture _first object _proposition) = object fixtureProposition :: StoreFixture -> Identity.CheckedPropositionContent fixtureProposition (StoreFixture _first _second proposition) = proposition makeStoreFixture :: IO (Identity.TheoryId, StoreFixture) makeStoreFixture = do foundation <- expectRight Foundation.checkedFoundation let theory = Identity.theoryId foundation first = intrinsicObject theory Core.Empty second = intrinsicObject theory Core.PairSet closure <- expectRight (Identity.validateObjectClosure theory [first, second]) proposition <- expectRight (Identity.validatePropositionContent closure (Core.CEq Core.TySet (Core.CGlobal (Identity.assertedObjectId first)) (Core.CGlobal (Identity.assertedObjectId first)))) pure ( theory , StoreFixture first second proposition ) intrinsicObject :: Identity.TheoryId -> Core.CoreIntrinsicTag -> Identity.AssertedObject intrinsicObject theory tag = Identity.assertedObject identity content where coreType = Core.coreIntrinsicType tag content = Identity.IntrinsicObjectContent theory tag coreType identity = Identity.intrinsicObjectId theory tag coreType withStoreFixture :: String -> ( FilePath -> Identity.TheoryId -> StoreFixture -> IO a ) -> IO a withStoreFixture template action = Temp.withSystemTempDirectory template \root -> do (theory, fixture) <- makeStoreFixture action (root Posix. "store.sqlite") theory fixture expectOpen :: FilePath -> Identity.TheoryId -> IO (Store.StoreStartup, Store.Store) expectOpen path theory = do result <- Store.openStore path theory case result of Left failure -> assertFailure (show failure) >> fail "unreachable" Right opened -> pure opened expectRight :: Show failure => Either failure value -> IO value expectRight = \case Left failure -> assertFailure (show failure) >> fail "unreachable" Right value -> pure value expectRightIO :: Show failure => IO (Either failure value) -> IO value expectRightIO action = expectRight =<< action assertFreshRemoved :: IORef.IORef (Maybe FilePath) -> Assertion assertFreshRemoved pathReference = do selected <- IORef.readIORef pathReference case selected of Nothing -> assertFailure "fresh store path was not allocated" Just path -> do assertBool "fresh database was removed" . not =<< Directory.doesPathExist path assertBool "fresh database directory was removed" . not =<< Directory.doesPathExist (Posix.takeDirectory path) withEnvironment :: String -> String -> IO value -> IO value withEnvironment name value action = Exception.bracket (Environment.lookupEnv name) restore \_previous -> do Environment.setEnv name value action where restore = \case Nothing -> Environment.unsetEnv name Just previous -> Environment.setEnv name previous