update to new version of achille
This commit is contained in:
flupe
parent
a66e4ac022
commit
d31b00b633
|
|
@ -1,4 +1,7 @@
|
||||||
packages: ../achille .
|
packages:
|
||||||
|
../achille-smc
|
||||||
|
../achille-smc/achille-yaml
|
||||||
|
../achille-smc/achille-stache
|
||||||
|
../achille-smc/achille-pandoc
|
||||||
|
.
|
||||||
|
|
||||||
package achille
|
|
||||||
flags: +pandoc
|
|
||||||
|
|
|
||||||
|
|
@ -87,8 +87,17 @@ main > * {
|
||||||
max-width: var(--small-width);
|
max-width: var(--small-width);
|
||||||
}
|
}
|
||||||
|
|
||||||
main > pre, main > details, div.sourceCode {
|
main code {
|
||||||
max-width: 100%;
|
background: #fff;
|
||||||
|
padding: .1em .5em;
|
||||||
|
border-radius: 3px;
|
||||||
|
}
|
||||||
|
|
||||||
|
main pre code { padding: 0; }
|
||||||
|
|
||||||
|
main pre, main details, main summary, main div.sourceCode, pre.Agda {
|
||||||
|
max-width: inherit;
|
||||||
|
width: 100%;
|
||||||
box-sizing: border-box;
|
box-sizing: border-box;
|
||||||
clear: both;
|
clear: both;
|
||||||
}
|
}
|
||||||
|
|
@ -165,7 +174,7 @@ pre {
|
||||||
background: #fff;
|
background: #fff;
|
||||||
border-radius: 4px;
|
border-radius: 4px;
|
||||||
padding: .5em 1em;
|
padding: .5em 1em;
|
||||||
}
|
}
|
||||||
|
|
||||||
details summary {
|
details summary {
|
||||||
border: 1px solid #000;
|
border: 1px solid #000;
|
||||||
|
|
@ -181,11 +190,18 @@ details[open] {
|
||||||
|
|
||||||
code {font-family: var(--mono-font), Asanb, monospace}
|
code {font-family: var(--mono-font), Asanb, monospace}
|
||||||
|
|
||||||
pre.Agda a { text-decoration: none; font-family: var(--mono-font), Asanb, monospace; }
|
pre.Agda {
|
||||||
.Keyword { color: #d08770 }
|
font-family: var(--mono-font), Asanb, monospace;
|
||||||
.Primitive { color: #5e81ac }
|
}
|
||||||
.InductiveConstructor { color: #a3be8c }
|
pre.Agda a { text-decoration: none; }
|
||||||
.Comment { color: #d8dee9 }
|
.Keyword { color: #777 }
|
||||||
|
.Symbol { color: #999 }
|
||||||
|
.Primitive { color: #444 }
|
||||||
|
.InductiveConstructor { color: #353535 }
|
||||||
|
.Comment { color: #666 }
|
||||||
|
.Module {
|
||||||
|
text-decoration: underline rgba(0, 0, 0, 0.5) !important;
|
||||||
|
}
|
||||||
.Hole {
|
.Hole {
|
||||||
background: #88c0d0;
|
background: #88c0d0;
|
||||||
border-radius: 4px;
|
border-radius: 4px;
|
||||||
|
|
|
||||||
|
|
@ -1,17 +0,0 @@
|
||||||
<!doctype html>
|
|
||||||
<html>
|
|
||||||
<head>
|
|
||||||
<meta charset="utf-8">
|
|
||||||
<meta name="viewport" content="width=device-width, initial-scale=1.0, user-scalable=yes">
|
|
||||||
<meta name="theme-color" content="#000000">
|
|
||||||
<meta name="robots" content="index, follow">
|
|
||||||
<link rel="stylesheet" href="/assets/theme.css">
|
|
||||||
<link rel="shortcut icon" type="image/svg" href="/assets/favicon.svg">
|
|
||||||
<title>{{ $title }}</title>
|
|
||||||
</head>
|
|
||||||
<body>
|
|
||||||
<nav>{{ $nav }}</nav>
|
|
||||||
<main>{{ $body }}</main>
|
|
||||||
<footer>2022 · <a href="https://creativecommons.org/licenses/by-nc/2.0/">CC BY-NC 2.0</a></footer>
|
|
||||||
</body>
|
|
||||||
</html>
|
|
||||||
|
|
@ -1,33 +1,35 @@
|
||||||
|
---
|
||||||
|
title: Lucas Escot
|
||||||
|
description: Professional page of Lucas Escot
|
||||||
|
---
|
||||||
|
|
||||||
## Lucas Escot {#me}
|
## Lucas Escot {#me}
|
||||||
|
|
||||||
As of 2022, I am a PhD student at [TU Delft](https://tudelft.nl),
|
As of 2022, I am a PhD student at [TU Delft], in the [Programming Languages
|
||||||
in the [Programming Languages Group](https://pl.ewi.tudelft.nl/),
|
Group][PL], under the supervision of Jesper Cockx. My work revolves around
|
||||||
under the supervision of Jesper Cockx. My work revolves around generic programming
|
generic programming in dependently-typed languages --- namely, [Agda].
|
||||||
in dependently-typed languages --- namely, [Agda](https://github.com/agda/agda).
|
|
||||||
|
|
||||||
## Notes {#notes}
|
[TU Delft]: https//tudelft.nl
|
||||||
|
[PL]: https://pl.ewi.tudelft.nl/
|
||||||
```{=html}
|
[Agda]: https://github.com/agda/agda
|
||||||
{{ $notes }}
|
|
||||||
```
|
|
||||||
|
|
||||||
## Miscellaneous {#misc}
|
## Miscellaneous {#misc}
|
||||||
|
|
||||||
On my spare time, I do a fair bit of drawing. Some of it may be found over at [acatalepsie.fr](https://acatalepsie.fr).
|
On my spare time, I do a fair bit of drawing. Some of it may be found over at
|
||||||
Along with a group of friends, I am part of the [sbi.re](https://sbi.re) network,
|
[acatalepsie.fr]. Along with a group of friends, I am part of the [sbi.re]
|
||||||
under which we self-host a bunch of services.
|
network, under which we self-host a bunch of services.
|
||||||
|
|
||||||
|
[acatalepsie.fr]: https://acatalepsie.fr
|
||||||
|
[sbi.re]: https://sbi.re
|
||||||
|
|
||||||
## Contact/Links {#contact}
|
## Contact/Links {#contact}
|
||||||
|
|
||||||
------- ------------------------------------------------------------------------------------------------
|
-------- ------------------------------------------------------------------------------------------------
|
||||||
Mail [lucas@escot.me](mailto:lucas@escot.me), [l.f.b.escot@tudelft.nl](mailto:l.f.b.escot@tudelft.nl)
|
Mail [lucas@escot.me](mailto:lucas@escot.me), [l.f.b.escot@tudelft.nl](mailto:l.f.b.escot@tudelft.nl)
|
||||||
GPG [lescot.gpg](/lescot.gpg)
|
Mastodon [@baboum@mastodon.social](https://mastodon.social/@baboum)
|
||||||
GH [flupe](https://github.com/flupe)
|
GPG [lescot.gpg](/static/lescot.gpg)
|
||||||
SRHT [flupe](https://sr.ht/~flupe)
|
GH [flupe](https://github.com/flupe)
|
||||||
------- ------------------------------------------------------------------------------------------------
|
SRHT [flupe](https://sr.ht/~flupe)
|
||||||
|
-------- ------------------------------------------------------------------------------------------------
|
||||||
|
|
||||||
## Publications
|
## Publications
|
||||||
|
|
||||||
```{=html}
|
|
||||||
{{ $publications }}
|
|
||||||
```
|
|
||||||
|
|
|
||||||
|
|
@ -0,0 +1,42 @@
|
||||||
|
<!doctype html>
|
||||||
|
<html>
|
||||||
|
<head>
|
||||||
|
<meta charset="utf-8">
|
||||||
|
<title>{{meta.title}}</title>
|
||||||
|
<meta name="viewport" content="width=device-width, initial-scale=1.0, user-scalable=yes">
|
||||||
|
<meta name="theme-color" content="#000000">
|
||||||
|
<meta name="robots" content="index, follow">
|
||||||
|
<meta property="og:title" content="{{meta.title}}">
|
||||||
|
<meta property="og:description" content="{{meta.description}}">
|
||||||
|
<link rel="stylesheet" href="/assets/theme.css">
|
||||||
|
<link rel="shortcut icon" type="image/svg" href="/assets/favicon.svg">
|
||||||
|
</head>
|
||||||
|
<body>
|
||||||
|
<nav>
|
||||||
|
{{#nav}}
|
||||||
|
<a href="{{url}}">{{title}}</a>
|
||||||
|
{{/nav}}
|
||||||
|
</nav>
|
||||||
|
<main>
|
||||||
|
{{{body}}}
|
||||||
|
<section class="pubs">
|
||||||
|
{{#pubs}}
|
||||||
|
<ul data-year="{{year}}">
|
||||||
|
{{#pubs}}
|
||||||
|
<li id="{{slug}}">
|
||||||
|
<p class="title"><a href="{{slug}}">{{title}}</a></p>
|
||||||
|
<p class="authors">{{{authors}}}</p>
|
||||||
|
<p class="venue"><a href="{{venue.url}}">{{venue.name}}</a></p>
|
||||||
|
<p class="buttons">
|
||||||
|
{{#file}}<a href="{{url}}">PDF</a>{{/file}}
|
||||||
|
{{#doi}}<a href="https://doi.org/{{doi}}">DOI</a>{{/doi}}
|
||||||
|
</p>
|
||||||
|
</li>
|
||||||
|
{{/pubs}}
|
||||||
|
</ul>
|
||||||
|
{{/pubs}}
|
||||||
|
</section>
|
||||||
|
</main>
|
||||||
|
<footer>2023 · <a href="https://creativecommons.org/licenses/by-nc/2.0/">CC BY-NC 2.0</a> · generated with <a href="https://achille.acatalepsie.fr/">achille</a></footer>
|
||||||
|
</body>
|
||||||
|
</html>
|
||||||
|
|
@ -1,28 +1,30 @@
|
||||||
- title: Practical generic programming over a universe of native datatypes
|
- year: "2022"
|
||||||
slug: generics-agda-2022
|
pubs:
|
||||||
authors:
|
- title: "Practical generic programming over a universe of native datatypes"
|
||||||
- Lucas Escot
|
slug: generics-agda-2022
|
||||||
- name: Jesper Cockx
|
authors:
|
||||||
url: https://jesper.sikanda.be
|
- Lucas Escot
|
||||||
file: papers/generics-agda-icfp22.pdf
|
- name: Jesper Cockx
|
||||||
doi: "10.1145/3547644"
|
url: https://jesper.sikanda.be
|
||||||
venue:
|
file: papers/generics-agda-icfp22.pdf
|
||||||
name: ICFP 2022
|
doi: "10.1145/3547644"
|
||||||
url: https://icfp22.sigplan.org/
|
venue:
|
||||||
|
name: ICFP 2022
|
||||||
|
url: https://icfp22.sigplan.org/
|
||||||
|
|
||||||
- title: "Reasonable Agda is correct Haskell: Writing verified Haskell using agda2hs"
|
- title: "Reasonable Agda is correct Haskell: Writing verified Haskell using agda2hs"
|
||||||
slug: agda2hs-2022
|
slug: agda2hs-2022
|
||||||
authors:
|
authors:
|
||||||
- name: Jesper Cockx
|
- name: Jesper Cockx
|
||||||
url: https://jesper.sikanda.be
|
url: https://jesper.sikanda.be
|
||||||
- name: Orestis Melkonian
|
- name: Orestis Melkonian
|
||||||
url: http://omelkonian.github.io/
|
url: http://omelkonian.github.io/
|
||||||
- Lucas Escot
|
- Lucas Escot
|
||||||
- name: James Chapman
|
- name: James Chapman
|
||||||
url: https://jmchapman.io
|
url: https://jmchapman.io
|
||||||
- Ulf Norell
|
- Ulf Norell
|
||||||
file: papers/agda2hs-haskell22.pdf
|
file: papers/agda2hs-haskell22.pdf
|
||||||
doi: "10.1145/3546189.3549920"
|
doi: "10.1145/3546189.3549920"
|
||||||
venue:
|
venue:
|
||||||
name: Haskell Symposium 2022
|
name: Haskell Symposium 2022
|
||||||
url: https://www.haskell.org/haskell-symposium/2022/
|
url: https://www.haskell.org/haskell-symposium/2022/
|
||||||
|
|
|
||||||
38
escot.cabal
38
escot.cabal
|
|
@ -9,38 +9,26 @@ executable escot
|
||||||
main-is: Main.hs
|
main-is: Main.hs
|
||||||
hs-source-dirs: src
|
hs-source-dirs: src
|
||||||
other-modules: Config
|
other-modules: Config
|
||||||
, Template
|
, Publications
|
||||||
, Markdown
|
|
||||||
build-depends: base
|
build-depends: base
|
||||||
, filepath
|
, achille >= 0.1.0 && < 0.2.0
|
||||||
, achille
|
, achille-pandoc >= 0.0.0 && < 0.1.0
|
||||||
, data-default
|
, achille-stache >= 0.0.0 && < 0.1.0
|
||||||
|
, achille-yaml >= 0.0.0 && < 0.1.0
|
||||||
|
, binary
|
||||||
, pandoc
|
, pandoc
|
||||||
, pandoc-types
|
, pandoc-types
|
||||||
, text
|
, text
|
||||||
, bytestring
|
|
||||||
, filepath
|
|
||||||
, aeson
|
, aeson
|
||||||
, yaml
|
|
||||||
, binary
|
|
||||||
, containers
|
|
||||||
, sort
|
|
||||||
, feed
|
|
||||||
, time
|
, time
|
||||||
, lucid
|
|
||||||
, optparse-applicative
|
|
||||||
, process
|
|
||||||
, directory
|
|
||||||
, megaparsec
|
|
||||||
, mtl
|
|
||||||
default-extensions: BlockArguments
|
default-extensions: BlockArguments
|
||||||
, TupleSections
|
|
||||||
, OverloadedStrings
|
|
||||||
, ScopedTypeVariables
|
|
||||||
, DeriveGeneric
|
|
||||||
, DeriveAnyClass
|
, DeriveAnyClass
|
||||||
|
, DerivingStrategies
|
||||||
|
, DuplicateRecordFields
|
||||||
|
, LambdaCase
|
||||||
|
, NoImplicitPrelude
|
||||||
|
, OverloadedStrings
|
||||||
|
, QualifiedDo
|
||||||
, RecordWildCards
|
, RecordWildCards
|
||||||
, NamedFieldPuns
|
|
||||||
ghc-options: -threaded
|
ghc-options: -threaded
|
||||||
-j8
|
default-language: GHC2021
|
||||||
default-language: Haskell2010
|
|
||||||
|
|
|
||||||
|
|
@ -1,22 +1,17 @@
|
||||||
module Config (config, ropts, wopts, SiteConfig(..), def) where
|
module Config where
|
||||||
|
|
||||||
import Data.Default
|
import Prelude
|
||||||
import Data.Text (Text)
|
import Data.Text (Text)
|
||||||
|
import GHC.Generics (Generic)
|
||||||
|
import Data.Aeson (FromJSON, ToJSON)
|
||||||
|
|
||||||
|
import Achille
|
||||||
|
import Achille.Task
|
||||||
|
import Achille.Path (Path)
|
||||||
|
import Achille.Pandoc (readPandocMetaWith, renderPandocWith)
|
||||||
|
import Text.Pandoc.Builder (Pandoc)
|
||||||
|
|
||||||
import Text.Pandoc.Options as Pandoc
|
import Text.Pandoc.Options as Pandoc
|
||||||
import Achille (Config(..))
|
|
||||||
|
|
||||||
|
|
||||||
config :: Achille.Config
|
|
||||||
config = def
|
|
||||||
{ deployCmd = Just $ "rsync -avzzr " <> root <> "_site/ --chmod=755 acatalepsie:/var/www/html"
|
|
||||||
, contentDir = root <> "content"
|
|
||||||
, outputDir = root <> "_site"
|
|
||||||
, cacheFile = root <> ".cache"
|
|
||||||
-- , ignore = [ "**/*.agdai"
|
|
||||||
-- , "**/*~"
|
|
||||||
-- ]
|
|
||||||
} where root = "/home/flupe/dev/site/"
|
|
||||||
|
|
||||||
|
|
||||||
ropts :: Pandoc.ReaderOptions
|
ropts :: Pandoc.ReaderOptions
|
||||||
ropts = def { readerExtensions = pandocExtensions }
|
ropts = def { readerExtensions = pandocExtensions }
|
||||||
|
|
@ -24,16 +19,19 @@ ropts = def { readerExtensions = pandocExtensions }
|
||||||
wopts :: Pandoc.WriterOptions
|
wopts :: Pandoc.WriterOptions
|
||||||
wopts = def { writerHTMLMathMethod = KaTeX "" }
|
wopts = def { writerHTMLMathMethod = KaTeX "" }
|
||||||
|
|
||||||
|
readPandoc :: FromJSON a => Task IO Path -> Task IO (a, Pandoc)
|
||||||
|
readPandoc = readPandocMetaWith ropts
|
||||||
|
|
||||||
data SiteConfig = SiteConfig
|
renderPandoc :: Task IO Pandoc -> Task IO Text
|
||||||
|
renderPandoc = renderPandocWith wopts
|
||||||
|
|
||||||
|
data PageInfo = PageInfo
|
||||||
{ title :: Text
|
{ title :: Text
|
||||||
, description :: Text
|
, description :: Text
|
||||||
, image :: Text
|
} deriving (Generic, ToJSON)
|
||||||
}
|
|
||||||
|
|
||||||
instance Default SiteConfig where
|
info :: PageInfo
|
||||||
def = SiteConfig
|
info = PageInfo
|
||||||
{ title = "sbbls"
|
{ title = "Lucas Escot"
|
||||||
, description = "my personal web space, for your enjoyment"
|
, description = "My professional page"
|
||||||
, image = "https://acatalepsie.fr/assets/card.png"
|
}
|
||||||
}
|
|
||||||
|
|
|
||||||
216
src/Main.hs
216
src/Main.hs
|
|
@ -1,193 +1,55 @@
|
||||||
{-# LANGUAGE LambdaCase, TypeSynonymInstances, FlexibleInstances, MultiParamTypeClasses, OverloadedStrings #-}
|
|
||||||
{-# LANGUAGE DuplicateRecordFields, ImportQualifiedPost #-}
|
|
||||||
|
|
||||||
module Main where
|
module Main where
|
||||||
|
|
||||||
import GHC.Generics (Generic)
|
import Prelude qualified as P
|
||||||
import Data.Aeson (FromJSON)
|
import Data.Foldable (toList)
|
||||||
import Data.Binary (Binary)
|
import Text.Pandoc.Shared (isHeaderBlock)
|
||||||
import Control.Monad ((>=>))
|
|
||||||
import Data.Function ((&))
|
|
||||||
import Data.Text (Text, pack)
|
|
||||||
import Data.Time (UTCTime, defaultTimeLocale)
|
|
||||||
import System.Directory qualified as System
|
|
||||||
import Data.List (intersperse)
|
|
||||||
import Data.Maybe (fromJust)
|
|
||||||
import Data.Yaml
|
|
||||||
import System.FilePath
|
|
||||||
import Lucid
|
|
||||||
import Control.Applicative ((<|>))
|
|
||||||
import Data.Aeson.KeyMap qualified as KeyMap
|
|
||||||
import Data.Text.Lazy qualified as LT
|
|
||||||
import Data.Functor
|
|
||||||
import Text.Pandoc.Options
|
|
||||||
import Text.Pandoc.Shared (isHeaderBlock)
|
|
||||||
import Text.Pandoc.Definition (Pandoc(Pandoc), Block(Header))
|
import Text.Pandoc.Definition (Pandoc(Pandoc), Block(Header))
|
||||||
|
|
||||||
import Achille
|
import Achille as A
|
||||||
import Achille.Writable (Writable)
|
import Achille.Prelude
|
||||||
import Achille.Writable qualified as Writable
|
import Achille.Yaml
|
||||||
import Achille.Internal.IO (AchilleIO)
|
import Achille.Stache
|
||||||
import Achille.Internal.IO qualified as AchilleIO
|
|
||||||
import Achille.Task.Pandoc
|
|
||||||
|
|
||||||
import Template (Template, Context, parseTemplate)
|
import Config
|
||||||
import Template qualified
|
import Publications
|
||||||
import Config (config, ropts, wopts, SiteConfig(title))
|
|
||||||
import Markdown qualified
|
|
||||||
|
|
||||||
|
|
||||||
-- Bibliography info
|
data NavItem = NavItem
|
||||||
|
{ title :: Text
|
||||||
|
, url :: Text
|
||||||
|
} deriving (Eq, Generic, Binary, ToJSON)
|
||||||
|
|
||||||
data Author = Author
|
data Meta = Meta
|
||||||
{ name :: Text
|
{ title :: Text
|
||||||
, url :: Maybe Text
|
, description :: Text
|
||||||
, orcid :: Maybe Text
|
} deriving (Eq, Generic, Binary, FromJSON, ToJSON)
|
||||||
} deriving (Eq, Show, Generic, Binary)
|
|
||||||
|
|
||||||
instance FromJSON Author where
|
data SiteContent = Content
|
||||||
parseJSON o =
|
{ meta :: Meta
|
||||||
withObject "Author info"
|
, nav :: [NavItem]
|
||||||
(\v -> Author <$> v .: "name"
|
, body :: Text
|
||||||
<*> v .:? "url"
|
, pubs :: [PubGroup]
|
||||||
<*> v .:? "orcid") o
|
} deriving (Generic, ToJSON)
|
||||||
<|> withText "Author name" (\n -> pure $ Author n Nothing Nothing) o
|
|
||||||
|
|
||||||
data Venue = Venue
|
|
||||||
{ name :: Text
|
|
||||||
, url :: Text
|
|
||||||
} deriving (Eq, Show, Generic, Binary, FromJSON)
|
|
||||||
|
|
||||||
data Publication = Publication
|
|
||||||
{ title :: Text
|
|
||||||
, slug :: Text
|
|
||||||
, authors :: [Author]
|
|
||||||
, file :: Maybe Text
|
|
||||||
, doi :: Maybe Text
|
|
||||||
, venue :: Venue
|
|
||||||
} deriving (Eq, Show, Generic, Binary, FromJSON)
|
|
||||||
|
|
||||||
parseYaml :: (AchilleIO m, FromJSON a) => FilePath -> Task m a
|
|
||||||
parseYaml p = do
|
|
||||||
res <- decodeEither' <$> readBS p
|
|
||||||
case res of
|
|
||||||
Left err -> fail (prettyPrintParseException err)
|
|
||||||
Right ok -> return ok
|
|
||||||
|
|
||||||
render :: Template -> Context -> Text -> LT.Text
|
|
||||||
render template ctx body =
|
|
||||||
KeyMap.insert "body" (String body) ctx
|
|
||||||
& Template.render template
|
|
||||||
|
|
||||||
-- writing Html to disk (efficiently)
|
|
||||||
instance AchilleIO m => Writable m (Html ()) where
|
|
||||||
write to = Writable.write to . renderBS
|
|
||||||
|
|
||||||
data Note = Note
|
|
||||||
{ date :: UTCTime
|
|
||||||
, title :: Text
|
|
||||||
}
|
|
||||||
deriving (Eq, Binary, Generic, FromJSON)
|
|
||||||
|
|
||||||
main = achille do
|
|
||||||
index <- readTemplate "index.html"
|
|
||||||
|
|
||||||
match_ "assets/*" copyFile
|
|
||||||
match_ "papers/*" copyFile
|
|
||||||
|
|
||||||
match_ "static/*" $ copyFileAs (makeRelative "static/")
|
|
||||||
|
|
||||||
(nav, index') <- matchFile "index.md" \src -> do
|
|
||||||
doc <- readPandocWith def {readerExtensions = pandocExtensions} src
|
|
||||||
|
|
||||||
let Pandoc _ blocks = doc
|
|
||||||
let headers = filter isHeaderBlock blocks
|
|
||||||
|
|
||||||
-- parsing rendered md as template
|
|
||||||
let template = renderText (Markdown.render doc) & LT.toStrict & parseTemplate & fromJust
|
|
||||||
|
|
||||||
return (LT.toStrict $ renderText $ renderNav headers, template)
|
|
||||||
|
|
||||||
|
|
||||||
pubs :: [Publication] <- matchFile "publications.yaml" parseYaml
|
main = achille A.do
|
||||||
|
index <- loadTemplate "index.mustache"
|
||||||
|
|
||||||
notes :: [(FilePath, Note)] <- match "notes/*.md" \src -> do
|
match "assets/*" copy
|
||||||
if ".lagda.md" /= takeExtensions src then do
|
match "papers/*" copy
|
||||||
(meta@Note{..}, doc) <- readPandocMetadataWith def {readerExtensions = pandocExtensions} src
|
match "static/*" copy
|
||||||
|
|
||||||
path <- LT.toStrict (renderText (Markdown.render doc))
|
meta :*: nav :*: content <- A.do
|
||||||
& write (src -<.> "html")
|
meta :*: doc <- readPandoc "index.md"
|
||||||
. render index (KeyMap.insert "title" (String title) $ KeyMap.insert "nav" (String nav) $ KeyMap.empty)
|
meta :*: (getNav <$> doc) :*: renderPandoc doc
|
||||||
return (path, meta)
|
|
||||||
else do
|
|
||||||
spath <- toAbsolute src
|
|
||||||
odir <- getOutputDir <&> (</> dropExtensions src)
|
|
||||||
tmp <- liftIO System.getTemporaryDirectory <&> (</> "escot")
|
|
||||||
|
|
||||||
liftIO $ System.createDirectoryIfMissing False tmp
|
pubs <- readYaml "publications.yaml"
|
||||||
liftIO $ System.createDirectoryIfMissing True odir
|
|
||||||
liftIO $ AchilleIO.copyFile spath (tmp </> "index.lagda.md")
|
|
||||||
|
|
||||||
dir <- liftIO System.getCurrentDirectory
|
Content <$> meta <*> nav <*> content <*> pubs
|
||||||
liftIO $ System.setCurrentDirectory tmp
|
& applyTemplate index
|
||||||
|
& write "index.html"
|
||||||
|
|
||||||
callCommand $
|
where getNav :: Pandoc -> [NavItem]
|
||||||
"agda --html "
|
getNav (Pandoc _ blocks) =
|
||||||
<> "--html-dir=. "
|
let hdToItem (Header _ (id, _, _) _) = NavItem id ("/#" <> id)
|
||||||
<> "--html-highlight=auto "
|
in hdToItem <$> toList (filter isHeaderBlock blocks)
|
||||||
<> "index.lagda.md"
|
|
||||||
|
|
||||||
liftIO $ System.setCurrentDirectory dir
|
|
||||||
callCommand $ "cp " <> tmp <> "/* " <> odir
|
|
||||||
|
|
||||||
(meta@Note{..}, doc) <- readAbsPandocMetadataWith def {readerExtensions = pandocExtensions} (tmp </> "index.md")
|
|
||||||
path <- renderPandoc doc >>= write (dropExtensions src </> "index.html")
|
|
||||||
. render index (KeyMap.insert "title" (String title) $ KeyMap.insert "nav" (String nav) $ KeyMap.empty)
|
|
||||||
return (takeDirectory path, meta)
|
|
||||||
|
|
||||||
let notesList :: Html () =
|
|
||||||
ul_ $ foldMap (\(src, Note{..}) -> li_ $ a_ [ href_ (pack src) ] $ toHtmlRaw title) notes
|
|
||||||
|
|
||||||
watch pubs $ watch notes do
|
|
||||||
let ctx = KeyMap.insert "nav" (String nav) $
|
|
||||||
KeyMap.insert "notes" (String (LT.toStrict $ renderText notesList)) $
|
|
||||||
KeyMap.insert "title" (String "Lucas Escot") $
|
|
||||||
KeyMap.insert "publications" (String (LT.toStrict $ renderText $ renderPublications pubs)) KeyMap.empty
|
|
||||||
|
|
||||||
write "index.html" $ render index ctx (LT.toStrict $ Template.render index' ctx)
|
|
||||||
|
|
||||||
where
|
|
||||||
renderNav :: [Block] -> Html ()
|
|
||||||
renderNav = ul_ . foldMap (\(Header _ (id, _, _) _) -> li_ $ a_ [href_ $ "/#" <> id] (toHtmlRaw id))
|
|
||||||
|
|
||||||
readTemplate :: FilePath -> Task IO Template
|
|
||||||
readTemplate src = readText src <&> parseTemplate >>= \case
|
|
||||||
Just t -> return t
|
|
||||||
Nothing -> fail $ "Could not parse template: " ++ src
|
|
||||||
|
|
||||||
-- TODO: fix year
|
|
||||||
renderPublications :: [Publication] -> Html ()
|
|
||||||
renderPublications pubs = section_ [class_ "pubs"] do
|
|
||||||
ul_ [ data_ "year" "2022" ] $ foldMap renderPub pubs
|
|
||||||
|
|
||||||
where renderPub :: Publication -> Html ()
|
|
||||||
renderPub Publication {..} = li_ [id_ slug] do
|
|
||||||
p_ [class_ "title"] $ a_ [href_ ("#" <> slug)] $ toHtmlRaw title
|
|
||||||
p_ [class_ "authors"] $ renderAuthors (reverse (fmap renderAuthor authors))
|
|
||||||
let Venue vName vUrl = venue
|
|
||||||
p_ [class_ "venue"] $ a_ [href_ vUrl] $ toHtmlRaw vName
|
|
||||||
p_ [class_ "buttons"] do
|
|
||||||
maybe mempty (\url -> a_ [href_ ("/" <> url)] "PDF") file
|
|
||||||
maybe mempty (\doi -> a_ [href_ ("https://doi.org/" <> doi)] "DOI") doi
|
|
||||||
|
|
||||||
renderAuthor :: Author -> Html ()
|
|
||||||
renderAuthor (Author name url orcid) =
|
|
||||||
case url of
|
|
||||||
Nothing -> toHtmlRaw name
|
|
||||||
Just url -> a_ [href_ url] (toHtmlRaw name)
|
|
||||||
|
|
||||||
renderAuthors :: [Html ()] -> Html ()
|
|
||||||
renderAuthors [] = mempty
|
|
||||||
renderAuthors [one] = one
|
|
||||||
renderAuthors (last:others) =
|
|
||||||
mconcat (intersperse ", " (reverse others)) <> " and " <> last
|
|
||||||
|
|
|
||||||
121
src/Markdown.hs
121
src/Markdown.hs
|
|
@ -1,121 +0,0 @@
|
||||||
{-# LANGUAGE FlexibleContexts #-}
|
|
||||||
module Markdown where
|
|
||||||
|
|
||||||
import Lucid
|
|
||||||
import Lucid.Base (makeElement)
|
|
||||||
import Data.Text (pack)
|
|
||||||
import Text.Pandoc.Builder
|
|
||||||
import Control.Monad (foldM)
|
|
||||||
import Control.Monad.Trans
|
|
||||||
import Data.Functor ((<&>))
|
|
||||||
import Data.Bifoldable (Bifoldable, bifoldMap, bifoldrM)
|
|
||||||
import Control.Monad.State.Strict
|
|
||||||
import Control.Monad.State.Class
|
|
||||||
import Control.Monad.Reader
|
|
||||||
import Control.Monad.Reader.Class
|
|
||||||
|
|
||||||
data MDState = MDState
|
|
||||||
{ stNoteCount :: Int -- count of notes that HAVE been printed
|
|
||||||
, stNotes :: [Html ()] -- notes that haven't be printed yet
|
|
||||||
}
|
|
||||||
|
|
||||||
defaultMDState :: MDState
|
|
||||||
defaultMDState = MDState
|
|
||||||
{ stNoteCount = 0
|
|
||||||
, stNotes = []
|
|
||||||
}
|
|
||||||
|
|
||||||
type BlockLevel = Int
|
|
||||||
|
|
||||||
render :: Pandoc -> Html ()
|
|
||||||
render (Pandoc meta blocks) =
|
|
||||||
fst $ runReader (runStateT (blocksToHtml blocks) defaultMDState) 0
|
|
||||||
|
|
||||||
inlineToHtml
|
|
||||||
:: (MonadState MDState m, MonadReader BlockLevel m)
|
|
||||||
=> Inline -> m (Html ())
|
|
||||||
inlineToHtml (Str str) = pure $ toHtml str
|
|
||||||
inlineToHtml (Emph ins) = em_ <$> inlinesToHtml ins
|
|
||||||
inlineToHtml (Underline ins) = makeElement "u" <$> inlinesToHtml ins
|
|
||||||
inlineToHtml (Strong ins) = strong_ <$> inlinesToHtml ins
|
|
||||||
inlineToHtml (Strikeout ins) = makeElement "s" <$> inlinesToHtml ins
|
|
||||||
inlineToHtml (Superscript ins) = sup_ <$> inlinesToHtml ins
|
|
||||||
inlineToHtml (Subscript ins) = sub_ <$> inlinesToHtml ins
|
|
||||||
inlineToHtml (SmallCaps ins) = span_ [class_ "sc"] <$> inlinesToHtml ins
|
|
||||||
inlineToHtml (Quoted typ ins) =
|
|
||||||
let (l, r) = case typ of
|
|
||||||
SingleQuote -> ("‘", "’")
|
|
||||||
DoubleQuote -> ("“", "”")
|
|
||||||
in pure l >> inlinesToHtml ins >> pure r
|
|
||||||
inlineToHtml (Cite cits ins) = undefined -- TODO: citations
|
|
||||||
inlineToHtml (Code attrs str) = pure $ code_ $ toHtml str
|
|
||||||
inlineToHtml Space = pure " "
|
|
||||||
inlineToHtml SoftBreak = pure "\n"
|
|
||||||
inlineToHtml LineBreak = pure $ br_ []
|
|
||||||
inlineToHtml (Math _ math) = pure $ span_ [class_ "math"] $ toHtml math -- TODO: compile-time katex math
|
|
||||||
inlineToHtml (RawInline f str) | f == "html" = pure $ toHtmlRaw str
|
|
||||||
inlineToHtml (RawInline f str) = pure mempty
|
|
||||||
inlineToHtml (Link attrs ins (src, title)) = a_ [href_ src, title_ title] <$> inlinesToHtml ins
|
|
||||||
inlineToHtml (Image attrs ins (src, title)) = pure $ img_ [href_ src, title_ title] -- TODO: handle image alt
|
|
||||||
inlineToHtml (Note blocks) = do
|
|
||||||
MDState {..} <- get
|
|
||||||
let currentIdx = stNoteCount + length stNotes + 1
|
|
||||||
note <- blocksToHtml blocks
|
|
||||||
modify \s -> s { stNotes = note : stNotes }
|
|
||||||
pure $ a_ [href_ $ "#note" <> pack (show currentIdx)] $ "[" <> toHtml (show currentIdx) <> "]"
|
|
||||||
inlineToHtml (Span attrs ins) = span_ <$> inlinesToHtml ins
|
|
||||||
|
|
||||||
inlinesToHtml
|
|
||||||
:: (MonadState MDState m, MonadReader BlockLevel m)
|
|
||||||
=> [Inline] -> m (Html ())
|
|
||||||
inlinesToHtml = foldMapM inlineToHtml
|
|
||||||
|
|
||||||
blockToHtml
|
|
||||||
:: (MonadState MDState m, MonadReader BlockLevel m)
|
|
||||||
=> Block -> m (Html ())
|
|
||||||
blockToHtml (Plain ins) = pre_ <$> inlinesToHtml ins
|
|
||||||
blockToHtml (Para ins) = p_ <$> inlinesToHtml ins
|
|
||||||
blockToHtml (LineBlock ins) = undefined
|
|
||||||
blockToHtml (CodeBlock attrs code) = pure $ pre_ $ code_ $ toHtmlRaw code -- TODO: highlighting
|
|
||||||
blockToHtml (RawBlock f str) | f == "html" = pure $ toHtmlRaw str
|
|
||||||
blockToHtml (RawBlock f str) = pure mempty
|
|
||||||
blockToHtml (BlockQuote blocks) = blockquote_ <$> blocksToHtml blocks
|
|
||||||
blockToHtml (OrderedList attrs items) = ol_ <$> foldMapM (fmap li_ . blocksToHtml) items -- TODO: handle attrs
|
|
||||||
blockToHtml (BulletList items) = ul_ <$> foldMapM (fmap li_ . blocksToHtml) items
|
|
||||||
blockToHtml (DefinitionList items) =
|
|
||||||
dl_ <$> foldMapM (bifoldMapM inlinesToHtml (foldMapM (fmap dd_ . blocksToHtml))) items
|
|
||||||
blockToHtml (Header k attrs ins) = h_ k <$> inlinesToHtml ins -- TODO: handle attrs (especially ID)
|
|
||||||
where h_ :: Applicative m => Int -> HtmlT m a -> HtmlT m a
|
|
||||||
h_ 1 = h1_
|
|
||||||
h_ 2 = h2_
|
|
||||||
h_ 3 = h3_
|
|
||||||
h_ 4 = h4_
|
|
||||||
h_ 5 = h5_
|
|
||||||
h_ _ = h6_
|
|
||||||
blockToHtml HorizontalRule = pure $ hr_ []
|
|
||||||
blockToHtml (Table attrs caption _ head rows foot) = pure mempty
|
|
||||||
blockToHtml (Div attrs blocks) = pure mempty
|
|
||||||
blockToHtml Null = pure mempty
|
|
||||||
|
|
||||||
blocksToHtml
|
|
||||||
:: (MonadState MDState m, MonadReader BlockLevel m)
|
|
||||||
=> [Block] -> m (Html ())
|
|
||||||
blocksToHtml = foldMapM \block -> do
|
|
||||||
html <- local (+1) $ blockToHtml block
|
|
||||||
lvl <- ask
|
|
||||||
|
|
||||||
MDState {..} <- get
|
|
||||||
let shouldPrintNotes = not (null stNotes) && lvl == 0
|
|
||||||
let notes = when shouldPrintNotes (ol_ [class_ "footnotes", start_ $ pack (show $ stNoteCount + 1)] $ foldMap li_ (reverse stNotes))
|
|
||||||
when shouldPrintNotes $ modify \s -> s {stNoteCount = stNoteCount + length stNotes, stNotes = [] }
|
|
||||||
|
|
||||||
pure $ html <> notes
|
|
||||||
|
|
||||||
foldMapM :: (Monad m, Monoid w, Foldable t) => (a -> m w) -> t a -> m w
|
|
||||||
foldMapM f = foldM (\acc a -> do
|
|
||||||
w <- f a
|
|
||||||
return $! mappend acc w)
|
|
||||||
mempty
|
|
||||||
|
|
||||||
bifoldMapM :: (Monad m, Monoid w, Bifoldable t) => (a -> m w) -> (b -> m w) -> t a b -> m w
|
|
||||||
bifoldMapM f g = bifoldrM (\a b -> f a <&> (`mappend` b)) (\a b -> g a <&> (`mappend` b)) mempty
|
|
||||||
|
|
@ -0,0 +1,75 @@
|
||||||
|
module Publications where
|
||||||
|
|
||||||
|
import Prelude
|
||||||
|
import Control.Applicative ((<|>))
|
||||||
|
import Data.Aeson
|
||||||
|
import Data.Aeson.Types
|
||||||
|
import Data.Text (Text)
|
||||||
|
import Data.Text.Lazy.Builder
|
||||||
|
import Data.Binary (Binary)
|
||||||
|
import GHC.Generics (Generic)
|
||||||
|
|
||||||
|
import Data.Text.Lazy qualified as LT
|
||||||
|
|
||||||
|
|
||||||
|
-- Some structured definitions for bibliography.
|
||||||
|
-- It's not *strictly* necessery per se, but this allows detecting formatting
|
||||||
|
-- errors at build-time rather than produce incorrect HTML.
|
||||||
|
|
||||||
|
|
||||||
|
-- publication authors may have a website and orcid
|
||||||
|
data Author = Author
|
||||||
|
{ name :: Text
|
||||||
|
, url :: Maybe Text
|
||||||
|
, orcid :: Maybe Text
|
||||||
|
} deriving (Eq, Show, Generic, Binary, ToJSON)
|
||||||
|
|
||||||
|
instance FromJSON Author where
|
||||||
|
parseJSON o = withObject "Author info" authorInfo o <|> withText "Author name" authorName o
|
||||||
|
where authorInfo :: Object -> Parser Author
|
||||||
|
authorInfo v =
|
||||||
|
Author <$> v .: "name"
|
||||||
|
<*> v .:? "url"
|
||||||
|
<*> v .:? "orcid"
|
||||||
|
|
||||||
|
authorName :: Text -> Parser Author
|
||||||
|
authorName s = pure $ Author s Nothing Nothing
|
||||||
|
|
||||||
|
|
||||||
|
-- wrapper around list of authors, with a custom ToJSON instance that produces a nicely separated list
|
||||||
|
newtype Authors = Authors [Author] deriving newtype (Eq, Binary, FromJSON)
|
||||||
|
|
||||||
|
instance ToJSON Authors where
|
||||||
|
toJSON (Authors authors) =
|
||||||
|
String $ LT.toStrict $ toLazyText $ joinSmart (fmap renderAuthor authors)
|
||||||
|
where renderAuthor :: Author -> Builder
|
||||||
|
renderAuthor (Author name Nothing orcid) = fromText name
|
||||||
|
renderAuthor (Author name (Just url) orcid) =
|
||||||
|
"<a href=\"" <> fromText url <> "\">" <> fromText name <> "</a>"
|
||||||
|
|
||||||
|
joinSmart :: [Builder] -> Builder
|
||||||
|
joinSmart chunks = case chunks of
|
||||||
|
[] -> mempty
|
||||||
|
[one] -> one
|
||||||
|
[one, two] -> one <> " and " <> two
|
||||||
|
first:rest -> first <> ", " <> joinSmart rest
|
||||||
|
|
||||||
|
-- publication venue
|
||||||
|
data Venue = Venue
|
||||||
|
{ name :: Text
|
||||||
|
, url :: Text
|
||||||
|
} deriving (Eq, Generic, Binary, FromJSON, ToJSON)
|
||||||
|
|
||||||
|
data Publication = Publication
|
||||||
|
{ title :: Text
|
||||||
|
, slug :: Text
|
||||||
|
, authors :: Authors
|
||||||
|
, file :: Maybe Text
|
||||||
|
, doi :: Maybe Text
|
||||||
|
, venue :: Venue
|
||||||
|
} deriving (Eq, Generic, Binary, FromJSON, ToJSON)
|
||||||
|
|
||||||
|
data PubGroup = PubGroup
|
||||||
|
{ year :: Text
|
||||||
|
, pubs :: [Publication]
|
||||||
|
} deriving (Generic, Eq, Binary, FromJSON, ToJSON)
|
||||||
106
src/Template.hs
106
src/Template.hs
|
|
@ -1,106 +0,0 @@
|
||||||
-- | Tiny templating engine
|
|
||||||
module Template where
|
|
||||||
|
|
||||||
import Data.Text
|
|
||||||
import Data.Text.Lazy.Encoding (encodeUtf8)
|
|
||||||
import Data.ByteString.Lazy (ByteString)
|
|
||||||
import Data.Binary
|
|
||||||
import Data.Functor (void)
|
|
||||||
import Data.Void
|
|
||||||
import GHC.Generics
|
|
||||||
import Text.Megaparsec
|
|
||||||
import Text.Megaparsec.Char
|
|
||||||
import Data.Aeson (Value(..))
|
|
||||||
|
|
||||||
import qualified Data.Text.Lazy as LT
|
|
||||||
import qualified Data.Aeson as Aeson
|
|
||||||
import qualified Data.Aeson.KeyMap as KeyMap
|
|
||||||
import qualified Data.Aeson.Key as Key
|
|
||||||
-- import qualified Data.HashMap.Strict as HashMap
|
|
||||||
|
|
||||||
|
|
||||||
data Chunk
|
|
||||||
= Raw Text
|
|
||||||
| Var [Text]
|
|
||||||
| For Text [Text] Template
|
|
||||||
| If [Text] Template
|
|
||||||
deriving (Eq, Show, Generic, Binary)
|
|
||||||
|
|
||||||
type Template = [Chunk]
|
|
||||||
type Context = Aeson.Object
|
|
||||||
|
|
||||||
type Parser = Parsec Void Text
|
|
||||||
|
|
||||||
|
|
||||||
-- RENDERING
|
|
||||||
|
|
||||||
render :: Template -> Context -> LT.Text
|
|
||||||
render chunks ctx = foldMap (renderChunk ctx) chunks
|
|
||||||
|
|
||||||
lookupCtx :: [Text] -> Context -> Maybe Aeson.Value
|
|
||||||
lookupCtx keys = aux keys . Aeson.Object
|
|
||||||
where
|
|
||||||
aux :: [Text] -> Aeson.Value -> Maybe Aeson.Value
|
|
||||||
aux [] v = Just v
|
|
||||||
aux (k:ks) (Object h) = KeyMap.lookup (Key.fromText k) h >>= aux ks
|
|
||||||
aux _ _ = Nothing
|
|
||||||
|
|
||||||
renderChunk :: Context -> Chunk -> LT.Text
|
|
||||||
renderChunk ctx (Raw t) = LT.fromStrict t
|
|
||||||
renderChunk ctx (Var ks) =
|
|
||||||
case Aeson.fromJSON <$> lookupCtx ks ctx of
|
|
||||||
Just (Aeson.Success v) -> v
|
|
||||||
_ -> mempty
|
|
||||||
renderChunk ctx (For kn ks c) =
|
|
||||||
case lookupCtx ks ctx of
|
|
||||||
Just (Aeson.Array arr) ->
|
|
||||||
foldMap (\v -> foldMap (renderChunk (KeyMap.insert (Key.fromText kn) v ctx)) c) arr
|
|
||||||
_ -> mempty
|
|
||||||
renderChunk ctx (If ks c) =
|
|
||||||
case lookupCtx ks ctx of
|
|
||||||
Just _ -> foldMap (renderChunk ctx) c
|
|
||||||
_ -> mempty
|
|
||||||
|
|
||||||
|
|
||||||
-- PARSING
|
|
||||||
|
|
||||||
parseTemplate :: Text -> Maybe Template
|
|
||||||
parseTemplate = parseMaybe templateP
|
|
||||||
|
|
||||||
templateP :: Parser Template
|
|
||||||
templateP = many chunkP
|
|
||||||
|
|
||||||
chunkP :: Parser Chunk
|
|
||||||
chunkP = choice [ varP , forP , ifP , rawP ]
|
|
||||||
where
|
|
||||||
identP :: Parser Text
|
|
||||||
identP = pack <$> ((:) <$> letterChar <*> many alphaNumChar)
|
|
||||||
|
|
||||||
keysP :: Parser [Text]
|
|
||||||
keysP = try $ "$" *> sepBy1 identP "."
|
|
||||||
|
|
||||||
varP :: Parser Chunk
|
|
||||||
varP = try $ Var <$> between ldelim rdelim
|
|
||||||
(space *> keysP <* space)
|
|
||||||
|
|
||||||
rawP :: Parser Chunk
|
|
||||||
rawP = Raw . pack <$>
|
|
||||||
someTill anySingle (eof <|> lookAhead ldelim)
|
|
||||||
|
|
||||||
forP :: Parser Chunk
|
|
||||||
forP = try do
|
|
||||||
ldelim *> space *> string "for" *> space1
|
|
||||||
key <- identP <* space1 <* "in" <* space1
|
|
||||||
val <- keysP <* space <* rdelim
|
|
||||||
chunks <- manyTill chunkP (try (between ldelim rdelim (space *> "end" *> space)))
|
|
||||||
return $ For key val chunks
|
|
||||||
|
|
||||||
ifP :: Parser Chunk
|
|
||||||
ifP = try do
|
|
||||||
ldelim *> space *> string "if" *> space1
|
|
||||||
val <- keysP <* space <* rdelim
|
|
||||||
chunks <- manyTill chunkP (try (between ldelim rdelim (space *> "end" *> space)))
|
|
||||||
return $ If val chunks
|
|
||||||
|
|
||||||
ldelim = void "{{"
|
|
||||||
rdelim = "}}"
|
|
||||||
Loading…
Reference in New Issue