Web-Projects/blog-static
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity
871 Commits 8 Branches 0 Tags 46 MiB
e40a05633c
Commit Graph

871 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
Danila Fedorin
291a1f0178 Update SPA article on Lattices with new math delimiters 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-13 18:22:21 -07:00
Danila Fedorin
2547b53aa2 Switch "Homework for an assignment" post 2 to new math delimiters 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-13 18:20:54 -07:00
Danila Fedorin
409f8b7186 Switch tokenizing article to new math delimiters 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-13 18:20:04 -07:00
Danila Fedorin
189422bf1e Convert AoC Coq article to new math delimiters 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-13 18:16:20 -07:00
Danila Fedorin
74daeee140 Enable goldmark passthrough 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-13 17:47:52 -07:00
Danila Fedorin
befcd3cf98 Add a sidenote about land and lor. 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-13 15:41:50 -07:00
Danila Fedorin
e063ff6aa5 Update the vanilla theme 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-12 18:58:44 -07:00
Danila Fedorin
6179c86919 Show the basic Nat lattice. 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-12 18:52:26 -07:00
Danila Fedorin
a20fe07a56 Move original 'monotone function' text into new post and heavily rework it 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-12 18:28:44 -07:00
Danila Fedorin
2b5dcf12d7 Rename the SPA intro to have a specific name 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-12 13:50:29 -07:00
Danila Fedorin
5873c1ca96 Write a high-level introduction for the SPA series 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-12 13:49:21 -07:00
Danila Fedorin
c6e2ecb996 Add first section of Agda program analysis article 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-03-14 22:25:17 -07:00
Danila Fedorin
2130b00752 Narrow some of the tags 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-03-13 15:59:46 -07:00
Danila Fedorin
474c3a8348 Switch bracket types in Agda expression pattern post 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-03-13 15:05:37 -07:00
Danila Fedorin
29a18b8b37 Add description to expr_pattern 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-03-11 23:26:07 -07:00
Danila Fedorin
21ab4f0a8b Update theme 2024-03-11 23:21:08 -07:00
Danila Fedorin
7d2842fd64 Add article about the 'deeply embedded expression' pattern 2024-03-11 23:15:56 -07:00
Danila Fedorin
cd4c121e07 Update the theme 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-03-11 15:50:40 -07:00
Danila Fedorin
d0570f876e Add the SPA code as a submodule 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-03-11 14:34:35 -07:00
Danila Fedorin
8bf99a1ab0 Update theme 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-02-02 21:05:48 -08:00
Danila Fedorin
fdcd4ddd60 Defer loading of KaTeX JS and Bergamot support code 2023-12-30 19:56:14 -08:00
Danila Fedorin
c09fff455f Update theme. 2023-12-30 19:40:10 -08:00
Danila Fedorin
0b3755c69a Use a shim instead of the real katex-expression because it hardcodes too much. 
We don't need a second bundle of KaTeX, or all of the fonts a second time, served
from a CDN we don't control.

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-30 19:38:37 -08:00
Danila Fedorin
e90fb64946 Update theme 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-30 16:31:46 -08:00
Danila Fedorin
d542a4790e Update theme 2023-12-30 16:16:10 -08:00
Danila Fedorin
bc5cb4009c Update theme 2023-12-30 16:02:52 -08:00
Danila Fedorin
6724533d0e Update theme and change config.toml to match 2023-12-30 14:48:16 -08:00
Danila Fedorin
0f0668b77b Make use of theme's support for Plausible. 2023-12-30 13:13:00 -08:00
Danila Fedorin
266bf9b4cf Add an exercise about conversions to types: basics 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-29 12:47:58 -08:00
Danila Fedorin
a6f3bccf64 Use markdown for exercises, since it works fine out of the box. 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-28 16:05:15 -08:00
Danila Fedorin
2d640f2e6a Center the 'no proofs' message 2023-12-28 13:20:19 -08:00
Danila Fedorin
d7d99205a1 Properly escape < in HTML content. 2023-12-28 00:36:58 -08:00
Danila Fedorin
9f437d5b9f Add a couple of exercises to types: basics. 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-28 00:13:13 -08:00
Danila Fedorin
0d3100ba33 Make exercises into details (so they can be collapsed) 2023-12-28 00:12:51 -08:00
Danila Fedorin
72fb69d87b Make minor changes to types: basics. 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-27 23:31:45 -08:00
Danila Fedorin
ed4fcf5e9d Start explaining exercises in types intro. 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-27 23:31:28 -08:00
Danila Fedorin
8742c6e7b9 Add a Bergamot exercise shortcode to give exercises. 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-27 23:31:00 -08:00
Danila Fedorin
d7d7254a7b Extract loading and closing bergamot into a helper script. 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-27 23:30:16 -08:00
Danila Fedorin
7e8870de6c Factor launching bergamot into a helper function 2023-12-27 13:27:20 -08:00
Danila Fedorin
8f2b2addc2 Rename the widget IDs to not include numbers. 2023-12-27 13:16:20 -08:00
Danila Fedorin
e4743bbdef Make some edits to 'types' part 1. 2023-12-26 14:02:48 -08:00
Danila Fedorin
80cdea6932 Update rendering rules for changes to Bergamot. 2023-12-26 13:22:38 -08:00
Danila Fedorin
645f2c5c9c Update inference rules to match new Bergamot's single-literal output 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-26 13:21:37 -08:00
Danila Fedorin
85b81ffc98 Modify rendering rules to handle precedence 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-25 18:42:43 -08:00
Danila Fedorin
fa5536f504 Add special styling for bergamot error messages 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-25 18:42:29 -08:00
Danila Fedorin
16086e79b0 Proofread and publish bergamot post 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-22 22:15:17 -08:00
Danila Fedorin
b001bba3b8 Tweak rendering rules to support int(x) and str(x). 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-22 22:00:46 -08:00
Danila Fedorin
0c895a2662 Add an initial draft of the Bergamot post. 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-22 22:00:06 -08:00
Danila Fedorin
6f0641f315 Render variables better 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-22 16:04:47 -08:00
Danila Fedorin
dc9dbe8a0f Update for bergamot requiring an 'input program' too 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-22 16:04:33 -08:00