From eafbbfb3b0805dc96c28d89bccab7ff77e9e7aec Mon Sep 17 00:00:00 2001 From: Jonathan Coates Date: Fri, 24 Feb 2023 03:37:53 +0000 Subject: [PATCH] Add an option to skip building Agda code (#190) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Closes #187. Currently [Agda code being embedded in code blocks](https://user-images.githubusercontent.com/4346137/217057817-b10648a1-9419-4f2a-969c-9a2ad9efc323.png) - I don't know if we want to add a special class to these, so they don't have a border? This is implemented by avoiding any build steps which would cause an Agda compile (specifically `_build/all-pages.json`). The alternative would be to rely on staler versions of those files, and simply not rebuild them. I think what I'm doing here is the correct thing to do. It keeps us honest with our task dependencies, and means `--skip-agda` works from a clean build directory. It does mean some site features (namely `agda://` links) won't work. Co-authored-by: Amélia --- support/shake/app/Main.hs | 43 +++++++++++++++++++--------- support/shake/app/Shake/AgdaRefs.hs | 12 ++++---- support/shake/app/Shake/LinkGraph.hs | 8 ++++-- support/shake/app/Shake/Markdown.hs | 12 ++++++-- support/shake/app/Shake/Options.hs | 10 +++++-- 5 files changed, 58 insertions(+), 27 deletions(-) diff --git a/support/shake/app/Main.hs b/support/shake/app/Main.hs index a38c69c00..b7d755eb9 100755 --- a/support/shake/app/Main.hs +++ b/support/shake/app/Main.hs @@ -77,22 +77,35 @@ rules = do to HTML with some additional post-processing steps (see 'buildMarkdown') -} "_build/html/*.html" %> \out -> do - let - modName = dropExtension (takeFileName out) - input = "_build/html0" modName + let modName = dropExtension (takeFileName out) modKind <- Map.lookup modName <$> getOurModules + agdaRefs <- agdaRefs + + skipAgda <- getSkipAgda + if skipAgda + then + let + input = case modName of + "all-pages" -> "_build/all-pages" + _ -> "src" map (\c -> if c == '.' then '/' else c) modName + in + case modKind of + Just WithText -> buildMarkdown agdaRefs modName (input <.> ".lagda.md") out + _ -> copyFile' (input <.> ".agda") out -- Wrong, but eh! + else + let input = "_build/html0" modName in + case modKind of + Just WithText -> do buildMarkdown agdaRefs modName (input <.> ".md") out + _ -> copyFile' (input <.> ".html") out - case modKind of - Just WithText -> do - agdaRefs <- agdaRefs - buildMarkdown agdaRefs (input <.> ".md") out - _ -> copyFile' (input <.> ".html") out "_build/search/*.json" %> \out -> need ["_build/html" takeFileName out -<.> "html"] "_build/html/static/search.json" %> \out -> do + skipAgda <- getSkipAgda modules <- filter ((==) WithText . snd) . Map.toList <$> getOurModules - let searchFiles = "_build/all-types.json":map (\(x, _) -> "_build/search" x <.> "json") modules + let searchFiles = (if skipAgda then [] else ["_build/all-types.json"]) + ++ map (\(x, _) -> "_build/search" x <.> "json") modules searchData :: [[SearchTerm]] <- traverse readJSONFile searchFiles liftIO $ encodeFile out (concat searchData) @@ -170,7 +183,7 @@ rules = do -- Profit! data ArgOption - = ASkipTypes + = AFlag Option | AWatching (Maybe String) deriving (Eq, Show) @@ -214,15 +227,17 @@ main = do ourOptsDescrs = [ Option "w" ["watch"] (OptArg AWatching "COMMAND") - "Start 1lab-shake in watch mode. Starts a persistent process which runs a subset of build tasks for \ - \interactive editing. Implies --skip-types. Optionally takes a command to run after the build has finished." - , Option [] ["skip-types"] (NoArg ASkipTypes) + "Start 1lab-shake in watch mode. Starts a persistent process which runs a subset of build tasks for \ + \interactive editing. Implies --skip-types.\nOptionally takes a command to run after the build has finished." + , Option [] ["skip-types"] (NoArg (AFlag SkipTypes)) "Skip generating type tooltips when compiling Agda to HTML." + , Option [] ["skip-agda"] (NoArg (AFlag SkipAgda)) + "Skip typechecking Agda. Markdown files are read from src/ directly." ] parseOptions :: [ArgOption] -> (Maybe String, [Option]) parseOptions [] = (Nothing, []) - parseOptions (ASkipTypes:xs) = (SkipTypes:) <$> parseOptions xs + parseOptions (AFlag f:xs) = (f:) <$> parseOptions xs parseOptions (AWatching watching:xs) = let (_, xs') = parseOptions xs in (watching, Watching:xs') diff --git a/support/shake/app/Shake/AgdaRefs.hs b/support/shake/app/Shake/AgdaRefs.hs index f1dad0d15..d8f7baf81 100644 --- a/support/shake/app/Shake/AgdaRefs.hs +++ b/support/shake/app/Shake/AgdaRefs.hs @@ -26,10 +26,12 @@ newtype AgdaRefs = AgdaRefs { unAgdaRefs :: HM.HashMap Text Text } getAgdaRefs :: Rules (Action AgdaRefs) getAgdaRefs = versioned 1 do rule <- newCache \() -> do - types :: [Identifier] <- readJSONFile "_build/all-types.json" - pure . AgdaRefs . HM.fromList . concatMap toModuleIdent $ types + types :: [Identifier] <- readJSONFile "_build/all-types.json" + pure . AgdaRefs . HM.fromList . concatMap toModuleIdent $ types - pure (rule ()) + pure do + skipAgda <- getSkipAgda + if skipAgda then pure . AgdaRefs $ mempty else rule () where toModuleIdent :: Identifier -> [(Text, Text)] @@ -53,8 +55,8 @@ parseAgdaLink modname fileIds x@(TagOpen "a" attrs) case HM.lookup ident (unAgdaRefs fileIds) of Just href -> pure $ TagOpen "a" (emplace [("href", href)] attrs) _ -> do - watching <- getWatching - unless watching $ error $ "Could not find Agda link " ++ Text.unpack ident ++ " in " ++ modname + skipTypes <- getSkipTypes + unless skipTypes $ error $ "Could not find Agda link " ++ Text.unpack ident ++ " in " ++ modname pure x parseAgdaLink _ _ x = pure x diff --git a/support/shake/app/Shake/LinkGraph.hs b/support/shake/app/Shake/LinkGraph.hs index c3e3f0b20..c1ddd3a69 100644 --- a/support/shake/app/Shake/LinkGraph.hs +++ b/support/shake/app/Shake/LinkGraph.hs @@ -55,15 +55,17 @@ linksRules = do -- graph of module names *with no self-loops*. -- While building this file, we also check links against the set of anchors above. "_build/html/static/links.json" %> \out -> do - watching <- getWatching + skipTypes <- getSkipTypes + skipAgda <- getSkipAgda + ourModules <- getOurModules - anchors <- anchors () + anchors <- if skipAgda then pure mempty else anchors () links :: [[String]] <- catMaybes . concat <$> forM (Map.keys ourModules) \source -> do let input = "_build/html" source <.> "html" need [input] links <- Set.toList . getInternalLinks source . parseTags <$> liftIO (Text.readFile input) forM links \link -> do - unless (watching || Text.pack link `Set.member` anchors) do + unless (skipTypes || Text.pack link `Set.member` anchors) do error $ "Could not find link target " ++ link ++ " in " ++ source let target = dropExtension . fst $ break (== '#') link pure if ( target /= source diff --git a/support/shake/app/Shake/Markdown.hs b/support/shake/app/Shake/Markdown.hs index 757fd6a80..1b543d5b6 100644 --- a/support/shake/app/Shake/Markdown.hs +++ b/support/shake/app/Shake/Markdown.hs @@ -42,18 +42,20 @@ import Text.Pandoc import Shake.LinkReferences import Shake.SearchData import Shake.AgdaRefs +import Shake.Options import Shake.KaTeX import Shake.Git import HTML.Emit buildMarkdown :: AgdaRefs -- ^ All Agda identifiers in the codebase. + -> String -- ^ The name of the Agda module. -> FilePath -- ^ Input markdown file, produced by the Agda compiler. -> FilePath -- ^ Output HTML file. -> Action () -buildMarkdown refs input output = do +buildMarkdown refs modname input output = do gitCommit <- gitCommit - let modname = dropDirectory1 (dropDirectory1 (dropExtension input)) + skipAgda <- getSkipAgda need [templateName, bibliographyName, autorefsName, input] @@ -86,7 +88,11 @@ buildMarkdown refs input output = do liftIO $ Dir.createDirectoryIfMissing False "_build/diagrams" let refMap = Map.fromList $ map (\x -> (Cite.unItemId . Cite.referenceId $ x, x)) references - markdown <- walkM (patchInline refMap autorefs) . walk patchInlines . linkReferences modname $ markdown + markdown <- + walkM (patchInline refMap autorefs) + . walk patchInlines + . (if skipAgda then id else linkReferences modname) + $ markdown (markdown, MarkdownState references dependencies) <- runWriterT (walkM patchBlock markdown) need dependencies diff --git a/support/shake/app/Shake/Options.hs b/support/shake/app/Shake/Options.hs index 049dc0af2..84e3c5753 100644 --- a/support/shake/app/Shake/Options.hs +++ b/support/shake/app/Shake/Options.hs @@ -6,6 +6,7 @@ module Shake.Options ( Option(..) , setOptions , getSkipTypes + , getSkipAgda , getWatching ) where @@ -16,6 +17,7 @@ import GHC.Generics (Generic) data Option = SkipTypes -- ^ Skip generating types when emitting HTML. + | SkipAgda -- ^ Skip typechecking Agda, emitting the markdown directly. | Watching -- ^ Launch in watch mode. Prevents some build tasks running. deriving (Eq, Show, Typeable, Generic) @@ -31,9 +33,13 @@ setOptions options = do _ <- addOracle (pure . getOption) pure () where - getOption SkipTypes = SkipTypes `elem` options || Watching `elem` options + getOption SkipTypes = SkipTypes `elem` options + || SkipAgda `elem` options + || Watching `elem` options + getOption SkipAgda = SkipAgda `elem` options getOption Watching = Watching `elem` options -getSkipTypes, getWatching :: Action Bool +getSkipTypes, getSkipAgda, getWatching :: Action Bool getSkipTypes = askOracle SkipTypes +getSkipAgda = askOracle SkipAgda getWatching = askOracle Watching