The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

I think I faced the same problem a while back. pdflatex does not seem to like unicode characters.

(I've heard that some alternative latex incarnations like unicode.)

You can work around this problem by adding coqdoc directives like:

(** printing θ $\theta$ #θ# *)

This directive tells coqdoc to replace θ by $\theta$ when emitting latex (and replace θ by θ when emitting HTML).

For example, I had to put many such directives at the top of the following file:

https://github.com/aa755/ROSCoq/blob/7949facbdfca8f4bdc38f4f2d0dc7e0a7b7c5fcd/examples/iCreateMoveToLoc.v

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Sun, Sep 6, 2015 at 2:33 PM, Benedikt Ahrens <benedikt.ahrens AT gmx.net> wrote:

Hello,

I have a Coq library that uses Unicode notation and identifiers, and I
am trying to produce latex documentation for this library, for inclusion
in an article.

The coqdoc tool with --latex option seems to work better than anything
else I have seen so far, and its output mostly compiles with pdflatex.
However, I am getting a few errors of several different kinds, examples
of which I post at the bottom of this email.

I would be grateful for any hints on how to patch coqdoc to remedy (some
of) these errors.

Alternatively, I would also be grateful for pointers to other tools that
allow the creation of latex code from Coq files containing Unicode. It
is important that the code can be compiled with pdflatex.

The coqdoc version used is from commit 76d6a8c (branch v8.5).
The texlive packages are the ones shipped in Debian 8. I can give more
precise information if necessary, of course.


Thanks a lot.
Best,
Benedikt


a)

! LaTeX Error: Command \textmu unavailable in encoding T1.

See the LaTeX manual or LaTeX Companion for explanation.
Type  H <return>  for immediate help.
 ...

l.621 ...s alt.xCExBC 0}{\coqdocdefinition{μ\_0}}


b)

! Undefined control sequence.
\u-default-964 #1->\texttau

l.457 ...84 LamE algebra on Lam}{\coqdoclemma{τ}}


c)

! Undefined control sequence.
<argument> \rrbracket

l.372 ... ',' x 'xE2x9FxA7'}{\coqdocnotation{⟧}}


d)

! Package ucs Error: Unknown Unicode character 10627 = U+2983,
(ucs)                possibly declared in uni-41.def.
(ucs)                Type H to see if it is available with options.

See the ucs package documentation for explanation.
Type  H <return>  for immediate help.
 ...

l.533 \coqdockw{Local} \coqdockw{Notation} "⦃
                                                f ⦄" :=
(\coqref{SubstSyst...

? H
Unicode character 10627 = U+2983:
LEFT WHITE CURLY BRACKET
Character is not defined in uni-*.def files.
Enter I!<RET> to define the glyph.
?