Add an option to skip building Agda code (#190)

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 <[email protected]>

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')

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
 

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

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
 

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