search

coq / coq.github.io

Source files of the coq.inria.fr website
https://coq.inria.fr/
Other
15 stars 37 forks source link

Moving to GitHub pages #82

Closed maximedenes closed 5 years ago

maximedenes commented 5 years ago

As part of a general strategy to reduce the sysadmin work we have to do in the team, @vbgl and I are preparing the move of the website to GitHub pages.

In this first step, we would keep the infrastructure unchanged, but the deployment would be done automatically using CI.

vbgl commented 5 years ago

The website of Coq https://coq.inria.fr currently offers:

The data sources are in two repositories hosted on GitHub:

I’ve been experimenting with using GitHub-Pages for hosting and Travis for automatic deployment, using my own account; preview is thus available at https://vbgl.github.io. This site is the superposition of two different ones:

The base addresses of these websites are not configurable, there are computed from the user/organization and repository names. However, it is possible to configure the domain name (see relevant GitHub Pages help), and superposition should work the same.

The two parts thus can independently evolve, be modified at their own pace.

In both cases, automatic deployment works as follows: whenever a modification is pushed to the main branch (of the repository holding the sources), e.g., when a pull request is merged, Travis starts a job which first builds the site and then, in case of success and using a GitHub access token, commits the result to the correct repository and branch. The details are in the corresponding configuration files: https://github.com/vbgl/vbgl.github.io/blob/sources/.travis.yml and https://github.com/vbgl/opam-coq-archive/blob/master/.travis.yml.

Should we use a dedicated GitHub user (e.g., @coqbot) to own the repositories in which the generated sites are stored?

ybertot commented 5 years ago

I did a rapid test of https://vbgl.github.io and there are a few 404 errors, for instance https://vbgl.github.io/what-is-coq . I just wanted to report the problem. Aside from this, the site seems to work like a charm.

vbgl commented 5 years ago

Thanks for the report. Has anyone got any hint about how to put that configuration file in use: https://vbgl.github.io/aliases.conf?

ybertot commented 5 years ago

A wild guess: rewrite rules to be used by an Apache web server?

Zimmi48 commented 5 years ago

GitHub pages won't support Apache rewrite rules AFAIK. That's unfortunate, but we have many existing redirects and I think we want to keep a lot of them. The alternative is HTML redirects.

@vbgl Why did you use the master branch to hold the generated HTML and sources for the real sources? GitHub allows you to use a different branch than master to old the "sources of the website" (i.e. the generated HTML).

vbgl commented 5 years ago

GitHub pages won't support Apache rewrite rules AFAIK. That's unfortunate, but we have many existing redirects and I think we want to keep a lot of them. The alternative is HTML redirects.

What about symlinks? or .htaccess?

Why did you use the master branch to hold the generated HTML and sources for the real sources? GitHub allows you to use a different branch than master to old the "sources of the website" (i.e. the generated HTML).

When I go to the “settings” page to choose the branch, I can read: “User pages must be built from the master branch.”

Zimmi48 commented 5 years ago

What about symlinks? or .htaccess?

From https://help.github.com/articles/redirects-on-github-pages/:

For the security of our users, GitHub Pages does not support customer server configuration files such as .htaccess or .conf.

When I go to the “settings” page to choose the branch, I can read: “User pages must be built from the master branch.”

Oh indeed! That's a shame.

vbgl commented 5 years ago

Here is an other question: what to do with https://coq.inria.fr/distrib/? Should we move it to GitHub-Pages too? In yet an other repo?

Zimmi48 commented 5 years ago

GitHub pages don't like so much the concept of committing binary files in the repo and send you an email to encourage the use of GitHub release for that purpose when you do so. Given that we have already stored these assets in GitHub releases down to 8.5pl3, I recommend setting redirects only (for these old releases), and redirecting to an archive somewhere else for the even older files.

However, as part of distrib, there is also the manual and the stdlib documentation and these of course need to be supported, if possible with continuous deployment.

Zimmi48 commented 5 years ago

It's probably time to close this issue. In the end, the action that was taken was to deploy only the documentation to GitHub pages automatically, and to set up a VPS at OVH to host the rest of the website (including the opam index, and the distrib/ subfolder).

Zimmi48 commented 5 years ago

Still note Maxime's comment in another issue:

The strategy is to make small steps. It is still not clear to me if we can target GitHub pages in the long run or not.