diff options
Diffstat (limited to 'source/Test/Unit/CommandLine.hs')
| -rw-r--r-- | source/Test/Unit/CommandLine.hs | 181 |
1 files changed, 147 insertions, 34 deletions
diff --git a/source/Test/Unit/CommandLine.hs b/source/Test/Unit/CommandLine.hs index ba31934..eeefbc3 100644 --- a/source/Test/Unit/CommandLine.hs +++ b/source/Test/Unit/CommandLine.hs @@ -3,10 +3,11 @@ module Test.Unit.CommandLine (unitTests) where import Base -import Api (VerificationReport(..), VerificationRoute(..)) +import Api (VerificationReport(..)) import CommandLine import Felix.Source (safeRelativePath) import Felix.Store qualified as Store +import Provers qualified import Render.Html.Output qualified as HtmlOutput import Report.Location (pattern Nowhere) @@ -67,8 +68,7 @@ unitTests = (exitCode, stdout, stderr) <- runCliWithSourceAndConfiguredVampire cliGapSource - \vampirePath -> - writeFile vampirePath "not executable" + writeNonExecutableFile exitCode `shouldBe` ExitSuccess stdout `shouldBe` "" stderr `shouldContain` @@ -95,8 +95,7 @@ unitTests = "UnsuccessfulVampireExit (ExitFailure 7)" , testCase "prover launch failure exits as infrastructure failure" do (exitCode, stdout, stderr) <- - runCliWithConfiguredVampire \vampirePath -> - writeFile vampirePath "not executable" + runCliWithConfiguredVampire writeNonExecutableFile exitCode `shouldBe` ExitFailure 2 stdout `shouldBe` "" stderr `shouldContain` "ProverLaunchFailed" @@ -110,8 +109,13 @@ unitTests = dumpAndHtmlVerifyOnce , testCase "semantic failure publishes no HTML" semanticFailurePublishesNoHtml + , testCase "fresh and cached presentation publish equal HTML" + freshAndCachedPresentationAgree , testCase "missing renderer data is a typed failure" missingRendererDataIsTyped + , testCase + "post-verification HTML failure retains authorization report" + htmlFailureRetainsAuthorizationReport ] ] @@ -142,6 +146,17 @@ parsesClosedCommands = do assertFailure ("unexpected default verify parse: " <> showParserResult other) + case parseCommandArguments ["input.tex", "--jobs", "3"] of + Success + (Verify + (Input "input.tex") + VerificationOptions + { verificationJobsOverride = Just jobs + }) -> + Provers.effectiveJobsValue jobs `shouldBe` 3 + other -> + assertFailure + ("unexpected jobs parse: " <> showParserResult other) case parseCommandArguments ["input.tex", "--fresh"] of Success (Verify @@ -159,6 +174,7 @@ rejectsConflictingOptions :: Assertion rejectsConflictingOptions = do for_ [ ["input.tex", "--parseonly", "--fresh"] + , ["input.tex", "--parseonly", "--jobs", "2"] , ["input.tex", "--parseonly", "--dump", "dump"] , ["input.tex", "--parseonly", "--html"] , ["input.tex", "--store", "store.sqlite", "--fresh"] @@ -173,6 +189,12 @@ rejectsConflictingOptions = do <> show arguments <> " as " <> showParserResult other) + case parseCommandArguments ["input.tex", "--jobs", "0"] of + Failure _failure -> pure () + other -> + assertFailure + ("non-positive jobs were accepted as " + <> showParserResult other) showParserResult :: ParserResult Command -> String showParserResult = \case @@ -195,10 +217,8 @@ versionNeedsNoInputOrStore = parseOnlyUsesNoAuthority :: Assertion parseOnlyUsesNoAuthority = - withCliFixture cliSource \fixture -> do - writeFile - (cliFixtureVampire fixture) - "not executable" + withCliFixture cliPreludeSyntaxSource \fixture -> do + writeNonExecutableFile (cliFixtureVampire fixture) (exitCode, stdout, stderr) <- runCliFixture fixture @@ -307,6 +327,7 @@ removesFailedDumpTemporary = dumpsExactExecutedRequest :: Assertion dumpsExactExecutedRequest = withCliFixture cliSource \fixture -> do + seedPackagedPreludeCache fixture let captured = cliFixtureRoot fixture </> "captured.p" writeExecutableScript (cliFixtureVampire fixture) @@ -316,31 +337,28 @@ dumpsExactExecutedRequest = (exitCode, _stdout, stderr) <- runCliFixture fixture [ "input.tex" - , "--fresh" , "--dump" , "dump" ] exitCode `shouldBe` ExitSuccess stderr `shouldContain` "Verification successful." dumped <- ByteString.readFile - (cliFixtureRoot fixture </> "dump" </> "1.p") + (cliFixtureRoot fixture </> "dump" </> "1-1.p") sent <- ByteString.readFile captured assertEqual "dump is the exact process input" sent dumped assertBool "request is dumped only once" . not =<< Directory.doesPathExist - (cliFixtureRoot fixture </> "dump" </> "2.p") + (cliFixtureRoot fixture </> "dump" </> "1-2.p") launchFailureDumpsNoRequest :: Assertion launchFailureDumpsNoRequest = withCliFixture cliSource \fixture -> do - writeFile - (cliFixtureVampire fixture) - "not executable" + seedPackagedPreludeCache fixture + writeNonExecutableFile (cliFixtureVampire fixture) (exitCode, _stdout, stderr) <- runCliFixture fixture [ "input.tex" - , "--fresh" , "--dump" , "dump" ] @@ -349,11 +367,12 @@ launchFailureDumpsNoRequest = assertBool "no request was dumped before process launch" . not =<< Directory.doesPathExist - (cliFixtureRoot fixture </> "dump" </> "1.p") + (cliFixtureRoot fixture </> "dump" </> "1-1.p") dumpsOnlyExecutedPrefix :: Assertion dumpsOnlyExecutedPrefix = withCliFixture cliTwoSource \fixture -> do + seedPackagedPreludeCache fixture writeExecutableScript (cliFixtureVampire fixture) [ "cat >/dev/null" @@ -362,7 +381,6 @@ dumpsOnlyExecutedPrefix = (exitCode, _stdout, stderr) <- runCliFixture fixture [ "input.tex" - , "--fresh" , "--dump" , "dump" ] @@ -370,15 +388,16 @@ dumpsOnlyExecutedPrefix = stderr `shouldContain` "prover found countermodel" assertBool "executed request was dumped" =<< Directory.doesFileExist - (cliFixtureRoot fixture </> "dump" </> "1.p") + (cliFixtureRoot fixture </> "dump" </> "1-1.p") assertBool "unexecuted request was not dumped" . not =<< Directory.doesPathExist - (cliFixtureRoot fixture </> "dump" </> "2.p") + (cliFixtureRoot fixture </> "dump" </> "1-2.p") dumpAndHtmlVerifyOnce :: Assertion dumpAndHtmlVerifyOnce = withCliFixture cliSource \fixture -> do + seedPackagedPreludeCache fixture let countPath = cliFixtureRoot fixture </> "vampire-runs" writeExecutableScript (cliFixtureVampire fixture) @@ -389,7 +408,6 @@ dumpAndHtmlVerifyOnce = (exitCode, _stdout, stderr) <- runCliFixture fixture [ "input.tex" - , "--fresh" , "--dump" , "dump" , "--html" @@ -400,7 +418,7 @@ dumpAndHtmlVerifyOnce = assertEqual "one semantic verification" ["run"] runs assertBool "request dump was published" =<< Directory.doesFileExist - (cliFixtureRoot fixture </> "dump" </> "1.p") + (cliFixtureRoot fixture </> "dump" </> "1-1.p") assertBool "root HTML page was published" =<< Directory.doesFileExist (cliFixtureRoot fixture </> "html" </> "input.html") @@ -414,6 +432,7 @@ dumpAndHtmlVerifyOnce = semanticFailurePublishesNoHtml :: Assertion semanticFailurePublishesNoHtml = withCliFixture cliSource \fixture -> do + seedPackagedPreludeCache fixture writeExecutableScript (cliFixtureVampire fixture) [ "cat >/dev/null" @@ -421,17 +440,56 @@ semanticFailurePublishesNoHtml = ] (exitCode, _stdout, stderr) <- runCliFixture fixture - ["input.tex", "--fresh", "--html"] + [ "input.tex" + , "--dump" + , "dump" + , "--html" + ] exitCode `shouldBe` ExitFailure 1 stderr `shouldContain` "prover found countermodel" + assertBool "semantic failure retains the executed request dump" + =<< Directory.doesFileExist + (cliFixtureRoot fixture </> "dump" </> "1-1.p") assertBool "semantic failure publishes no HTML" . not =<< Directory.doesPathExist (cliFixtureRoot fixture </> "html") +freshAndCachedPresentationAgree :: Assertion +freshAndCachedPresentationAgree = + withCliFixture cliSource \fixture -> do + seedPackagedPreludeCache fixture + writeExecutableScript + (cliFixtureVampire fixture) + [ "cat >/dev/null" + , "printf '%s\\n' '% SZS status Theorem for cli'" + ] + (freshExit, _freshStdout, freshStderr) <- + runCliFixture fixture ["input.tex", "--html"] + freshExit `shouldBe` ExitSuccess + freshStderr `shouldContain` "Verification successful." + let htmlRoot = cliFixtureRoot fixture </> "html" + page = htmlRoot </> "input.html" + support = + htmlRoot </> "_static" </> "naproche-html.js" + freshPage <- ByteString.readFile page + freshSupport <- ByteString.readFile support + Directory.removePathForcibly htmlRoot + writeNonExecutableFile (cliFixtureVampire fixture) + (warmExit, _warmStdout, warmStderr) <- + runCliFixture fixture ["input.tex", "--html"] + warmExit `shouldBe` ExitSuccess + warmStderr `shouldContain` "Verification successful." + warmPage <- ByteString.readFile page + warmSupport <- ByteString.readFile support + assertEqual "fresh/cache-hit page bytes" freshPage warmPage + assertEqual "fresh/cache-hit support bytes" + freshSupport warmSupport + missingRendererDataIsTyped :: Assertion missingRendererDataIsTyped = withCliFixture cliSource \fixture -> do + seedPackagedPreludeCache fixture Directory.removeFile (cliFixtureRoot fixture </> "library" </> "lexicon.tsv") writeExecutableScript @@ -440,7 +498,7 @@ missingRendererDataIsTyped = , "printf '%s\\n' '% SZS status Theorem for cli'" ] (exitCode, stdout, stderr) <- - runCliFixture fixture ["input.tex", "--fresh", "--html"] + runCliFixture fixture ["input.tex", "--html"] exitCode `shouldBe` ExitFailure 2 stdout `shouldBe` "" stderr `shouldContain` "HTML preparation failed:" @@ -452,27 +510,44 @@ missingRendererDataIsTyped = =<< Directory.doesPathExist (cliFixtureRoot fixture </> "html") +htmlFailureRetainsAuthorizationReport :: Assertion +htmlFailureRetainsAuthorizationReport = + withCliFixture cliGapSource \fixture -> do + seedPackagedPreludeCache fixture + Directory.removeFile + (cliFixtureRoot fixture </> "library" </> "lexicon.tsv") + writeNonExecutableFile (cliFixtureVampire fixture) + (exitCode, stdout, stderr) <- + runCliFixture fixture ["input.tex", "--html"] + exitCode `shouldBe` ExitFailure 2 + stdout `shouldBe` "" + stderr `shouldContain` + "Verification succeeded, but HTML preparation failed:" + stderr `shouldContain` + "Direct source authorization summary: 0 source axioms, 1 explicit proof gap." + stderr `shouldContain` "Explicit proof gap at input.tex 5:5" + assertBool "failed output publishes no HTML" + . not + =<< Directory.doesPathExist + (cliFixtureRoot fixture </> "html") + outcomeCases :: [(CommandOutcome, ExitCode)] outcomeCases = [ (CommandCompleted, ExitSuccess) , (VerificationSucceeded emptyReport, ExitSuccess) , (VerificationCompletedWithGaps emptyReport, ExitSuccess) - , ( VerificationRejected Nowhere (CountermodelFound "") + , ( VerificationRejected emptyReport Nowhere (CountermodelFound "") , ExitFailure 1 ) - , (ProverFailed Nowhere (ProverIndeterminate ""), ExitFailure 2) + , ( ProverFailed emptyReport Nowhere (ProverIndeterminate "") + , ExitFailure 2 + ) ] emptyReport :: VerificationReport emptyReport = VerificationReport - { verificationRoute = LegacyVerificationRoute - , verificationLegacyDeclaredAssumptionCount = 0 - , verificationTypedDeclaredAssumptionCount = 0 - , verificationTrustedVampireCount = 0 - , verificationExplicitGapLocations = [] - , verificationTrustedLegacyRuleCount = 0 - , verificationKernelProofCount = 0 + { verificationDirectEscapes = [] } runCliWithFakeVampire @@ -495,8 +570,9 @@ runCliWithSourceAndConfiguredVampire -> IO (ExitCode, String, String) runCliWithSourceAndConfiguredVampire source prepareVampire = withCliFixture source \fixture -> do + seedPackagedPreludeCache fixture prepareVampire (cliFixtureVampire fixture) - runCliFixture fixture ["input.tex", "--fresh"] + runCliFixture fixture ["input.tex"] data CliFixture = CliFixture { cliFixtureRoot :: !FilePath @@ -562,6 +638,27 @@ runCliFixture fixture arguments = }) "" +-- | Populate only the packaged final-prelude root. Process-boundary tests +-- can then exercise the requested ordinary module outcome without making +-- their fake prover depend on the prelude's private obligation count. +seedPackagedPreludeCache :: CliFixture -> Assertion +seedPackagedPreludeCache fixture = do + let sourcePath = cliFixtureRoot fixture </> "input.tex" + original <- ByteString.readFile sourcePath + writeExecutableScript + (cliFixtureVampire fixture) + [ "cat >/dev/null" + , "printf '%s\\n' '% SZS status Theorem for prelude seed'" + ] + (exitCode, stdout, stderr) <- + (do + writeFile sourcePath "% cache the packaged final prelude\n" + runCliFixture fixture ["input.tex"]) + `Exception.finally` ByteString.writeFile sourcePath original + exitCode `shouldBe` ExitSuccess + stdout `shouldBe` "" + stderr `shouldContain` "Verification successful." + assertNoDefaultStore :: CliFixture -> Assertion assertNoDefaultStore fixture = assertBool "default store was not created" @@ -577,6 +674,14 @@ writeExecutableScript path scriptLines = do Directory.setPermissions path (Directory.setOwnerExecutable True permissions) +writeNonExecutableFile :: FilePath -> IO () +writeNonExecutableFile path = do + exists <- Directory.doesPathExist path + if exists + then Directory.removeFile path + else pure () + writeFile path "not executable" + requireZfExecutable :: IO FilePath requireZfExecutable = do executable <- Directory.findExecutable "zf" @@ -603,6 +708,14 @@ cliSource = , "\\end{proposition}" ] +cliPreludeSyntaxSource :: String +cliPreludeSyntaxSource = + unlines + [ "\\begin{proposition}\\label{parse_prelude_syntax}" + , " For all $x$ we have $\\preludeSuccessor{x} = \\preludeSuccessor{x}$." + , "\\end{proposition}" + ] + cliGapSource :: String cliGapSource = unlines |