Stream: Archive Mirror: Isabelle Users Mailing List

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


view this post on Zulip Email Gateway (Aug 18 2022 at 12:49):

From: Alfio Ricardo de B Martini <alfio.martini@pucrs.br>
Dear Makarius,

Thanks a lot! It is working perfectly fine now!

All the best!

|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

view this post on Zulip Email Gateway (Aug 18 2022 at 12:56):

From: Alfio Ricardo de B Martini <alfio.martini@pucrs.br>
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:
|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

view this post on Zulip Email Gateway (Aug 18 2022 at 12:58):

From: Makarius <makarius@sketis.net>
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


Last updated: May 03 2024 at 04:19 UTC