Add script to generate HTML for all Agda files appropriately
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
parent
6ffd3afeaa
commit
54844fb954
36
build-agda-html.rb
Normal file
36
build-agda-html.rb
Normal file
|
@ -0,0 +1,36 @@
|
||||||
|
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]}"
|
||||||
|
`agda --local-interfaces #{file} --html --html-dir=html`
|
||||||
|
end
|
||||||
|
end
|
Loading…
Reference in New Issue
Block a user