|
| 1 | +# ProofFrog Website |
| 2 | + |
| 3 | +This is the documentation website for [ProofFrog](https://github.com/ProofFrog/ProofFrog), a tool for verifying game-hopping cryptographic proofs. The site is published at https://prooffrog.github.io. |
| 4 | + |
| 5 | +## Tech stack |
| 6 | + |
| 7 | +- **Jekyll 4.4** static site generator with the **Just the Docs 0.12.0** theme |
| 8 | +- **jekyll-katex** plugin for math rendering (use `{% katex %}...{% endkatex %}` blocks) |
| 9 | +- **jekyll-redirect-from** plugin for URL redirects (via `redirect_from:` in front matter) |
| 10 | +- Custom Rouge syntax highlighter for FrogLang DSL (`_plugins/rouge_prooffrog.rb`) |
| 11 | +- Ruby gems managed via `Gemfile` |
| 12 | + |
| 13 | +## Building locally |
| 14 | + |
| 15 | +```bash |
| 16 | +bundle install |
| 17 | +bundle exec jekyll serve |
| 18 | +``` |
| 19 | + |
| 20 | +## Content structure |
| 21 | + |
| 22 | +- `manual/` — primary user-facing documentation |
| 23 | + - `installation.md` — installation guide (all platforms) |
| 24 | + - `tutorial/` — step-by-step getting started tutorials |
| 25 | + - `worked-examples/` — detailed worked proof examples |
| 26 | + - `language-reference/` — FrogLang language reference |
| 27 | + - `cli-reference.md`, `web-editor.md`, `editor-plugins.md`, etc. |
| 28 | +- `researchers/` — content aimed at researchers (engine internals, publications, soundness) |
| 29 | +- `examples.md` — catalogue of supported proof examples |
| 30 | +- `_data/linear_sequence.yml` — ordered page sequence for the linear "Getting Started" navigation path |
| 31 | + |
| 32 | +## Page conventions |
| 33 | + |
| 34 | +- All content pages are Markdown with YAML front matter |
| 35 | +- Two layouts: `default` (standard) and `linear` (sequential reading path with prev/next links) |
| 36 | +- Pages using `layout: linear` must also appear in `_data/linear_sequence.yml` |
| 37 | +- Use `{: .no_toc }` after the top-level heading, then the TOC block: |
| 38 | + ``` |
| 39 | + - TOC |
| 40 | + {:toc} |
| 41 | + ``` |
| 42 | +- Internal links use Jekyll's `{% link path/to/file.md %}` tag |
| 43 | +- Callout blocks use Just the Docs IAL syntax: `{: .note }`, `{: .warning }`, `{: .important }`, `{: .highlight }`, `{: .new }` |
| 44 | +- Code blocks should use appropriate language identifiers (`bash`, `powershell`, `fish`, etc.) |
| 45 | +- FrogLang code blocks use the custom `prooffrog` language identifier |
| 46 | + |
| 47 | +## Navigation hierarchy |
| 48 | + |
| 49 | +Pages declare their position via front matter: `parent`, `grand_parent`, `nav_order`, `has_children`. The Manual section is the main nav parent; subsections (Tutorial, Language Reference, etc.) are children of Manual. |
0 commit comments