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

Peter Lammich lammich at in.tum.de
Thu Sep 26 10:11:02 CEST 2013


Correction: The file unpacks correctly, the messages seem to be only
warnings. 

I forgot to build the logic, immediately starting "isabelle emacs".

Peter

On Do, 2013-09-26 at 10:01 +0200, Peter Lammich wrote:
> I cannot unpack the tar-file. My Linux (Ubuntu 12.04.2 LTS) gives me a
> bunch of error messages:
> 
> tar: Ignoring unknown extended header keyword `SCHILY.ino'
> tar: Ignoring unknown extended header keyword `SCHILY.nlink'
> tar: Ignoring unknown extended header keyword `SCHILY.dev'
> ...
> 
> And the unpacked folder does not contain all necessary files, 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
> 
> 
> Best,
>   Peter
> 
> 
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev





More information about the isabelle-dev mailing list