content: {-# LANGUAGE DeriveAnyClass #-}
  {-# LANGUAGE DeriveGeneric #-}
  {-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
  
  {-# HLINT ignore "Redundant <&>" #-}
  {-# HLINT ignore "Monad law, left identity" #-}
  
  module Main where
  
  import Buildfile.Author (Author (..))
  import Buildfile.Book (Book (..), Chapter (..), ChapterTable, Part (..), fromBook, nextChapter, previousChapter)
  import Buildfile.Contributor (Contributor (..))
  import Buildfile.Script qualified as Script (fromFilePath, inline)
  import Buildfile.Stylesheet (Stylesheet (stylesheetEnabled, stylesheetId))
  import Buildfile.Stylesheet qualified as Stylesheet (alternate, fromFilePath)
  import Control.Exception (assert, catch)
  import Control.Monad (forM, forM_, unless, when, (>=>))
  import Control.Monad.Except (MonadError (throwError))
  import Control.Monad.IO.Class (MonadIO)
  import Control.Monad.State (evalState)
  import Data.Base64.Types qualified as Base64
  import Data.ByteString.Lazy qualified as LazyByteString
  import Data.ByteString.Lazy.Base64 qualified as Base64
  import Data.Default.Class (Default (def))
  import Data.Digest.Pure.SHA qualified as Digest (bytestringDigest, sha512)
  import Data.Either (fromRight, isRight)
  import Data.Function (on, (&))
  import Data.Functor ((<&>))
  import Data.Hashable (Hashable)
  import Data.List (isPrefixOf, sortBy)
  import Data.List qualified as List
  import Data.Maybe (fromMaybe, isJust, isNothing, maybeToList)
  import Data.Text (Text)
  import Data.Text qualified as Text
  import Data.Text.Encoding qualified as Text
  import Data.Text.Lazy qualified as LazyText
  import Data.Text.Lazy.Encoding qualified as LazyText
  import Data.Traversable (for)
  import GHC.Generics (Generic)
  import GHC.Stack.Types (HasCallStack)
  import Shoggoth.Agda qualified as Agda
  import Shoggoth.Configuration
  import Shoggoth.Metadata
  import Shoggoth.PostInfo
  import Shoggoth.Prelude
  import Shoggoth.Routing (Router (..), RoutingTable, Stages (..), permalinkRouter)
  import Shoggoth.Routing qualified as Route
  import Shoggoth.TagSoup qualified as TagSoup
  import Shoggoth.Template.Pandoc (Extension (..), HTMLMathMethod (..), HighlightStyle, Inlines, Lang, Locale, MetaValue, ObfuscationMethod (..), Pandoc (..), ReaderOptions (..), Reference, WriterOptions (..), defaultKaTeXURL, extensionsFromList, runPandoc, runPandocWith)
  import Shoggoth.Template.Pandoc qualified as Pandoc
  import Shoggoth.Template.Pandoc.Builder qualified as Builder
  import Shoggoth.Template.Pandoc.Citeproc qualified as Citeproc
  import System.Directory (findExecutable, makeAbsolute)
  import System.Exit (ExitCode (..), exitWith)
  import Text.Printf (printf)
  
  outDir, tmpDir :: FilePath
  outDir = "_site"
  tmpDir = "_cache"
  
  dataDir, authorDir, contributorDir, bibliographyFile, tableOfContentsFile :: FilePath
  dataDir = "data"
  authorDir = dataDir </> "authors"
  contributorDir = dataDir </> "contributors"
  tableOfContentsFile = dataDir </> "tableOfContents.yml"
  bibliographyFile = dataDir </> "bibliography.bib"
  
  bookDir, chapterDir, courseDir :: FilePath
  bookDir = "book"
  chapterDir = "src"
  courseDir = "courses"
  
  epubDir, epubFontsDir, epubStyleDir, epubTemplateDir :: FilePath
  epubDir = bookDir </> "epub"
  epubFontsDir = epubDir </> "fonts"
  epubStyleDir = epubDir </> "sass"
  epubTemplateDir = epubDir </> "templates"
  
  webDir, webAssetDir, webPostDir, webStyleDir, webTemplateDir :: FilePath
  webDir = "web"
  webAssetDir = webDir </> "assets"
  webPostDir = webDir </> "posts"
  webStyleDir = webDir </> "sass"
  webTemplateDir = webDir </> "templates"
  
  tmpRawAgdaHtmlDir, tmpAgdaHtmlDir, tmpBodyHtmlDir, tmpEpubDir :: FilePath
  tmpRawAgdaHtmlDir = tmpDir </> "raw_agda_html" -- Compile literate Agda code blocks to raw HTML
  tmpAgdaHtmlDir = tmpDir </> "agda_html" -- Fix Agda HTML output
  tmpBodyHtmlDir = tmpDir </> "body_html" -- Compile Markdown to HTML
  tmpEpubDir = tmpDir </> "epub"
  
  --------------------------------------------------------------------------------
  -- Rules
  
  main :: IO ()
  main = do
    absTmpDir <- makeAbsolute tmpDir
    shakeArgs
      shakeOptions
        { shakeFiles = tmpDir,
          shakeProgress = progressSimple,
          shakeExtra =
            mempty
              & addShakeExtra (OutputDirectory outDir)
              & addShakeExtra (CacheDirectory absTmpDir)
              & addShakeExtra (TemplateDirectory webTemplateDir)
              & addShakeExtra readerOpts
              & addShakeExtra writerOpts
        }
      $ do
        --------------------------------------------------------------------------------
        -- Agda resource & libraries
  
        agda <- newResource "agda" 1
        Agda.makeVersionOracle
        Agda.makeStandardLibraryOracle "standard-library"
  
        getAgdaFileInfo <- newCache $ \src -> do
          project <- failOnError $ getProject src
          agdaLibraries <- getAgdaLibrariesForProject project
          fileInfo@Agda.AgdaFileInfo {library, libraryIncludePath, outputFileForHtml, moduleName} <-
            failOnError $ Agda.resolveFileInfo agdaLibraries src
          -- NOTE: Each Agda file compiles to its own directory, i.e., the
          --       `agdaHtmlPathName` is included in the path. Otherwise,
          --       Agda will regenerate files it already generated in a
          --       previous task, and you'll get an error saying that the
          --       temporary file has "changed since being depended upon".
          let libraryRawAgdaHtmlDir = tmpRawAgdaHtmlDir </> Text.unpack moduleName </> Agda.libraryRoot library </> libraryIncludePath
          let rawAgdaHtmlPath = libraryRawAgdaHtmlDir </> outputFileForHtml
          let agdaHtmlPath = tmpAgdaHtmlDir </> replaceExtensions src (takeExtension outputFileForHtml)
          return (RichAgdaFileInfo fileInfo libraryRawAgdaHtmlDir rawAgdaHtmlPath agdaHtmlPath project agdaLibraries)
  
        --------------------------------------------------------------------------------
        -- Routing table
  
        let postOrPermalinkRouter :: FilePath -> Action FilePath
            postOrPermalinkRouter src
              | isPostSource src = do
                  PostInfo {..} <- failOnError $ parsePostSource (takeFileName src)
                  return $ outDir </> postYear </> postMonth </> postDay </> postSlug </> "index.html"
              | otherwise = permalinkRouter src
  
        let postOrPermalinkRouterWithAgda :: FilePath -> Action Stages
            postOrPermalinkRouterWithAgda src = do
              let bodyHtml = tmpBodyHtmlDir </> replaceExtensions src "html"
              out <- postOrPermalinkRouter src
              let commonStages = "body_html" :@ bodyHtml :> Output out
              if Agda.isAgdaFile src
                then do
                  AgdaFileInfo {rawAgdaHtmlPath, agdaHtmlPath} <- getAgdaFileInfo src
                  return $ rawAgdaHtmlPath :> "agda_html" :@ agdaHtmlPath :> commonStages
                else return commonStages
  
        let ?routingTable =
              mconcat
                [ -- Book (Web Version)
                  ["README.md"] |-> postOrPermalinkRouterWithAgda,
                  ["CONTRIBUTING.md"] |-> postOrPermalinkRouterWithAgda,
                  [webDir </> "TableOfContents.md"] |-> postOrPermalinkRouterWithAgda,
                  [chapterDir </> "plfa" <//> "*.md"] *|-> postOrPermalinkRouterWithAgda,
                  -- Book (Standalone HTML)
                  Route.create (outDir </> "plfa.html"),
                  -- Book (EPUB Version)
                  Route.create (outDir </> "plfa.epub"),
                  -- Announcements
                  [webDir </> "Announcements.md"] |-> postOrPermalinkRouterWithAgda,
                  [webDir </> "rss.xml"] |-> outDir </> "rss.xml",
                  [webPostDir <//> "*.md"] *|-> postOrPermalinkRouterWithAgda,
                  -- Documentation
                  [webDir </> "Citing.md"] |-> postOrPermalinkRouterWithAgda,
                  [webDir </> "Notes.md"] |-> postOrPermalinkRouterWithAgda,
                  [webDir </> "StyleGuide.md"] |-> postOrPermalinkRouterWithAgda,
                  -- Courses
                  [courseDir <//> "*.md"] *|-> postOrPermalinkRouterWithAgda,
                  [courseDir <//> "*.pdf"] *|-> \src -> outDir </> makeRelative courseDir src,
                  -- Assets
                  [webDir </> "404.md"] |-> permalinkRouter,
                  [webStyleDir </> "light.scss"] |-> outDir </> "assets/css/light.css",
                  [webStyleDir </> "dark.scss"] |-> outDir </> "assets/css/dark.css",
                  Route.create (outDir </> "assets/css/highlight.css"),
                  [webAssetDir <//> "*"] *|-> \src -> outDir </> "assets" </> makeRelative webAssetDir src
                ]
  
        --------------------------------------------------------------------------------
        -- Caches
  
        getAuthors <- newCache $ \() -> do
          authorFiles <- getDirectoryFiles authorDir ["*.yml"]
          authors <- traverse (\src -> readYaml $ authorDir </> src) authorFiles
          return (authors :: [Author])
        let ?getAuthors = getAuthors
  
        getContributors <- newCache $ \() -> do
          contributorFiles <- getDirectoryFiles "" [contributorDir </> "*.yml"]
          contributors <- traverse readYaml contributorFiles
          let sortedContributors = sortBy (compare `on` contributorCount) contributors
          return (sortedContributors :: [Contributor])
  
        getTableOfContents <- newCache $ \() -> do
          readYaml @Book tableOfContentsFile
        let ?getTableOfContents = getTableOfContents
  
        getChapterTable <- newCache $ \() -> do
          fromBook <$> getTableOfContents ()
        let ?getChapterTable = getChapterTable
  
        getDefaultMetadata <- newCache $ \() -> do
          metadata <- readYaml @Metadata (dataDir </> "metadata.yml")
          authorField <- constField "author" <$> ?getAuthors ()
          buildDateField <- currentDateField "%Y-%m" "build_date"
          buildDateRfc822Field <- currentDateField rfc822DateFormat "build_date_rfc822"
          return $ mconcat [metadata, authorField, buildDateField, buildDateRfc822Field]
        let ?getDefaultMetadata = getDefaultMetadata
  
        getReferences <- newCache $ \() -> do
          bibliographyFileBody <- readFile' bibliographyFile
          bibliographyFileDoc@(Pandoc meta _) <- runPandoc $ Pandoc.readBibTeX readerOpts bibliographyFileBody
          case Pandoc.lookupMeta "references" meta of
            Just references -> return references
            Nothing -> fail $ printf "Could not read references from '%s'" bibliographyFile
        let ?getReferences = getReferences
  
        getAgdaLinkFixer <- newCache $ \src -> do
          info@AgdaFileInfo {moduleName, project, libraries} <- getAgdaFileInfo src
          standardLibrary <- Agda.getStandardLibrary
          Agda.makeAgdaLinkFixer (Just standardLibrary) (List.delete standardLibrary libraries) []
  
        getTemplateFile <- Pandoc.makeCachedTemplateFileGetter
        let ?getTemplateFile = getTemplateFile
  
        getDigest <- newCache $ \src ->
          getMode >>= \case
            Development -> return Nothing
            Production -> do
              need [src]
              liftIO $ do
                stream <- LazyByteString.readFile src
                let digest = Digest.sha512 stream
                return . Just $ "sha512-" <> Base64.extractBase64 (Base64.encodeBase64 (Digest.bytestringDigest digest))
        let ?getDigest = getDigest
  
        --------------------------------------------------------------------------------
        -- Phony targets
  
        "build" ~> do
          need =<< Route.outputs
  
        let clean = do
              removeFilesAfter tmpRawAgdaHtmlDir ["//*"]
              removeFilesAfter tmpAgdaHtmlDir ["//*"]
              removeFilesAfter tmpBodyHtmlDir ["//*"]
              removeFilesAfter tmpEpubDir ["//*"]
  
        "clean" ~> clean
  
        let clobber = do
              clean
              removeFilesAfter outDir ["//*"]
  
        "clobber" ~> clobber
  
        --------------------------------------------------------------------------------
        -- Table of Contents
  
        let getTableOfContentsField () = do
              tocMetadata <- toMetadata <$> getTableOfContents ()
              tocResolved <- resolveIncludes (fmap fst . getFileWithMetadata) tocMetadata
              return $ constField "toc" tocResolved
  
        -- Build /
        outDir </> "index.html" %> \out -> do
          src <- Route.source out
          tocField <- getTableOfContentsField ()
          (fileMetadata, indexMarkdownTemplate) <- getFileWithMetadata src
          stylesheetField <- getStylesheetField
          scriptField <- getScriptField
          scriptInBodyField <- getScriptInBodyField
          let metadata = mconcat [tocField, fileMetadata, stylesheetField, scriptField, scriptInBodyField]
          return indexMarkdownTemplate
            >>= Pandoc.applyAsTemplate metadata
            >>= markdownToHtml5
            >>= Pandoc.applyTemplates ["page.html", "default.html"] metadata
            >>= writeHtml5 outDir out
  
        --------------------------------------------------------------------------------
        -- Compile Markdown & Agda to HTML
  
        -- Stage 1: Compile literate Agda code blocks to raw HTML
        tmpRawAgdaHtmlDir <//> "*.md" %> \next -> do
          (src, prev) <- (,) <$> Route.source next <*> Route.prev next
          Agda.getVersion
          AgdaFileInfo {libraryRawAgdaHtmlDir, libraries} <- getAgdaFileInfo src
          need [prev]
          withResource agda 1 $
            Agda.compileTo Agda.Html libraries libraryRawAgdaHtmlDir prev
  
        -- Stage 2: Fix raw Agda HTML output
        tmpAgdaHtmlDir <//> "*.md" %> \next -> do
          (src, prev) <- (,) <$> Route.source next <*> Route.prev next
          need [prev]
          RichAgdaFileInfo {agdaFileInfo} <- getAgdaFileInfo src
          agdaLinkFixer <- getAgdaLinkFixer src
          readFileWithMetadata prev
            <&> snd
            <&> TagSoup.parseTagsOptions (TagSoup.parseOptionsEntities (const Nothing)) {TagSoup.optTagPosition = True}
            <&> Agda.runAgdaSoup . traverse (Agda.qualifyIdSoup agdaFileInfo . TagSoup.mapUrls agdaLinkFixer)
            <&> TagSoup.renderTagsOptions TagSoup.renderOptions {TagSoup.optEscape = id}
            >>= writeFile' next
  
        -- Stage 3: Compile Markdown to HTML
        tmpBodyHtmlDir <//> "*.html" %> \next -> do
          (src, prev, out) <- (,,) <$> Route.source next <*> Route.prev next <*> Route.output next
          readFile' prev
            >>= markdownToHtml5
            >>= writeFile' next
  
        -- Stage 4: Apply HTML templates
        outDir <//> "*.html" %> \out -> do
          (src, prev) <- (,) <$> Route.source out <*> Route.prev out
          (fileMetadata, htmlBody) <- getFileWithMetadata prev
          stylesheetField <- getStylesheetField
          scriptField <- getScriptField
          scriptInBodyField <- getScriptInBodyField
          let metadata = mconcat [fileMetadata, stylesheetField, scriptField, scriptField, scriptInBodyField]
          let htmlTemplates
                | isPostSource src = ["post.html", "default.html"]
                | otherwise = ["page.html", "default.html"]
          html <- Pandoc.applyTemplates htmlTemplates metadata htmlBody
          html <- postProcessHtml5 outDir out html
          writeFile' out html
  
        --------------------------------------------------------------------------------
        -- Posts
  
        let getPostsField () = do
              posts <- filter isPostSource <$> Route.sources
              postsMetadata <- forM posts $ \post -> do
                bodyHtml <- Route.anchor "body_html" post
                (fileMetadata, body) <- getFileWithMetadata bodyHtml
                let bodyHtmlField = constField "body_html" body
                url <- failOnError $ fileMetadata ^. "url"
                let htmlTeaserField = ignoreError $ htmlTeaserFieldFromHtml url body "teaser_html"
                let textTeaserField = ignoreError $ textTeaserFieldFromHtml body "teaser_plain"
                return $ mconcat [fileMetadata, bodyHtmlField, htmlTeaserField, textTeaserField]
              return $ constField "post" (reverse postsMetadata)
  
        -- Build /Announcements/index.html
        outDir </> "Announcements" </> "index.html" %> \out -> do
          src <- Route.source out
          postsField <- getPostsField ()
          (fileMetadata, indexMarkdownTemplate) <- getFileWithMetadata src
          stylesheetField <- getStylesheetField
          scriptField <- getScriptField
          scriptInBodyField <- getScriptInBodyField
          let metadata = mconcat [postsField, fileMetadata, stylesheetField, scriptField, scriptInBodyField]
          return indexMarkdownTemplate
            >>= Pandoc.applyAsTemplate metadata
            >>= markdownToHtml5
            >>= Pandoc.applyTemplates ["page.html", "default.html"] metadata
            >>= writeHtml5 outDir out
  
        -- Build /Acknowledgements/index.html
        outDir </> "Acknowledgements" </> "index.html" %> \out -> do
          src <- Route.source out
          contributorField <- constField "contributor" <$> getContributors ()
          (fileMetadata, acknowledgmentsMarkdownTemplate) <- getFileWithMetadata src
          stylesheetField <- getStylesheetField
          scriptField <- getScriptField
          scriptInBodyField <- getScriptInBodyField
          let metadata = mconcat [contributorField, fileMetadata, stylesheetField, scriptField, scriptInBodyField]
          return acknowledgmentsMarkdownTemplate
            >>= Pandoc.applyAsTemplate metadata
            >>= markdownToHtml5
            >>= Pandoc.applyTemplates ["page.html", "default.html"] metadata
            >>= writeHtml5 outDir out
  
        -- Build rss.xml
        outDir </> "rss.xml" %> \out -> do
          src <- Route.source out
          postsField <- getPostsField ()
          (fileMetadata, rssXmlTemplate) <- getFileWithMetadata src
          let metadata = mconcat [postsField, fileMetadata]
          return rssXmlTemplate
            >>= Pandoc.applyAsTemplate metadata
            >>= writeFile' out
  
        --------------------------------------------------------------------------------
        -- Assets
  
        -- Build 404.html
        outDir </> "404.html" %> \out -> do
          src <- Route.source out
          (fileMetadata, errorMarkdownBody) <- getFileWithMetadata src
          stylesheetField <- getStylesheetField
          scriptField <- getScriptField
          scriptInBodyField <- getScriptInBodyField
          let metadata = mconcat [fileMetadata, stylesheetField, scriptField, scriptInBodyField]
          return errorMarkdownBody
            >>= markdownToHtml5
            >>= Pandoc.applyTemplates ["page.html", "default.html"] metadata
            >>= writeHtml5 outDir out
  
        -- Build assets/css/light.css
        outDir </> "assets/css/light.css" %> \out -> do
          src <- Route.source out
          need =<< getDirectoryFiles "" [webStyleDir <//> "*.scss"]
          sass [] ["--load-path=" <> webStyleDir, "--style=compressed", src, out] Nothing
  
        -- Build assets/css/dark.css
        outDir </> "assets/css/dark.css" %> \out -> do
          src <- Route.source out
          need =<< getDirectoryFiles "" [webStyleDir <//> "*.scss"]
          sass [] ["--load-path=" <> webStyleDir, "--style=compressed", src, out] Nothing
  
        -- Build assets/css/highlight.css
        outDir </> "assets/css/highlight.css" %> \out -> do
          sass [] ["--style=compressed", out] (Just $ LazyText.pack highlightCss)
  
        -- Copy static assets
        outDir </> "assets" <//> "*" %> \out -> do
          src <- Route.source out
          copyFile' src out
  
        -- Copy course PDFs
        --
        -- TODO: build from source instead of copying
        -- TODO: remove PDFs from repository
        --
        outDir <//> "*.pdf" %> \out -> do
          src <- Route.source out
          copyFile' src out
  
        --------------------------------------------------------------------------------
        -- Standalone HTML
  
        outDir </> "plfa.html" %> \out -> do
          -- Require all assets, rss.xml, and standalone template:
          assets <- filter ((outDir </> "assets" <//> "*") ?==) <$> Route.outputs
          need assets
          need [outDir </> "rss.xml", webTemplateDir </> "standalone.html"]
  
          defaultMetadata <- ?getDefaultMetadata ()
  
          let routeChapter src =
                if Agda.isAgdaFile src then Route.anchor "agda_html" src else return src
  
          bookDoc <- makeBookDoc routeChapter
  
          standaloneHtmlTemplate <- Pandoc.compileTemplateFile (webTemplateDir </> "standalone.html")
  
          let writerOptsForStandaloneHtml =
                writerOpts
                  { writerTemplate = Just standaloneHtmlTemplate,
                    writerTableOfContents = True,
                    writerCiteMethod = Pandoc.Natbib,
                    writerWrapText = Pandoc.WrapPreserve,
                    writerTopLevelDivision = Pandoc.TopLevelPart,
                    writerTOCDepth = 2,
                    writerReferenceLocation = Pandoc.EndOfDocument
                  }
  
          let pandocToStandaloneHtml doc = do
                html5 <- runPandoc (Pandoc.writeHtml5String writerOptsForStandaloneHtml doc)
                html5 <- postProcessHtml5 outDir out html5
                runPandoc $ do
                  Pandoc.setResourcePath [outDir]
                  Pandoc.makeSelfContained html5
  
          return bookDoc
            >>= pandocToStandaloneHtml
            >>= writeFile' out
  
        --------------------------------------------------------------------------------
        -- EPUB
  
        -- Polish EPUB with Calibre
        outDir </> "plfa.epub" %> \out -> do
          let src = tmpEpubDir </> "plfa_unpolished.epub"
          need [src]
          maybeEbookPolish <- liftIO $ findExecutable "ebook-polish"
          case maybeEbookPolish of
            Nothing -> do
              putWarn "Could not find 'ebook-polish' on the PATH; plfa.epub is unpolished"
              copyFile' src out
            Just ebookPolish -> do
              command
                []
                ebookPolish
                [ "--smarten-punctuation",
                  "--remove-unused-css",
                  "--add-soft-hyphens",
                  "--upgrade-book",
                  "--jacket",
                  "--embed-fonts",
                  "--subset-fonts",
                  src,
                  out
                ]
  
        -- Build unpolished EPUB
        tmpEpubDir </> "plfa_unpolished.epub" %> \out -> do
          -- Require metadata and stylesheet
          need [tmpEpubDir </> "epub-metadata.xml", tmpEpubDir </> "style.css"]
  
          let routeChapter src =
                if Agda.isAgdaFile src then Route.anchor "agda_html" src else return src
  
          bookDoc <-
            makeBookDoc routeChapter
              <&> Pandoc.setMeta "css" [tmpEpubDir </> "style.css"]
              <&> Pandoc.setMeta "highlighting-css" highlightCss
  
          -- Set writer options
          epubMetadata <- readFile' (tmpEpubDir </> "epub-metadata.xml")
          epubFonts <- getDirectoryFiles "" [epubFontsDir </> "*.woff2"]
          epubTemplate <- Pandoc.compileTemplateFile (epubTemplateDir </> "epub.html")
  
          let writerOptsForEpub =
                writerOpts
                  { writerTemplate = Just epubTemplate,
                    writerTableOfContents = True,
                    writerCiteMethod = Pandoc.Natbib,
                    writerWrapText = Pandoc.WrapPreserve,
                    writerTopLevelDivision = Pandoc.TopLevelPart,
                    writerEpubMetadata = Just epubMetadata,
                    writerEpubFonts = epubFonts,
                    writerSplitLevel = 2,
                    writerTOCDepth = 2,
                    writerReferenceLocation = Pandoc.EndOfDocument
                  }
  
          epub <- runPandoc $ Pandoc.writeEPUB3 writerOptsForEpub bookDoc
          liftIO $ LazyByteString.writeFile out epub
  
        -- Build EPUB metadata
        tmpEpubDir </> "epub-metadata.xml" %> \out -> do
          let src = epubTemplateDir </> "epub-metadata.xml"
          defaultMetadata <- getDefaultMetadata ()
          contributors <- getContributors ()
          let metadata = mconcat [defaultMetadata, constField "contributor" contributors]
          readFile' src
            >>= Pandoc.applyAsTemplate metadata
            >>= writeFile' out
  
        -- Build EPUB stylesheet
        tmpEpubDir </> "style.css" %> \out -> do
          let src = epubStyleDir </> "style.scss"
          need =<< getDirectoryFiles "" [epubStyleDir <//> "*.scss"]
          sass [] ["--load-path=" <> epubStyleDir, "--style=compressed", src, out] Nothing
  
  --------------------------------------------------------------------------------
  -- Agda
  
  data Project
    = Main
    | Post
    | Course {courseId :: String}
    deriving (Show, Typeable, Eq, Generic, Hashable, Binary, NFData)
  
  getCourseId :: (MonadError String m) => FilePath -> m String
  getCourseId src
    | courseDir `List.isPrefixOf` src = return $ makeRelative courseDir (takeDirectory src)
    | otherwise = throwError $ printf "Courses must be in '%s', '%s':" courseDir src
  
  getProject :: (MonadError String m) => FilePath -> m Project
  getProject src
    | chapterDir `List.isPrefixOf` src = return Main
    | courseDir `List.isPrefixOf` src = Course <$> getCourseId src
    | webPostDir `List.isPrefixOf` src = return Post
    | otherwise = throwError $ printf "Not part of an Agda project: '%s'" src
  
  getAgdaLibrariesForProject :: Project -> Action [Agda.Library]
  getAgdaLibrariesForProject project = do
    standardLibrary <- Agda.getStandardLibrary
    return $
      case project of
        Main -> [standardLibrary, mainLibrary]
        Post -> [standardLibrary, mainLibrary, postLibrary]
        Course courseId -> [standardLibrary, mainLibrary, courseLibrary]
          where
            courseLibrary :: Agda.Library
            courseLibrary =
              Agda.Library
                { libraryName = Text.replace "/" "." (Text.pack courseId),
                  libraryRoot = courseDir </> courseId,
                  includePaths = ["."],
                  canonicalBaseUrl = "https://plfa.github.io/" <> Text.pack courseId
                }
  
  mainLibrary :: Agda.Library
  mainLibrary =
    Agda.Library
      { libraryName = "plfa",
        libraryRoot = chapterDir,
        includePaths = ["."],
        canonicalBaseUrl = "https://plfa.github.io/"
      }
  
  postLibrary :: Agda.Library
  postLibrary =
    Agda.Library
      { libraryName = "announcements",
        libraryRoot = webPostDir,
        includePaths = ["."],
        canonicalBaseUrl = "https://plfa.github.io/"
      }
  
  --------------------------------------------------------------------------------
  -- Posts
  
  -- match posts/YYYY-MM-DD-<slug><file-extensions>
  isPostSource :: FilePath -> Bool
  isPostSource src = isRight $ parsePostSource (makeRelative webPostDir src)
  
  -- match _site/YYYY/MM/DD/<slug>/index.html
  isPostOutput :: FilePath -> Bool
  isPostOutput out = isRight $ parsePostOutput (makeRelative outDir out)
  
  --------------------------------------------------------------------------------
  -- File Reader
  
  getScriptField ::
    ( ?getDigest :: FilePath -> Action (Maybe LazyText.Text),
      ?routingTable :: RoutingTable
    ) =>
    Action Metadata
  getScriptField = do
    anchorjs <- Script.fromFilePath (outDir </> "assets/js/anchor.js")
    darkmode <- Script.fromFilePath (outDir </> "assets/js/darkmode.js")
    main <- Script.fromFilePath (outDir </> "assets/js/main.js")
    return $ constField "script" [anchorjs, darkmode, main]
  
  getScriptInBodyField ::
    ( ?getDigest :: FilePath -> Action (Maybe LazyText.Text),
      ?routingTable :: RoutingTable
    ) =>
    Action Metadata
  getScriptInBodyField = do
    rubyTags <- Script.fromFilePath (outDir </> "assets/js/ruby-tags.js")
    return $ constField "scriptInBody" [rubyTags]
  
  getStylesheetField ::
    ( ?getDigest :: FilePath -> Action (Maybe LazyText.Text),
      ?routingTable :: RoutingTable
    ) =>
    Action Metadata
  getStylesheetField = do
    light <- Stylesheet.fromFilePath (outDir </> "assets/css/light.css")
    dark <- Stylesheet.alternate <$> Stylesheet.fromFilePath (outDir </> "assets/css/dark.css")
    return $ constField "stylesheet" [light, dark]
  
  getFileWithMetadata ::
    ( ?getDefaultMetadata :: () -> Action Metadata,
      ?getChapterTable :: () -> Action ChapterTable,
      ?routingTable :: RoutingTable
    ) =>
    FilePath ->
    Action (Metadata, Text)
  getFileWithMetadata cur = do
    (src, out, url) <- (,,) <$> Route.source cur <*> Route.output cur <*> Route.url cur
  
    -- Default metadata:
    defaultMetadata <- ?getDefaultMetadata ()
  
    -- Metadata from source file and body from current file:
    (head, body) <-
      if src == cur
        then do
          readFileWithMetadata src
        else do
          (head, _) <- readFileWithMetadata src
          (_, body) <- readFileWithMetadata cur
          return (head, body)
  
    let titleVariants = ignoreError $ titleVariantMetadata <$> head ^. "title"
    let sourceField = constField "source" src
    let bodyField = constField "body" body
    let urlField = constField "url" url
  
    -- Previous and next chapter URLs:
    chapterTable <- ?getChapterTable ()
    maybePrevUrl <- traverse Route.url (previousChapter chapterTable src)
    let prevField = ignoreNothing $ constField "prev" <$> maybePrevUrl
    maybeNextUrl <- traverse Route.url (nextChapter chapterTable src)
    let nextField = ignoreNothing $ constField "next" <$> maybeNextUrl
  
    -- Dates:
    modifiedDateField <- lastModifiedISO8601Field src "modified_date"
    let dateField = fromRight mempty $ postDateField "%a %-d %b, %Y" src "date"
    let dateRfc822Field = fromRight mempty $ postDateField rfc822DateFormat src "date_rfc822"
  
    let metadata =
          mconcat
            [ defaultMetadata,
              head,
              urlField,
              bodyField,
              titleVariants,
              sourceField,
              prevField,
              nextField,
              modifiedDateField,
              dateField,
              dateRfc822Field
            ]
  
    return (metadata, body)
  
  --------------------------------------------------------------------------------
  -- Create Pandoc document for book (for single-document formats)
  
  makeBookDoc ::
    ( ?getDefaultMetadata :: () -> Action Metadata,
      ?getChapterTable :: () -> Action ChapterTable,
      ?getTableOfContents :: () -> Action Book,
      ?getAuthors :: () -> Action [Author],
      ?getReferences :: () -> Action MetaValue,
      ?routingTable :: RoutingTable
    ) =>
    (FilePath -> Action FilePath) ->
    Action Pandoc
  makeBookDoc routeChapter = do
    -- Read the table of contents
    toc <- ?getTableOfContents ()
  
    -- Compose documents for each part
    parts <- for (zip [1 ..] (bookParts toc)) $ \(number, part) -> do
      -- Compose documents for each chapter
      chapters <- for (partChapters part) $ \chapter -> do
        -- Get chapter document
        let chapterSrc = chapterInclude chapter
        (chapterHtml, chapterUrl) <- (,) <$> routeChapter chapterSrc <*> Route.url chapterSrc
        (chapterMetadata, chapterBody) <- getFileWithMetadata chapterHtml
        Pandoc _ chapterBlocks <- Pandoc.markdownToPandoc chapterBody
        -- Get chapter title & ident
        chapterTitle <- failOnError $ chapterMetadata ^. "title"
        let chapterIdent = urlToIdent chapterUrl
        -- Compose chapter document
        let chapterDoc =
              Builder.divWith (chapterIdent, [], [("epub:type", chapterEpubType chapter)]) $
                Builder.header 2 (Builder.text chapterTitle)
                  <> Builder.fromList
                    ( chapterBlocks
                        & Pandoc.shiftHeadersBy 1
                        & Pandoc.withIds (qualifyIdent True chapterUrl)
                        & Pandoc.withUrls (qualifyAnchor chapterUrl)
                    )
        return chapterDoc
  
      -- Compose part document
      let partIdent = Text.pack $ "Part-" <> show @Int number
      let partDoc =
            Builder.divWith (partIdent, [], []) $
              Builder.header 1 (Builder.text (partTitle part))
                <> mconcat chapters
      return partDoc
  
    -- Get metadata
    defaultMetadata <- ?getDefaultMetadata ()
    title <- failOnError $ defaultMetadata ^. "pagetitle"
    author <- fmap authorName <$> ?getAuthors ()
    rights <- failOnError $ defaultMetadata ^. "license.name"
    date <- failOnError $ defaultMetadata ^. "build_date"
  
    -- Compose book
    return (Builder.doc (mconcat parts))
      <&> Pandoc.withUrls internalizeUrl
      >>= processCitations
      <&> Pandoc.setMeta "title" (Builder.str title)
      <&> Pandoc.setMeta "author" author
      <&> Pandoc.setMeta "rights" (Builder.str rights)
      <&> Pandoc.setMeta "date" (Builder.str date)
  
  internalizeUrl :: Url -> Url
  internalizeUrl url
    | isAbsoluteUrl url = "#" <> qualifyIdent False urlPath hashAndAnchor
    | otherwise = url
    where
      (urlPath, hashAndAnchor) = Text.breakOn "#" url
  
  qualifyAnchor :: Url -> Url -> Url
  qualifyAnchor urlPath url
    | "#" `Text.isPrefixOf` url = "#" <> qualifyIdent False urlPath url
    | otherwise = url
  
  qualifyIdent :: Bool -> Url -> Text -> Text
  qualifyIdent emptyAnchorMeansNoId urlPath hashAndAnchor
    | Text.null anchor = if emptyAnchorMeansNoId then "" else ident
    | otherwise = ident <> "_" <> anchor
    where
      anchor = Text.dropWhile (== '#') hashAndAnchor
      ident = urlToIdent urlPath
  
  urlToIdent :: Url -> Text
  urlToIdent url =
    assert (isNothing $ Text.find (== '#') url) $
      assert (isAbsoluteUrl url) $
        Text.intercalate "-" (filter (not . Text.null) (Text.splitOn "/" (removeIndexHtml url)))
  
  --------------------------------------------------------------------------------
  -- Node.js
  
  npmExec :: (HasCallStack, CmdResult r) => [CmdOption] -> String -> [String] -> Action r
  npmExec cmdOpts package args = do
    need ["package.json"]
    command (AddEnv "npm_config_yes" "true" : Traced package : Shell : cmdOpts) "npm" ("exec" : package : "--" : args)
  
  sass :: (HasCallStack, CmdResult r) => [CmdOption] -> [String] -> Maybe LazyText.Text -> Action r
  sass cmdOpts args maybeStdin = do
    let stdinCmdOpt = [StdinBS (LazyText.encodeUtf8 stdin) | stdin <- maybeToList maybeStdin]
    let stdinArg = ["--stdin" | isJust maybeStdin]
    npmExec (stdinCmdOpt <> cmdOpts) "sass" (stdinArg <> args)
  
  data CmdOutput r where
    OutputToFile :: FilePath -> CmdOutput ()
    OutputToText :: CmdOutput Text
  
  defaultHtmlMinifierArgs :: [String]
  defaultHtmlMinifierArgs =
    [ "--collapse-boolean-attributes",
      "--collapse-whitespace",
      "--minify-css",
      "--minify-js",
      "--minify-urls",
      "--quote-character=\\\"",
      "--remove-comments",
      "--remove-empty-attributes",
      "--remove-redundant-attributes",
      "--remove-script-type-attributes",
      "--remove-style-link-type-attributes"
    ]
  
  htmlMinifier :: (HasCallStack) => CmdOutput r -> [CmdOption] -> [String] -> LazyText.Text -> Action r
  htmlMinifier cmdOutput cmdOpts args stdin =
    getMode >>= \case
      Development -> do
        let body = Text.concat $ LazyText.toChunks stdin
        case cmdOutput of
          OutputToFile out -> writeFile' out body
          OutputToText -> return body
      Production -> do
        let stdinCmdOpt = StdinBS (LazyText.encodeUtf8 stdin)
        case cmdOutput of
          OutputToFile out ->
            npmExec (stdinCmdOpt : cmdOpts) "html-minifier" (["--output=" <> out] <> args)
          OutputToText -> do
            Stdout minifiedHtml <- npmExec (stdinCmdOpt : cmdOpts) "html-minifier" args
            return (Text.decodeUtf8 minifiedHtml)
  
  --------------------------------------------------------------------------------
  -- HTML5 post-processing
  --
  -- - removes "/index.html" from URLs
  -- - relativizes URLs
  -- - adds a default table header scope
  -- - minifies HTML using html-minifier
  
  writeHtml5 :: FilePath -> FilePath -> Text -> Action ()
  writeHtml5 outDir out html = do
    trackWrite [out]
    genericPostProcessHtml5 (OutputToFile out) outDir out html
  
  postProcessHtml5 :: FilePath -> FilePath -> Text -> Action Text
  postProcessHtml5 = genericPostProcessHtml5 OutputToText
  
  genericPostProcessHtml5 :: CmdOutput r -> FilePath -> FilePath -> Text -> Action r
  genericPostProcessHtml5 cmdOutput outDir out html = do
    let body =
          html
            & TagSoup.withUrls (removeIndexHtml . relativizeUrl outDir out)
            & TagSoup.addDefaultTableHeaderScope "col"
    let stdin = LazyText.fromChunks [body]
    htmlMinifier cmdOutput [] defaultHtmlMinifierArgs stdin
  
  -- | Convert Markdown to HTML5 using Pandoc.
  markdownToHtml5 :: (?getReferences :: () -> Action MetaValue) => Text -> Action Text
  markdownToHtml5 = Pandoc.markdownToPandoc >=> processCitations >=> Pandoc.pandocToHtml5
  
  -- | Process Markdown citations with citeproc using the references returned by @?getReferences@.
  processCitations :: (?getReferences :: () -> Action MetaValue) => Pandoc -> Action Pandoc
  processCitations doc = do
    references <- ?getReferences ()
    Pandoc.processCitations (Pandoc.setMeta "references" references doc)
  
  readerOpts :: ReaderOptions
  readerOpts =
    def
      { readerExtensions =
          extensionsFromList
            [ Ext_all_symbols_escapable,
              Ext_auto_identifiers,
              Ext_backtick_code_blocks,
              Ext_citations,
              Ext_footnotes,
              Ext_header_attributes,
              Ext_intraword_underscores,
              Ext_markdown_in_html_blocks,
              Ext_shortcut_reference_links,
              Ext_smart,
              Ext_superscript,
              Ext_subscript,
              Ext_strikeout,
              Ext_task_lists,
              Ext_yaml_metadata_block,
              Ext_raw_html,
              Ext_raw_attribute,
              Ext_fenced_code_blocks,
              Ext_backtick_code_blocks,
              Ext_fenced_divs,
              Ext_bracketed_spans
            ]
      }
  
  writerOpts :: WriterOptions
  writerOpts =
    def
      { writerHTMLMathMethod = KaTeX defaultKaTeXURL,
        writerEmailObfuscation = JavascriptObfuscation,
        writerHighlightStyle = Just highlightStyle
      }
  
  highlightStyle :: HighlightStyle
  highlightStyle = Pandoc.pygments
  
  highlightCss :: String
  highlightCss = Pandoc.styleToCss highlightStyle
  
  --------------------------------------------------------------------------------
  -- Agda file info
  
  data RichAgdaFileInfo = RichAgdaFileInfo
    { agdaFileInfo :: Agda.AgdaFileInfo,
      _libraryRawAgdaHtmlDir :: FilePath,
      _rawAgdaHtmlPath :: FilePath,
      _agdaHtmlPath :: FilePath,
      _project :: Project,
      _libraries :: [Agda.Library]
    }
    deriving (Show, Typeable, Eq, Generic, Hashable, Binary, NFData)
  
  pattern AgdaFileInfo ::
    Agda.Library ->
    FilePath ->
    FilePath ->
    Agda.ModuleName ->
    FilePath ->
    FilePath ->
    FilePath ->
    FilePath ->
    FilePath ->
    Project ->
    [Agda.Library] ->
    RichAgdaFileInfo
  pattern AgdaFileInfo
    { library,
      libraryIncludePath,
      modulePath,
      moduleName,
      outputFileForLaTeX,
      outputFileForHtml,
      libraryRawAgdaHtmlDir,
      rawAgdaHtmlPath,
      agdaHtmlPath,
      project,
      libraries
    } =
    RichAgdaFileInfo
      ( Agda.AgdaFileInfo
          library
          libraryIncludePath
          modulePath
          moduleName
          outputFileForLaTeX
          outputFileForHtml
        )
      libraryRawAgdaHtmlDir
      rawAgdaHtmlPath
      agdaHtmlPath
      project
      libraries
  
  --------------------------------------------------------------------------------
  -- Helper functions
  
  failOnError :: (MonadFail m) => Either String a -> m a
  failOnError = either fail return
  
  failOnNothing :: (MonadFail m) => String -> Maybe a -> m a
  failOnNothing msg = maybe (fail msg) return
  
  ignoreError :: (Monoid a) => Either String a -> a
  ignoreError = fromRight mempty
  
  ignoreNothing :: (Monoid a) => Maybe a -> a
  ignoreNothing = fromMaybe mempty
  
  rightToMaybe :: Either e a -> Maybe a
  rightToMaybe = either (const Nothing) Just
  