On Thu, 26 Sep 2013, Peter Lammich wrote:
And the unpacked folder does not contain all necessary files
The bundled heap images were already discontinued in Isabelle2013 -- this
became possible due to isabelle build and getting rid of non-portable Unix
"make". Consequently, users have a few minutes longer wait time on the
first start, but it usually works reliably. Before Isabelle2013, Linux
users usually got x86 vs. x86_64 wrong in the first and second attempt and
had to download the platform heaps again, or just gave up silently.
on startup, isabelle tells me:
Unknown logic "HOL" -- no heap file found in:
/home/lammich/.isabelle/Isabelle_25-Sep-2013/heaps/polyml-5.5.1_x86-linux
/home/lammich/opt/Isabelle_25-Sep-2013/heaps/polyml-5.5.1_x86-linux
Some further notes on startup of "Isabelle".
The official release bundles have a toplevel "app" entry point. On Linux
this is just a shell script: Isabelle_25-Sep-2013/Isabelle_25-Sep-2013.
Running that should work out of the box, although some Linux distributions
now open a plain text editor when clicking on an executable script
(notably regular Ubuntu -- argh).
That way the required logic image is built, and the default Isabelle user
interface is started: Isabelle/jEdit.
In the past times of Proof General, I had tried hard over some years to
get to that point, but it never worked out since Emacs cannot be bundled.
(Emacs users never agree on the best Emacs version anyway.)
There may a few remaining snags in the current Isabelle "apps" on all
platforms, but I am trying to get on. People who are used to "latest
repository snapshots" should try to get a feeling how premium users will
experience Isabelle -- without command-line by default.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
