makarius at sketis.net
Tue Jan 15 21:29:03 CET 2013
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
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:
> Is this a bug or a feature? I understand jEdit now has this convenience built-in.
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.
More information about the isabelle-dev