diff --git a/.github/workflows/preview.yml b/.github/workflows/preview.yml
index d078985fe..1a876514b 100644
--- a/.github/workflows/preview.yml
+++ b/.github/workflows/preview.yml
@@ -51,7 +51,7 @@ jobs:
NIX_BUILD_SHELL: bash
build_command: |
set -eu
- 1lab-shake -j all --skip-agda
+ 1lab-shake -j all --skip-agda -b https://plt-amy.github.io/1lab-previews/pr-256/
eval "$installPhase"
cp -rv _build/site pr-${{ github.event.number }}
diff --git a/support/shake/app/Definitions.hs b/support/shake/app/Definitions.hs
index bb79f43d2..22bb57b28 100644
--- a/support/shake/app/Definitions.hs
+++ b/support/shake/app/Definitions.hs
@@ -127,7 +127,7 @@ addDefinition key@(getMangled -> keyt) def (Glossary ge) = Glossary (go False ke
_ -> Map.insert key def{definitionCopy = c} ge
definitionTarget :: Definition -> Text
-definitionTarget def = "/" <> Text.pack (definitionModule def) <> ".html#" <> definitionAnchor def
+definitionTarget def = Text.pack (definitionModule def) <> ".html#" <> definitionAnchor def
glossaryRules :: Rules ()
glossaryRules = do
diff --git a/support/shake/app/Main.hs b/support/shake/app/Main.hs
index 403ad4d4e..b4e374fd6 100755
--- a/support/shake/app/Main.hs
+++ b/support/shake/app/Main.hs
@@ -8,7 +8,7 @@ import Control.Exception
import qualified Data.Map.Strict as Map
import qualified Data.Set as Set
-import Data.Aeson
+import Data.Aeson hiding (Options, defaultOptions)
import Data.Bifunctor
import Data.Foldable
import Data.Either
@@ -183,11 +183,6 @@ rules = do
-- Profit!
-data ArgOption
- = AFlag Option
- | AWatching (Maybe String)
- deriving (Eq, Show)
-
main :: IO ()
main = do
args <- getArgs
@@ -196,10 +191,13 @@ main = do
exitFailure
let (opts, extra, errs) = getOpt Permute optDescrs args
- (shakeOpts, ourOpts) = partitionEithers opts
+ (shakeOpts, ourOpts_) = partitionEithers opts
(errs', shakeOpts') = first (++errs) $ partitionEithers shakeOpts
- (watchingCmd, ourOpts') = parseOptions ourOpts
- rules' = setOptions ourOpts' >> rules
+ ourOpts = foldr (.) id ourOpts_ defaultOptions
+
+ rules' = do
+ setOptions ourOpts
+ rules
shakeOptions' = foldl' (flip ($)) shakeOptions{shakeFiles="_build", shakeChange=ChangeDigest} shakeOpts'
(shakeRules, wanted) = case extra of
@@ -210,12 +208,10 @@ main = do
for_ errs' $ putStrLn . ("1lab-shake: " ++)
exitFailure
- let watching = Watching `elem` ourOpts'
-
(ok, after) <- shakeWithDatabase shakeOptions' shakeRules \db -> do
- case watching of
- False -> buildOnce db wanted
- True -> buildMany db wanted watchingCmd
+ case _optWatching ourOpts of
+ Nothing -> buildOnce db wanted
+ Just cmd -> buildMany db wanted cmd
shakeRunAfter shakeOptions' after
reportTimes
@@ -223,25 +219,8 @@ main = do
unless ok exitFailure
where
- optDescrs :: [OptDescr (Either (Either String (ShakeOptions -> ShakeOptions)) ArgOption)]
- optDescrs = map (fmap Left) shakeOptDescrs ++ map (fmap Right) ourOptsDescrs
-
- 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.\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 (AFlag f:xs) = (f:) <$> parseOptions xs
- parseOptions (AWatching watching:xs) =
- let (_, xs') = parseOptions xs
- in (watching, Watching:xs')
+ optDescrs :: [OptDescr (Either (Either String (ShakeOptions -> ShakeOptions)) (Options -> Options))]
+ optDescrs = map (fmap Left) shakeOptDescrs ++ map (fmap Right) _1LabOptDescrs
buildOnce :: ShakeDatabase -> [Action ()] -> IO (Bool, [IO ()])
buildOnce db wanted = do
diff --git a/support/shake/app/Shake/Markdown.hs b/support/shake/app/Shake/Markdown.hs
index 70eff7e06..904604774 100644
--- a/support/shake/app/Shake/Markdown.hs
+++ b/support/shake/app/Shake/Markdown.hs
@@ -149,8 +149,9 @@ buildMarkdown refs modname input output = do
(markdown, MarkdownState references dependencies) <- runWriterT (walkM patchBlock markdown)
need dependencies
+ baseUrl <- getBaseUrl
text <- liftIO $ either (fail . show) pure =<<
- runIO (renderMarkdown authors references modname markdown)
+ runIO (renderMarkdown authors references modname baseUrl markdown)
tags <- mapM (parseAgdaLink modname refs) . foldEquations False $ parseTags text
traverse_ (checkMarkup input) tags
@@ -285,11 +286,11 @@ renderMarkdown :: PandocMonad m
=> [Text] -- ^ List of authors
-> [Val Text] -- ^ List of references
-> String -- ^ Name of the current module
+ -> String -- ^ Base URL
-> Pandoc -> m Text
-renderMarkdown authors references modname markdown = do
+renderMarkdown authors references modname baseUrl markdown = do
template <- getTemplate templateName >>= runWithPartials . compileTemplate templateName
>>= either (throwError . PandocTemplateError . Text.pack) pure
-
let
authors' = case authors of
[] -> "Nobody"
@@ -300,6 +301,7 @@ renderMarkdown authors references modname markdown = do
[ ("is-index", toVal (modname == "index"))
, ("authors", toVal authors')
, ("reference", toVal references)
+ , ("base-url", toVal (Text.pack baseUrl))
]
options = def { writerTemplate = Just template
diff --git a/support/shake/app/Shake/Options.hs b/support/shake/app/Shake/Options.hs
index 84e3c5753..ccdf64f31 100644
--- a/support/shake/app/Shake/Options.hs
+++ b/support/shake/app/Shake/Options.hs
@@ -1,45 +1,82 @@
{-# LANGUAGE BlockArguments, ScopedTypeVariables, TupleSections #-}
-{-# LANGUAGE DeriveGeneric, TypeFamilies #-}
+{-# LANGUAGE DeriveGeneric, TypeFamilies, DerivingStrategies #-}
-- | Global build options.
module Shake.Options
- ( Option(..)
+ ( Options(..), _1LabOptDescrs
+ , defaultOptions
, setOptions
+
, getSkipTypes
, getSkipAgda
, getWatching
+ , getBaseUrl
) where
import Development.Shake.Classes
import Development.Shake
+import Data.Maybe
+
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.
+import System.Console.GetOpt
+
+data Options = Options
+ { _optSkipTypes :: !Bool
+ -- ^ Skip generating types when emitting HTML.
+ , _optSkipAgda :: !Bool
+ -- ^ Skip typechecking Agda, emitting the markdown directly.
+ , _optWatching :: Maybe (Maybe String)
+ -- ^ Launch in watch mode. Prevents some build tasks running.
+ , _optBaseUrl :: String
+ -- ^ Base URL for absolute paths
+ }
deriving (Eq, Show, Typeable, Generic)
-instance Hashable Option where
-instance Binary Option where
-instance NFData Option where
+instance Hashable Options
+instance Binary Options
+instance NFData Options
+
+defaultOptions :: Options
+defaultOptions = Options
+ { _optSkipTypes = False
+ , _optSkipAgda = False
+ , _optWatching = Nothing
+ , _optBaseUrl = "https://1lab.dev"
+ }
-type instance RuleResult Option = Bool
+data GetOptions = GetOptions deriving (Eq, Show, Typeable, Generic)
+
+instance Hashable GetOptions
+instance Binary GetOptions
+instance NFData GetOptions
+
+type instance RuleResult GetOptions = Options
-- | Set which option flags are enabled.
-setOptions :: [Option] -> Rules ()
+setOptions :: Options -> Rules ()
setOptions options = do
- _ <- addOracle (pure . getOption)
+ _ <- addOracle $ \GetOptions -> pure options
pure ()
- where
- getOption SkipTypes = SkipTypes `elem` options
- || SkipAgda `elem` options
- || Watching `elem` options
- getOption SkipAgda = SkipAgda `elem` options
- getOption Watching = Watching `elem` options
getSkipTypes, getSkipAgda, getWatching :: Action Bool
-getSkipTypes = askOracle SkipTypes
-getSkipAgda = askOracle SkipAgda
-getWatching = askOracle Watching
+getSkipTypes = _optSkipTypes <$> askOracle GetOptions
+getSkipAgda = _optSkipAgda <$> askOracle GetOptions
+getWatching = isJust . _optWatching <$> askOracle GetOptions
+
+getBaseUrl :: Action String
+getBaseUrl = _optBaseUrl <$> askOracle GetOptions
+
+_1LabOptDescrs :: [OptDescr (Options -> Options)]
+_1LabOptDescrs =
+ [ Option "w" ["watch"] (OptArg (\s r -> r { _optWatching = Just s, _optSkipTypes = True }) "COMMAND")
+ "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 (\r -> r { _optSkipTypes = True }))
+ "Skip generating type tooltips when compiling Agda to HTML."
+ , Option [] ["skip-agda"] (NoArg (\r -> r { _optSkipAgda = True, _optSkipTypes = True }))
+ "Skip typechecking Agda. Markdown files are read from src/ directly."
+ , Option "b" ["base-url"] (ReqArg (\s r -> r { _optBaseUrl = s }) "URL")
+ "The base URL to use for absolute links. Should include the protocol."
+ ]
diff --git a/support/web/template.html b/support/web/template.html
index 6910c09d0..56021f72e 100644
--- a/support/web/template.html
+++ b/support/web/template.html
@@ -7,15 +7,15 @@
$pagetitle$ - 1Lab
-
-
+
+
-
+
-
+
@@ -29,7 +29,7 @@
$endif$
-
+