plutus icon indicating copy to clipboard operation
plutus copied to clipboard

fix jekyll generation of agda markdown files (2)

Open jmchapman opened this issue 1 year ago • 3 comments

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

jmchapman avatar Mar 10 '23 11:03 jmchapman

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)

jmchapman avatar Mar 10 '23 11:03 jmchapman

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

jmchapman avatar Mar 10 '23 15:03 jmchapman

The style is intended to match https://plfa.github.io/

jmchapman avatar Mar 10 '23 15:03 jmchapman

This should be superseded by a forthcoming PR from @ramsay-t , so I'll close it.

kwxm avatar Feb 28 '24 14:02 kwxm