search

coq / coq.github.io

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

Figures is epsent in Reference Manual #65

Closed FeelUsM closed 6 years ago

FeelUsM commented 6 years ago

at page https://coq.inria.fr/distrib/current/refman/gallina.html (and may be at other pages, I didn't see) figures 1.1, 1.2 and 1.3 are absent

letouzey commented 6 years ago

Hi, thanks for the report, but currently I cannot reproduce the issue, the figures in this page appear correctly in my browser (Firefox 52.7). Could you please check the direct links to these figures : 1.1 and 1.2 and 1.3 ? Be careful that these links point unfortunately to the bottom of the figures, so you might need to scroll up a bit in your browser to make them appear.

FeelUsM commented 6 years ago

In chrome 65.0 screenshotes: page: https://yadi.sk/i/47-lrjHv3UTvvW , code of page: https://yadi.sk/i/A0JuMO0a3UTw3y I scpecially disable AdBlockPlus and MuBlock. In Firefox 57.0 the same situation. I want to see links on amages itself.

letouzey commented 6 years ago

Thanks for the screenshots. I confirm, no real bug here, just some misleading html code produced by the latex-to-html converter we're using (hevea). The actual content of figure 1.1 is indeed there in the page, just before the caption saying Figure 1.1 : Syntax of terms. This content is actually the bunch of grammar rules starting by term ::= forall binders , term and ending with sort ::= Prop | Set | Type. You may notice the two <hr> lines that delimit this figure, one before these grammar rules, the other after the caption. And the next <hr> immediately below is the start of figure 1.2. For large figures like this one, having the caption at the end is indeed quite unclear. Moreover, as I already said, the html anchor <a id="term-syntax"> is quite badly placed (after the caption). Sorry for the inconvenience.

Actually, we're currently converting the Coq documentation to a deeply different system (sphinx instead of latex + hevea). See for instance https://coq.inria.fr/distrib/V8.8+beta1/refman/language/gallina-extensions.html for a page that has already been converted. This effort isn't fully finished yet, but it should hopefully be a matter of weeks now, stay tuned. This will drastically improve the aspect of the documentation pages, and in particular should fix these sub-optimal "figures".

maximedenes commented 6 years ago

but it should hopefully be a matter of weeks now

I would say a matter of hours, even :)