[isabelle-dev] AFP/Shivers-CFA latex document problem

Brian Huffman brianh at cs.pdx.edu
Fri Nov 19 19:42:03 CET 2010

On Fri, Nov 19, 2010 at 8:58 AM, Tobias Nipkow <nipkow at in.tum.de> wrote:
> I don't understand this: why does latex work for the release version but
> not the development version? But indeed, it fails for me too.

I created an extremely simplified version of the Shivers-CFA entry
(building on Isabelle/Pure instead of HOLCF) that still reproduces the
latex error, and did some bisection. The origin of the problem is this

basic setup for literal replacement text in PDF, to support copy/paste
of Isabelle symbols;

The root.tex of the Shivers-CFA entry contains the following two lines:

\newcommand{\isactrlps}[1]{{\uline #1}}

Here is the stripped-down version of the entry I used for testing:

theory Computability
imports Pure

definition foo :: "'a => 'a" ("\<^ps>") where
  "\<^ps>f == f"


... and here is the diff of the generated Computability.tex files,
comparing revision b646316f8b3c (+) to its parent revision (-).

-\ foo\ {\isacharcolon}{\isacharcolon}\
{\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\
-\ \ {\isachardoublequoteopen}\isactrlps f\
{\isacharequal}{\isacharequal}\ f{\isachardoublequoteclose}\isanewline
+\ foo\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\
+\ \ {\isaliteral{22}{\isachardoublequoteopen}}\isaliteral{5C3C5E70733E}{}\isactrlps
f\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\

Finally, here are the relevant LaTeX error messages:

*** (./session.tex (./Computability.tex
*** ! Undefined control sequence.
*** <argument> \UL at spfactor
*** l.27 ...\isaliteral{22}{\isachardoublequoteclose}}
*** ! Undefined control sequence.
*** \UL at word ...kip \unskip \spacefactor \UL at spfactor
***                                                   \let \UL at word
\egroup \els...
*** l.27 ...\isaliteral{22}{\isachardoublequoteclose}}
*** ! Missing number, treated as zero.
*** <to be read again>
***                    \let
*** l.27 ...\isaliteral{22}{\isachardoublequoteclose}}
*** ! Bad space factor (0).
*** <to be read again>
***                    \let
*** l.27 ...\isaliteral{22}{\isachardoublequoteclose}}
*** ))

- Brian

> Brian Huffman schrieb:
>> On Fri, Nov 19, 2010 at 7:28 AM, Brian Huffman <brianh at cs.pdx.edu> wrote:
>>> The latex document generation still doesn't work, though (at least on
>>> my machine), and I don't understand the error messages that it
>>> produces. Maybe it has something to do with the non-ascii unicode
>>> characters in some of the files?
>> I determined that the latex errors were due to the \uline command,
>> which is defined in the "ulem" latex package. If I replace {\uline
>> foo} with \underline{foo} throughout the sources, then the document
>> generation works. However, I'm not sure whether the typesetting in the
>> output is the same for the two commands.
>> I assume Joachim tested the latex output before submitting the entry,
>> so I wonder if my latex installation has a different version of the
>> ulem package? If the document generation is sensitive to package
>> versions, it might be a good idea to put a copy of ulem.sty in the
>> document directory of the AFP entry.
>> Also, it appears that the unicode apostrophes in the source files
>> don't cause any latex errors, although they are silently omitted from
>> the output. It would probably be a good idea to change them all to
>> ordinary ascii apostrophes.
>> - Brian

More information about the isabelle-dev mailing list