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



Hi Everyone,
 
I am new to the list and I am struggling in order to make PG work with Isabelle/XEmacs (Emacs).
See the message I have sent to David Aspinall below.
 
Many thanks in advance!
--------------------------------------------------------------------------------------------------------------------------------------------
 
Hi, I'm sorry I can't help you with this as I don't use Cygwin.  It
sounds like an installation problem with Cygwin/Windows.  I suggest
asking on the Isabelle mailing list.  - D.

Alfio Ricardo de B Martini wrote:
> Dear PG Mantainer (David),
> 
> 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")'
> 
> and the file is treated as a normal text one. The same happens with
> emacs with
> the corresponding .emas file.
> 
> XEmacs: 21.4.21
> Emacs: 21.2.1
> 
> 
> 2) I have tried executing the proofgeneral script, after setting
> PGHOMEDEFAULT
> correctly, but when I run it, it gives the message:
> 
> line 109: locale: command not found
> 
> Then it launches emacs (not xemacs) and it loads succesfully PG. But
> when I load
> a file (like /ProofGeneral/isar/Example.thy) nothing hapens. It treats
> it like
> a normal text file and it gives again the message:
> 
> 'File mode specification error: (file-error: "Doing Fork" "Resources
> temporalily unavailable")'
> 
> 
> 3) When executing Isabelle -p xemacs (or emacs) it tries to load
> PG (ocassionally it succeeds with xemacs, the PG menu toolbar appears,
> etc), but it fails because
> I get again the following message (with both emcasen):
> 
> 'File mode specification error: (file-error: "Doing Fork" "Resources
> temporalily unavailable")'
> 
> 4) As an experiment, I reinstalled GNU emacs (22.1.1), and the very same
> reported problems
> persist.
> 
> 
> Thanks for any help!
> 
> PS: Although  I thought it was unecessary, also went through all those
> make commands,
> e.g., make->make compile-> etc..but the problems still remains.
> 
> PS2: Both polyml (5.2) and Isabelle2008 were installed succesfully.
> 

|Prof. Alfio Martini
|http://www.inf.pucrs.br/~alfio
|PUCRS - Pontificia Universidade Catolica do Rio Grande do Sul
|Faculty of Informatics -- Av. Ipiranga 6681
|Predio 32 -- 90619 - 900
|Porto Alegre - RS - Brasil
|Tel: +55 (051) 3320-8707
|Fax: +55 (051) 3320-3758 




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