[isabelle-dev] PG 3.x vs. 4.x settings

[Makarius]

> On 14 Dec 2012, at 14:02, Makarius <makarius at sketis.net> wrote:
>
>> So we merely need to figure out where the .elc stuff is going: Is it in 
>> the component and deleted for other platforms?  Is it not in the 
>> component, but created by the administrative script that produces the 
>> Isabelle.app for Mac OS X?

On Sat, 15 Dec 2012, Lawrence Paulson wrote:

> Surely those files belong in the Isabelle app?

Yes, but somehow the files need to be put there, using a well-defined 
reproducible process.


Thinking about it again, the easiest way is probably to make a 4.2 version 
of http://isabelle.in.tum.de/components/ProofGeneral-4.1.tar.gz *without* 
the .elc files as usual.  This will then work on most Emacsen, especially 
the many possibilities on Linux.  (We can forget about Windows/Cygwin 
here, because that never quite worked in the past anyway.)

The .elc make process is then part of the makebundle script that does some 
post-hoc patching for the different platform families.  See also 
http://isabelle.in.tum.de/repos/isabelle/file/765c22baa1c9/Admin/Release/makebundle

It is my job to keep makebundle in shape.  It is your job as ProofGeneral 
component maintainers to produce a component.  See again 
http://isabelle.in.tum.de/repos/isabelle/file/765c22baa1c9/Admin/components/README
-- and tell me if I've forgotten anything important in that description.

See also the Admin/ProofGeneral/ space within the Isabelle repository -- 
little has happened there in the past few years.


Note that component names cannot be recycled, so if you care about literal 
"ProofGeneral-4.1.tar.gz" instead of "ProofGeneral-4.1-X.tar.gz" for X = 
1, 2, 3, ... you should experiment first (and show me the result), before 
registering the component officially.


A still pending question is how the implicit build_dialog should be 
integrated with Proof General.  The plan is to omit logic images from the 
release bundles, and make it easy for users to get them on the spot 
without thinking (but 2-3 extra minutes waiting).


 	Makarius