Locate exact proof obligation failures

1 files changed, 69 insertions, 0 deletions

diff --git a/source/Test/Unit/Module.hs b/source/Test/Unit/Module.hs
index f14018c..012b9f4 100644
--- a/source/Test/Unit/Module.hs
+++ b/source/Test/Unit/Module.hs
@@ -1088,6 +1088,75 @@ retainsExactPrefixBeforeFailure = do
         Right{} ->
             assertFailure "unmatched proof was admitted"
 
+    runtimeFailure <-
+        Temp.withSystemTempDirectory "felix-runtime-proof-failure" \root -> do
+            foundation <- expectRight Foundation.checkedFoundation
+            bootstrap <-
+                expectRight
+                    =<< Module.buildBootstrapPreludeSession
+                        foundation
+                        unusedResolver
+            repository <- getCurrentDirectory
+            mounts <- exactFixtureMounts repository
+            workspace <- parseExactWorkspace
+                bootstrap mounts "test/phase5/exact-runtime-failure.tex"
+            let executable = root Posix.</> "vampire"
+            writeFile executable
+                (unlines
+                    [ "#!/bin/sh"
+                    , "cat >/dev/null"
+                    , "printf '%s\\n' '% SZS status Theorem for located-proof'"
+                    ])
+            permissions <- getPermissions executable
+            setPermissions executable
+                (setOwnerExecutable True permissions)
+            runs <- newIORef (0 :: Int)
+            let resolver = Declaration.vampireResolver \prepared -> do
+                    runNumber <- readIORef runs
+                    modifyIORef' runs (+ 1)
+                    if runNumber == 0
+                        then
+                            runNoLoggingT
+                                (Provers.runPreparedTypedProver
+                                    (Provers.vampire
+                                        executable
+                                        Provers.defaultTimeLimit
+                                        Provers.defaultMemoryLimit)
+                                    prepared)
+                        else
+                            pure
+                                (Right
+                                    (Provers.CounterSatisfiable
+                                        "later exact obligation"))
+                parsed = Parse.parsedWorkspaceRootModule workspace
+            input <- expectRight
+                (Module.typedModuleInput
+                    foundation
+                    (Module.bootstrapWalkingReadiness bootstrap)
+                    resolver
+                    Declaration.FreshValidation
+                    parsed
+                    [])
+            Module.runTypedModule input
+    case runtimeFailure of
+        Module.TypedModuleFailed
+                failure@(Module.TypedDeclarationFailed
+                    (Declaration.ProofObligationFailedAt
+                        location
+                        Declaration.VampireObligationRejected{}))
+                prefix -> do
+            assertEqual "later rejected obligation line"
+                11
+                (locLine location)
+            assertEqual "typed failure retains obligation location"
+                (Just location)
+                (Module.typedModuleFailureLocation failure)
+            assertEqual "runtime proof failure publishes no theorem"
+                1
+                (length (Declaration.pendingModulePrefixBatches prefix))
+        _result ->
+            assertFailure "unexpected runtime proof failure"
+
 routesProductionVerification :: Assertion
 routesProductionVerification = do
     producer <- verifyFixture "test/phase3/typed-producer.tex"