The Coq mailing list

[Edsko de Vries <devriese AT cs.tcd.ie>]

On Wed, Apr 11, 2007 at 11:22:20PM -0400, Geoffrey Alan Washburn wrote:
> Edsko de Vries wrote:
> 
> >I have a coq file (.v) with lots of unicode in it. When I try to generate 
> >the
> >latex file using
> >
> >coqdoc --latex -g --inputenc utf8x stlu.v
> >
> >and then try to compile the Latex, I get
> >
> >! Package utf8x Error: Malformed UTF-8 sequence.
> 
> I'm not sure about this.
> 
> >If I use the coqdoc --utf8 option instead, I get a similar error
> >
> >! Package inputenc Error: Unicode char 
> >\u8:ￜ\check@icr\expandafter
> > not
> >set up f or use with LaTeX.
> >
> >Any ideas?
> 
> The above error message means that LaTeX does not know how to interpret 
> the given Unicode glyph.  Some mappings are provided by default, but 
> many Unicode glyphs are not given a default behavior.  Perhaps someone 
> else has done something like this for the glyphs you are using. If not, 
> for each glyph you need to define you will need to add a LaTeX commmand like
> 
> \DeclareUnicodeCharacter{03B1}{%my mapping for ??%}
> 
> where the first argument is the hexadecimal identity of the Unicode 
> glyph and the second argument is arbitrary LaTeX.  For example, I use
> 
> \DeclareUnicodeCharacter{03B1}{\textalpha}
> 
> where \textalpha is a macro that selects the ?? gylph from the 
> appropriate font.

Thanks for your answer. I've now declared every unicode character I use
in the manner you suggest, but there's another problem, and I suspect
it's a bug in coqdoc.  When I run a UTF8 validity tester over the .tex
file generated by coqdoc, it reports loads of malformed UTF8 sequences
(that's also the reason for the error reported by utf8x, and also for
the strange error message reported by the utf8 package, which should
read: Unicode char ?? not set up for..", where ?? is some unicode
character; there shouldn't be any tex code there).

I think they are all due to the same problem. Here's a line with such a
malformed sequence:

\coqdockw{Notation} "\coqdocid{<E2>}<80><A2>" := \coqdocid{Unique}.\coqdoceol

where I've replaced the UTF8 sequence with their ASCII codes for
clarity. The sequence <E2><80><A2> corresponds to the unicode 0x2202 (I
think), but the problem is clear: the closing curly is in the middle of
the sequence! It should read

\coqdockw{Notation} "\coqdocid{<E2><80><A2>}" := \coqdocid{Unique}.\coqdoceol

If I manually fix those curlies (and insert the DeclareUnicodeCharacter
statements), everything works.

Edsko