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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
