Re: [isabelle] Help with PG/Isabelle/XEmacs (Emacs) in cygwin



On Thu, 8 Jan 2009, Alfio Ricardo de B Martini wrote:

> > I am having a problem to install Proof General for XEmacs (Emacs). I
> > have tried my best, but
> > some problems still happen:
> > 
> > 1) I have a added the following line to my .xemacs/init.el file
> >  (load-file "/home/ProofGeneral/generic/proof-site.el"). Then,
> > when  I load for instance, /ProofGeneal/isar/Example.thy,
> > it tries to load PG (there is even a wellcome PG file) but
> > soon after I get the message:
> > 
> > 'File mode specification error: (file-error: "Doing Fork" "Resources
> > temporalily unavailable")'

In all these variations, the "Resources temporalily unavailable" error 
seems to be the common problem.  It looks like you have too little memory, 
or Cygwin thinks it has too little memory.


Trying it myself, I now realize that after the latest updates of Cygwin/X 
the whole X11 setup has changed, and you only get xemacs without X by 
default, which will make the important xsymbol feature fail.

This is how it worked for me at the moment:

  * Ensure that packages "xinit" and "xterm" of Cygwin are installed.

  * Run the X session like this on a regular Cygwin shell:

    startx /usr/bin/xterm -- -multiwindow

  * Now within the xterm, run Isabelle Proof General like this:

    isabelle-interface -p xemacs -x true

Please excuse the ugly look-and-feel of XEmacs, we are trying hard to get 
rid of it in the near future.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.