index.html

[motrellin]

Currently, a index.md-file is generated. For the use of Github Pages, it would be really nice to also have an equivalent index.html-file. Is it possible to add one to this template repository?

[erikmd]

OK but AFAIK, github pages directly supports index.md as well?
Given github pages allows one to use Jekyll as a Markdown-to-HTML engine...

[liyishuai]

I forgot why coq-ext-lib used pandoc to explicitly translate Markdown into HTML.

Maybe because index.md is only accessible by example.com/index rather than example.com/.
If so, a simple renaming into README.md (beyond the current generate.sh script) might actually solve the problem. I'll try it out next week and report the results here.

[erikmd]

Maybe because index.md is only accessible by example.com/index rather than example.com/.
If so, a simple renaming into README.md

I don't think so, the homepage always comes from index.md or docs/index.md, not from README.md

Minimal working example (not for a coq project, just for an ocaml project, but this doesn't matter):

• https://github.com/ocaml-sf/learn-ocaml/blob/master/docs/index.md
• no README.md nor index.html in https://github.com/ocaml-sf/learn-ocaml/tree/master/docs/
• http://ocaml-sf.org/learn-ocaml/index.html

[erikmd]

Actually, I found relevant info in the official docs:

https://docs.github.com/en/pages/getting-started-with-github-pages/creating-a-github-pages-site#creating-your-site

TL;DR: index.md is officially supported.

Create the entry file for your site. GitHub Pages will look for an index.html, index.md, or README.md file as the entry file for your site.

If your publishing source is a branch and folder, the entry file must be at the top level of the source folder on the source branch. For example, if your publishing source is the /docs folder on the main branch, your entry file must be located in the /docs folder on a branch called main.

If your publishing source is a GitHub Actions workflow, the artifact that you deploy must include the entry file at the top level of the artifact. Instead of adding the entry file to your repository, you may choose to have your GitHub Actions workflow generate your entry file when the workflow runs.

[motrellin]

Minimal working example (not for a coq project, just for an ocaml project, but this doesn't matter):

* https://github.com/ocaml-sf/learn-ocaml/blob/master/docs/index.md

* `no README.md nor index.html` in https://github.com/ocaml-sf/learn-ocaml/tree/master/docs/

* http://ocaml-sf.org/learn-ocaml/index.html

I think, the main difference is, that this repository uses the standard pages mechanism without a github action, right? I'm currently trying to use actions, here is my current example:

• Last run
• Current workflow

If your publishing source is a GitHub Actions workflow, the artifact that you deploy must include the entry file at the top level of the artifact. Instead of adding the entry file to your repository, you may choose to have your GitHub Actions workflow generate your entry file when the workflow runs.

This information sounds quite confusing for me: If I understand my workflow correctly, my entry file index.md is "generated" when the workflow runs, by copying it from resources/.

OTOH In an earlier version, I added an explicit index.html, concretely the standard (renamed) indexpage.html from coqdocjs. See here. This worked as an entrypoint. That's why I think, an generated index.html could be helpful.

[erikmd]

Hi @motrellin !

In brief: yes.
The standard pages mechanism where GitHub Actions is not involved does not need to think about index.html;
but if you generate the pages programatically, you may need to generate the index.html yourself.

Anyway, I believe this GHA workflow example could be useful to you:
https://github.com/actions/starter-workflows/blob/main/pages/jekyll-gh-pages.yml

[motrellin]

Thank you very much @erikmd ! I made it work now.

Working example

• I put everything together in some template: https://github.com/motrellin/comoproj
• My old working example: https://github.com/motrellin/comoalg
• Pages-Output: https://motrellin.github.io/comoalg/

Back to the original question to this project: As I'm not sure whether this Jekyll mechanism is a suitable solution for everyone, what do you think about a auto-generated index.html-file? If it's not that much extra work (Sorry, I have no experience with mustache!), this could be a nice extension to these templates IMO.

[liyishuai]

I forgot why coq-ext-lib used pandoc to explicitly translate Markdown into HTML.

Reason: index.md renders fine by itself, but the default Jekyll workflow (out-of-the-box from "Settings - Pages") breaks the Coqdocjs rendering. Since coq-ext-lib page hosts the Coqdocs for the tagged versions instead of the master branch, it's rather complex to generate the Pages automatically.