check markup validity in mangleMarkdown

Author: plt-amy

.gitignore

@@ -29,6 +29,10 @@ hie.yaml
 *.o-boot
 /rubtmp*
 
+*.eventlog
+*.prof
+*.html
+
 # LaTeX stuff that occasionally gets generated
 *.log
 *.synctex.gz

default.nix

@@ -2,6 +2,8 @@
   inNixShell ? false
   # Do we want the full Agda package for interactive use? Set to false in CI
 , interactive ? true
+  # Do we only want GHC?
+, ghcOnly ? false
 , system ? builtins.currentSystem
 }:
 let
@@ -68,7 +70,7 @@ in
         ".github"
       ] ./.;
 
-    nativeBuildInputs = deps;
+    nativeBuildInputs = if ghcOnly then [ our-ghc ] else deps;
 
     shellHook = ''
       export out=_build/site

src/1Lab/Equiv.lagda.md

@@ -562,6 +562,7 @@ x_1$. This square _also_ has a filler, connecting $\pi_0$ and $\pi_1$
 over the line $g\ y ≡ \pi\ i$.
 
 <div class=mathpar>
+
 ~~~{.quiver}
 \[\begin{tikzcd}
   {g\ y} && {g\ y} \\

src/Cat/Instances/MarkedGraphs.lagda.md

@@ -317,7 +317,7 @@ instead, which we encode in Agda via the following higher-inductive type.
       → Marking p q → Marking r s
       → Marking (p ++ r) (q ++ s)
     trunc : ∀ {x y} {p q : Path-in G.graph x y} → is-prop (Marking p q)
-  ```
+```
 
 <!--
 ```agda

src/Data/Char/Base.lagda.md

@@ -47,3 +47,4 @@ open P public renaming
 instance
   Discrete-Char : Discrete Char
   Discrete-Char = Discrete-inj' _ (primCharToNatInjective _ _)
+```

src/Meta/Traversable.lagda.md

@@ -40,3 +40,4 @@ sequence
       {a : Type ℓ}
   → F.₀ (M.₀ a) → M.₀ (F.₀ a)
 sequence = traverse id
+```

support/shake/app/Definitions.hs

@@ -41,12 +41,11 @@ import Development.Shake
 
 import GHC.Generics (Generic)
 
-import HTML.Backend (moduleName)
 
 import Text.Pandoc.Walk
 import Text.Pandoc
 
-import {-# SOURCE #-} Shake.Markdown (readLabMarkdown)
+import Shake.Modules (moduleName, getOurModules, ModKind (WithText), markdownSource)
 import Shake.Digest (shortDigest)
 
 newtype Mangled = Mangled { getMangled :: Text }
@@ -66,9 +65,9 @@ mangleLink = doit where
   wordChar '[' = True
   wordChar c = isAsciiLower c || isDigit c
 
-parseDefinitions :: MonadIO m => FilePath -> FilePath -> m Glossary
-parseDefinitions anchor input = liftIO do
-  Pandoc _meta markdown <- readLabMarkdown input
+parseDefinitions :: MonadIO m => (FilePath -> m Pandoc) -> FilePath -> FilePath -> m Glossary
+parseDefinitions read anchor input = do
+  Pandoc _meta markdown <- read input
   pure $ appEndo (query (definitionBlock input anchor) markdown) (Glossary mempty)
 
 data Definition = Definition
@@ -138,17 +137,18 @@ addDefinition key@(getMangled -> keyt) def (Glossary ge) = Glossary (go False ke
 definitionTarget :: Definition -> Text
 definitionTarget def = Text.pack (definitionModule def) <> ".html#" <> definitionAnchor def
 
-glossaryRules :: Rules ()
-glossaryRules = do
+glossaryRules :: (FilePath -> Action Pandoc) -> Rules ()
+glossaryRules read = do
   _ <- addOracleCache \(ModuleGlossaryQ fp) -> do
     need [fp]
     let modn = moduleName (dropExtensions (dropDirectory1 fp)) <.> "html"
-    traced "parsing definitions" (parseDefinitions modn fp)
+    parseDefinitions read modn fp
 
   _ <- addOracle \GlossaryQ -> do
-    md   <- fmap ("src" </>) <$> getDirectoryFiles "src" ["**/*.lagda.md"]
-    need md
-    outs <- askOracles (ModuleGlossaryQ <$> md)
+    mods <- Map.keys . Map.filter (== WithText) <$> getOurModules
+    files <- traverse markdownSource mods
+    need files
+    outs <- askOracles (ModuleGlossaryQ <$> files)
 
     let
       alldefs :: [(Mangled, Definition)]