The Coq mailing list

[Peter LeFanu Lumsdaine <p.l.lumsdaine AT gmail.com>]

Just out of interest, is there a reason why these lines are commented out in trunk?

According to https://github.com/coq/coq/blame/trunk/tools/coqdoc/cpretty.mll#L266 they’ve been commented out ever since they were added in 2009.

–p.

On Mon, Oct 20, 2014 at 5:12 PM, Guillaume Melquiond <guillaume.melquiond AT inria.fr> wrote:

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