require "json" require "set" require "optparse" # 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| 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"] files.each do |file| 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 end end