wip: workflow for previewing the website

.github/workflows/build.yml

@@ -1,5 +1,12 @@
-name: Build
 on: [push, pull_request]
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: ${{ github.ref != 'refs/heads/main' }}
+
+
+name: Build
+
 jobs:
   build:
     runs-on: ubuntu-latest

.github/workflows/preview.yml

@@ -0,0 +1,76 @@
+name: PR Preview
+
+on:
+  pull_request:
+    types:
+      - opened
+      - reopened
+      - synchronize
+      - closed
+
+permissions:
+  pull-requests: write
+
+jobs:
+  pr-preview:
+    runs-on: ubuntu-latest
+
+    env:
+      mailmap: ${{ secrets.MAILMAP }}
+
+    steps:
+      - name: Checkout ⬇️
+        uses: actions/checkout@v3
+        with:
+          fetch-depth: 0 # we need the commit history for authors
+
+      - name: Install Nix ❄️
+        uses: cachix/install-nix-action@v20
+
+      - name: Set up Cachix ♻️
+        uses: cachix/cachix-action@v12
+        with:
+          name: 1lab
+          skipPush: true
+
+      - name: Build the Shakefile 🧰
+        run: |
+          hash=$(nix-build -A shakefile --no-out-link)
+          hash=${hash#/nix/store/} hash=${hash%%-*}
+          echo "shake_version=$hash" >> "$GITHUB_ENV"
+
+      - name: Cache _build ♻️
+        uses: actions/cache@v3
+        with:
+          path: _build
+          key: prose-4-${{ env.shake_version }}-${{ github.run_id }}
+          restore-keys: prose-4-${{ env.shake_version }}-
+
+      - name: Build the prose ✍️
+        run: |
+          echo "$mailmap" > .mailmap
+          nix-shell --arg interactive false --run "$build_command"
+        env:
+          NIX_BUILD_SHELL: bash
+          build_command: |
+            set -eu
+            1lab-shake -j all --skip-agda -b "https://plt-amy.github.io/1lab-previews/pr-${{ github.event.number }}"
+            eval "$installPhase"
+            cp -rv _build/site pr-${{ github.event.number }}
+
+      - name: Upload 📦
+        uses: dmnemec/copy_file_to_another_repo_action@main
+        env:
+          API_TOKEN_GITHUB: ${{ secrets.PREVIEW_TOKEN }}
+        with:
+          source_file: pr-${{ github.event.number }}
+          destination_repo: 'plt-amy/1lab-previews'
+          user_email: '[email protected]'
+          user_name: 'plt-amy'
+          commit_message: 'Preview of PR #${{ github.event.number }}'
+
+      - name: Inform ℹ️
+        uses: marocchino/sticky-pull-request-comment@v2
+        with:
+          message: |
+            [Rendered preview](https://plt-amy.github.io/1lab-previews/pr-${{ github.event.number }})

src/Authors.lagda.md

@@ -28,7 +28,7 @@ pronouns.
 
 <div class="profile pfp-left">
 <div class="profile-pfp">
-<img alt="Amélia's profile picture" src="/static/pfps/amelia.png" />
+<img alt="Amélia's profile picture" src="static/pfps/amelia.png" />
 <span class="profile-name">Amélia</span>
 <span class="profile-pronouns">they/them</span>
 <span><a href="https://twitter.com/plt_amy">\@plt_amy</a></span>
@@ -59,7 +59,7 @@ about type theory and the implementation of programming languages, and
 
 <div class="profile pfp-right">
 <div class="profile-pfp">
-<img alt="Astra's profile picture" src="/static/pfps/astra.png" />
+<img alt="Astra's profile picture" src="static/pfps/astra.png" />
 <span class="profile-name">Astra</span>
 <span class="profile-pronouns">she/her</span>
 <span><a href="https://twitter.com/astradiol">\@astradiol</a></span>

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

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,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

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

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."
+  ]

support/web/css/code.scss

@@ -10,7 +10,7 @@
   font-weight: 400;
   font-stretch: normal;
   font-style: normal;
-  src: url('/static/ttf/julia-mono.ttf') format('truetype');
+  src: url('../static/ttf/julia-mono.ttf') format('truetype');
 }
 
 code, pre, .sourceCode {

support/web/css/default.scss

@@ -607,14 +607,14 @@ span.qed {
  * it; An arrow with #000 stroke in light theme and #ABB2BF stroke in
  * dark theme. */
 span.enclosing.liesover {
-  background: url('/static/lies-over-light.svg') no-repeat;
+  background: url('../static/lies-over-light.svg') no-repeat;
   background-size: contain;
   background-position: center center;
 }
 
 @media (prefers-color-scheme: dark) {
   span.enclosing.liesover {
-    background: url('/static/lies-over-dark.svg') no-repeat;
+    background: url('../static/lies-over-dark.svg') no-repeat;
     background-size: contain;
     background-position: center center;
   }

support/web/js/depgraph.tsx

@@ -237,7 +237,7 @@ const modal = (close = () => { }) => {
 };
 
 document.addEventListener('DOMContentLoaded', async () => {
-  const data = (await fetch("/static/links.json").then(r => r.json())).slice(0, -1);
+  const data = (await fetch("static/links.json").then(r => r.json())).slice(0, -1);
   const { nodes, edges } = nbhoodSubgraph(page, data);
   makeColours(nodes);
 

support/web/js/search.tsx

@@ -172,7 +172,7 @@ const startSearch = (mirrorInput: HTMLInputElement | null) => {
   // Fetch the search index if not available and start searching
   if (!loadingIndex) {
     loadingIndex = true;
-    fetch("/static/search.json")
+    fetch("static/search.json")
       .then(r => r.json())
       .then(entries => {
         index = new Searcher(entries, {