Turn theory appendix in book into the Pikelet specification

[brendanzab]

I've been looking at the Web Assembly specification, and have been very impressed. I'm thinking it might be nice to follow its lead with regard to notation and approach. At the moment I just use the formal notation on the theory page, but it would nice to be able to expand it to a larger specification.

Static site generators

I'm not sure what we should use for documentation. Mdbook has been nice, but the support for maths notation support in pulldown-cmark is lacking right now. It would be lovely if pulldown-cmark supported setting the class of inline and block elements, kind of like: {katex}`\Gamma \vdash x : \tau` - this way it would also render ok in Github's previews, but I don't know what it would take to get that merged.

The features I need are:

• Math support:
  • preferrably KaTeX, but MathJax if necessary
  • ideally include math only on the pages I need it
  • not have to do double-backslashes all the time
  • ability to add global macros that I can use between documents
• Ability to add a custom syntax highlighting - currently I use a fork of highlight.js for this

So yeah some other options available to us:

Tool	Language	Markup Language	Math support	Custom syntax highlighting	Docs theme	Boots to SPA	Versions	PDF Export
Gutenburg	Rust	Markdown	No (could be added)	Awkward	Yes	No	No	No
Hakyll	Haskell	Markdown	MathJax or KaTeX	Unknown	No	No	No	No
Slick	Haskell	Markdown	MathJax or KaTeX	Unknown	No	No	No	No
Sphinx	Python	ReStructured text	MathJax or KaTeX	Unknown	Yes	No	Yes	Yes
VuePress	Javascript	Markdown	KaTeX (server rendered)	Yes	Yes	Yes	No	No
Docusaurus	Javascript	Markdown	KaTeX (server rendered)	Yes	Yes	No	Yes	No

Separate repository

Should we put the spec and/or site in a separate repository? Or continue with the mono-repo approach?

Existing Specs

• Web Assembly specification
• Agda Core Spec (unfinished)
• Coq Docs: Calculus of Inductive Constructions
• Standard ML Grammar
• The Definition of Standard ML, Revised - Github
• Futhark Language Reference (not really a spec)

[Keats]

Coming from reddit for Gutenberg: am I correct in thinking that katex/mathjax rendering is done in JavaScript? If so it could easily be done as a shortcode no?

[brendanzab]

Thanks for stopping by! I was kind of assuming you'd use the autorender extension, but then you get the issue of escaping all the maths with the double back slashes. Wish there was a way to give inline code and code blocks ids. That way you could just mark the elements you wanted to apply the maths to, and still have it be visible in the github markdown previews.

[brendanzab]

For reference, this is what the theory page looks like currently in Github. Blergh.

[brendanzab]

I mean, ideally this would all be done using KaTeX's serverside rendering feature. This would require executing bits of Javascript and then inlining the results into the rendered page though, which might be a pain to implement in Gutenberg.

[Keats]

This would require executing bits of Javascript and then inlining the results into the rendered page though, which might be a pain to implement in Gutenberg.

Yeah running JS from Rust is not going to be nice. Ideally there would be a C/Rust implementation that could have a wasm target for browsers but I'm not sure some people have that much free time/will to reimplement. Unless that happens, I don't think you will get nice markdown output using anything other than a JavaScript environment :/

[brendanzab]

Yeah, after messing around with a few options, I'm thinking I'm going to be going with a JavaScript solution, like VuePress or Docusaurus, for better or worse! Thanks a bunch for your assistance though, I really appreciate it! I have a bit of a weird use case I'll admit! 😅