Lightly edit and publish the Agda+Hugo post
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
parent
13636a0d29
commit
b66c58b68e
|
@ -1,7 +1,6 @@
|
||||||
---
|
---
|
||||||
title: "Integrating Agda's HTML Output with Hugo"
|
title: "Integrating Agda's HTML Output with Hugo"
|
||||||
date: 2024-05-25T21:02:10-07:00
|
date: 2024-05-30T00:29:26-07:00
|
||||||
draft: true
|
|
||||||
tags: ["Agda", "Hugo", "Ruby"]
|
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.
|
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.
|
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.
|
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.
|
code on the site.
|
||||||
5. Ideally, I should be able to use my regular method for referencing code.
|
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,
|
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,
|
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
|
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:
|
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
|
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
|
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
|
The chief such attribute is `data-agda-block`; my script traverses all
|
||||||
elements with this attribute.
|
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
|
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:
|
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;
|
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,
|
thus, I'll have folders `project1` or `project2` inside `code`, and those
|
||||||
I guess that the first directory should be discarded, while the rest should be
|
will always be project roots. As a result,
|
||||||
included in the path. The only exception to this is Git submodules: if an Agda
|
I guess that the first directory relative to `code` should be discarded,
|
||||||
file is included using a submodule, the root directory of the submodule is
|
while the rest should be included in the path. The only exception to this is
|
||||||
considered the Agda project root. My Hugo theme indicates the submodule using
|
Git submodules: if an Agda file is included using a submodule, the root
|
||||||
an additional `data-base-path` attribute; in all, that leads to the
|
directory of the submodule is considered the Agda project root. My Hugo theme
|
||||||
following logic:
|
indicates the submodule using an additional `data-base-path` attribute; in all,
|
||||||
|
that leads to the following logic:
|
||||||
|
|
||||||
```Ruby
|
```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,
|
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.
|
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
|
Unfortunately, the additional metadata I had my theme insert makes it
|
||||||
to be built. Since different articles have different modules (possibly with
|
harder for others to use this approach out of the box. However, I hope that by
|
||||||
the same name), I would need to keep them separate. Also, I'm not ruling
|
sharing my experience, others who write Agda and post about it might be able
|
||||||
out the possibility of one project including another as a submodule. To
|
to get a similar solution working. And of course, it's always fun to write
|
||||||
make this work, I wrote a little Ruby script to find all Agda files,
|
about a recent project or endeavor.
|
||||||
guess their project folder, and invoke the Agda compiler there. It boils
|
|
||||||
down to something like this:
|
|
||||||
|
|
||||||
```Ruby
|
Happy (dependently typed) programming and blogging!
|
||||||
# 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,
|
|
||||||
|
|
Loading…
Reference in New Issue
Block a user