Stream: Coq users

Topic: Online documentation broken?


view this post on Zulip Jerome Hugues (Oct 02 2023 at 12:59):

Hi,

I am having some issues accessing online documentation
This link works : https://coq.inria.fr/library/Coq.Sets.Ensembles.html#Singleton:13
Now, go to https://coq.inria.fr/library/index.html and click on "Logic" under Init.

Then the URL becomes: https://coq.inria.fr/doc/V8.17.1/refman/V8.17.1/refman/V8.17.1/refman/V8.17.1/refman/V8.17.1/refman/V8.17.1/refman/V8.17.1/refman/V8.17.1/refman/V8.17.1/refman/V8.17.1/refman/V8.17.1/refman/V8.17.1/refman/V8.17.1/refman/V8.17.1/refman/V8.17.1/refman/V8.17.1/refman/V8.17.1/refman/V8.17.1/refman/V8.17.1/refman/V8.17.1/stdlib/Coq.Init.Logic.html

From the table of contents, no issue looking at, e.g., Notations.

Looks like a redirection error to me, not sure this is related to my setting or not.
Can anyone confirm?

Thanks

view this post on Zulip Théo Zimmermann (Oct 02 2023 at 13:03):

This is related to the ongoing website migration to GitHub pages but it should be fixed now.

view this post on Zulip Julin Shaji (Oct 03 2023 at 08:50):

Thanks. The CSS looks fine as well.

view this post on Zulip Karl Palmskog (Oct 03 2023 at 08:51):

maybe the CSS was affected by DNS, and now DNS changes have propagated

view this post on Zulip Paolo Giarrusso (Oct 03 2023 at 08:55):

The CSS looks broken and e.g. https://coq.inria.fr/modules/node/node.css (and https://coq.inria.fr/modules/system/defaults.css, I won't test the rest) gives 404

view this post on Zulip Karl Palmskog (Oct 03 2023 at 08:58):

ah, always trouble with cache stuff. I tested a few times on different machines and got 404 there, so I agree CSS needs some more checking

view this post on Zulip Notification Bot (Oct 03 2023 at 09:00):

Paolo Giarrusso has marked this topic as unresolved.

view this post on Zulip Paolo Giarrusso (Oct 03 2023 at 09:01):

indeed — another test seemed to work a bit, but only because the old CSS was cached — Shift+Reload to clear the cache revealed the problem again

view this post on Zulip Ralf Jung (Oct 03 2023 at 13:51):

Cc @Théo Zimmermann -- who would be able to look into the CSS issue?

view this post on Zulip Théo Zimmermann (Oct 03 2023 at 13:53):

Anyone can: all the source code is public now that the website is hosted on GitHub Pages. What prevents me from looking into it is mostly a lack of time to allocate to this before Friday. Maybe we can request the help of @Romain Tetley (even though, AFAIK, he has never worked on the website before)...


Last updated: Jun 22 2024 at 16:02 UTC