diff --git a/content/assets/theme.css b/content/assets/theme.css
index 7004fc5..20e9c5c 100644
--- a/content/assets/theme.css
+++ b/content/assets/theme.css
@@ -77,6 +77,15 @@ hr {
margin: 2.5em 0;
}
+main > ul { list-style: none }
+main > ul li > span {
+ font: 13px monospace;
+ margin-right: 1em;
+ padding: .1em .5em;
+ border-radius: 3px;
+ background: #eaeaef;
+}
+
details summary {
cursor: pointer;
padding: .5em 1em;
@@ -142,8 +151,8 @@ main ul { padding: 0 0 0 1.5em }
main ul.projects {
padding: 0;
margin: 2.5em 0 0;
-background: #fafafb;
-list-style: none;
+ background: #fafafb;
+ list-style: none;
border-radius: 2px;
}
@@ -248,6 +257,23 @@ figure {
text-align: center;
}
+ul.pages {
+ padding: 0;
+ margin: 2em 0 2.5em;
+ list-style:none;
+ border-radius: 3px;
+ overflow: hidden;
+}
+ul.pages li a {
+ display: block;
+ line-height: 2.4em;
+ padding: 0 1em;
+ background: #eceff4;
+}
+ul.pages li a:hover {
+ background: #f2f4f7;
+}
+
figure img {
max-width: 100%;
vertical-align: top;
diff --git a/content/index.rst b/content/index.rst
index a65139a..a67ed1d 100644
--- a/content/index.rst
+++ b/content/index.rst
@@ -1 +1 @@
- Oh god why
+ Oh god why
diff --git a/content/posts/2020-05-21-generic-genericity.lagda.rst b/content/posts/2020-05-21-generic-genericity.lagda.rst
deleted file mode 100644
index 7e5f0d3..0000000
--- a/content/posts/2020-05-21-generic-genericity.lagda.rst
+++ /dev/null
@@ -1,591 +0,0 @@
----
-title: Parametricity for described datatypes
-draft: yes
----
-
-.. highlight:: agda
-.. default-role:: math
-
-This entry is just me figuring stuff out by writing it down.
-The goal is to **derive automatically the logical relation generated by
-a datatype** in Agda, without metaprogramming. Or, to be correct,
-without *unsafe* metaprogramming --- no reflection allowed.
-
-*The title means nothing and this is WIP.*
-
-Only one thing to keep in mind: we are using the dirtiest of tricks, :code:`--type-in-type`.
-For the time being, this will do just fine.
-
-.. raw:: html
-
-
- Prelude
-
-::
-
- {-# OPTIONS --type-in-type #-}
-
- open import Agda.Primitive
- open import Agda.Builtin.Unit
- open import Agda.Builtin.Sigma
- open import Agda.Builtin.Equality
- open import Agda.Builtin.Nat
- open import Agda.Builtin.List
-
- variable A B : Set
-
- infixr -1 _$_
- infixl 2 _∘_
-
- id : {A : Set} → A → A
- id x = x
-
- const : {A : Set} → A → {B : Set} → B → A
- const x _ = x
-
- _$_ : {A : Set} {P : A → Set} (f : ∀ x → P x) (x : A) → P x
- f $ x = f x
-
- _×_ : (A B : Set) → Set
- A × B = Σ A (const B)
-
- case_of_ : {A : Set} {P : A → Set} (x : A) → ((x : A) → P x) → P x
- case x of f = f x
-
- _∘_ : {A : Set} {P : A → Set} {Q : {x : A} → P x → Set}
- (g : {x : A} → (y : P x) → Q y) (f : (x : A) → P x)
- → (x : A) → Q (f x)
- _∘_ g f x = g (f x)
-
- data Fin : Nat → Set where
- zero : ∀ {n} → Fin (suc n)
- suc : ∀ {n} → Fin n → Fin (suc n)
-
- data Vec (A : Set) : Nat → Set where
- [] : Vec A 0
- _∷_ : ∀ {n} → A → Vec A n → Vec A (suc n)
-
- lookup : {A : Set} {n : Nat}
- → Vec A n → Fin n → A
- lookup (x ∷ _) zero = x
- lookup (_ ∷ xs) (suc n) = lookup xs n
-
- map : (A → B) → {n : Nat} → Vec A n → Vec B n
- map f [] = []
- map f (x ∷ xs) = f x ∷ map f xs
-
- Rel : Set → Set → Set
- Rel A B = A → B → Set
-
-.. raw:: html
-
-
-
-A universe of descriptions
-~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-The first step is to equip ourselves with a universe of descriptions to encode
-inductive indexed datatypes. See the work from Pierre-Evariste Dagand[#dagand]_
-to learn about descriptions. The one chosen here is an extension of Yorick
-Sijsling's [#yorick]_, with some additions:
-
-.. [#dagand] In particular, his PhD thesis:
- `Reusability and Dependent Types
- `_
-.. [#yorick] https://github.com/yoricksijsling/ornaments-thesis
-
-- indices now depend on the parameters;
-- recursive occurences can have different parameters.
- **Actually I removed this for the time being, since it's not really important for what we are trying
- to achieve. Still, can be done.**
-
-Encoding telescopes 🔭
----------------------
-
-So we begin by defining an encoding of telescopes to encode the parameters and
-indices of datatypes. I just found out it is very similar to what is
-introduced in [Akaposi2015]_. What we are apparently doing is adding telescopes
-and telescope substitutions in our theory, whereas they leave them outside of types.
-
-.. [Akaposi2015] | **Towards cubical type theory**
- | Thorsten Altenkirch, Ambrus Kaposi
- | https://akaposi.github.io/nominal.pdf
-
-In summary, we define **the type of telescopes** parametrized by some set `A`.
-And given a telescope, and an element of `A`, we define **the type of telescope substitutions**:
-
-.. math::
- \gdef\set{\textsf{Set}}
- \gdef\tele#1{\textsf{Tele}\ #1}
- \gdef\rel#1#2{\textsf{Rel}\ #1\ #2}
-
- A : \set\ &⊢\ \tele A : \set \\
- A : \set,\ Ω : \tele A,\ x : A\ &⊢ ⟦ Ω ⟧\ x \ : \set
-
-For our purposes, a telescope substitution is a huge Σ-type containing an element for
-every type in the telescope. We can introduce empty telescopes or extend them by the right.
-
-.. math::
- \frac{}{A : \set \ ⊢\ ε : \tele A} \quad
- \frac
- {A : \set,\ Ω : \tele A,\ ⊢\ F : Σ\ A\ ⟦ Ω ⟧ → \set}
- {A : \set,\ Ω : \tele A\ ⊢\ Ω\ ▷\ F : \tele A}
-
-::
-
- infixl 1 _▷_ _▷₀_
-
- data Tele (A : Set) : Set
- ⟦_⟧ : {A : Set} → Tele A → A → Set
-
- data Tele A where
- ε : Tele A
- _▷_ : (T : Tele A) → (Σ A ⟦ T ⟧ → Set) → Tele A
-
- ⟦ ε ⟧ x = ⊤
- ⟦ T ▷ F ⟧ x = Σ (⟦ T ⟧ x) (F ∘ (x ,_))
-
- _▷₀_ : {A : Set} (T : Tele A) (B : Set) → Tele A
- T ▷₀ B = T ▷ const B
-
-Because telescopes are parametrized by some :code:`Set`,
-we can define a telescope that depend on the telescope substitution of another telescope.
-**That's how we encode parameters-dependent indices**. Describing the parameters and indices
-of a datatype boils down to exhibiting some :code:`P` and :code:`I` such that
-:code:`P : Tele ⊤` and :code:`I : Tele (⟦ T ⟧ tt)`.
-
-We too can **extend telescopes with telescopes**.
-For our purposes, it only makes sense to extend non-parametrized telescopes:
-
-.. math::
- Ω : \tele ⊤,\ Ω' : \tele (⟦ Ω ⟧\ tt)\
- &⊢ \textsf{extend}\ Ω' : \tele ⊤ \\
- Ω : \tele ⊤,\ Ω' : \tele (⟦ Ω ⟧\ tt)\
- &⊢ \textsf{pr}\ : ⟦ \textsf{extend}\ Ω' ⟧\ tt → Σ\ (⟦ Ω ⟧\ tt)\ ⟦ Ω' ⟧
-
-::
-
- ExTele : Tele ⊤ → Set
- ExTele T = Tele (⟦ T ⟧ tt)
-
- Ctx : {T : Tele ⊤} → ExTele T → Set
- Ctx Γ = Σ _ ⟦ Γ ⟧
-
- extend : {T : Tele ⊤} → ExTele T → Tele ⊤
- pr : {T : Tele ⊤} {Γ : ExTele T}
- → ⟦ extend Γ ⟧ tt → Ctx Γ
-
- extend {T} ε = T
- extend (G ▷ F) = extend G ▷ F ∘ pr ∘ snd
-
- pr {Γ = ε} γ = γ , tt
- pr {Γ = Γ ▷ F} (γ′ , x) =
- let (t , γ) = pr γ′ in t , γ , x
-
-Constructors
-------------
-
-Like Yorick we describe constructors first and datatypes second by giving a vector
-of constructor descriptions. This has the benefit of following more closely the structure
-of Agda datatypes::
-
- data ConDesc {P : Tele ⊤} (Γ I : ExTele P) : Set
-
-Both the constructor's current context :code:`Γ` and its indices :code:`I` are extensions
-of the datatype parameters. The rest is pretty standard:
-
-- :code:`κ` **marks the end of a constructor**. We simply compute indices from the current context.
-- :code:`ι` **marks the position of a recursive occurence**. Here we provide indices
- computed from the context. I am saddened by the fact that this
- recursive occurence is not added to the context of the rest of the constructor.
- This can probably be done but would require too much effort for what it's worth.
- Who does that anyway?
-- :code:`σ` **marks the introduction of a variable**. Its type is computed from the local context,
- and the variable is added to the context for the rest of the constructor.
-
-::
-
- data ConDesc {P} Γ I where
- κ : (f : (γ : Ctx Γ) → ⟦ I ⟧ (γ .fst)) → ConDesc Γ I
- ι : (f : (γ : Ctx Γ) → ⟦ I ⟧ (γ .fst)) → ConDesc Γ I → ConDesc Γ I
- σ : (S : Ctx Γ → Set ) → ConDesc (Γ ▷ S) I → ConDesc Γ I
-
-..
-
-::
-
- ⟦_⟧ᶜ : {P : Tele ⊤} {Γ I : ExTele P}
- (C : ConDesc Γ I)
- → (Ctx I → Set)
- → (Σ (⟦ P ⟧ tt) (λ p → ⟦ Γ ⟧ p × ⟦ I ⟧ p) → Set)
-
- ⟦ κ f ⟧ᶜ X (p , γ , i) = f (p , γ) ≡ i
- ⟦ ι f C ⟧ᶜ X g@(p , γ , _) = X (p , f (p , γ)) × ⟦ C ⟧ᶜ X g
- ⟦ σ S C ⟧ᶜ X (p , γ , i) = Σ (S (p , γ)) λ s → ⟦ C ⟧ᶜ X (p , (γ , s) , i)
-
-Datatypes
----------
-
-Moving on, we encode datatypes as a vector of constructor descriptions that
-share the same parameters and indices telescopes. Then we tie the knot::
-
- Desc : (P : Tele ⊤) (I : ExTele P) → Nat → Set
- Desc P I n = Vec (ConDesc ε I) n
-
- ⟦_⟧ᵈ : {P : Tele ⊤} {I : ExTele P} {n : Nat}
- (D : Desc P I n)
- → (Ctx I → Set)
- → (Ctx I → Set)
-
- ⟦_⟧ᵈ {n = n} D X (p , i) = Σ (Fin n) λ k → ⟦ lookup D k ⟧ᶜ X (p , tt , i)
-
- data μ {n} {P : Tele ⊤} {I : ExTele P}
- (D : Desc P I n) (pi : Ctx I) : Set where
- ⟨_⟩ : ⟦ D ⟧ᵈ (μ D) pi → μ D pi
-
-
-We can also define some helper :code:`constr` to easily retrieve the `k` th constructor from a description::
-
- module _ {P : Tele ⊤} {I : Tele (⟦ P ⟧ tt)} {n : Nat} (D : Desc P I n) where
-
- Constr′ : {Γ : Tele (⟦ P ⟧ tt)}
- → ConDesc Γ I
- → Ctx Γ
- → Set
- Constr′ (κ f ) pg = μ D (fst pg , f pg)
- Constr′ (ι f C) pg = μ D (fst pg , f pg) → Constr′ C pg
- Constr′ (σ S C) (p , γ) = (s : S (p , γ)) → Constr′ C (p , γ , s)
-
- module _ {C′ : ConDesc ε I} (mk : {(p , i) : Ctx I} → ⟦ C′ ⟧ᶜ (μ D) (p , tt , i) → μ D (p , i)) where
-
- constr′ : {Γ : Tele (⟦ P ⟧ tt)}
- (C : ConDesc Γ I)
- ((p , γ) : Ctx Γ)
- → ({i : ⟦ I ⟧ p} → ⟦ C ⟧ᶜ (μ D) (p , γ , i) → ⟦ C′ ⟧ᶜ (μ D) (p , tt , i))
- → Constr′ C (p , γ)
- constr′ (κ f ) pg tie = mk (tie refl)
- constr′ (ι f C) pg tie x = constr′ C pg (tie ∘ (x ,_))
- constr′ (σ S C) (p , γ) tie s = constr′ C (p , γ , s) (tie ∘ (s ,_))
-
- -- | type of the kth constructor
- Constr : (k : Fin n) (p : ⟦ P ⟧ tt) → Set
- Constr k p = Constr′ (lookup D k) (p , tt)
-
- -- | kth constructor
- constr : (k : Fin n) (p : ⟦ P ⟧ tt) → Constr k p
- constr k p = constr′ (λ x → ⟨ k , x ⟩) (lookup D k) (p , tt) id
-
-Another useful operation is to retrieve a telescope for every constructor of datatype.
-
-::
-
- module _ {P : Tele ⊤} {I : ExTele P} (X : Ctx I → Set) where
- contotele′ : {Γ : ExTele P}
- → ConDesc Γ I
- → (T : ExTele P)
- → (((p , γ) : Ctx T) → ⟦ Γ ⟧ p)
- → ExTele P
- contotele′ (κ _) T mk = T
- contotele′ (ι f C) T mk =
- contotele′ C (T ▷ λ (p , γ) → X (p , f (p , mk (p , γ))))
- λ (p , γ , x) → mk (p , γ)
- contotele′ (σ S C) T mk =
- contotele′ C (T ▷ λ (p , γ) → S (p , (mk (p , γ))))
- λ (p , γ , s) → (mk (p , γ)) , s
-
-
- contotele : {P : Tele ⊤} {I : ExTele P} {n : Nat}
- → Desc P I n
- → Fin n
- → ExTele P
- contotele D k = contotele′ (μ D) (lookup D k) ε (const tt)
-
-Examples
---------
-
-Some examples to reassure ourselves as to whether it works as intended::
-
- module Examples where
-
- natD : Desc ε ε 2
- natD = κ (const tt)
- ∷ ι (const tt) (κ (const tt))
- ∷ []
-
- nat : Set
- nat = μ natD (tt , tt)
-
- ze : Constr natD zero tt
- ze = constr natD zero tt
-
- su : Constr natD (suc zero) tt
- su = constr natD (suc zero) tt
-
- vecD : Desc (ε ▷₀ Set) (ε ▷₀ nat) 2
- vecD = κ (const (tt , ze))
- ∷ σ (const nat)
- (σ (λ (p , _) → p .snd)
- (ι (λ (p , ((tt , n) , x )) → tt , n)
- (κ (λ (_ , ((tt , n) , _)) → tt , (su n)))))
- ∷ []
-
- vec : (A : Set) → nat → Set
- vec A n = μ vecD ((tt , A) , tt , n)
-
- nil : {A : Set} → Constr vecD zero (tt , A)
- nil {A} = constr vecD zero (tt , A)
-
- cons : {A : Set} → Constr vecD (suc zero) (tt , A)
- cons {A} = constr vecD (suc zero) (tt , A)
-
- xs : vec nat (su (su ze))
- xs = cons _ (su ze) (cons _ (su (su ze)) nil)
-
-So far so good. Let's move to the fun part, we're in for the big bucks.
-
-
-From descriptions to descriptions
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-To keep our goal in sight, here is what should happen for lists::
-
- module Translation where
-
- module Goal where
-
- listD : Desc (ε ▷ const Set) ε 2
- listD = κ (const tt)
- ∷ σ (λ ((tt , A) , γ) → A)
- (ι (λ (p , γ) → tt)
- (κ (const tt)))
- ∷ []
-
- list : Set → Set
- list A = μ listD ((tt , A) , tt)
-
- nil : {A : Set} → list A
- nil {A} = ⟨ zero , refl ⟩
-
- cons : {A : Set} → A → list A → list A
- cons x xs = ⟨ suc zero , x , xs , refl ⟩
-
- -- the following is the description we want to derive
- -- listᵣD : Desc (ε ▷₀ Set ▷₀ Set ▷ λ (tt , (tt , A) , B) → Rel A B)
- -- (ε ▷ (λ ((((_ , A) , B) , R) , tt) → list A)
- -- ▷ (λ ((((_ , A) , B) , R) , tt , _) → list B)) 2
- -- listᵣD = κ (λ ((((tt , A) , B) , R) , tt) → (tt , nil) , nil)
- -- ∷ ( σ (λ (((( A) , B) , R) , tt) → A )
- -- $ σ (λ ((((tt , A) , B) , R) , tt , _) → B )
- -- $ σ (λ ((_ , R) , (tt , x) , y) → R x y )
- -- $ σ (λ ((((tt , A) , B ) , R) , _) → list A )
- -- $ σ (λ ((((tt , A) , B ) , R) , _) → list B )
- -- $ ι (λ (γ , (_ , xs) , ys) → γ , (tt , xs) , ys )
- -- $ κ (λ (_ , (((((_ , x) , y) , _) , xs) , ys)) → (tt , cons x xs) , cons y ys)
- -- )
- -- ∷ []
-
- -- listᵣ : {A B : Set} (R : Rel A B) → list A → list B → Set
- -- listᵣ {A} {B} R xs ys = μ listᵣD ((((tt , A) , B) , R) , (tt , xs) , ys)
-
- -- nilᵣ : {A B : Set} {R : Rel A B} → listᵣ R nil nil
- -- nilᵣ = ⟨ zero , refl ⟩
-
- -- consᵣ : {A B : Set} {R : Rel A B}
- -- → ∀ {x y } (x≈y : R x y)
- -- → ∀ {xs ys} (xs≈ys : listᵣ R xs ys)
- -- → listᵣ R (cons x xs) (cons y ys)
- -- consᵣ {x = x} {y} x≈y {xs} {ys} xs≈ys =
- -- ⟨ suc zero , x , y , x≈y , xs , ys , xs≈ys , refl ⟩
-
-Hm. What we expect to generate looks like a mess. On a positive note it does
-seem like we do not need to add recursive occurences to the context. It is also reassuring that
-we can indeed encode the relation. Tbh the relation on its own is not *that* useful.
-What would be great is if we were able to derive the abstraction theorem for this datatype too::
-
- -- param : (R : Rel A A) (PA : ∀ x → R x x)
- -- → (xs : list A) → listᵣ R xs xs
- -- param R PA ⟨ zero , refl ⟩ = nilᵣ
- -- param R PA ⟨ suc zero , x , xs , refl ⟩ = consᵣ (PA x) (param R PA xs)
-
-This also looks quite doable.
-
-Moving forward while keeping our head down.
-
-
-Relating telescope substitutions
---------------------------------
-
-The first thing we need is a relation on telescope substitutions.
-Naturally, because substitutions are encoded as Σ-types, two substitutions are related
-iff their elements are related one to one, using the relational
-interpretation of their respective types.
-
-.. math::
- T : \tele A,\ x_1 : A,\ x_2 : A,\ x_r : ⟦A⟧_p
- \ ⊢ ⟦Π\ A\ ⟦ T ⟧ ⟧_p\ x_1\ x_2\ x_r : \rel {(⟦ T ⟧\ x_1)} {(⟦ T ⟧\ x_2)}
-
-.. math::
- ⟦Π\ A\ ⟦ε⟧⟧_p\ x_1\ x_2\ x_r\ t_1\ t_2 &≡ ⊤ \\
- ⟦Π\ A\ ⟦T\ ▷\ F⟧⟧_p\ x_1\ x_2\ x_r\ (t_1 , s_1)\ (t_2 , s_2) &≡
- Σ\ (⟦Π\ A\ ⟦T⟧⟧_p\ x_1\ x_2\ x_r\ t_1\ t_2)\ λ\ t_r\ .
- \ ⟦ F ⟧_p\ t_1\ t_2\ t_r\ s_1\ s_2
-
-The only problem here is that we need `⟦A⟧_p` and `⟦F⟧_p`. We cannot possibly compute it,
-because `A` could be virtually *anything*, not just one of our friendly described datatypes.
-An easy way out is to kindly ask for these relations. Therefore we introduce a new type
-`\textsf{Help}\ T` associated with the telescope `T` we're trying to translate,
-whose inhabitants must hold every required relation.
-
-::
-
- Help : Tele A → A → A → Set
-
- -- I suspect we don't care about xᵣ so I'm omitting it
- ₜ⟦_⟧ₚ : (T : Tele A) {x y : A} → Help T x y → Rel (⟦ T ⟧ x) (⟦ T ⟧ y)
-
- Help ε _ _ = ⊤
- Help (T ▷ F) x₁ x₂ = Σ (Help T x₁ x₂)
- λ H → ∀ t₁ t₂ (tᵣ : ₜ⟦ T ⟧ₚ H t₁ t₂)
- → Rel (F (x₁ , t₁)) (F (x₂ , t₂))
-
- ₜ⟦ ε ⟧ₚ tt tt tt = ⊤
- ₜ⟦ T ▷ F ⟧ₚ (H , HF) (t₁ , s₁) (t₂ , s₂) =
- Σ (ₜ⟦ T ⟧ₚ H t₁ t₂) λ tᵣ → HF t₁ t₂ tᵣ s₁ s₂
-
- ExHelp : {P : Tele ⊤} → ExTele P → Set
- ExHelp I = ∀ p₁ p₂ → Help I p₁ p₂
-
-
-Not my type
------------
-
-Our relation will be inductively defined, so we need to figure out beforehand its
-parameters and indices. Parameters are easy, we expect two substitutions of the initial
-parameters' telescope, and a proof that they are related.
-
-::
-
- module _ {P : Tele ⊤} {I : ExTele P} {n : Nat}
- (D : Desc P I n)
- (HP : Help P tt tt) (HI : ExHelp I)
- where
-
- Pₚ : Tele ⊤
- Pₚ = ε
- ▷₀ ⟦ P ⟧ tt
- ▷₀ ⟦ P ⟧ tt
- ▷ λ (_ , (_ , p₁) , p₂) → ₜ⟦ P ⟧ₚ HP p₁ p₂
-
- p₁ : ⟦ Pₚ ⟧ tt → ⟦ P ⟧ tt
- p₁ (((_ , p) , _) , _) = p
-
- p₂ : ⟦ Pₚ ⟧ tt → ⟦ P ⟧ tt
- p₂ (((_ , _) , p) , _) = p
-
- Iₚ : ExTele Pₚ
- Iₚ = ε
- ▷ (λ ((((_ , p₁) , _) , _) , _) → ⟦ I ⟧ p₁)
- ▷ (λ ((((_ , _) , p₂) , _) , _) → ⟦ I ⟧ p₂)
- ▷ (λ ((((_ , p₁) , _) , _) , (_ , i₁) , _) → μ D (p₁ , i₁))
- ▷ (λ ((((_ , _) , p₂) , _) , (_ , i₂) , _) → μ D (p₂ , i₂))
-
-
-Apart from the typical clumsiness of dealing with substitutions, we have our parameters and indices.
-
-----
-
-::
-
- Cₚ′ : {Γₚ : ExTele Pₚ}
- {Γ : ExTele P}
- → (C : ConDesc Γ I)
- → (c₁ : {p : ⟦ Pₚ ⟧ tt} → ⟦ Γₚ ⟧ p → ⟦ Γ ⟧ (p₁ p))
- → (c₂ : {p : ⟦ Pₚ ⟧ tt} → ⟦ Γₚ ⟧ p → ⟦ Γ ⟧ (p₂ p))
- → (f₁ : ⟦ C ⟧ᶜ (μ D) ({!!} , {!!}) → μ D ({!!} , {!!}))
- → (ConDesc Γₚ Iₚ → ConDesc ε Iₚ)
- → ConDesc ε Iₚ
-
- Cₚ′ (κ f) g₁ g₂ _ tie =
- tie (κ (λ (p , g) → (((tt , ( f (p₁ p , g₁ g)))
- , f (p₂ p , g₂ g))
- , {!!}) , {!!}))
-
- Cₚ′ (ι f C) c₁ c₂ _ tie =
- Cₚ′ C
- (c₁ ∘ λ ((p , _) , _) → p)
- (c₂ ∘ λ ((p , _) , _) → p)
- {!!}
- (tie ∘ λ C → σ (λ (p , g) → μ D (p₁ p , f (p₁ p , c₁ g)))
- $ σ (λ (p , g , _) → μ D (p₂ p , f (p₂ p , c₂ g)))
- $ ι (λ (p , (_ , x) , y) → (((tt , _) , _) , x) , y)
- $ C)
-
- Cₚ′ (σ S C) c₁ c₂ _ tie =
- Cₚ′ C
- (λ (((g , s₁) , _) , _) → c₁ g , s₁)
- (λ (((g , _) , s₂) , _) → c₂ g , s₂)
- {!!}
- (tie ∘ λ C → σ (λ (p , g) → S (p₁ p , c₁ g))
- $ σ (λ (p , g , _) → S (p₂ p , c₂ g))
- $ σ {!!} -- we need some some relation here
- $ C)
-
- Cₚ : ConDesc ε I → ConDesc ε Iₚ
- Cₚ C = Cₚ′ C id id {!!} id
-
- Dₚ : Desc Pₚ Iₚ n
- Dₚ = map Cₚ D
-
-CPS all the way.
-
-----
-
-Assuming we had implement what's missing above, we would have the relation we wanted::
-
- ⟦_⟧ₚ : {p₁ p₂ : ⟦ P ⟧ tt} (pᵣ : ₜ⟦ P ⟧ₚ HP p₁ p₂)
- {i₁ : ⟦ I ⟧ p₁} {i₂ : ⟦ I ⟧ p₂}
- → Rel (μ D (p₁ , i₁)) (μ D (p₂ , i₂))
- ⟦_⟧ₚ pᵣ t₁ t₂ = μ Dₚ ((_ , pᵣ) , (_ , t₁) , t₂)
-
-The abstraction theorem becomes::
-
- -- param : ∀ {p i} (t : μ D (p , i)) → ⟦_⟧ₚ {!!} {!!} t t
- -- param = {!!}
-
-
-----
-
-An exemple on lists:
-
-----
-
-Conclusion
-~~~~~~~~~~
-
-Now, why should we care? Well, I don't really know just yet.
-I do think there is value in having such transformations implemented in a type-safe way.
-Still, because these representations are not intrinsic to how datatypes are defined in the theory,
-it make for a clumsy experience. Add the lack of cumulativity and everything becomes quite tedious.
-
-Things I would like to explore next:
-
-- Derive the proofs that any datatype and its constructors are univalently parametric.
- As of now we can derive the relation, what remains to be proven is deriving an equivalence (easy)
- and a proof that the two are equivalent.
-
-- Get rid of the :code:`--type-in-type` flag, using Effectfully's technique, or embracing :code:`--cumulativity`?
-
-- Investigate encodings of other constructions: Co-inductive types? Records?
-
-- Look into Formality's encoding of datatypes and what it means for generic programming.
-
-----
-
-.. [Bernardy2010] | **Parametricity and Dependent Types**
- | Jean-Philippe Bernardy, Patrik Jansson, Ross Paterson
- | http://www.staff.city.ac.uk/~ross/papers/pts.pdf
-
-.. [Tabareau2019] | **The Marriage of Univalence and Parametricity**
- | Nicolas Tabareau, Eric Tanter, Matthieu Sozeau
- | https://arxiv.org/pdf/1909.05027.pdf
-
diff --git a/content/projects/achille/index.markdown b/content/projects/achille/index.markdown
index 78db6e3..76ebd5d 100644
--- a/content/projects/achille/index.markdown
+++ b/content/projects/achille/index.markdown
@@ -10,531 +10,5 @@ labels:
**achille** [aʃil] is a tiny Haskell library for building your very own **static site
generator**. It is in spirit a direct successor to [Hakyll][Hakyll].
-## Motivation
-
-Static site generators (SSG) have proven to be very useful tools for easily
-generating static websites from neatly organised content files. Most of them
-support using **markup languages** like markdown for writing content, and offer
-**incremental compilation** so that updating a website stays **fast**,
-regardless of its size. However, most SSGs are very opinionated about how you
-should manage your content. As soon as your specific needs deviate slightly
-from what your SSG supports, it becomes a lot more tedious.
-
-This leads to many people writing their own personal static site generators
-from scratch. This results in a completely personalised workflow, but without
-good libraries it is a time-consuming endeavor, and incremental compilation is often
-out of the equation as it is hard to get right.
-
-This is where **achille** and [Hakyll][Hakyll] come in: they provide a *domain
-specific language* embedded in Haskell to easily yet very precisely describe
-how to build your site. Compile this description and **you get a full-fledged
-static site generator with incremental compilation**, tailored specifically to
-your needs.
-
[Hakyll]: https://jaspervdj.be/hakyll
-### Why Hakyll is not enough
-
-To provide incremental compilation, Hakyll relies on a global store, in which
-all your *intermediate values* are stored. It is *your* responsibility to
-populate it with *snapshots*. There are some severe limitations to this
-approach:
-
-- The store is **fundamentally untyped**, so **retrieving snapshots may fail at
- runtime** if you're not careful when writing your build rules. You may
- argue that's not very critical --- I think it shouldn't be possible in the
- first place. We are using a strongly typed language, so we shouldn't have
- to rely on flaky coercions at runtime to manipulate intermediate values.
-
-- **Loading snapshots with glob patterns is awkward**. With Hakyll, *the*
- way to retrieve intermediate values is by querying the store,
- using glob patterns. This indirect way of managing values is very
- clumsy. In Haskell, the very purpose of variables is to store intermediate
- values, so we should only have to deal with plain old variables.
-
-- **Dependencies are not explicit**. Because it relies on a global store for
- handling intermediate values, Hakyll has to make sure that the snaphots you
- want to load have been generated already. And because rules have no imposed
- order despite implicit inter-dependencies, Hakyll has to evaluate very
- carefully each rule, eventually pausing them to compute missing dependencies.
- This is very complex and quite frankly impressive, yet I believe we can strive
- for a simpler model of evaluation. If we used plain old variables to hold
- intermediate values, we simply would not be allowed to refer to an undefined
- variable.
-
-There are other somewhat debatable design decisions:
-
-- In Hakyll, every rule will produce an output file, and only one, if you're
- restricting yourself to the API they provide. I argue
- such a library should not care whether a rule produces any output on the
- filesystem. Its role is merely to know *if the rule must be executed*. Because of
- this requirement, producing multiple outputs from the same file is a tad
- cumbersome.
-- Because Hakyll stores many content files directly in the store, the resulting
- cache is *huge*. This is unnecessary, the files are right here in the content
- directory.
-- Hakyll uses a *lot* of abstractions --- `Compiler`, `Item`, `Rule`, `RuleSet`
- --- whose purpose is not obvious to a newcomer.
-- It defines monads to allow the convenient `do` notation to be used, but
- disregards completely the very benefit of using monads --- it composes!
-
-### Other tools
-
-As always when thinking I am onto something, I jumped straight into code
-and forgot to check whether there were alternatives. By fixating on Hakyll, I did not
-realize many people have had the same comments about the shortcomings of Hakyll
-and improved upon it. Therefore, it's only after building most of **achille**
-in a week that I realized there were many
-other similar tools available, namely: [rib][rib], [slick][slick], [Pencil][pencil] &
-[Lykah][lykah].
-
-[rib]: https://rib.srid.ca/
-[slick]: https://hackage.haskell.org/package/slick
-[pencil]: http://elbenshira.com/pencil/
-[lykah]: https://hackage.haskell.org/package/Lykah
-
-Fortunately, I still believe **achille** is a significant improvement over these libraries.
-
-- As far as I can tell, **pencil** does not provide incremental generation.
- It also relies on a global store, no longer untyped but very
- restrictive about what you can store. It implements its own templating language.
-- Likewise, no incremental generation in **Lykah**.
- Reimplements its own HTML DSL rather than use *lucid*.
- Very opinionated, undocumented and unmaintained.
-- **rib** and **slick** are the most feature-complete of the lot.
- They both provide a minimalist web-focused interface over the very powerful build system
- [Shake][Shake].
-
-[Shake]: https://shakebuild.com/
-
-## How achille works
-
-In **achille** there is a single abstraction for reasoning about build rules:
-`Recipe m a b`. A **recipe** of type `Recipe m a b` will produce a value of type
-`m b` given some input of type `a`.
-Conveniently, if `m` is a monad then **`Recipe m a` is a monad** too, so
-you can retrieve the output of a recipe to reuse it in another recipe.
-
-*(Because of caching, a recipe is **not** just a Kleisli arrow)*
-
-
-```haskell
--- the (>>=) operator, restricted to recipes
-(>>=) :: Monad m => Recipe m a b -> (b -> Recipe m a c) -> Recipe m a c
-```
-
-With only this, **achille** tackles every single one of the limitations highlighted above.
-
-- Intermediate values are plain old Haskell variables.
-
- ```haskell
- renderPost :: Recipe IO FilePath Post
- buildPostIndex :: [Post] -> Recipe a ()
-
- renderPosts :: Task IO ()
- renderPosts = do
- posts <- match "posts/*" renderPost
- buildPostIndex posts
- ```
-
- See how a correct ordering of build rules is enforced by design: you can only
- use an intermediate value once the recipe it is originating from has been
- executed.
-
- Note: a **task** is a recipe that takes no input.
-
- ```haskell
- type Task m = Recipe m ()
- ```
-
-- **achille** does not care what happens during the execution of a recipe.
- It only cares about the input and return type of the recipe --- that is, the
- type of intermediate values.
- In particullar, **achille** does not expect every recipe to produce a file,
- and lets you decide when to actually write on the filesystem.
-
- For example, it is very easy to produce multiple versions of a same source file:
-
- ```haskell
- renderPage :: Recipe IO FilePath FilePath
- renderPage = do
- -- Copy the input file as is to the output directory
- copyFile
-
- -- Render the input file with pandoc,
- -- then save it to the output dir with extension ".html"
- compilePandoc >>= saveTo (-<.> "html")
- ```
-
-Once you have defined the recipe for building your site, you forward
-this description to **achille** in order to get a command-line interface for
-your generator, just as you would using Hakyll:
-
-```haskell
-buildSite :: Task IO ()
-
-main :: IO ()
-main = achille buildSite
-```
-
-Assuming we compiled the file above into an executable called `site`, running
-it gives the following output:
-
-```bash
-$ site
-A static site generator for fun and profit
-
-Usage: site COMMAND
-
-Available options:
- -h,--help Show this help text
-
-Available commands:
- build Build the site once
- deploy Server go brrr
- clean Delete all artefacts
-```
-
-That's it, you now have your very own static site generator!
-
-### Caching
-
-So far we haven't talked about caching and incremental builds.
-Rest assured: **achille produces generators with robust incremental
-builds** for free. To understand how this is done, we can simply look at the
-definition of `Recipe m a b`:
-
-```haskell
--- the cache is simply a lazy bytestring
-type Cache = ByteString
-
-newtype Recipe m a b = Recipe (Context a -> m (b, Cache))
-```
-
-In other words, when a recipe is run, it is provided a **context** containing
-the input value, **a current cache** *local* to the recipe, and some more
-information. The IO action is executed, and we update the local cache with the
-new cache returned by the recipe. We say *local* because of how composition of
-recipes is handled internally. When the *composition* of two recipes (made with
-`>>=` or `>>`) is being run, we retrieve two bytestrings from the local cache
-and feed them as local cache to both recipes respectively. Then we gather the two updated
-caches, join them and make it the new cache of the composition.
-
-This way, a recipe is guaranteed to receive the same local cache it returned
-during the last run, *untouched by other recipes*. And every recipe is free to
-dispose of this local cache however it wants.
-
-As a friend noted, **achille** is "just a library for composing memoized
-computations".
-
-----
-
-#### High-level interface
-
-Because we do not want the user to carry the burden of updating the cache
-manually, **achille** comes with many utilies for common operations, managing
-the cache for us under the hood. Here is an exemple highlighting how we keep
-fine-grained control over the cache at all times, while never having to
-manipulate it directly.
-
-Say you want to run a recipe for every file maching a glob pattern, *but do
-not care about the output of the recipe*. A typical exemple would be to copy
-every static asset of your site to the output directory. **achille** provides
-the `match_` function for this very purpose:
-
-```haskell
-match_ :: Glob.Pattern -> Recipe FilePath b -> Recipe a ()
-```
-
-We would use it in this way:
-
-```haskell
-copyAssets :: Recipe a ()
-copyAssets = match_ "assets/*" copyFile
-
-main :: IO ()
-main = achille copyAssets
-```
-
-Under the hood, `match_ p r` will cache every filepath for which the recipe was
-run. During the next run, for every filepath matching the pattern, `match_ p r` will
-lookup the path in its cache. If it is found and hasn't been modified since,
-then we do nothing for this path. Otherwise, the task is run and the filepath
-added to the cache.
-
-Now assume we do care about the output of the recipe we want to run on every filepath.
-For example if we compile every blogpost, we want to retrieve each blogpost's title and
-the filepath of the compiled `.html` file. In that case, we can use the
-built-in `match` function:
-
-```haskell
-match :: Binary b
- => Glob.Pattern -> Recipe FilePath b -> Recipe a [b]
-```
-
-Notice the difference here: we expect the type of the recipe output `b` to have
-an instance of `Binary`, **so that we can encode it in the cache**. Fortunately,
-many of the usual Haskell types have an instance available. Then we can do:
-
-```haskell
-data PostMeta = PostMeta { title :: Text }
-renderPost :: Text -> Text -> Text
-renderIndex :: [(Text, FilePath)] -> Text
-
-buildPost :: Recipe FilePath (Text, FilePath)
-buildPost = do
- (PostMeta title, pandoc) <- compilePandocMeta
- renderPost title pdc & saveAs (-<.> "html")
- <&> (title,)
-
-buildPost :: Recipe a [(Text, FilePath)]
-buildPosts = match "posts/*.md" buildPost
-
-buildIndex :: [(Text, FilePath)] -> Recipe
-```
-
-#### Shortcomings
-
-The assertion *"A recipe will always receive the same cache between two runs"*
-can only violated in the two following situations:
-
-- There is **conditional branching in your recipes**, and more specifically,
- **branching for which the branch taken can differ between runs**.
-
- For example, it is **not** problematic to do branching on the extension of a file,
- as the same path will be taken each execution.
-
- But assuming you want to parametrize by some boolean value for whatever reason,
- whose value you may change between runs, then because the two branches will
- share the same cache, every time the boolean changes, the recipe will start
- from an inconsistent cache so it will recompute from scratch, and overwrite
- the existing cache.
-
- ```haskell
- buildSection :: Bool -> Task IO ()
- buildSection isProductionBuild =
- if isProductionBuild then
- someRecipe
- else
- someOtherRecipe
- ```
-
- Although I expect few people ever do this kind of conditional branching for
- generating a static site, **achille** still comes with combinators for branching.
- You can use `if` in order to keep two separate caches for the two branches:
-
- ```haskell
- if :: Bool -> Recipe m a b -> Recipe m a b -> Recipe m a b
- ```
-
- The previous example becomes:
-
- ```haskell
- buildSection :: Bool -> Task IO ()
- buildSection isProductionBuild =
- Achille.if isProductionBuild
- someRecipe
- someOtherRecipe
- ```
-
-### No runtime failures
-
-All the built-in cached recipes **achille** provides are implemented carefully
-so that **they never fail in case of cache corruption**. That is, in the
-eventuality of failing to retrieve the desired values from the cache, our
-recipes will automatically recompute the result from the input, ignoring the
-cache entirely. To make sure this is indeed what happens, every cached recipe
-in **achille** has been tested carefully (not yet really, but it is on the todo
-list).
-
-This means the only failures possible are those related to poor content
-formatting from the user part: missing frontmatter fields, watching files
-that do not exist, etc. All of those are errors are gracefully reported to the
-user.
-
-### Parallelism
-
-**achille** could very easily support parallelism for free, I just didn't take
-the time to make it a reality.
-
-
-## Making a blog from scratch
-
-Let's see how to use **achille** for making a static site generator for a blog.
-First we decide what will be the structure of our source directory.
-We choose the following:
-
-```bash
-content
-└── posts
- ├── 2020-04-13-hello-world.md
- ├── 2020-04-14-another-article.md
- └── 2020-05-21-some-more.md
-```
-
-We define the kind of metadata we want to allow in the frontmatter header
-of our markdown files:
-
-```haskell
-{-# LANGUAGE DeriveGeneric #-}
-
-import GHC.Generics
-import Data.Aeson
-import Data.Text (Text)
-
-data Meta = Meta
- { title :: Text
- } deriving (Generic)
-
-instance FromJSON Meta
-```
-
-This way we enfore correct metadata when retrieving the content of our files.
-Every markdown file will have to begin with the following header for our
-generator to proceed:
-
-```markdown
----
-title: Something about efficiency
----
-```
-
-Then we create a generic template for displaying a page, thanks to lucid:
-
-```haskell
-{-# LANGUAGE OverloadedStrings #-}
-{-# LANGUAGE BlockArguments #-}
-
-import Lucid.Html5
-
-renderPost :: Text -> Text -> Html a
-renderPost title content = wrapContent do
- h1_ $ toHtml title
- toHtmlRaw content
-
-renderIndex :: [(Text, FilePath)] -> Html a
-renderIndex = wrapContent .
- ul_ . mconcat . map \(title, path) ->
- li_ $ a_ [href_ path] $ toHtml title
-
-wrapContent :: Html a -> Html a
-wrapContent content = doctypehtml_ do
- head_ do
- meta_ [charset_ "utf-8"]
- title_ "my very first blog"
-
- body_ do
- header_ $ h1_ "BLOG"
- content_
-```
-
-We define a recipe for rendering every post:
-
-```haskell
-buildPosts :: Task IO [(String, FilePath)]
-buildPosts =
- match "posts/*.md" do
- (Meta title, text) <- compilePandocMetadata
- saveFileAs (-<.> "html") (renderPost title text)
- <&> (title,)
-```
-
-We can define a simple recipe for rendering the index, given a list of posts:
-
-```haskell
-buildIndex :: [(Text, FilePath)] -> Task IO FilePath
-buildIndex posts =
- save (renderIndex posts) "index.html"
-```
-
-Then, it's only a matter of composing the recipes and giving them to **achille**:
-
-```haskell
-main :: IO ()
-main = achille do
- posts <- buildPosts
- buildIndex posts
-```
-
-And that's it, you now have a very minimalist incremental blog generator!
-
-## Recursive recipes
-
-It is very easy to define recursive recipes in **achille**. This allows us to
-traverse and build tree-like structures, such as wikis.
-
-For example, given the following structure:
-
-```bash
-content
-├── index.md
-├── folder1
-│ └── index.md
-└── folder2
- ├── index.md
- ├── folder21
- │ └── index.md
- ├── folder22
- │ └── index.md
- └── folder23
- ├── index.md
- ├── folder231
- │ └── index.md
- ├── folder222
- │ └── index.md
- └── folder233
- └── index.md
-```
-
-We can generate a site with the same structure and in which each index page has
-links to its children:
-
-```haskell
-renderIndex :: PageMeta -> [(PageMeta, FilePath)] -> Text -> Html
-
-buildIndex :: Recipe IO a (PageMeta, FilePath)
-buildIndex = do
- children <- walkDir
-
- matchFile "index.*" do
- (meta, text) <- compilePandoc
- renderIndex meta children text >>= save (-<.> "html")
- return $ (meta,) <$> getInput
-
-walkDir :: Recipe IO a [(PageMeta, FilePath)]
-walkDir = matchDir "*/" buildIndex
-
-main :: IO ()
-main = achille buildIndex
-```
-
-## Forcing the regeneration of output
-
-Currently, **achille** doesn't track what files a recipe produces in the output
-dir. This means you cannot ask for things like *"Please rebuild
-output/index.html"*.
-
-That's because we make the assumption that the output dir is untouched between
-builds. The only reason I can think of for wanting to rebuild a specific page
-is if the template used to generate it has changed.
-But in that case, the template is *just another input*.
-So you can treat it as such by putting it in your content directory and doing
-the following:
-
-```haskell
-import Templates.Index (renderIndex)
-
-buildIndex :: Task IO ()
-buildIndex =
- watchFile "Templates/Index.hs" $ match_ "index.*" do
- compilePandoc <&> renderIndex >>= write "index.html"
-```
-
-This way, **achille** will automatically rebuild your index if the template has
-changed!
-
-While writing these lines, I realized it would be very easy for **achille**
-to know which recipe produced which output file,
-so I might just add that. Still, it would still require you to ask for an output
-file to be rebuilt if a template has changed. With the above pattern, it is
-handled automatically!
diff --git a/content/projects/jibniz/index.markdown b/content/projects/jibniz/index.markdown
index 5d6013e..0b59ebd 100644
--- a/content/projects/jibniz/index.markdown
+++ b/content/projects/jibniz/index.markdown
@@ -8,7 +8,20 @@ labels:
---
**jibniz** is a javascript implementation of the IBNIZ virtual machine.
-IBNIZ is an esoteric stack-based programming language created by _, in which almost every
+IBNIZ is an esoteric stack-based programming language created by _, in which every
instruction is one character long. The code is intended to be ran for each
-pixel on a 256x256 screen, at every frame, thus making it possible to produce
-animations.
+pixel on a 256x256 screen, at every frame --- making it possible to produce
+animations and interactive demos.
+
+## Limitations
+
+- Currently, this implementation has **no support for audio**. At the time I remember
+ the WebAudio API to be very poorly designed, and I did not understand how it was
+ implemented in the official IBNIZ VM.
+- I use WebGL for color conversion because I never figured out how to actually
+ reliably convert YUV to RGB. The original C implementation uses SDL2
+ Overlays or something, and I was not able to reverse engineer the conversion.
+ I found floating-point formulas, hence the GLSL shader, etc.
+- At some point I wanted to compile the entire IBNIZ programs to WASM, rather
+ than build an interpreter. The problem is that IBNIZ programs are *unstructured*.
+ the `J` instruction allows you to jump *anywhere* in the program.
diff --git a/content/quid.rst b/content/quid.rst
index b486584..7cf92ef 100644
--- a/content/quid.rst
+++ b/content/quid.rst
@@ -7,8 +7,8 @@ otherwise. In other words, you are free to copy, redistribute and edit this
content, provided you: give appropriate credit; indicate where changes were made
and do not do so for commercial purposes.
-This website is self-hosted on a OneProvider
-dedicated server in Paris. The domain name `acatalepsie.fr `_ has
+This website is hosted on a 2014 RPi Model B+ somewhere in France.
+The domain name `acatalepsie.fr `_ has
been registered at `gandi.net `_.
.. _CC BY-NC 2.0: https://creativecommons.org/licenses/by-nc/2.0/
diff --git a/content/visual/2019-03-11-dress.jpg b/content/visual/2019-03-11-dress.jpg
new file mode 120000
index 0000000..ccdcbe4
--- /dev/null
+++ b/content/visual/2019-03-11-dress.jpg
@@ -0,0 +1 @@
+../../.git/annex/objects/gZ/XG/SHA256E-s184840--08fe7d08c0d946d119eef787f31d0f28224fdfa001975450e83b66d7691072da.jpg/SHA256E-s184840--08fe7d08c0d946d119eef787f31d0f28224fdfa001975450e83b66d7691072da.jpg
\ No newline at end of file
diff --git a/content/visual/2019-03-11-duo2.png b/content/visual/2019-03-11-duo2.png
new file mode 120000
index 0000000..0b60c91
--- /dev/null
+++ b/content/visual/2019-03-11-duo2.png
@@ -0,0 +1 @@
+../../.git/annex/objects/k3/30/SHA256E-s631729--32753a717b3349dfdce80e732b32e53de3eb4361e8f77c76258b663c9e8cfa32.png/SHA256E-s631729--32753a717b3349dfdce80e732b32e53de3eb4361e8f77c76258b663c9e8cfa32.png
\ No newline at end of file
diff --git a/content/visual/2019-03-11-mashup.png b/content/visual/2019-03-11-mashup.png
new file mode 120000
index 0000000..aa202c8
--- /dev/null
+++ b/content/visual/2019-03-11-mashup.png
@@ -0,0 +1 @@
+../../.git/annex/objects/4p/V6/SHA256E-s918970--e7a695c389a762320704a52f5390c37a162dae81ff2df614ce38f40df03be73d.png/SHA256E-s918970--e7a695c389a762320704a52f5390c37a162dae81ff2df614ce38f40df03be73d.png
\ No newline at end of file
diff --git a/content/visual/2019-03-12-forest.png b/content/visual/2019-03-12-forest.png
new file mode 120000
index 0000000..f1453d5
--- /dev/null
+++ b/content/visual/2019-03-12-forest.png
@@ -0,0 +1 @@
+../../.git/annex/objects/J5/jZ/SHA256E-s1346919--a6f9e1df5e2593fa1a868244769f16522defbf4bd2c38e0c9014e379d93fdd68.png/SHA256E-s1346919--a6f9e1df5e2593fa1a868244769f16522defbf4bd2c38e0c9014e379d93fdd68.png
\ No newline at end of file
diff --git a/content/visual/2019-04-02-tat2.png b/content/visual/2019-04-02-tat2.png
new file mode 120000
index 0000000..70ba38f
--- /dev/null
+++ b/content/visual/2019-04-02-tat2.png
@@ -0,0 +1 @@
+../../.git/annex/objects/wj/7m/SHA256E-s299494--9826507fe82e22161368e3b8008aab5df58d6f4fdb8b29c4f47279faa3a35f74.png/SHA256E-s299494--9826507fe82e22161368e3b8008aab5df58d6f4fdb8b29c4f47279faa3a35f74.png
\ No newline at end of file
diff --git a/content/visual/2019-04-12-dragons.png b/content/visual/2019-04-12-dragons.png
new file mode 120000
index 0000000..46c43dd
--- /dev/null
+++ b/content/visual/2019-04-12-dragons.png
@@ -0,0 +1 @@
+../../.git/annex/objects/9J/X7/SHA256E-s670715--d1841af7719367ad43becc186af1d3c520b775bb2bf54da2cb92c135911dbbfb.png/SHA256E-s670715--d1841af7719367ad43becc186af1d3c520b775bb2bf54da2cb92c135911dbbfb.png
\ No newline at end of file
diff --git a/content/visual/2019-07-01-duo.png b/content/visual/2019-07-01-duo.png
new file mode 120000
index 0000000..4c42b1f
--- /dev/null
+++ b/content/visual/2019-07-01-duo.png
@@ -0,0 +1 @@
+../../.git/annex/objects/wp/jK/SHA256E-s321424--297046f12e2941743a19183faaaa8ebd55428367bc0ee2f457c467495481423c.png/SHA256E-s321424--297046f12e2941743a19183faaaa8ebd55428367bc0ee2f457c467495481423c.png
\ No newline at end of file
diff --git a/content/visual/2019-09-02-gauche.png b/content/visual/2019-09-02-gauche.png
new file mode 120000
index 0000000..3a0ea97
--- /dev/null
+++ b/content/visual/2019-09-02-gauche.png
@@ -0,0 +1 @@
+../../.git/annex/objects/m1/gJ/SHA256E-s1364718--8fdba85d9550064e2acab434042fcc0aeb376563516a8bf9ad3e2244db00021c.png/SHA256E-s1364718--8fdba85d9550064e2acab434042fcc0aeb376563516a8bf9ad3e2244db00021c.png
\ No newline at end of file
diff --git a/content/visual/2019-11-27-softsoft.jpg b/content/visual/2019-11-27-softsoft.jpg
new file mode 120000
index 0000000..eaaee62
--- /dev/null
+++ b/content/visual/2019-11-27-softsoft.jpg
@@ -0,0 +1 @@
+../../.git/annex/objects/gF/87/SHA256E-s458925--e06294cd0c55b73f4ff119ac3299d4f96139ede37ae2fb18110a126b48eede91.jpg/SHA256E-s458925--e06294cd0c55b73f4ff119ac3299d4f96139ede37ae2fb18110a126b48eede91.jpg
\ No newline at end of file
diff --git a/content/visual/2019-11-29-tandem6.png b/content/visual/2019-11-29-tandem6.png
new file mode 120000
index 0000000..9732e33
--- /dev/null
+++ b/content/visual/2019-11-29-tandem6.png
@@ -0,0 +1 @@
+../../.git/annex/objects/Q6/MF/SHA256E-s1949616--8f6aee3703fcec5d6e16724c39ad938d26e96b477855b9e05de180bad5bf6e51.png/SHA256E-s1949616--8f6aee3703fcec5d6e16724c39ad938d26e96b477855b9e05de180bad5bf6e51.png
\ No newline at end of file
diff --git a/content/visual/2020-01-05-collard.png b/content/visual/2020-01-05-collard.png
new file mode 120000
index 0000000..002f1ae
--- /dev/null
+++ b/content/visual/2020-01-05-collard.png
@@ -0,0 +1 @@
+../../.git/annex/objects/86/p5/SHA256E-s8693437--b5cde85117ffee4fc0ef1f9ae4a9887c12dced028baca4ce76939efef5568b84.png/SHA256E-s8693437--b5cde85117ffee4fc0ef1f9ae4a9887c12dced028baca4ce76939efef5568b84.png
\ No newline at end of file
diff --git a/content/visual/2020-02-10-mashup.png b/content/visual/2020-02-10-mashup.png
new file mode 120000
index 0000000..7ca7152
--- /dev/null
+++ b/content/visual/2020-02-10-mashup.png
@@ -0,0 +1 @@
+../../.git/annex/objects/27/kP/SHA256E-s600318--d1e1ae2cef2879eae698498f3c4e3b4907a9f39b227b0c3816fe020e34df066c.png/SHA256E-s600318--d1e1ae2cef2879eae698498f3c4e3b4907a9f39b227b0c3816fe020e34df066c.png
\ No newline at end of file
diff --git a/content/visual/2020-02-11-mattress2.png b/content/visual/2020-02-11-mattress2.png
new file mode 120000
index 0000000..eff7ebe
--- /dev/null
+++ b/content/visual/2020-02-11-mattress2.png
@@ -0,0 +1 @@
+../../.git/annex/objects/FF/Fp/SHA256E-s2521385--1ad730393c6d1c8159c966019893fbfacfef84b64eef47a26b4d0869e0f8fd58.png/SHA256E-s2521385--1ad730393c6d1c8159c966019893fbfacfef84b64eef47a26b4d0869e0f8fd58.png
\ No newline at end of file
diff --git a/content/visual/2020-03-14-mashupppp.png b/content/visual/2020-03-14-mashupppp.png
new file mode 120000
index 0000000..0375b13
--- /dev/null
+++ b/content/visual/2020-03-14-mashupppp.png
@@ -0,0 +1 @@
+../../.git/annex/objects/42/v4/SHA256E-s1446118--c14985cde38d539fe967254266bcacd35feb89fb9c2817e969ce916ae8967989.png/SHA256E-s1446118--c14985cde38d539fe967254266bcacd35feb89fb9c2817e969ce916ae8967989.png
\ No newline at end of file
diff --git a/content/visual/2020-04-09-mebee.png b/content/visual/2020-04-09-mebee.png
new file mode 120000
index 0000000..f11a25e
--- /dev/null
+++ b/content/visual/2020-04-09-mebee.png
@@ -0,0 +1 @@
+../../.git/annex/objects/1p/9X/SHA256E-s1411058--46562b966839842feae88561bdd7cd0e6106138ac17b79de7aa0228846d32aad.png/SHA256E-s1411058--46562b966839842feae88561bdd7cd0e6106138ac17b79de7aa0228846d32aad.png
\ No newline at end of file
diff --git a/content/visual/2020-04-12-guilt.png b/content/visual/2020-04-12-guilt.png
new file mode 120000
index 0000000..059e87f
--- /dev/null
+++ b/content/visual/2020-04-12-guilt.png
@@ -0,0 +1 @@
+../../.git/annex/objects/91/mZ/SHA256E-s1841625--21ce2fad4fa27a77c23eeb8dd2d84ab9d3a5c4b130ef1d4687b6a2c0122d9f24.png/SHA256E-s1841625--21ce2fad4fa27a77c23eeb8dd2d84ab9d3a5c4b130ef1d4687b6a2c0122d9f24.png
\ No newline at end of file
diff --git a/content/visual/2020-05-13-tatss.png b/content/visual/2020-05-13-tatss.png
new file mode 120000
index 0000000..7f1a6e3
--- /dev/null
+++ b/content/visual/2020-05-13-tatss.png
@@ -0,0 +1 @@
+../../.git/annex/objects/j1/04/SHA256E-s202502--d067dc4336ca30160227a30c48722e6df50626c5f777f56b6b2a5e8767c26848.png/SHA256E-s202502--d067dc4336ca30160227a30c48722e6df50626c5f777f56b6b2a5e8767c26848.png
\ No newline at end of file
diff --git a/content/visual/2020-05-18-hairy.png b/content/visual/2020-05-18-hairy.png
new file mode 120000
index 0000000..635c339
--- /dev/null
+++ b/content/visual/2020-05-18-hairy.png
@@ -0,0 +1 @@
+../../.git/annex/objects/07/26/SHA256E-s919785--393de0aeef6648c5dd5faba83ec92d182d7cc827e5d75599d155c99a826e5c26.png/SHA256E-s919785--393de0aeef6648c5dd5faba83ec92d182d7cc827e5d75599d155c99a826e5c26.png
\ No newline at end of file
diff --git a/content/visual/2020-05-31-plantsss.png b/content/visual/2020-05-31-plantsss.png
new file mode 120000
index 0000000..80109e7
--- /dev/null
+++ b/content/visual/2020-05-31-plantsss.png
@@ -0,0 +1 @@
+../../.git/annex/objects/xx/0f/SHA256E-s495379--3b920599ddf4ed84c19616f1bfd2cdc76a7a876785ebb2432b21e20085eaa2ea.png/SHA256E-s495379--3b920599ddf4ed84c19616f1bfd2cdc76a7a876785ebb2432b21e20085eaa2ea.png
\ No newline at end of file
diff --git a/content/visual/_main/2019-03-11-dress.jpg b/content/visual/_main/2019-03-11-dress.jpg
deleted file mode 120000
index 431feee..0000000
--- a/content/visual/_main/2019-03-11-dress.jpg
+++ /dev/null
@@ -1 +0,0 @@
-../../../.git/annex/objects/gZ/XG/SHA256E-s184840--08fe7d08c0d946d119eef787f31d0f28224fdfa001975450e83b66d7691072da.jpg/SHA256E-s184840--08fe7d08c0d946d119eef787f31d0f28224fdfa001975450e83b66d7691072da.jpg
\ No newline at end of file
diff --git a/content/visual/_main/2019-03-11-duo2.png b/content/visual/_main/2019-03-11-duo2.png
deleted file mode 120000
index 8dec1cf..0000000
--- a/content/visual/_main/2019-03-11-duo2.png
+++ /dev/null
@@ -1 +0,0 @@
-../../../.git/annex/objects/k3/30/SHA256E-s631729--32753a717b3349dfdce80e732b32e53de3eb4361e8f77c76258b663c9e8cfa32.png/SHA256E-s631729--32753a717b3349dfdce80e732b32e53de3eb4361e8f77c76258b663c9e8cfa32.png
\ No newline at end of file
diff --git a/content/visual/_main/2019-03-11-mashup.png b/content/visual/_main/2019-03-11-mashup.png
deleted file mode 120000
index aabafc4..0000000
--- a/content/visual/_main/2019-03-11-mashup.png
+++ /dev/null
@@ -1 +0,0 @@
-../../../.git/annex/objects/4p/V6/SHA256E-s918970--e7a695c389a762320704a52f5390c37a162dae81ff2df614ce38f40df03be73d.png/SHA256E-s918970--e7a695c389a762320704a52f5390c37a162dae81ff2df614ce38f40df03be73d.png
\ No newline at end of file
diff --git a/content/visual/_main/2019-03-12-forest.png b/content/visual/_main/2019-03-12-forest.png
deleted file mode 120000
index f44e8d1..0000000
--- a/content/visual/_main/2019-03-12-forest.png
+++ /dev/null
@@ -1 +0,0 @@
-../../../.git/annex/objects/J5/jZ/SHA256E-s1346919--a6f9e1df5e2593fa1a868244769f16522defbf4bd2c38e0c9014e379d93fdd68.png/SHA256E-s1346919--a6f9e1df5e2593fa1a868244769f16522defbf4bd2c38e0c9014e379d93fdd68.png
\ No newline at end of file
diff --git a/content/visual/_main/2019-04-02-tat2.png b/content/visual/_main/2019-04-02-tat2.png
deleted file mode 120000
index be8d73c..0000000
--- a/content/visual/_main/2019-04-02-tat2.png
+++ /dev/null
@@ -1 +0,0 @@
-../../../.git/annex/objects/wj/7m/SHA256E-s299494--9826507fe82e22161368e3b8008aab5df58d6f4fdb8b29c4f47279faa3a35f74.png/SHA256E-s299494--9826507fe82e22161368e3b8008aab5df58d6f4fdb8b29c4f47279faa3a35f74.png
\ No newline at end of file
diff --git a/content/visual/_main/2019-04-12-dragons.png b/content/visual/_main/2019-04-12-dragons.png
deleted file mode 120000
index 7134ab5..0000000
--- a/content/visual/_main/2019-04-12-dragons.png
+++ /dev/null
@@ -1 +0,0 @@
-../../../.git/annex/objects/9J/X7/SHA256E-s670715--d1841af7719367ad43becc186af1d3c520b775bb2bf54da2cb92c135911dbbfb.png/SHA256E-s670715--d1841af7719367ad43becc186af1d3c520b775bb2bf54da2cb92c135911dbbfb.png
\ No newline at end of file
diff --git a/content/visual/_main/2019-07-01-duo.png b/content/visual/_main/2019-07-01-duo.png
deleted file mode 120000
index 15bcd07..0000000
--- a/content/visual/_main/2019-07-01-duo.png
+++ /dev/null
@@ -1 +0,0 @@
-../../../.git/annex/objects/wp/jK/SHA256E-s321424--297046f12e2941743a19183faaaa8ebd55428367bc0ee2f457c467495481423c.png/SHA256E-s321424--297046f12e2941743a19183faaaa8ebd55428367bc0ee2f457c467495481423c.png
\ No newline at end of file
diff --git a/content/visual/_main/2019-09-02-gauche.png b/content/visual/_main/2019-09-02-gauche.png
deleted file mode 120000
index de0344e..0000000
--- a/content/visual/_main/2019-09-02-gauche.png
+++ /dev/null
@@ -1 +0,0 @@
-../../../.git/annex/objects/m1/gJ/SHA256E-s1364718--8fdba85d9550064e2acab434042fcc0aeb376563516a8bf9ad3e2244db00021c.png/SHA256E-s1364718--8fdba85d9550064e2acab434042fcc0aeb376563516a8bf9ad3e2244db00021c.png
\ No newline at end of file
diff --git a/content/visual/_main/2019-11-27-softsoft.jpg b/content/visual/_main/2019-11-27-softsoft.jpg
deleted file mode 120000
index 8f239e1..0000000
--- a/content/visual/_main/2019-11-27-softsoft.jpg
+++ /dev/null
@@ -1 +0,0 @@
-../../../.git/annex/objects/gF/87/SHA256E-s458925--e06294cd0c55b73f4ff119ac3299d4f96139ede37ae2fb18110a126b48eede91.jpg/SHA256E-s458925--e06294cd0c55b73f4ff119ac3299d4f96139ede37ae2fb18110a126b48eede91.jpg
\ No newline at end of file
diff --git a/content/visual/_main/2019-11-29-tandem6.png b/content/visual/_main/2019-11-29-tandem6.png
deleted file mode 120000
index 6845993..0000000
--- a/content/visual/_main/2019-11-29-tandem6.png
+++ /dev/null
@@ -1 +0,0 @@
-../../../.git/annex/objects/Q6/MF/SHA256E-s1949616--8f6aee3703fcec5d6e16724c39ad938d26e96b477855b9e05de180bad5bf6e51.png/SHA256E-s1949616--8f6aee3703fcec5d6e16724c39ad938d26e96b477855b9e05de180bad5bf6e51.png
\ No newline at end of file
diff --git a/content/visual/_main/2020-01-05-collard.png b/content/visual/_main/2020-01-05-collard.png
deleted file mode 120000
index 6037f34..0000000
--- a/content/visual/_main/2020-01-05-collard.png
+++ /dev/null
@@ -1 +0,0 @@
-../../../.git/annex/objects/86/p5/SHA256E-s8693437--b5cde85117ffee4fc0ef1f9ae4a9887c12dced028baca4ce76939efef5568b84.png/SHA256E-s8693437--b5cde85117ffee4fc0ef1f9ae4a9887c12dced028baca4ce76939efef5568b84.png
\ No newline at end of file
diff --git a/content/visual/_main/2020-02-10-mashup.png b/content/visual/_main/2020-02-10-mashup.png
deleted file mode 120000
index 3ba27ba..0000000
--- a/content/visual/_main/2020-02-10-mashup.png
+++ /dev/null
@@ -1 +0,0 @@
-../../../.git/annex/objects/27/kP/SHA256E-s600318--d1e1ae2cef2879eae698498f3c4e3b4907a9f39b227b0c3816fe020e34df066c.png/SHA256E-s600318--d1e1ae2cef2879eae698498f3c4e3b4907a9f39b227b0c3816fe020e34df066c.png
\ No newline at end of file
diff --git a/content/visual/_main/2020-02-11-mattress2.png b/content/visual/_main/2020-02-11-mattress2.png
deleted file mode 120000
index 017bc99..0000000
--- a/content/visual/_main/2020-02-11-mattress2.png
+++ /dev/null
@@ -1 +0,0 @@
-../../../.git/annex/objects/FF/Fp/SHA256E-s2521385--1ad730393c6d1c8159c966019893fbfacfef84b64eef47a26b4d0869e0f8fd58.png/SHA256E-s2521385--1ad730393c6d1c8159c966019893fbfacfef84b64eef47a26b4d0869e0f8fd58.png
\ No newline at end of file
diff --git a/content/visual/_main/2020-03-14-mashupppp.png b/content/visual/_main/2020-03-14-mashupppp.png
deleted file mode 120000
index db344ab..0000000
--- a/content/visual/_main/2020-03-14-mashupppp.png
+++ /dev/null
@@ -1 +0,0 @@
-../../../.git/annex/objects/42/v4/SHA256E-s1446118--c14985cde38d539fe967254266bcacd35feb89fb9c2817e969ce916ae8967989.png/SHA256E-s1446118--c14985cde38d539fe967254266bcacd35feb89fb9c2817e969ce916ae8967989.png
\ No newline at end of file
diff --git a/content/visual/_main/2020-04-09-mebee.png b/content/visual/_main/2020-04-09-mebee.png
deleted file mode 120000
index ff5196a..0000000
--- a/content/visual/_main/2020-04-09-mebee.png
+++ /dev/null
@@ -1 +0,0 @@
-../../../.git/annex/objects/1p/9X/SHA256E-s1411058--46562b966839842feae88561bdd7cd0e6106138ac17b79de7aa0228846d32aad.png/SHA256E-s1411058--46562b966839842feae88561bdd7cd0e6106138ac17b79de7aa0228846d32aad.png
\ No newline at end of file
diff --git a/content/visual/_main/2020-04-12-guilt.png b/content/visual/_main/2020-04-12-guilt.png
deleted file mode 120000
index 072470c..0000000
--- a/content/visual/_main/2020-04-12-guilt.png
+++ /dev/null
@@ -1 +0,0 @@
-../../../.git/annex/objects/91/mZ/SHA256E-s1841625--21ce2fad4fa27a77c23eeb8dd2d84ab9d3a5c4b130ef1d4687b6a2c0122d9f24.png/SHA256E-s1841625--21ce2fad4fa27a77c23eeb8dd2d84ab9d3a5c4b130ef1d4687b6a2c0122d9f24.png
\ No newline at end of file
diff --git a/content/visual/_main/2020-05-13-tatss.png b/content/visual/_main/2020-05-13-tatss.png
deleted file mode 120000
index c7a6667..0000000
--- a/content/visual/_main/2020-05-13-tatss.png
+++ /dev/null
@@ -1 +0,0 @@
-../../../.git/annex/objects/j1/04/SHA256E-s202502--d067dc4336ca30160227a30c48722e6df50626c5f777f56b6b2a5e8767c26848.png/SHA256E-s202502--d067dc4336ca30160227a30c48722e6df50626c5f777f56b6b2a5e8767c26848.png
\ No newline at end of file
diff --git a/content/visual/_main/2020-05-18-hairy.png b/content/visual/_main/2020-05-18-hairy.png
deleted file mode 120000
index cd4fba2..0000000
--- a/content/visual/_main/2020-05-18-hairy.png
+++ /dev/null
@@ -1 +0,0 @@
-../../../.git/annex/objects/07/26/SHA256E-s919785--393de0aeef6648c5dd5faba83ec92d182d7cc827e5d75599d155c99a826e5c26.png/SHA256E-s919785--393de0aeef6648c5dd5faba83ec92d182d7cc827e5d75599d155c99a826e5c26.png
\ No newline at end of file
diff --git a/content/visual/_main/2020-05-31-plantsss.png b/content/visual/_main/2020-05-31-plantsss.png
deleted file mode 120000
index da1ed8c..0000000
--- a/content/visual/_main/2020-05-31-plantsss.png
+++ /dev/null
@@ -1 +0,0 @@
-../../../.git/annex/objects/xx/0f/SHA256E-s495379--3b920599ddf4ed84c19616f1bfd2cdc76a7a876785ebb2432b21e20085eaa2ea.png/SHA256E-s495379--3b920599ddf4ed84c19616f1bfd2cdc76a7a876785ebb2432b21e20085eaa2ea.png
\ No newline at end of file
diff --git a/site.cabal b/site.cabal
index 22a1aeb..6f7523a 100644
--- a/site.cabal
+++ b/site.cabal
@@ -15,6 +15,7 @@ executable site
build-depends: base >=4.12 && <4.13
, filepath
, achille
+ , data-default
, blaze-html
, blaze-markup
, pandoc
diff --git a/src/Main.hs b/src/Main.hs
index c5f923d..699e3f0 100644
--- a/src/Main.hs
+++ b/src/Main.hs
@@ -1,10 +1,14 @@
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE DuplicateRecordFields #-}
+{-# LANGUAGE DisambiguateRecordFields #-}
+{-# LANGUAGE NamedFieldPuns #-}
-import Data.Functor ((<&>))
+import Data.Functor
import Data.Maybe (fromMaybe, mapMaybe)
-import System.FilePath ((-<.>))
+import Control.Monad (when)
+import System.FilePath
import Text.Pandoc.Options
import Achille
@@ -12,25 +16,76 @@ import Achille.Recipe.Pandoc
import Page
import Templates
+import Types
+
config :: Config
config = def
- { deployCmd = Just "rsync -avzzr _site/ --chmod=755 flupe@duckduck.me:/var/www/acatalepsie"
- }
+ { deployCmd = Just "rsync -avzzr _site/ --chmod=755 pi@192.168.0.45:/var/www/html"
+
+ -- by making everything absolute you can run the command from anywhere
+ , contentDir = "/home/flupe/dev/acatalepsie/content"
+ , outputDir = "/home/flupe/dev/acatalepsie/_site"
+ , cacheFile = "/home/flupe/dev/acatalepsie/.cache"
+ }
+
+
+-- pandoc options
+ropts :: ReaderOptions
+ropts = def
+ { readerExtensions =
+ enableExtension Ext_smart githubMarkdownExtensions
+ }
+
+wopts :: WriterOptions
+wopts = def
+ { writerHTMLMathMethod = KaTeX ""
+ }
+
+
+buildProject :: Recipe IO a (Project, FilePath)
+buildProject = do
+ name <- takeBaseName <$> getCurrentDir
+
+ -- task $ match_ "*" copyFile
+ match "*" copyFile
+
+ children <- buildChildren
+
+ watch children $ matchFile "index.*" do
+ (meta, doc) <- readPandocMetadataWith ropts
+ renderPandocWith wopts doc <&> renderProject meta children
+ >>= saveFileAs (-<.> "html")
+ >> (meta,) <$> getCurrentDir
+ where
+ buildChildren :: Recipe IO a [(String, FilePath)]
+ buildChildren = match "pages/*" do
+ (TitledPage title _, doc) <- readPandocMetadataWith ropts
+ renderPandocWith wopts doc
+ <&> outerWith (def {title = title})
+ >>= saveFileAs ((-<.> "html") . takeFileName)
+ <&> (title,)
+
main :: IO ()
main = achilleWith config do
match_ "assets/*" copyFile
- match_ "./quid.rst" $ compilePandoc <&> outer >>= saveFileAs (-<.> "html")
+
+ -----------
+ -- QUID
+
+ match_ "./quid.rst" $
+ compilePandoc <&> outerWith def {title = "quid"}
+ >>= saveFileAs (-<.> "html")
-----------
-- VISUAL
- pictures <- match "visual/*/*" do
- copyFile
- runCommandWith (-<.> "thumb.png")
- (\a b -> "convert -resize 740x " <> a <> " " <> b)
- <&> timestamped
+ pictures <- match "visual/*" do
+ copyFile
+ runCommandWith (-<.> "thumb.png")
+ (\a b -> "convert -resize 740x " <> a <> " " <> b)
+ <&> timestamped
watch pictures $ match_ "./visual.rst" do
txt <- compilePandoc
@@ -39,13 +94,7 @@ main = achilleWith config do
-------------
-- PROJECTS
- projects <- matchDir "projects/*/" do
- task $ match_ "*" copyFile
- matchFile "index.*" do
- (meta, doc) <- readPandocMetadataWith ropts
- renderPandoc doc <&> renderProject meta
- >>= saveFileAs (-<.> "html")
- >> (meta,) <$> getCurrentDir
+ projects <- matchDir "projects/*/" buildProject
watch projects $ match_ "./projects.rst" do
debug "rendering project index"
@@ -57,7 +106,7 @@ main = achilleWith config do
posts <- match "posts/*" do
src <- copyFile
- (Page title d, pdc) <- readPandocMetadata
+ (Page title d, pdc) <- readPandocMetadataWith ropts
renderPandocWith wopts pdc
<&> renderPost title src
@@ -75,9 +124,3 @@ main = achilleWith config do
compilePandoc
<&> renderIndex visible
>>= saveFileAs (-<.> "html")
-
-ropts :: ReaderOptions
-ropts = def { readerExtensions = enableExtension Ext_smart githubMarkdownExtensions }
-
-wopts :: WriterOptions
-wopts = def { writerHTMLMathMethod = KaTeX "" }
diff --git a/src/Templates.hs b/src/Templates.hs
index 478ac09..69a8184 100644
--- a/src/Templates.hs
+++ b/src/Templates.hs
@@ -1,10 +1,14 @@
-{-# LANGUAGE OverloadedStrings #-}
-{-# LANGUAGE BlockArguments #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE BlockArguments #-}
+{-# LANGUAGE DuplicateRecordFields #-}
+{-# LANGUAGE DisambiguateRecordFields #-}
+{-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE RecordWildCards #-}
module Templates where
import Data.String (fromString)
-import Control.Monad (forM_)
+import Control.Monad (forM_, when)
import System.FilePath
import Text.Blaze.Internal as I
@@ -13,17 +17,20 @@ import Text.Blaze.Html5.Attributes as A
import Data.Dates.Types (DateTime(..), months, capitalize)
import Achille
-import Types (Project)
+import Types
import qualified Types
import qualified Data.Map.Strict as Map
showDate :: DateTime -> String
showDate (DateTime y m d _ _ _) = month <> " " <> show d <> ", " <> show y
- where month = capitalize (months !! (m - 1))
+ where month = take 3 $ capitalize (months !! (m - 1))
loading :: AttributeValue -> Attribute
loading = I.customAttribute "loading"
+property :: AttributeValue -> Attribute
+property = I.customAttribute "property"
+
toLink :: FilePath -> Html -> Html
toLink url = H.a ! A.href (fromString $ "/" <> url)
@@ -33,14 +40,14 @@ renderIndex posts content =
outer do
content
H.h2 "Latest notes"
- H.ul $ forM_ posts \(Timestamped d (title, src)) ->
+ H.ul ! A.id "pidx" $ forM_ posts \(Timestamped d (title, src)) ->
H.li do
- H.span $ fromString $ showDate d <> ": "
+ H.span $ fromString $ showDate d
toLink src (fromString title)
renderPost :: String -> FilePath -> Html -> Html
renderPost title source content =
- outer do
+ outerWith def {Types.title = title} do
H.h1 $ fromString title
toLink source "View source"
content
@@ -54,20 +61,23 @@ renderVisual txt imgs =
H.figure $ H.img ! A.src (fromString p)
! loading "lazy"
-renderProject :: Project -> Html -> Html
-renderProject project content =
- outer do
+renderProject :: Project -> [(String, FilePath)] -> Html -> Html
+renderProject (project@Project{title,..}) children content =
+ outerWith def {Types.title = title} do
H.header ! A.class_ "project" $ do
H.div $ H.img ! A.src "logo.svg"
H.div do
- H.h1 $ fromString $ Types.title project
- H.p $ fromString $ Types.subtitle project
- H.ul $ forM_ (Map.toList $ Types.labels project) \(k, v) -> H.li do
+ H.h1 $ fromString $ title
+ H.p $ fromString $ subtitle
+ H.ul $ forM_ (Map.toList labels) \(k, v) -> H.li do
fromString k <> ": "
if k == "repo" then
H.a ! A.href (fromString $ "https://github.com/" <> v)
$ fromString v
else fromString v
+ when (length children > 0) $
+ H.ul ! A.class_ "pages" $ forM_ children \(t,l) ->
+ H.li $ H.a ! A.href (fromString l) $ (fromString t)
content
renderProjects :: Html -> [(Project, FilePath)] -> Html
@@ -75,11 +85,11 @@ renderProjects txt paths =
outer do
txt
H.ul ! A.class_ "projects" $ do
- forM_ paths \(project, link) -> H.li $ H.a ! A.href (fromString link) $ do
+ forM_ paths \(Project{title,..}, link) -> H.li $ H.a ! A.href (fromString link) $ do
H.div $ H.img ! A.src (fromString $ link "logo.svg")
H.div do
- H.h2 $ fromString (Types.title project)
- H.p $ fromString (Types.subtitle project)
+ H.h2 $ fromString title
+ H.p $ fromString subtitle
-- H.ul $ forM_ (Map.toList $ Types.labels project) \(k, v) ->
-- H.li $ (fromString k <> ": " <> fromString v)
@@ -87,7 +97,10 @@ logo :: Html
logo = preEscapedString ""
outer :: Html -> Html
-outer content = H.docTypeHtml do
+outer = outerWith def
+
+outerWith :: SiteConfig -> Html -> Html
+outerWith SiteConfig{title,..} content = H.docTypeHtml do
H.head do
H.meta ! A.name "viewport"
! A.content "width=device-width, initial-scale=1.0, user-scalable=yes"
@@ -95,7 +108,21 @@ outer content = H.docTypeHtml do
H.meta ! A.name "robots" ! A.content "index, follow"
H.meta ! charset "utf-8"
H.link ! A.rel "stylesheet" ! A.href "/assets/theme.css"
- H.title "sbbls"
+
+ -- OpenGraph
+ H.meta ! property "og:title"
+ ! A.content (fromString title)
+
+ H.meta ! property "og:type"
+ ! A.content "website"
+
+ H.meta ! property "og:image"
+ ! A.content (fromString image)
+
+ H.meta ! property "og:description"
+ ! A.content (fromString description)
+
+ H.title (fromString title)
H.body do
H.header ! A.id "hd" $ H.section do
@@ -112,3 +139,4 @@ outer content = H.docTypeHtml do
H.a ! A.href "https://creativecommons.org/licenses/by-nc/2.0/" $ "CC BY-NC 2.0"
" · "
H.a ! A.href "https://instagram.com/ba.bou.m/" $ "instagram"
+
diff --git a/src/Types.hs b/src/Types.hs
index 6961149..a8ace3f 100644
--- a/src/Types.hs
+++ b/src/Types.hs
@@ -1,10 +1,12 @@
-{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE DuplicateRecordFields #-}
module Types where
import GHC.Generics
import Data.Aeson.Types (FromJSON)
import Data.Binary (Binary, put, get)
+import Data.Default
import qualified Data.Map.Strict as Map
data Project = Project
@@ -15,8 +17,28 @@ data Project = Project
, gallery :: Maybe Bool
} deriving (Generic, Eq, Show)
+data TitledPage = TitledPage
+ { title :: String
+ , description :: Maybe String
+ } deriving (Generic, Eq, Show)
+
instance FromJSON Project
+instance FromJSON TitledPage
+
instance Binary Project where
put (Project t s y l g) = put t >> put s >> put y >> put l >> put g
get = Project <$> get <*> get <*> get <*> get <*> get
+
+data SiteConfig = SiteConfig
+ { title :: String
+ , description :: String
+ , image :: String
+ }
+
+instance Default SiteConfig where
+ def = SiteConfig
+ { title = "sbbls"
+ , description = "my personal web space, for your enjoyment"
+ , image = "https://acatalepsie.fr/assets/card.png"
+ }