The Coq mailing list

[Clément Pit--Claudel <clement.pit AT gmail.com>]

Hi Benedikt,

This isn't noise; the \DeclareUnicodeCharacter tip is useful.
I've given up on pdfLaTeX a while ago; the horrible unicode support makes it 
extremely hard to type documents in mixed scripts. Instead, I use xeLaTeX; it 
handles unicode out of the box, it lets you change fonts at various points in 
your document, and fonts are loaded directly from the system fonts database. 
Font fallback is still tricky, but generally it provides a much nicer 
workflow for mixed-scripts documents. The unicodemath package, in particular, 
lets you use unicode in your math formula, meaning you can write \(∀ α ⋅ ∃ β 
⋅ α = β + 1\) directly, and it renders properly.

Clément.

On 09/06/2015 07:36 PM, Benedikt Ahrens wrote:
> 
> 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.
>>> ?
>>>
>>>
>>>
>>>
>>>
>>>
>>
>