plutus
plutus copied to clipboard
fix jekyll generation of agda markdown files (2)
We currently generate html (e.g., Type.html) from the markdown files (e.g, Type.md) generated from the agda files (e.g, Type.lagda.md) but jekyll is not configured properly so the generated html doesn't look right.
I am testing this locally as follows:
$ nix develop
$ cd plutus/plutus-metatheory/src
$ agda --html --html-highlight=auto --html-dir=site index.lagda.md
$ cd site
$ jekyll serve
I have added the jekyll config files to the the html
folder. When I try to run jekyll serve
I get this error:
Configuration file: plutus/plutus-metatheory/src/html/_config.yml
------------------------------------------------
Jekyll 4.2.0 Please append `--trace` to the `serve` command
for any additional information or backtrace.
------------------------------------------------
Traceback (most recent call last):
23: from /nix/store/p43xrakwcb8byvkpm5vqpgbbn1rbgvz3-jekyll-4.2.0/bin/.jekyll-wrapped:35:in `<main>'
22: from /nix/store/p43xrakwcb8byvkpm5vqpgbbn1rbgvz3-jekyll-4.2.0/bin/.jekyll-wrapped:35:in `load'
21: from /nix/store/p43xrakwcb8byvkpm5vqpgbbn1rbgvz3-jekyll-4.2.0/lib/ruby/gems/2.7.0/gems/jekyll-4.2.0/exe/jekyll:15:in `<top (required)>'
20: from /nix/store/qb7sa9lwd9x636yrphr39r0xbbv1wjfm-ruby2.7.6-mercenary-0.4.0/lib/ruby/gems/2.7.0/gems/mercenary-0.4.0/lib/mercenary.rb:21:in `program'
19: from /nix/store/qb7sa9lwd9x636yrphr39r0xbbv1wjfm-ruby2.7.6-mercenary-0.4.0/lib/ruby/gems/2.7.0/gems/mercenary-0.4.0/lib/mercenary/program.rb:44:in `go'
18: from /nix/store/qb7sa9lwd9x636yrphr39r0xbbv1wjfm-ruby2.7.6-mercenary-0.4.0/lib/ruby/gems/2.7.0/gems/mercenary-0.4.0/lib/mercenary/command.rb:221:in `execute'
17: from /nix/store/qb7sa9lwd9x636yrphr39r0xbbv1wjfm-ruby2.7.6-mercenary-0.4.0/lib/ruby/gems/2.7.0/gems/mercenary-0.4.0/lib/mercenary/command.rb:221:in `each'
16: from /nix/store/qb7sa9lwd9x636yrphr39r0xbbv1wjfm-ruby2.7.6-mercenary-0.4.0/lib/ruby/gems/2.7.0/gems/mercenary-0.4.0/lib/mercenary/command.rb:221:in `block in execute'
15: from /nix/store/a0madl81y1f31x9dilc4y2wb28gzaih7-ruby2.7.6-jekyll-4.2.0/lib/ruby/gems/2.7.0/gems/jekyll-4.2.0/lib/jekyll/commands/serve.rb:86:in `block (2 levels) in init_with_program'
14: from /nix/store/a0madl81y1f31x9dilc4y2wb28gzaih7-ruby2.7.6-jekyll-4.2.0/lib/ruby/gems/2.7.0/gems/jekyll-4.2.0/lib/jekyll/command.rb:91:in `process_with_graceful_fail'
13: from /nix/store/a0madl81y1f31x9dilc4y2wb28gzaih7-ruby2.7.6-jekyll-4.2.0/lib/ruby/gems/2.7.0/gems/jekyll-4.2.0/lib/jekyll/command.rb:91:in `each'
12: from /nix/store/a0madl81y1f31x9dilc4y2wb28gzaih7-ruby2.7.6-jekyll-4.2.0/lib/ruby/gems/2.7.0/gems/jekyll-4.2.0/lib/jekyll/command.rb:91:in `block in process_with_graceful_fail'
11: from /nix/store/a0madl81y1f31x9dilc4y2wb28gzaih7-ruby2.7.6-jekyll-4.2.0/lib/ruby/gems/2.7.0/gems/jekyll-4.2.0/lib/jekyll/commands/build.rb:30:in `process'
10: from /nix/store/a0madl81y1f31x9dilc4y2wb28gzaih7-ruby2.7.6-jekyll-4.2.0/lib/ruby/gems/2.7.0/gems/jekyll-4.2.0/lib/jekyll/commands/build.rb:30:in `new'
9: from /nix/store/a0madl81y1f31x9dilc4y2wb28gzaih7-ruby2.7.6-jekyll-4.2.0/lib/ruby/gems/2.7.0/gems/jekyll-4.2.0/lib/jekyll/site.rb:23:in `initialize'
8: from /nix/store/a0madl81y1f31x9dilc4y2wb28gzaih7-ruby2.7.6-jekyll-4.2.0/lib/ruby/gems/2.7.0/gems/jekyll-4.2.0/lib/jekyll/site.rb:60:in `config='
7: from /nix/store/a0madl81y1f31x9dilc4y2wb28gzaih7-ruby2.7.6-jekyll-4.2.0/lib/ruby/gems/2.7.0/gems/jekyll-4.2.0/lib/jekyll/site.rb:510:in `configure_theme'
6: from /nix/store/a0madl81y1f31x9dilc4y2wb28gzaih7-ruby2.7.6-jekyll-4.2.0/lib/ruby/gems/2.7.0/gems/jekyll-4.2.0/lib/jekyll/site.rb:510:in `new'
5: from /nix/store/a0madl81y1f31x9dilc4y2wb28gzaih7-ruby2.7.6-jekyll-4.2.0/lib/ruby/gems/2.7.0/gems/jekyll-4.2.0/lib/jekyll/theme.rb:13:in `initialize'
4: from /nix/store/a0madl81y1f31x9dilc4y2wb28gzaih7-ruby2.7.6-jekyll-4.2.0/lib/ruby/gems/2.7.0/gems/jekyll-4.2.0/lib/jekyll/theme.rb:19:in `root'
3: from /nix/store/a0madl81y1f31x9dilc4y2wb28gzaih7-ruby2.7.6-jekyll-4.2.0/lib/ruby/gems/2.7.0/gems/jekyll-4.2.0/lib/jekyll/theme.rb:80:in `gemspec'
2: from /nix/store/9lc10qqdnn20x2xsvlfx9czyjcwzqsv2-ruby-2.7.6/lib/ruby/2.7.0/rubygems/specification.rb:1021:in `find_by_name'
1: from /nix/store/9lc10qqdnn20x2xsvlfx9czyjcwzqsv2-ruby-2.7.6/lib/ruby/2.7.0/rubygems/dependency.rb:323:in `to_spec'
/nix/store/9lc10qqdnn20x2xsvlfx9czyjcwzqsv2-ruby-2.7.6/lib/ruby/2.7.0/rubygems/dependency.rb:311:in `to_specs': Could not find 'minima' (>= 0) among 88 total gem(s) (Gem::MissingSpecError)
Checked in 'GEM_PATH=/Users/james/.gem/ruby/2.7.0:/nix/store/9lc10qqdnn20x2xsvlfx9czyjcwzqsv2-ruby-2.7.6/lib/ruby/gems/2.7.0:/nix/store/p43xrakwcb8byvkpm5vqpgbbn1rbgvz3-jekyll-4.2.0/lib/ruby/gems/2.7.0' , execute `gem env` for more information
21: from /nix/store/p43xrakwcb8byvkpm5vqpgbbn1rbgvz3-jekyll-4.2.0/bin/.jekyll-wrapped:35:in `<main>'
20: from /nix/store/p43xrakwcb8byvkpm5vqpgbbn1rbgvz3-jekyll-4.2.0/bin/.jekyll-wrapped:35:in `load'
19: from /nix/store/p43xrakwcb8byvkpm5vqpgbbn1rbgvz3-jekyll-4.2.0/lib/ruby/gems/2.7.0/gems/jekyll-4.2.0/exe/jekyll:15:in `<top (required)>'
18: from /nix/store/qb7sa9lwd9x636yrphr39r0xbbv1wjfm-ruby2.7.6-mercenary-0.4.0/lib/ruby/gems/2.7.0/gems/mercenary-0.4.0/lib/mercenary.rb:21:in `program'
17: from /nix/store/qb7sa9lwd9x636yrphr39r0xbbv1wjfm-ruby2.7.6-mercenary-0.4.0/lib/ruby/gems/2.7.0/gems/mercenary-0.4.0/lib/mercenary/program.rb:44:in `go'
16: from /nix/store/qb7sa9lwd9x636yrphr39r0xbbv1wjfm-ruby2.7.6-mercenary-0.4.0/lib/ruby/gems/2.7.0/gems/mercenary-0.4.0/lib/mercenary/command.rb:221:in `execute'
15: from /nix/store/qb7sa9lwd9x636yrphr39r0xbbv1wjfm-ruby2.7.6-mercenary-0.4.0/lib/ruby/gems/2.7.0/gems/mercenary-0.4.0/lib/mercenary/command.rb:221:in `each'
14: from /nix/store/qb7sa9lwd9x636yrphr39r0xbbv1wjfm-ruby2.7.6-mercenary-0.4.0/lib/ruby/gems/2.7.0/gems/mercenary-0.4.0/lib/mercenary/command.rb:221:in `block in execute'
13: from /nix/store/a0madl81y1f31x9dilc4y2wb28gzaih7-ruby2.7.6-jekyll-4.2.0/lib/ruby/gems/2.7.0/gems/jekyll-4.2.0/lib/jekyll/commands/serve.rb:86:in `block (2 levels) in init_with_program'
12: from /nix/store/a0madl81y1f31x9dilc4y2wb28gzaih7-ruby2.7.6-jekyll-4.2.0/lib/ruby/gems/2.7.0/gems/jekyll-4.2.0/lib/jekyll/command.rb:91:in `process_with_graceful_fail'
11: from /nix/store/a0madl81y1f31x9dilc4y2wb28gzaih7-ruby2.7.6-jekyll-4.2.0/lib/ruby/gems/2.7.0/gems/jekyll-4.2.0/lib/jekyll/command.rb:91:in `each'
10: from /nix/store/a0madl81y1f31x9dilc4y2wb28gzaih7-ruby2.7.6-jekyll-4.2.0/lib/ruby/gems/2.7.0/gems/jekyll-4.2.0/lib/jekyll/command.rb:91:in `block in process_with_graceful_fail'
9: from /nix/store/a0madl81y1f31x9dilc4y2wb28gzaih7-ruby2.7.6-jekyll-4.2.0/lib/ruby/gems/2.7.0/gems/jekyll-4.2.0/lib/jekyll/commands/build.rb:30:in `process'
8: from /nix/store/a0madl81y1f31x9dilc4y2wb28gzaih7-ruby2.7.6-jekyll-4.2.0/lib/ruby/gems/2.7.0/gems/jekyll-4.2.0/lib/jekyll/commands/build.rb:30:in `new'
7: from /nix/store/a0madl81y1f31x9dilc4y2wb28gzaih7-ruby2.7.6-jekyll-4.2.0/lib/ruby/gems/2.7.0/gems/jekyll-4.2.0/lib/jekyll/site.rb:23:in `initialize'
6: from /nix/store/a0madl81y1f31x9dilc4y2wb28gzaih7-ruby2.7.6-jekyll-4.2.0/lib/ruby/gems/2.7.0/gems/jekyll-4.2.0/lib/jekyll/site.rb:60:in `config='
5: from /nix/store/a0madl81y1f31x9dilc4y2wb28gzaih7-ruby2.7.6-jekyll-4.2.0/lib/ruby/gems/2.7.0/gems/jekyll-4.2.0/lib/jekyll/site.rb:510:in `configure_theme'
4: from /nix/store/a0madl81y1f31x9dilc4y2wb28gzaih7-ruby2.7.6-jekyll-4.2.0/lib/ruby/gems/2.7.0/gems/jekyll-4.2.0/lib/jekyll/site.rb:510:in `new'
3: from /nix/store/a0madl81y1f31x9dilc4y2wb28gzaih7-ruby2.7.6-jekyll-4.2.0/lib/ruby/gems/2.7.0/gems/jekyll-4.2.0/lib/jekyll/theme.rb:13:in `initialize'
2: from /nix/store/a0madl81y1f31x9dilc4y2wb28gzaih7-ruby2.7.6-jekyll-4.2.0/lib/ruby/gems/2.7.0/gems/jekyll-4.2.0/lib/jekyll/theme.rb:19:in `root'
1: from /nix/store/a0madl81y1f31x9dilc4y2wb28gzaih7-ruby2.7.6-jekyll-4.2.0/lib/ruby/gems/2.7.0/gems/jekyll-4.2.0/lib/jekyll/theme.rb:79:in `gemspec'
/nix/store/a0madl81y1f31x9dilc4y2wb28gzaih7-ruby2.7.6-jekyll-4.2.0/lib/ruby/gems/2.7.0/gems/jekyll-4.2.0/lib/jekyll/theme.rb:82:in `rescue in gemspec': The minima theme could not be found. (Jekyll::Errors::MissingDependencyException)
It is supposed to look like this:
https://input-output-hk.github.io/plutus-metatheory/ https://input-output-hk.github.io/plutus-metatheory/Type.html
^ this is some old content I generated manually using the files committed in this PR
The style is intended to match https://plfa.github.io/
This should be superseded by a forthcoming PR from @ramsay-t , so I'll close it.