Separation of content from HTML file

[palmskog]

The HTML file (index.html) is currently huge and difficult to edit for would-be contributors. This problem could be addressed by separating the file content from the HTML tags.

For example, the content could use a format such as JSON or YAML (and be akin to an editable database), and some tool or script could generate index.html. One possibility might be to use a mustache template.

One example of how this can be done is Lean's list of undergraduate mathematics: YAML source, generated HTML

[jmadiot]

Note that the content is messier than Lean's list, since there is some formatted html (text with several links per entry), and the statement itself, which may require other escape sequences and addition of some escape sequences when translating to HTML. I'm not sure a JSON or YAML file would be less huge or easier to edit, since there is now one more level of indirection? I initially used a database, and then switched to one html file with much satisfaction.

I'm not against it, I just wanted to mention the complications.

[jmadiot]

f3f9cd1 should solve this issue with a few yaml files, although the main one is still big. I guess removing index.html from the repo would be best since it is generated, but I've kept it as it is more practical for me for now.

[palmskog]

There's also the possibility of generating index.html (and possibly other files) via GitHub Actions continuous integration and committing it to a specific branch, say gh-pages, for each commit to the master branch. To give an example, we generate JavaScript from Coq/OCaml and deploy it to the gh-pages branch in the Sudoku project (generated file, GitHub Actions configuration).