diff --git a/build-agda-html.rb b/build-agda-html.rb index 54c37dc..e6582d0 100644 --- a/build-agda-html.rb +++ b/build-agda-html.rb @@ -1,8 +1,33 @@ require "json" require "set" +require "optparse" -code_paths = Dir.glob("code/*").to_set -code_paths += JSON.parse(File.read("data/submodules.json")).keys +# 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.exists? 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| @@ -17,7 +42,7 @@ max_path = ->(path) { } files_for_paths = {} -Dir.glob("code/**/*.agda") do |agda_file| +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] = [] @@ -28,10 +53,13 @@ end original_wd = Dir.getwd files_for_paths.each do |path, files| - Dir.chdir(File.join [original_wd, path]) + Dir.chdir(original_wd) + Dir.chdir(File.join(root_path, path)) + html_dir = File.join [target_dir, path, "html"] files.each do |file| - puts "Invoking 'agda' on file: #{File.join [Dir.getwd, file]}" - `#{ARGV[0]} --local-interfaces #{file} --html --html-dir=html` + command = "#{ARGV[0]} --local-interfaces #{file} --html --html-dir=#{html_dir}" + puts command + `#{command}` # Allow some programs to fail (e.g., IO.agda in SPA without --guardedness) # fail unless $? == 0