Commit Graph

785 Commits

Author SHA1 Message Date
Danila Fedorin 6a168f2fe1 Start on a draft about Agda and Hugo
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-25 23:28:18 -07:00
Danila Fedorin 04f12b545d Minor edits to 'lattices 2'
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-25 20:45:19 -07:00
Danila Fedorin 711b01175d Put the number back to what it was
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-24 23:12:27 -07:00
Danila Fedorin 272c2666c5 Inconsequential tweak to test Agda caching in build system
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-24 13:44:34 -07:00
Danila Fedorin 60ba43378a Make the destination folders
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-24 13:21:33 -07:00
Danila Fedorin 1da60b3b28 Print result of executing command
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-24 13:17:44 -07:00
Danila Fedorin ee118b07e5 Make build-agda-html.rb more configurable
This should use it from Nix, and cache the Agda compilations

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-24 12:31:26 -07:00
Danila Fedorin 06ee998d54 Allow executing non-remote JS for KaTeX
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-23 21:14:49 -07:00
Danila Fedorin c197a45540 Port over the HTML conversion script to execute JS
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-23 21:03:03 -07:00
Danila Fedorin 4d23b45633 Update theme
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-23 00:57:07 -07:00
Danila Fedorin c027efa931 Stop crashing on failed Agda invocation
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-23 00:31:36 -07:00
Danila Fedorin 96c4d6fecc Fail if couldn't build Agda
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-23 00:04:13 -07:00
Danila Fedorin 4e1fd54c58 Add Gemfile and lock for nokogiri since a script now uses it
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-22 23:14:51 -07:00
Danila Fedorin d6db020e1c Adjust build script to accept Agda invocation
This might come in useful from NixOS

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-22 23:05:36 -07:00
Danila Fedorin c0f4fe017f Replace absolute links with relrefs
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-22 23:05:11 -07:00
Danila Fedorin 11d726a6ad Fix absolute link in favor of relref
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-22 23:01:26 -07:00
Danila Fedorin 37399afc68 Update theme to generate series meta
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-22 22:42:04 -07:00
Danila Fedorin 5c19fc4208 Automatically group files using the series meta
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-22 22:41:32 -07:00
Danila Fedorin 00f0f13b93 Support cross-file linking
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-22 22:29:26 -07:00
Danila Fedorin 54844fb954 Add script to generate HTML for all Agda files appropriately
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-22 17:34:32 -07:00
Danila Fedorin 6ffd3afeaa Update theme
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-22 17:07:37 -07:00
Danila Fedorin 9d0dcd98bd Improve support when code occurrs multiple times
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-22 17:05:38 -07:00
Danila Fedorin f78f877e21 Support blocks that are the entire file
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-22 16:50:45 -07:00
Danila Fedorin 5d0b903c03 Support non-submodule code
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-22 16:47:42 -07:00
Danila Fedorin 032411fe9c Add a script to generate links using Agda's HTML output
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-22 16:28:00 -07:00
Danila Fedorin 76b061d699 Update theme
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-22 16:23:47 -07:00
Danila Fedorin 08d37c839c Update theme
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-21 23:51:08 -07:00
Danila Fedorin 0a26230fe1 Remove unused shortcodes
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-21 20:09:48 -07:00
Danila Fedorin 2e59beda0c Update theme 2024-05-21 19:05:07 -07:00
Danila Fedorin ee8b1f5dc0 Write a bit more, enable support for paragraph links
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-21 19:04:08 -07:00
Danila Fedorin 4938cdaecd Work some more on lattices 2
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-20 22:46:18 -07:00
Danila Fedorin 84f28ae5ce Add tags to Agda articles
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-20 21:46:14 -07:00
Danila Fedorin 58e7a1f2dc Start on a draft of 'combining lattices'
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-20 21:39:03 -07:00
Danila Fedorin 78bba7a0e9 Update the blog for series navigation
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-20 00:37:16 -07:00
Danila Fedorin 9d31764073 Tie up Lattices (1), and plan to write Lattices (2)
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-19 22:29:24 -07:00
Danila Fedorin d787548915 Update theme
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-16 16:17:01 -07:00
Danila Fedorin a29bca499f Switch to using data/ for submodule information
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-16 15:52:33 -07:00
Danila Fedorin 60d3b3025a Flesh out the Lattices post some more
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-14 21:43:12 -07:00
Danila Fedorin c036041339 Update theme
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-14 20:32:37 -07:00
Danila Fedorin 1df315612a Update "typesafe interpreter" article to new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-13 19:08:17 -07:00
Danila Fedorin 15beddf96b Update btree article with new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-13 19:07:44 -07:00
Danila Fedorin 20d8b18a9b Update 'stack language recursion' article to new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-13 19:07:01 -07:00
Danila Fedorin 53ff0c39e4 Update "search as polynomial" article to new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-13 19:06:33 -07:00
Danila Fedorin 357a3bef09 Update the modulo patterns article to use new delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-13 19:04:08 -07:00
Danila Fedorin 81eef51e88 Update 'math rendering is wrong' to new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-13 19:02:14 -07:00
Danila Fedorin 10dfb2fe49 Update "church encoding" article to new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-13 19:01:42 -07:00
Danila Fedorin ef76149112 Update 'newtype' article to new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-13 19:01:08 -07:00
Danila Fedorin a6a330a78e Update Haskell LSP article to new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-13 19:00:23 -07:00
Danila Fedorin 7f4d0df366 Update "catemorphisms" article to new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-13 18:59:54 -07:00
Danila Fedorin 3eddac0a89 Update "proving my compiler incorrect" to new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-05-13 18:58:50 -07:00