search

affeldt-aist / coq2html

An HTML documentation generator for Coq source files
GNU General Public License v2.0
1 stars 3 forks source link

links to section variables #11

Closed affeldt-aist closed 5 months ago

affeldt-aist commented 8 months ago

serious: links to section variables can be broken, for instance https://yoshihiro503.github.io/coq2html/mathcomp.analysis.measure.html#classes.G @proux01

yoshihiro503 commented 8 months ago

This is due to coqc.

The glob file for the Context command is incorrect. The path of the variable is incorrect in the glob file when using the Context command. This causes the same problem with coqdoc.

The following simple coq code Hoge.v will show us the glob file error.

Section Sec.
Context (foo : nat).
Definition f := foo.
End Sec.

We got the following Hoge.glob: 

DIGEST f2eaf1911fb0a5cbba737f02a91995ae
FHoge
sec 8:10 <> Sec
R28:30 Coq.Init.Datatypes <> nat ind
binder 22:24 <> foo:1
def 45:45 <> f
R50:52 Hoge <> Sec.foo var
R59:61 Hoge Sec <> sec

My Environment

yoshihiro503 commented 8 months ago

I posted the issue on coq/coq : https://github.com/coq/coq/issues/18516

proux01 commented 5 months ago

Fixed upstream by https://github.com/coq/coq/pull/18527