Add building and linking Agda as build step
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
@@ -25,6 +25,12 @@ cp -r $webFiles/* static/
|
||||
# Build site with Hugo
|
||||
hugo $hugoFlags --config=config.toml,config-urls.toml
|
||||
|
||||
# Run Agda to generate HTML files for all Agda projects
|
||||
# Agda will write interface files, so make .code/ writable
|
||||
chmod -R u+w code
|
||||
agdaCommand="agda -l standard-library -i . "
|
||||
ruby ./build-agda-html.rb "$agdaCommand"
|
||||
|
||||
# Create generated files
|
||||
# Can't do submodules because nix flake inputs get their .git deleted
|
||||
mkdir -p static/graph && ruby ./analyze.rb > static/graph/graph.gen.js # Graph files
|
||||
@@ -39,4 +45,6 @@ mkdir $out
|
||||
cp -r public/$publicPath/* $out/
|
||||
|
||||
# Render math in HTML and XML files.
|
||||
find $out/ -regex "$out/.*\.html" | xargs katex-html
|
||||
htmlfiles=$(find $out/ -regex "$out/.*\.html")
|
||||
echo $htmlfiles | xargs katex-html
|
||||
echo $htmlfiles | xargs ${gems}/bin/bundle exec ${ruby}/bin/ruby ./agda.rb
|
||||
|
||||
Reference in New Issue
Block a user