blog-static/build-agda-html.rb

require "json"
require "set"

code_paths = Dir.glob("code/*").to_set
code_paths += JSON.parse(File.read("data/submodules.json")).keys

max_path = ->(path) {
  code_paths.max_by do |code_path|
    count = 0
    path.chars.zip(code_path.chars) do |c1, c2|
      break unless c1 == c2
      count += 1
    end

    next count
  end
}

files_for_paths = {}
Dir.glob("code/**/*.agda") 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

  files_for_path << agda_file[best_path.length + File::SEPARATOR.length..-1]
end

original_wd = Dir.getwd
files_for_paths.each do |path, files|
  Dir.chdir(File.join [original_wd, path])
  files.each do |file|
    puts "Invoking 'agda' on file: #{File.join [Dir.getwd, file]}"
    `#{ARGV[0]} --local-interfaces #{file} --html --html-dir=html`

    # Allow some programs to fail (e.g., IO.agda in SPA without --guardedness)
    # fail unless $? == 0
  end
end