71 lines
1.9 KiB
Ruby
71 lines
1.9 KiB
Ruby
require "json"
|
|
require "set"
|
|
require "optparse"
|
|
require "fileutils"
|
|
|
|
# For target_dir, use absolute paths because when invoking Agda, we'll be
|
|
# using chdir.
|
|
root_path = "code"
|
|
target_dir = File.expand_path "code"
|
|
data_file = "data/submodules.json"
|
|
OptionParser.new do |opts|
|
|
opts.banner = "Usage: build-agda-html.rb [options]"
|
|
|
|
opts.on("--root-path=PATH", "Search for Agda project folders in the given location") do |f|
|
|
root_path = f
|
|
end
|
|
opts.on("--target-dir=PATH", "Generate HTML files into the given directory") do |f|
|
|
target_dir = File.expand_path f
|
|
end
|
|
opts.on("--data-file=FILE", "Specify the submodules.json that encodes nested submodule structure") do |f|
|
|
data_file = f
|
|
end
|
|
end.parse!
|
|
files = ARGV
|
|
|
|
code_paths = Dir.entries(root_path).select do |f|
|
|
File.directory?(File.join(root_path, f)) and f != '.' and f != '..'
|
|
end.to_set
|
|
code_paths += JSON.parse(File.read(data_file)).keys if File.exist? data_file
|
|
# Extending code_paths from submodules.json means that nested Agda modules
|
|
# have their root dir correctly set.
|
|
|
|
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("**/*.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
|
|
|
|
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(original_wd)
|
|
Dir.chdir(File.join(root_path, path))
|
|
html_dir = File.join [target_dir, path, "html"]
|
|
FileUtils.mkdir_p html_dir
|
|
|
|
files.each do |file|
|
|
command = "#{ARGV[0]} #{file} --html --html-dir=#{html_dir}"
|
|
puts command
|
|
puts `#{command}`
|
|
|
|
# Allow some programs to fail (e.g., IO.agda in SPA without --guardedness)
|
|
# fail unless $? == 0
|
|
end
|
|
end
|