[isabelle-dev] AFP failure in Lam-ml-Normalization

Makarius makarius at sketis.net
Thu Nov 17 14:09:51 CET 2011

On Thu, 17 Nov 2011, Makarius wrote:

>> When it comes to the AFP failure, there's a second AFP failure, in 
>> JinjaThreads, that's obviously related to the servers' being down 
>> yesterday; the Lam-ml-Normalization failure could be due to that, too.
> I am experiencing Lam-ml-Normalization problems since a couple of weeks, 
> but this is only due to an update of my LaTeX installation on Mac OS X. 
> Otherwise the session seems to be fine, and should still work on the 
> usual Linux systems.

For the record: this is what Latex complains about on my Mac OS box.

*** ! LaTeX Error: You have run the document with pdflatex, but PSTricks
***                requires latex->dvips->ps2pdf or alternatively the use
***                of the package `auto-pst-pdf'. Then you can run
***                  `pdflatex -shell-escape <file>' (TeX Live)
***                or
***                  `pdflatex -enable-write18 <file>' (MikTeX).

This is AFP fb06f7fec099.


More information about the isabelle-dev mailing list