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

[Brian Huffman]

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
revision:

http://isabelle.in.tum.de/repos/isabelle/rev/b646316f8b3c
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:

\usepackage[normalem]{ulem}
\newcommand{\isactrlps}[1]{{\uline #1}}

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

theory Computability
imports Pure
begin

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

end

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

 \isanewline
 \isanewline
 \isacommand{definition}\isamarkupfalse%
-\ foo\ {\isacharcolon}{\isacharcolon}\
{\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\
{\isacharprime}a{\isachardoublequoteclose}\
{\isacharparenleft}{\isachardoublequoteopen}\isactrlps
{\isachardoublequoteclose}{\isacharparenright}\
\isakeyword{where}\isanewline
-\ \ {\isachardoublequoteopen}\isactrlps f\
{\isacharequal}{\isacharequal}\ f{\isachardoublequoteclose}\isanewline
+\ foo\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\
{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\
{\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\
{\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequoteclose}}\
{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}\isaliteral{5C3C5E70733E}{}\isactrlps
{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}\
\isakeyword{where}\isanewline
+\ \ {\isaliteral{22}{\isachardoublequoteopen}}\isaliteral{5C3C5E70733E}{}\isactrlps
f\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\
f{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
 %
 \isadelimtheory
 \isanewline

Finally, here are the relevant LaTeX error messages:

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

- 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
>