The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 20/10/2014 14:38, Benedikt Ahrens wrote:
> Hello,
>
> running coqdoc with options -utf8 and -interpolate on the following Coq
> code will result in an HTML file where "[phi]" in the comment is turned
> into a link, but not any of the variants containing a unicode \varphi.
>
> ======= Utest.v
> Definition phi := 1.
> Definition ϕ := 1.
> Definition ϕ2 := 1.
> (** [phi] [ϕ] [ϕ2] *)
> =======
>
> The exact commands I am using are
> $ coqc Utest.v
> $ coqdoc - utf8 -interpolate Utest.v
>
> The Coq version I have tried is
> commit 6e0c5c81e9e81c2e5369427643b2ac51b9aa17e6 .
>
> Is there a way to obtain links for the latter two, too?

Not without fixing coqdoc, sorry.

The issue is that coqdoc recognizes hardly any utf8 characters 
(contrarily to coqc). So it wrongly assumes that \varphi cannot be a 
valid identifier character.

If you feel like getting your hands dirty, there is an easy fix. Open 
tools/coqdoc/cpretty.mll, look for a commented line containing '\xCF', 
uncomment it, recompile coqdoc, and that is it.

Best regards,

Guillaume