From b66c58b68e9c507f47b5b9ef8fb8d85281502ffe Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Thu, 30 May 2024 00:30:05 -0700 Subject: [PATCH] Lightly edit and publish the Agda+Hugo post Signed-off-by: Danila Fedorin --- content/blog/agda_hugo.md | 82 ++++++++++++--------------------------- 1 file changed, 24 insertions(+), 58 deletions(-) diff --git a/content/blog/agda_hugo.md b/content/blog/agda_hugo.md index 99bdcb6..baa4bc2 100644 --- a/content/blog/agda_hugo.md +++ b/content/blog/agda_hugo.md @@ -1,7 +1,6 @@ --- title: "Integrating Agda's HTML Output with Hugo" -date: 2024-05-25T21:02:10-07:00 -draft: true +date: 2024-05-30T00:29:26-07:00 tags: ["Agda", "Hugo", "Ruby"] --- @@ -100,7 +99,7 @@ In summary: 1. I want to create cross-links between symbols in Agda blocks in a blog post. 2. These code blocks could include code from disjoint files, and be out of order. 3. Code blocks among a whole series of posts should be cross-linked too. -4. The code blocks should be syntax highlighting the same way as the rest of the +4. The code blocks should be syntax highlighted the same way as the rest of the code on the site. 5. Ideally, I should be able to use my regular method for referencing code. @@ -127,7 +126,7 @@ with links as I discover them. Effectively, what I need to do is a "link transfer": I need to identify regions of code that are highlighted in Agda's HTML, find those regions in Hugo's HTML output, and mark them with links. In addition, I'll need to fix up the links themselves: the HTML output assumes that each -Agda file is its own HTML page, but this is ruled out by the second constraint. +Agda file is its own HTML page, but this is ruled out by the second constraint of mine. As a little visualization, the overall problems looks something like this: @@ -227,7 +226,7 @@ example above, the script might produce: Given such line information, the next step is to transfer it onto existing Hugo HTML files. Within a file, I've made my `codelines` shortcode emit -custom attributes that can be used to find syntax highlighting Agda code. +custom attributes that can be used to find syntax-highlighted Agda code. The chief such attribute is `data-agda-block`; my script traverses all elements with this attribute. @@ -271,13 +270,14 @@ Thus, the fully qualified module name for `File.agda` could be `File`, files named after the fully qualified module name, the script needs to guess what the module file is. This is where some conventions come in play: I keep my code in folders directly nested within a top-level `code` directory; -thus, I'll have folders `project1` or `project2`. As a result, -I guess that the first directory should be discarded, while the rest should be -included in the path. The only exception to this is Git submodules: if an Agda -file is included using a submodule, the root directory of the submodule is -considered the Agda project root. My Hugo theme indicates the submodule using -an additional `data-base-path` attribute; in all, that leads to the -following logic: +thus, I'll have folders `project1` or `project2` inside `code`, and those +will always be project roots. As a result, +I guess that the first directory relative to `code` should be discarded, +while the rest should be included in the path. The only exception to this is +Git submodules: if an Agda file is included using a submodule, the root +directory of the submodule is considered the Agda project root. My Hugo theme +indicates the submodule using an additional `data-base-path` attribute; in all, +that leads to the following logic: ```Ruby # ... @@ -543,51 +543,17 @@ those documentation pages, or expecting the Agda standard library HTML pages to remain stable and hosted at a fixed URL. Neither was simple enough to do, so I opted for the conservative "just don't insert links" approach. -{{< todo >}}This isn't as important probably, but might be worth talking about. {{< /todo >}} +And that's all of the approach that I wanted to show off today! There +are other details, like finding posts in the same series (I achieve this +with a `meta` element) and invoking `agda --html` on the necessary source files +(my [`build-agda-html.rb`](https://dev.danilafe.com/Web-Projects/blog-static/src/branch/master/build-agda-html.rb) +script is how I personally do this), but I don't think it's all that valuable +to describe them here. -The most challenging step is probably to identify the Agda "projects" that need -to be built. Since different articles have different modules (possibly with -the same name), I would need to keep them separate. Also, I'm not ruling -out the possibility of one project including another as a submodule. To -make this work, I wrote a little Ruby script to find all Agda files, -guess their project folder, and invoke the Agda compiler there. It boils -down to something like this: +Unfortunately, the additional metadata I had my theme insert makes it +harder for others to use this approach out of the box. However, I hope that by +sharing my experience, others who write Agda and post about it might be able +to get a similar solution working. And of course, it's always fun to write +about a recent project or endeavor. -```Ruby -# For each Agda file, find the most specific project / subproject to which -# it belongs. -files_for_paths = {} -Dir.glob("**/*.agda", base: root_path) do |agda_file| - best_path = max_path.call(agda_file) - files_for_path = files_for_paths.fetch(best_path) do - files_for_paths[best_path] = [] - end - - # Strip the project prefix from the Agda file's path, since - # Agda compiler will be invoked in the project's folder. - files_for_path << agda_file[best_path.length + File::SEPARATOR.length..-1] -end - -original_wd = Dir.getwd -files_for_paths.each do |path, files| - # There might be a cleaner way of doing this, but it's convenient. - Dir.chdir(original_wd) - Dir.chdir(File.join(root_path, path)) - - # Wherever the target directory is, create a folder that corresponds to - # the project being built, to avoid "cross-contaminating" the output - # folder with distinct modules with the same name. - html_dir = File.join [target_dir, path, "html"] - FileUtils.mkdir_p html_dir - - # Just shell out to Agda using the --html folder. - files.each do |file| - command = "#{ARGV[0]} --local-interfaces #{file} --html --html-dir=#{html_dir}" - puts command - puts `#{command}` - end -end -``` - -In short, it traverses all the folders in my `code` directory -- which is where -I keep my code -- looking for Agda source files. Once it finds them, +Happy (dependently typed) programming and blogging!