[isabelle-dev] Latex issue (Fwd: isabelle dist build failed)

[Alexander Krauss]

Thanks, the nightly isatest works again.

Alex

On 05/30/2011 05:14 PM, Lawrence Paulson wrote:
> There were broken index entries in most of the old documentation. For some reason, the | symbol didn't cause a problem in the tutorial. One index entry here was fixed to use ?? (as opposed to !) as the sort key.
> Larry
>
> On 30 May 2011, at 15:28, Lawrence Paulson wrote:
>
>> It seems it can be fixed by
>>
>> (a) using ! rather than | as the sort key (the sorting of special symbols is arbitrary anyway)
>> (b) using \char124 to denote the | symbol
>>
>> I would expect to see this problem in any index entry involving the | symbol.
>>
>> Larry
>>
>> On 30 May 2011, at 14:58, Lawrence Paulson wrote:
>>
>>> My impression from fooling around a little is that this is a bug that has been around for a year and a half. The comment seems to suggest that | no longer works as an index item (even when protected using"), so we have to give up index entries for the symbols | and |-|. I wonder whether there is some sort of workaround?
>>>
>>> http://r.789695.n4.nabble.com/Recent-TeX-changes-and-R-package-manuals-td956056.html
>>>
>>>> (ii) there have been intermittent problems with (LaTeX) special
>>>> characters in indices.  But (hyperref 6.79d)
>>>>
>>>>   Full support of makeindex’s encap feature (e.g.
>>>>   \index{alpha|textbf}). \hyperpage and the formatting command are
>>>>   cascaded via \hyperindexformat. Internally \index{alpha|textbf} is
>>>>   transferred to \index{alpha|hyperindexformat{\textbf}}.
>>>>   \hyperindexformat calls the formatting command in its first argument
>>>>   with the page range as argument that is put into \hyperpage. The
>>>>   formatting command may call \hyperpage itself, it will be disabled
>>>>   automatically to prevent nested \hyperpage commands.
>>>>
>>>> has broken '|' as an index item ('||' was already broken) so I added
>>>> some special-casing (this does look like a bug in hyperref).
>>>
>>> Larry
>>>
>>> On 30 May 2011, at 09:39, Alexander Krauss wrote:
>>>
>>>> Hi all,
>>>>
>>>> The nightly isatest stopped working after the tex distribution on our servers was updated to Tex Live 2010 (at least we suspect that this is the cause of the problem).
>>>>
>>>> This seems to be an obscure latex problem that arises when buliding doc-src/Logics. It seems that the (generated!) file logics.ind is somehow malformed, which makes the subsequent tex run crash.
>>>>
>>>> Could someone who knows more about this document setup look into this issue?
>>>>
>>>> Steps to reproduce:
>>>>
>>>> * Log into macbroy20-28
>>>> * On some repository clone, go to ~~/doc-src/Logics and run
>>>>
>>>> make clean dvi
>>>>
>>>>
>>>> Note that the regular nightly isatest will not run until this is fixed, because it first builds the documentation (as part of the distribution). The new testing framework is not affected by it (since it effectively ignores documentation at the moment).
>>>>
>>>> Alex
>>>>
>>>>
>>>> -------- Original Message --------
>>>> Subject: isabelle dist build failed
>>>> Date: Mon, 30 May 2011 00:18:04 +0200
>>>> From: isatest at macbroy28.informatik.tu-muenchen.de (Account Isatest)
>>>> To: krauss at in.tum.de
>>>>
>>>> Could not build isabelle distribution. Log file available at
>>>> macbroy28:/home/isatest/log/isatest-makedist-2011-05-30.log
>>>> _______________________________________________
>>>> isabelle-dev mailing list
>>>> isabelle-dev at in.tum.de
>>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>>
>>