A suggestion and some compliments...
Larry

Begin forwarded message:

> From: James Frank <s...@gmx.com>
> Subject: Needed ghostscript package to build PDF in Cygwin
> Date: 5 October 2011 15:54:30 GMT+01:00
> To: l...@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

_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to