The Coq mailing list

[Benedikt Ahrens <benedikt.ahrens AT gmx.net>]

Thanks a lot for your answer.

In the end it turned out that the problems were general latex problems,
and not specific to coqdoc.

[ For sake of completeness, a) - c) were fixed by adding a few packages
(textgreek, stmaryrd) to the created latex files. d) was fixed by adding
\DeclareUnicodeCharacter{10627}{{\(\llparenthesis\)}}.
Both can be done using the -p option of coqdoc. ]

Sorry for the noise.
Benedikt


On 09/06/2015 10:05 PM, Abhishek Anand wrote:
> 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.
>> ?
>>
>>
>>
>>
>>
>>
>