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

826 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
Danila Fedorin
d3fa7336a2 Update "compiler: execution" to new math delimiters 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-13 18:38:05 -07:00
Danila Fedorin
96545a899f Update "compiler: typechecking" to new math delimiters 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-13 18:33:30 -07:00
Danila Fedorin
6ef5ae2394 Update "types: variables" to new math delimiters 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-13 18:31:52 -07:00
Danila Fedorin
05a31dd4d4 Update 'compiler: parsing' article to new string literals 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-13 18:30:27 -07:00
Danila Fedorin
d9d5c8bf14 Switch 'types: basics' to new math delimiters 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-05-13 18:28:36 -07:00
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