Commit Graph

710 Commits

Author SHA1 Message Date
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
Danila Fedorin 0b8096f973 Tweak the menu selector style
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2023-12-22 16:04:04 -08:00
Danila Fedorin d58a2a9975 Add overflow scroll to proof tree view.
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2023-12-21 21:27:39 -08:00
Danila Fedorin a83268a6e3 Update use of the bergamot widget
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2023-12-21 17:26:19 -08:00
Danila Fedorin 5c83f234c6 Include rendering rules in Bergamot widget.
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2023-12-03 00:03:08 -08:00
Danila Fedorin 24abec4045 Add some more CSS for the updates to the bergamot widget
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2023-12-03 00:01:49 -08:00
Danila Fedorin 56ff56281e Add missing SCSS file for bergamot. 2023-11-29 23:26:09 -08:00
Danila Fedorin c25f9ad9ae Add the work-in-progress Bergamot widget to the basics page. 2023-11-29 23:21:15 -08:00
Danila Fedorin 5041c90ac0 Add some partials to load and create a Bergamot widget.
I've set up some infrastructure to build and host a bergamot JS
file using Nix on static.danilafe.com.

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2023-11-29 22:29:14 -08:00
Danila Fedorin 2855675fa5 Update theme
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2023-11-29 22:28:31 -08:00
Danila Fedorin 209689c5f4 Update the theme
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2023-11-27 22:18:15 -08:00
Danila Fedorin 3d64b0aa28 Update the 'vanilla' theme
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2023-11-24 11:04:42 -08:00