CI: Automatically Generating Html Documentation for each Pull Requests

[yoshihiro503]

Motivation for this change

@proux01

This will generate Html documentation of PR at the address: https://math-comp.github.io/analysis/doc/pr/[BRANCH-NAME]/

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Reference: How to document

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[affeldt-aist]

There are 4 failures in the CI. 3 are maybe unrelated, but the first one is maybe causing a problem:

Run peaceiris/actions-gh-pages@v4
[INFO] Usage https://github.com/peaceiris/actions-gh-pages#readme
Dump inputs
Setup auth token
Prepare publishing assets
Setup Git config
Create a commit
Push the commit or tag
  /usr/bin/git push origin gh-pages
  remote: Permission to math-comp/analysis.git denied to github-actions[bot].
  fatal: unable to access 'https://github.com/math-comp/analysis.git/': The requested URL returned error: 403
  Error: Action failed with "The process '/usr/bin/git' failed with exit code 128"

Does it mean we are lacking some permission?

[yoshihiro503]

@CohenCyril (cc: @affeldt-aist )
I would like this PR to automatically generate html docs from all PRs.
I want to use Github Actions to automatically deploy it to my gh-pages branch, but it doesn't seem to be working.

Do I need to configure anything about GITHUB_TOKEN?

[CohenCyril]

I'm trying to figure what is the best practice here, meanwhile you can generate a token here:
https://docs.github.com/en/authentication/keeping-your-account-and-data-secure/managing-your-personal-access-tokens (with just the bare necessary access rights)
And I will add it to the environment variable.

[CohenCyril]

Dear @yoshihiro503 please revoke your token ASAP.
You must never ever post a token publicly!

[yoshihiro503]

I removed the token now.