[isabelle-dev] Fwd: Needed ghostscript package to build PDF in Cygwin

[Lawrence Paulson]

A suggestion and some compliments...
Larry

Begin forwarded message:

> From: James Frank <sets at gmx.com>
> Subject: Needed ghostscript package to build PDF in Cygwin
> Date: 5 October 2011 15:54:30 GMT+01:00
> To: lp15 at cam.ac.uk
> 
> Dear Dr. Paulson,
> 
> The problem I had with building the Isabelle PDF documents under Cygwin is actually an excuse to thank you for producing Isabelle.
> 
> You might consider adding ghostscript as a Cygwin package requirement on:
> http://www.cl.cam.ac.uk/research/hvg/Isabelle/download.html
> 
> I built the HOL, ZF, and IsarMathLib document.pdf files several times, but then it started complaining about not piping to ghostscript, although it would build the FOL document.pdf. I installed the Cygwin ghostscript package, and then it started working again.
> 
> I was tempted to go with Coq, since I wasn't set up with a Unix environment, but now, the more I learn about Isabelle, the happier I get about it.
> 
> With the choice between HOL and ZF, and the combination of all the tools, Isabelle is incredible. I run jEdit under Cygwin to get the benefits of the tree view and continuous proving, and I run Proof General under Ubuntu in VirtualBox to get the extra information it gives me, along with the ATPs running better under Linux.
> 
> I could go on. The integration with Latex is super cool. I live and die by tree views, particularly in IDE's and using the bookmarks of a PDF. With the Isabelle sectioning commands, along with jEdit sidekick, and the ability to create PDFs using LaTeX, it's all good. Documentation is a huge part of being able to use a software tool.
> 
> Thanks again. Proof assistants open a whole new dimension in regards to finding opportunity in math.
> 
> -- James Frank