Migrate to `Felix` namespaceHEADhotg

1 files changed, 0 insertions, 799 deletions

diff --git a/source/Test/Unit/CommandLine.hs b/source/Test/Unit/CommandLine.hs
deleted file mode 100644
index 110e00d..0000000
--- a/source/Test/Unit/CommandLine.hs
+++ /dev/null
@@ -1,799 +0,0 @@
-{-# LANGUAGE OverloadedStrings #-}
-
-module 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 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 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 "")