Skip to content

Commit

Permalink
add an option for changing the base url
Browse files Browse the repository at this point in the history
  • Loading branch information
plt-amy committed Sep 12, 2023
1 parent e6e2e43 commit 786e937
Show file tree
Hide file tree
Showing 6 changed files with 84 additions and 66 deletions.
2 changes: 1 addition & 1 deletion .github/workflows/preview.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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 }}
Expand Down
2 changes: 1 addition & 1 deletion support/shake/app/Definitions.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
45 changes: 12 additions & 33 deletions support/shake/app/Main.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -183,11 +183,6 @@ rules = do

-- Profit!

data ArgOption
= AFlag Option
| AWatching (Maybe String)
deriving (Eq, Show)

main :: IO ()
main = do
args <- getArgs
Expand All @@ -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
Expand All @@ -210,38 +208,19 @@ 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

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
Expand Down
8 changes: 5 additions & 3 deletions support/shake/app/Shake/Markdown.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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"
Expand All @@ -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
Expand Down
79 changes: 58 additions & 21 deletions support/shake/app/Shake/Options.hs
Original file line number Diff line number Diff line change
@@ -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."
]
14 changes: 7 additions & 7 deletions support/web/template.html
Original file line number Diff line number Diff line change
Expand Up @@ -7,15 +7,15 @@

<title>$pagetitle$ - 1Lab</title>

<link rel="stylesheet" href="/css/default.css" />
<link rel="stylesheet" href="/css/katex.min.css" />
<link rel="stylesheet" href="$base-url$/css/default.css" />
<link rel="stylesheet" href="$base-url$/css/katex.min.css" />

<meta name="twitter:card" content="summary" />
<meta name="twitter:title" content="$pagetitle$ - 1Lab" />
<meta name="twitter:image" content="https://1lab.dev/static/cube-128x.png" />
<meta name="twitter:image" content="$base_url$/static/cube-128x.png" />

<meta name="og:title" content="$pagetitle$ - 1Lab" />
<meta name="og:image" content="https://1lab.dev/static/cube-128x.png" />
<meta name="og:image" content="$base-url$/static/cube-128x.png" />
<meta name="og:site-name" content="1Lab" />
<meta name="og:type" content="website" />

Expand All @@ -29,7 +29,7 @@
<meta name="description" content="A formalised, explorable online resource for Homotopy Type Theory." />
$endif$

<script defer src="/main.js"></script>
<script defer src="$base-url$/main.js"></script>

<noscript>
<style>
Expand Down Expand Up @@ -68,7 +68,7 @@ <h3 class="Agda" style="margin-top: 0; margin-bottom: 0; white-space: pre;">
<!-- Cube logo -->
<a id=logo href="/">
<img alt="1Lab"
src="/static/cube-72x.png"
src="$base-url$/static/cube-72x.png"
style="display: block; margin-bottom: 1em; margin: auto;"
width="32px"
height="32px"
Expand Down Expand Up @@ -120,7 +120,7 @@ <h3 class="Agda" style="margin-top: 0; margin-bottom: 0; white-space: pre;">

$if(is-index)$
$else$
<a href="/">back to index</a> <br />
<a href="$base-url$">back to index</a> <br />
$endif$
<a href="all-pages.html">view all pages</a> <br />
<a href="https://github.com/plt-amy/1lab/blob/$source$">link to source</a> <br />
Expand Down

0 comments on commit 786e937

Please sign in to comment.