website coqdoc outdated / release process incomplete

[gares]

At some point @maximedenes made the website available at https://math-comp.github.io/ but the release process documented at https://github.com/math-comp/math-comp/wiki/Howto-Release misses a step to synchronize the websites (since the authoritative contents are still in the .../math-comp/ repo I guess).

[gares]

CC @CohenCyril @affeldt-aist Ping @maximedenes

[gares]

FTR, the website at http://math-comp.github.io/math-comp/ has the update coqdoc, while the one at https://math-comp.github.io/ has not!

[affeldt-aist]

I didn't realize the website was duplicated.

[gares]

it's a bug ;-)

[CohenCyril]

Should we take down http://math-comp.github.io/math-comp/ or keep it as a documentation-specific website?

[CohenCyril]

PS: Many links (papers, website, posts, chat messages) might still reference http://math-comp.github.io/math-comp/ as the main page, so I advocate we keep the page alive but re-purpose it as I said. What do you think?

[amahboubi]

I think that keeping the two is a bad idea, because it will be too confusing for both users and maintainers of the website.

Can't we just redirect http://math-comp.github.io/math-comp/ to http://math-comp.github.io?

[CohenCyril]

Can't we just redirect http://math-comp.github.io/math-comp/ to http://math-comp.github.io?

yes I think we can

[amahboubi]

Great! Yet this redirection topic is slightly different from the one of the present issue, which is about the bad version of the documentation linked from http://math-comp.github.io.

[amahboubi]

Ping @maximedenes .

[maximedenes]

Sorry for this confusing situation. Can you clarify what you want me to do?

[amahboubi]

Today the coqdoc documentation linked from the new location of the website is outdated. E.g.:
https://math-comp.github.io/htmldoc/mathcomp.ssreflect.ssreflect.html
The one in sync lives at the previous location. E.g.:
http://math-comp.github.io/math-comp/htmldoc/mathcomp.ssreflect.ssreflect.html

Actions needed:

1. repair
2. update the release instructions so that this does not happen anymore
3. Redirect http://math-comp.github.io/math-comp/ to http://math-comp.github.io

Point 3 is addressed by #365 but points 1 and 2 are not done, and should precede 3.

[maximedenes]

Working on 1.

For 2., I'll need to discuss with @gares how to separate concerns between math-comp proper and the website. The current html doc build script does very strange things, including mangling source files in place without warning... Not sure I can write reliable and reasonable release instructions with this state of affairs.

[amahboubi]

Working on 1.

Many thanks @maximedenes !

[maximedenes]

Wait! @gares didn't your import-doc Makefile target already address this?

https://github.com/math-comp/math-comp.github.io/blob/master/Makefile

The file header is a bit terse.

[maximedenes]

including mangling source files in place without warning

And of course it is not idempotent. So I got incorrect results, and will need to rebuild math comp entirely. Please bear with me.

[gares]

https://github.com/math-comp/math-comp.github.io/blob/master/Makefile

This should be dropped (it was used when we could not release by tagging master).

including mangling source files in place without warning... Not sure I can write reliable and reasonable release instructions with this state of affairs.

The Makefile in https://github.com/math-comp/math-comp/blob/master/docs/htmldoc/Makefile is idempotent when it succeeds (it checks your tree is clean and uses git to restore the old files at the end).

If you move the Makefile elsewhere you could get in input the git url to clone (a tag for the release, a branch for testing things)

[maximedenes]

The Makefile in https://github.com/math-comp/math-comp/blob/master/docs/htmldoc/Makefile is idempotent when it succeeds (it checks your tree is clean and uses git to restore the old files at the end).

Yeah but a successful build is typically one you don't restart, whereas failing ones...

[maximedenes]

If you move the Makefile elsewhere you could get in input the git url to clone (a tag for the release, a branch for testing things)

Yes, I think that's what we should do (although not sure it should be a Makefile). This way we could solve both problems, by working on a temporary copy of the repo (no modification in place) and not relying on the doc and the sources being in the same repo.

[gares]

It leaves you the thing that did not compile, so that you can inspect it. I really don't get what the problem is.

[maximedenes]

It leaves you the thing that did not compile, so that you can inspect it. I really don't get what the problem is.

The problem (IIUC) is that when you fix the problem and relaunch the build, it will mangle the sources more, and you get formatting issues in the final html.

[gares]

Then the check must be incomplete (since I guess you did not commit the mangled sources).
The script should just refuse to run if the sources are already mangled (it could be smarter, but this is not the problem here). Why does not it stop saying you have uncommitted changes?

[maximedenes]

Yes, the test is broken. We are discussing it in the other thread.

Anyway, it seems I finally got the updated HTML documentation. Will create a PR.

[maximedenes]

@amahboubi For 1., see math-comp/math-comp.github.io#7

[amahboubi]

Very good, thanks! One last thing regarding 1 and 3. As far as I can see, we now how two versions of the coqdoc,e.g.:
https://math-comp.github.io/htmldoc/mathcomp.ssreflect.ssreflect.html
and
http://math-comp.github.io/math-comp/htmldoc/mathcomp.ssreflect.ssreflect.html

Today, there are identical, but will they stay so? Can we either remove the 2nd one, or redirect to the first? It seems to me that #365 only addresses the re-direction of the root of the site. @CohenCyril can you confirm?