path: root/source/Test/Unit/CommandLine.hs

{-# 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 "")