[isabelle-dev] Isabelle_11-Jan-2013

[Makarius]

On Tue, 15 Jan 2013, Jasmin Christian Blanchette wrote:

>> http://www4.in.tum.de/~wenzelm/test/Isabelle_11-Jan-2013/ is an early snapshot for the coming release.  It is mainly a test of Isabelle packaging technology (not web technology).  Components are taken from the Admin/components/ space within the repository.
>
> It's nice to have Aquamacs back for Proof General.

This is the only thing I changed.  Everything else is as before, i.e. the 
officially registered 
http://isabelle.in.tum.de/components/ProofGeneral-4.1.tar.gz that was also 
shipped with Isabelle2012.

Any updates need to materialize as a new component, with a new name.


> However, it greets me
>
> Unknown logic "HOL" -- no heap file found in:
>  /Users/blanchet/.isabelle/Isabelle_11-Jan-2013/heaps/polyml-5.5.0_x86-darwin
>  /Volumes/Isabelle_11-Jan-2013/Isabelle_11-Jan-2013.app/Contents/Resources/Isabelle_11-Jan-2013/heaps/polyml-5.5.0_x86-darwin
>
> Is this a bug or a feature? I understand jEdit now has this convenience built-in.

See again 
http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg03594.html

The "isabelle build_dialog" wrapper was done in a way to make it 
reasonably easy to include it in "isabelle emacs", for example. 
Otherwise, I could have made it internal to the Prover IDE.

I did not pursue this further, because I also have the impression that 
Proof General users like to do old-style tinkering.  The "installation" 
part of the website will somehow mention "isabelle build -s -b HOLCF" as 
example to do it independently of any front-end.


 	Makarius