[isabelle-dev] Proof General 4.1 on Mac OS X

[Lucas Dixon]

I've had what I consider to be success with a very similar setup...

I'm using:
Isabelle (isa2011-test1: January 2011, which has Proof General Version 
4.1pre110112)
but with Aquamacs Distribution 2.1
on MacOS 10.6

I'm loading Aquamacs from the dock, so I don't get background noise.

Menus respond with usual swiftness and long arrows/unicode tokens etc 
look good.
Setup .emacs config:
(custom-set-variables
  '(isa-isabelle-command "/Applications/isa2011-test1.app/Isabelle 
/bin/isabelle"))
(load-file 
"/Applications/isa2011-test1.app/Isabelle/contrib/ProofGeneral/generic/proof-site.el")

Light blue background looks just right on my screen/default setup.

I wasn't able to reproduce the syntax-highlighting bug.

best,
lucas



On 23/01/2011 18:57, Clemens Ballarin wrote:
> I repeated my recent try of ProofGeneral on my Mac with
> ProofGeneral-4.1pre110118. If used with Aquamacs I observe these issues:
>
> - Menus respond slowly (> 1 second) when invoked for the first time.
> This is fine if Aquamacs is used without ProofGeneral.
> - Noise on the background shell.
> - Fontification fails in one situation. See attached image.
> - Long arrows are displayed as boxes (I probably don't have a suitable
> font for this.)
> - Light blue background of processed portion of the buffer is hard to see.
>
> Unicode symbols that are available are displayed in the right size. This
> is much better than with my previous setup with PG 3.7.1.1 and Carbonemacs.
>
> If the slow menus can be fixed this might be a suitable companion for
> Isabelle 2011.
>
> Clemens
>
> PS. I did use this configuration:
> - Aquamacs 2.1 distribution
> - ProofGeneral-4.1pre110118
> - MacOS X 10.5.8
>
>
> Quoting Makarius <makarius at sketis.net>:
>
>> On Fri, 21 Jan 2011, Mamoun FILALI-AMINE wrote:
>>
>>> a remark: previously, there was aquamacs instead of emacs? I find
>>> auqamacs more convenient than emacs.
>>
>> In recent Isabelle releases the default combination was Proof General
>> 3.7.1.1 with Aquamacs based on Emacs 22. That turned out as
>> half-decent, half-working -- after many weeks of desparate search in
>> the Mac OS X ecosphere.
>>
>> In Isabelle2011 the default Proof General is going to be 4.1, which
>> has quite different Emacs requirements, and generally quite different
>> behaviour concerning special symbols etc.
>>
>>
>> So far, I did not spend much time to try all possible combinations of
>> Emacsen with PG 4.1. According to ProofGeneral/COMPATIBILITY, plain
>> GNU Emacs 23.2 is recommended (aka the "no nonsense version").
>> Aquamacs 2.1 is also based on that code base, so it could in principle
>> work as well, despite fancy additions.
>>
>> When I've tried the slightly older Aquamacs 2.0 some months ago, it
>> turned out much slower than plain GNU Emacs 23 -- see also
>> http://proofgeneral.inf.ed.ac.uk/trac/ticket/324 -- but that might be
>> obsolete in several respects.
>>
>>
>> I hope to get more concrete feedback from Mac users. So far I've
>> mainly found out that most people are stuck with very old versions of
>> Proof General, sometimes even in combination with ancient XEmacs.
>>
>>
>> Makarius
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>
>>
>
>
>
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.