Potential improvements to generate.sh

[liyishuai]

• The generated index.md does not render a GitHub Page directly, and needs to be converted into index.html via pandoc index.md -o index.html pandoc -s index.md -o index.html. Is it worth adding this conversion to generate.sh?
• Add option flag to generate one file without overwriting others.

[Zimmi48]

Regarding the conversion from Markdown to HTML, since the index.md file is already an auto-generated file, I wonder what's the point of using Markdown and if the template should not be already an HTML file. We could also document what's the user is expected to do in the case they activate coqdoc (setting up a gh-pages branch, what to push there, etc.) Couldn't the management of gh-pages be automated through a GitHub Action? cc @palmskog

Other possible improvements:

• Only generate index.md when coqdoc is set to true.
• Move index.md to appropriate subdirectory. In https://github.com/coq-community/huffman and https://github.com/coq-community/lemma-overloading, it is resources.

[Zimmi48]

I just test running pandoc index.md -o index.html in the ATBR repository, and it seems like the actual command should be more complex than this because a lot seems to be lost when running just this command.

[erikmd]

@Zimmi48

Couldn't the management of gh-pages be automated through a GitHub Action?

yes that seems doable indeed, e.g. using this action?
https://github.com/appleboy/gh-pages-action#usage

[found in https://github.com/sdras/awesome-actions#github-pages]

[erikmd]

Regarding the conversion from Markdown to HTML, since the index.md file is already an auto-generated file, I wonder what's the point of using Markdown and if the template should not be already an HTML file.

Even if GitHub Pages supports the two formats (.html and .md, via the Jekyll machinery), maybe the .md is more legible when we directly see the .md in the GitHub repository view?

but both choices would be fine anyway!

[liyishuai]

I just test running pandoc index.md -o index.html in the ATBR repository, and it seems like the actual command should be more complex than this because a lot seems to be lost when running just this command.

I must have missed the -s (--standalone) flag. Does adding -s solve your problem?

[Zimmi48]

Yes, thanks!

[liyishuai]

Regarding the Coqdoc generation, I've tried to push documentations to gh-pages automatically, but later decided to only generate them and upload manually, until a better automation comes up.
Things to consider:

1. What versions should be automatically pushed to gh-pages? (Every tag and every branch?)
2. Where should gh-pages diverge from master branch? (Initial commit?)
3. Can the developer push to gh-pages manually?

[Zimmi48]

1. Every tag and every branch does sound reasonable to me. What does @palmskog think?
2. Yes, it seems to me that the two branches should be completely unrelated.
3. I would say no if we provide good enough automation.

[palmskog]

1. I think it should only be done on (every) tag. I don't understand why one would want it for a branch, though.
2. I personally start the gh-pages branch with a clean/nonexistent history (git checkout --orphan gh-pages, see for example here).
3. I can definitely see scenarios where one would want to push to gh-pages and add some static artifact, but generally we should discourage from this with good automation.

[Zimmi48]

Regarding why pushing doc also for branches, we do this in the Coq repo (see https://coq.github.io/doc/) and it's pretty convenient to point to the doc of unreleased stuff or to preview the documentation before releasing. But I guess this really depends on the size of the project. This could be an option that's disabled by default.