diff options
Diffstat (limited to 'source/Test/Unit/CommandLine.hs')
| -rw-r--r-- | source/Test/Unit/CommandLine.hs | 775 |
1 files changed, 0 insertions, 775 deletions
diff --git a/source/Test/Unit/CommandLine.hs b/source/Test/Unit/CommandLine.hs deleted file mode 100644 index 9f567f1..0000000 --- a/source/Test/Unit/CommandLine.hs +++ /dev/null @@ -1,775 +0,0 @@ -{-# LANGUAGE OverloadedStrings #-} - -module Test.Unit.CommandLine (unitTests) where - -import Base -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) - -import Control.Exception (IOException, bracket) -import Control.Exception qualified as Exception -import Data.ByteString qualified as ByteString -import Data.List qualified as List -import Data.Text qualified as Text -import Options.Applicative (ParserResult(..)) -import Options.Applicative qualified as Options -import System.Directory qualified as Directory -import System.Environment (getEnvironment) -import System.Exit (ExitCode(..)) -import System.FilePath.Posix ((</>)) -import System.Process - ( CreateProcess(..) - , proc - , readCreateProcessWithExitCode - ) -import Test.Tasty -import Test.Tasty.HUnit - -unitTests :: TestTree -unitTests = - testGroup "Command line" - [ testCase "parses the closed command model" - parsesClosedCommands - , testCase "rejects conflicting command options" - rejectsConflictingOptions - , testCase "maps structured outcomes to process status" do - for_ outcomeCases \(outcome, expectedExitCode) -> - commandOutcomeExitCode outcome - `shouldBe` expectedExitCode - , testCase "reports the committed HTML prefix" - reportsCommittedHtmlPrefix - , testCase "removes an unpublished dump temporary" - removesFailedDumpTemporary - , testGroup "process boundary" - [ testCase "version needs no input or store" - versionNeedsNoInputOrStore - , testCase "parse-only uses no store or Vampire" - parseOnlyUsesNoAuthority - , testCase "malformed source has a stable failure class" - malformedSourceHasStableFailure - , testCase "invalid output needs no source pass or store startup" - invalidOutputPrecedesStoreStartup - , testCase "nested HTML routes fail before store startup" - nestedHtmlRoutesPrecedeStoreStartup - , testCase "verified theorem exits successfully" do - (exitCode, stdout, stderr) <- runCliWithFakeVampire - [ "printf '%s\\n' '% SZS status Theorem for cli'" - , "exit 0" - ] - exitCode `shouldBe` ExitSuccess - stdout `shouldBe` "" - stderr `shouldContain` "Verification successful." - , testCase "omitted proof reports a located explicit gap" do - (exitCode, stdout, stderr) <- - runCliWithSourceAndConfiguredVampire - cliGapSource - writeNonExecutableFile - exitCode `shouldBe` ExitSuccess - stdout `shouldBe` "" - stderr `shouldContain` - "Verification completed with explicit proof gaps." - stderr `shouldContain` "1 explicit proof gap" - stderr `shouldContain` "input.tex 5:5" - , testCase "countermodel exits as verification rejection" do - (exitCode, stdout, stderr) <- runCliWithFakeVampire - [ "printf '%s\\n' '% SZS status CounterSatisfiable for cli'" - , "exit 0" - ] - exitCode `shouldBe` ExitFailure 1 - stdout `shouldBe` "" - stderr `shouldContain` - "Verification failed: prover found countermodel" - , testCase "failed prover exits as infrastructure failure" do - (exitCode, stdout, stderr) <- runCliWithFakeVampire - [ "printf '%s\\n' '% SZS status Theorem for cli'" - , "exit 7" - ] - exitCode `shouldBe` ExitFailure 2 - stdout `shouldBe` "" - stderr `shouldContain` - "UnsuccessfulVampireExit (ExitFailure 7)" - , testCase "prover launch failure exits as infrastructure failure" do - (exitCode, stdout, stderr) <- - runCliWithConfiguredVampire writeNonExecutableFile - exitCode `shouldBe` ExitFailure 2 - stdout `shouldBe` "" - stderr `shouldContain` "ProverLaunchFailed" - , testCase "dumps the exact executed request once" - dumpsExactExecutedRequest - , testCase "launch failure dumps no request" - launchFailureDumpsNoRequest - , testCase "failed verification retains its executed dump subset" - dumpsOnlyExecutedPrefix - , testCase "dump and HTML share one verification" - 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 - ] - ] - -parsesClosedCommands :: Assertion -parsesClosedCommands = do - case parseCommandArguments ["--version"] of - Success Version -> - pure () - other -> - assertFailure - ("unexpected version parse: " <> showParserResult other) - case parseCommandArguments ["input.tex", "--parseonly"] of - Success (ParseOnly (Input "input.tex")) -> - pure () - other -> - assertFailure - ("unexpected parse-only parse: " <> showParserResult other) - case parseCommandArguments ["input.tex"] of - Success - (Verify - (Input "input.tex") - VerificationOptions - { verificationStoreSelection = - Store.DefaultStore - }) -> - pure () - other -> - 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 - (Input "input.tex") - VerificationOptions - { verificationStoreSelection = - Store.FreshTemporaryStore - }) -> - pure () - other -> - assertFailure - ("unexpected verify parse: " <> showParserResult other) - -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"] - ] - \arguments -> - case parseCommandArguments arguments of - Failure _failure -> - pure () - other -> - assertFailure - ("conflicting options were accepted: " - <> 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 - Success selected -> - show selected - Failure failure -> - fst (Options.renderFailure failure "zf") - CompletionInvoked _completion -> - "completion invoked" - -versionNeedsNoInputOrStore :: Assertion -versionNeedsNoInputOrStore = - withCliFixture cliSource \fixture -> do - (exitCode, stdout, stderr) <- - runCliFixture fixture ["--version"] - exitCode `shouldBe` ExitSuccess - stdout `shouldContain` "Version 0.3.0.0" - stderr `shouldBe` "" - assertNoDefaultStore fixture - -parseOnlyUsesNoAuthority :: Assertion -parseOnlyUsesNoAuthority = - withCliFixture cliPreludeSyntaxSource \fixture -> do - writeNonExecutableFile (cliFixtureVampire fixture) - (exitCode, stdout, stderr) <- - runCliFixture - fixture - ["input.tex", "--parseonly"] - exitCode `shouldBe` ExitSuccess - stdout `shouldBe` "" - stderr `shouldBe` "" - assertNoDefaultStore fixture - -malformedSourceHasStableFailure :: Assertion -malformedSourceHasStableFailure = - withCliFixture malformedCliSource \fixture -> do - (exitCode, stdout, stderr) <- - runCliFixture - fixture - ["input.tex", "--parseonly"] - exitCode `shouldBe` ExitFailure 1 - stdout `shouldBe` "" - stderr `shouldContain` "Parsing failed: project:input.tex" - stderr `shouldContain` "input.tex 2:5" - stderr `shouldContain` "unconsumed word" - assertBool "does not print an internal error constructor" - (not ("SourceParseError" `List.isInfixOf` stderr)) - assertNoDefaultStore fixture - -invalidOutputPrecedesStoreStartup :: Assertion -invalidOutputPrecedesStoreStartup = - withCliFixture cliSource \fixture -> do - let dump = cliFixtureRoot fixture </> "dump" - Directory.removeFile - (cliFixtureRoot fixture </> "input.tex") - Directory.createDirectory dump - writeFile (dump </> "stale.p") "stale" - (exitCode, stdout, stderr) <- - runCliFixture fixture - ["input.tex", "--dump", "dump"] - exitCode `shouldBe` ExitFailure 2 - stdout `shouldBe` "" - stderr `shouldContain` "Verification output preflight failed:" - stderr `shouldContain` (Text.pack (show dump)) - stderr `shouldContain` "choose an absent or empty directory" - stderr `shouldContain` "stale.p" - assertNoDefaultStore fixture - -reportsCommittedHtmlPrefix :: Assertion -reportsCommittedHtmlPrefix = do - first <- checkedRelative "a.html" - second <- checkedRelative "nested/b.html" - failed <- checkedRelative "nested/c.html" - assertEqual - "deterministic committed prefix" - [ "HTML publication failed at \"nested/c.html\": disk full" - , "HTML files published before the failure: \"a.html\", \"nested/b.html\"" - ] - (HtmlOutput.renderHtmlPublicationError - (HtmlOutput.IncompleteHtmlPublication - [first, second] - failed - "disk full")) - where - checkedRelative path = - case safeRelativePath path of - Left problem -> - assertFailure - ("invalid test route " <> show path <> ": " <> show problem) - >> fail "unreachable" - Right relative -> - pure relative - -nestedHtmlRoutesPrecedeStoreStartup :: Assertion -nestedHtmlRoutesPrecedeStoreStartup = - withCliFixture nestedHtmlRootSource \fixture -> do - let root = cliFixtureRoot fixture - nested = root </> "a.html" - Directory.createDirectory nested - writeFile (root </> "a.tex") cliSource - writeFile (nested </> "b.tex") cliSource - (exitCode, stdout, stderr) <- - runCliFixture fixture ["input.tex", "--html"] - exitCode `shouldBe` ExitFailure 2 - stdout `shouldBe` "" - stderr `shouldContain` "HTML route planning failed:" - stderr `shouldContain` "\"a.html\"" - stderr `shouldContain` "\"a.html/b.html\"" - assertNoDefaultStore fixture - -removesFailedDumpTemporary :: Assertion -removesFailedDumpTemporary = - withTemporaryDirectory "felix-dump-atomic" \root -> do - let destination = root </> "1.p" - Directory.createDirectory destination - result <- Exception.try - (publishDumpFile destination "complete request") - :: IO (Either IOException ()) - case result of - Left _failure -> - pure () - Right () -> - assertFailure "dump publication unexpectedly succeeded" - contents <- List.sort <$> Directory.listDirectory root - assertEqual - "only the pre-existing final target remains" - ["1.p"] - contents - -dumpsExactExecutedRequest :: Assertion -dumpsExactExecutedRequest = - withCliFixture cliSource \fixture -> do - seedPackagedPreludeCache fixture - let captured = cliFixtureRoot fixture </> "captured.p" - writeExecutableScript - (cliFixtureVampire fixture) - [ "cat > " <> show captured - , "printf '%s\\n' '% SZS status Theorem for cli'" - ] - (exitCode, _stdout, stderr) <- - runCliFixture fixture - [ "input.tex" - , "--dump" - , "dump" - ] - exitCode `shouldBe` ExitSuccess - stderr `shouldContain` "Verification successful." - dumped <- ByteString.readFile - (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" </> "1-2.p") - -launchFailureDumpsNoRequest :: Assertion -launchFailureDumpsNoRequest = - withCliFixture cliSource \fixture -> do - seedPackagedPreludeCache fixture - writeNonExecutableFile (cliFixtureVampire fixture) - (exitCode, _stdout, stderr) <- - runCliFixture fixture - [ "input.tex" - , "--dump" - , "dump" - ] - exitCode `shouldBe` ExitFailure 2 - stderr `shouldContain` "ProverLaunchFailed" - assertBool "no request was dumped before process launch" - . not - =<< Directory.doesPathExist - (cliFixtureRoot fixture </> "dump" </> "1-1.p") - -dumpsOnlyExecutedPrefix :: Assertion -dumpsOnlyExecutedPrefix = - withCliFixture cliTwoSource \fixture -> do - seedPackagedPreludeCache fixture - writeExecutableScript - (cliFixtureVampire fixture) - [ "cat >/dev/null" - , "printf '%s\\n' '% SZS status CounterSatisfiable for cli'" - ] - (exitCode, _stdout, stderr) <- - runCliFixture fixture - [ "input.tex" - , "--dump" - , "dump" - ] - exitCode `shouldBe` ExitFailure 1 - stderr `shouldContain` "prover found countermodel" - assertBool "executed request was dumped" - =<< Directory.doesFileExist - (cliFixtureRoot fixture </> "dump" </> "1-1.p") - -- Prospective execution may start a source-later request before the - -- admission cursor observes this first rejection. Dump ownership is - -- therefore the actual executed subset, not a semantic prefix. - -dumpAndHtmlVerifyOnce :: Assertion -dumpAndHtmlVerifyOnce = - withCliFixture cliSource \fixture -> do - seedPackagedPreludeCache fixture - let countPath = cliFixtureRoot fixture </> "vampire-runs" - writeExecutableScript - (cliFixtureVampire fixture) - [ "cat >/dev/null" - , "printf '%s\\n' run >> " <> show countPath - , "printf '%s\\n' '% SZS status Theorem for cli'" - ] - (exitCode, _stdout, stderr) <- - runCliFixture fixture - [ "input.tex" - , "--dump" - , "dump" - , "--html" - ] - exitCode `shouldBe` ExitSuccess - stderr `shouldContain` "Verification successful." - runs <- List.lines <$> readFile countPath - assertEqual "one semantic verification" ["run"] runs - assertBool "request dump was published" - =<< Directory.doesFileExist - (cliFixtureRoot fixture </> "dump" </> "1-1.p") - assertBool "root HTML page was published" - =<< Directory.doesFileExist - (cliFixtureRoot fixture </> "html" </> "input.html") - assertBool "HTML support asset was published" - =<< Directory.doesFileExist - (cliFixtureRoot fixture - </> "html" - </> "_static" - </> "naproche-html.js") - -semanticFailurePublishesNoHtml :: Assertion -semanticFailurePublishesNoHtml = - withCliFixture cliSource \fixture -> do - seedPackagedPreludeCache fixture - writeExecutableScript - (cliFixtureVampire fixture) - [ "cat >/dev/null" - , "printf '%s\\n' '% SZS status CounterSatisfiable for cli'" - ] - (exitCode, _stdout, stderr) <- - runCliFixture fixture - [ "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 - (cliFixtureVampire fixture) - [ "cat >/dev/null" - , "printf '%s\\n' '% SZS status Theorem for cli'" - ] - (exitCode, stdout, stderr) <- - runCliFixture fixture ["input.tex", "--html"] - exitCode `shouldBe` ExitFailure 2 - stdout `shouldBe` "" - stderr `shouldContain` "HTML preparation failed:" - stderr `shouldContain` "renderer data \"lexicon.tsv\" was not found" - assertBool "does not expose an ErrorCall" - (not ("ErrorCall" `List.isInfixOf` stderr)) - assertBool "failed preparation publishes no HTML" - . not - =<< 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 emptyReport Nowhere (CountermodelFound "") - , ExitFailure 1 - ) - , ( ProverFailed emptyReport Nowhere (ProverIndeterminate "") - , ExitFailure 2 - ) - ] - -emptyReport :: VerificationReport -emptyReport = - VerificationReport - { verificationDirectEscapes = [] - } - -runCliWithFakeVampire - :: [String] - -> IO (ExitCode, String, String) -runCliWithFakeVampire scriptLines = - runCliWithConfiguredVampire \vampirePath -> do - writeExecutableScript vampirePath - (["cat >/dev/null"] <> scriptLines) - -runCliWithConfiguredVampire - :: (FilePath -> IO ()) - -> IO (ExitCode, String, String) -runCliWithConfiguredVampire = - runCliWithSourceAndConfiguredVampire cliSource - -runCliWithSourceAndConfiguredVampire - :: String - -> (FilePath -> IO ()) - -> IO (ExitCode, String, String) -runCliWithSourceAndConfiguredVampire source prepareVampire = - withCliFixture source \fixture -> do - seedPackagedPreludeCache fixture - prepareVampire (cliFixtureVampire fixture) - runCliFixture fixture ["input.tex"] - -data CliFixture = CliFixture - { cliFixtureRoot :: !FilePath - , cliFixtureExecutable :: !FilePath - , cliFixtureVampire :: !FilePath - , cliFixtureCacheRoot :: !FilePath - , cliFixtureEnvironment :: ![(String, String)] - } - -withCliFixture - :: String - -> (CliFixture -> IO value) - -> IO value -withCliFixture source action = - withTemporaryDirectory "felix-cli" \temp -> do - zfExecutable <- requireZfExecutable - repositoryRoot <- Directory.getCurrentDirectory - let sourcePath = temp </> "input.tex" - vampirePath = temp </> "vampire" - libraryPath = temp </> "library" - debugPath = temp </> "debug" - cacheRoot = temp </> "cache" - Directory.createDirectory libraryPath - Directory.createDirectory debugPath - Directory.createDirectory cacheRoot - writeFile sourcePath source - ByteString.readFile - (repositoryRoot </> "library" </> "lexicon.tsv") - >>= ByteString.writeFile - (libraryPath </> "lexicon.tsv") - inheritedEnvironment <- getEnvironment - let processEnvironment = - setEnvironmentVariable - "XDG_CACHE_HOME" - cacheRoot - (setEnvironmentVariable - "NAPROCHE_ZF_VAMPIRE" - vampirePath - (setEnvironmentVariable - "NAPROCHE_LIB" - libraryPath - inheritedEnvironment)) - action - CliFixture - { cliFixtureRoot = temp - , cliFixtureExecutable = zfExecutable - , cliFixtureVampire = vampirePath - , cliFixtureCacheRoot = cacheRoot - , cliFixtureEnvironment = processEnvironment - } - -runCliFixture - :: CliFixture - -> [String] - -> IO (ExitCode, String, String) -runCliFixture fixture arguments = - readCreateProcessWithExitCode - ((proc - (cliFixtureExecutable fixture) - arguments) - { cwd = Just (cliFixtureRoot fixture) - , env = Just (cliFixtureEnvironment fixture) - }) - "" - --- | 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" - . not - =<< Directory.doesPathExist - (cliFixtureCacheRoot fixture </> "felix") - -writeExecutableScript :: FilePath -> [String] -> IO () -writeExecutableScript path scriptLines = do - writeFile path - (unlines (["#!/bin/sh"] <> scriptLines)) - permissions <- Directory.getPermissions path - 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" - case executable of - Just path -> - pure path - Nothing -> do - assertFailure "zf build tool is not available on PATH" - pure "zf" - -setEnvironmentVariable - :: String - -> String - -> [(String, String)] - -> [(String, String)] -setEnvironmentVariable name value environment = - (name, value) : List.filter ((/= name) . fst) environment - -cliSource :: String -cliSource = - unlines - [ "\\begin{proposition}\\label{cli_test}" - , " $\\forall x. x = x$." - , "\\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 - [ "\\begin{proposition}\\label{cli_gap}" - , " $\\forall x. x = x$." - , "\\end{proposition}" - , "\\begin{proof}" - , " Omitted." - , "\\end{proof}" - ] - -cliTwoSource :: String -cliTwoSource = - unlines - [ "\\begin{proposition}\\label{cli_first}" - , " $\\forall x. x = x$." - , "\\end{proposition}" - , "\\begin{proposition}\\label{cli_second}" - , " $\\forall y. y = y$." - , "\\end{proposition}" - ] - -malformedCliSource :: String -malformedCliSource = - unlines - [ "\\begin{proposition}\\label{malformed}" - , " This is not a proposition." - , "\\end{proposition}" - ] - -nestedHtmlRootSource :: String -nestedHtmlRootSource = - unlines - [ "\\import{a.tex}" - , "\\import{a.html/b.tex}" - ] - -withTemporaryDirectory :: String -> (FilePath -> IO a) -> IO a -withTemporaryDirectory template = - bracket create Directory.removePathForcibly - where - create = do - systemTemp <- Directory.getTemporaryDirectory - (path, handle) <- openTempFile systemTemp template - hClose handle - Directory.removeFile path - Directory.createDirectory path - pure path - -shouldContain :: String -> Text -> Assertion -shouldContain actual expected = - assertBool - ("expected " <> show actual <> " to contain " <> show expected) - (expected `Text.isInfixOf` Text.pack actual) - -shouldBe :: (Eq a, Show a, HasCallStack) => a -> a -> Assertion -shouldBe = - flip (assertEqual "") |