On 14 Dec 2012, at 14:02, Makarius <[email protected]> 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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
