[isabelle-dev] Isabelle_25-Sep-2013 integration test

[Makarius]

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