diff options
Diffstat (limited to 'source/Felix/Test/Unit/CommandLine.hs')
| -rw-r--r-- | source/Felix/Test/Unit/CommandLine.hs | 799 |
1 files changed, 799 insertions, 0 deletions
diff --git a/source/Felix/Test/Unit/CommandLine.hs b/source/Felix/Test/Unit/CommandLine.hs new file mode 100644 index 0000000..f2a4a10 --- /dev/null +++ b/source/Felix/Test/Unit/CommandLine.hs @@ -0,0 +1,799 @@ +{-# LANGUAGE OverloadedStrings #-} + +module Felix.Test.Unit.CommandLine (unitTests) where + +import Base +import Felix.CommandLine +import Felix.Output.Atomic qualified as Atomic +import Felix.Source (safeRelativePath) +import Felix.Store qualified as Store +import Felix.Verification qualified as Verification +import Felix.Provers qualified as Provers +import Felix.Render.Html.Output qualified as HtmlOutput +import Felix.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 Data.Text.Encoding qualified as TextEncoding +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 "felix") + 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 + (Atomic.writeBytesAtomically + destination + (TextEncoding.encodeUtf8 "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 emptySlowReport, ExitSuccess) + , (VerificationCompletedWithGaps emptyReport emptySlowReport, ExitSuccess) + , ( VerificationRejected + emptyReport + (Verification.FailedVerification + Nowhere + (Verification.CountermodelFailure "")) + emptySlowReport + , ExitFailure 1 + ) + , ( VerificationRejected + emptyReport + (Verification.FailedVerification + Nowhere + (Verification.IndeterminateFailure "")) + emptySlowReport + , ExitFailure 2 + ) + , ( VerificationCheckingRejected + emptyReport + (Verification.VerificationModuleSchedulerInvariant "test") + emptySlowReport + , ExitFailure 2 + ) + ] + +emptyReport :: Verification.VerificationReport +emptyReport = + Verification.VerificationReport + { Verification.verificationDirectEscapes = [] + } + +emptySlowReport :: Provers.SlowAtpReport +emptySlowReport = Provers.SlowAtpReport 0 [] + +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 + felixExecutable <- requireFelixExecutable + 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 + "FELIX_VAMPIRE" + vampirePath + (setEnvironmentVariable + "NAPROCHE_LIB" + libraryPath + inheritedEnvironment)) + action + CliFixture + { cliFixtureRoot = temp + , cliFixtureExecutable = felixExecutable + , 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" + +requireFelixExecutable :: IO FilePath +requireFelixExecutable :: IO FilePath + = do + executable <- Directory.findExecutable "felix" + case executable of + Just path -> + pure path + Nothing -> do + assertFailure "felix build tool is not available on PATH" + pure "felix" + +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 "") |