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

Makarius makarius at sketis.net
Thu Sep 26 13:47:15 CEST 2013


On Thu, 26 Sep 2013, Lars Noschinski wrote:

> On 26.09.2013 10:01, 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'
>> ...
>
> This seems to happen when using GNU tar to unpack files created by the OS 
> X-version of tar and is not an error. This irritating warning can be avoided 
> by using GNU tar to build the tar files (obviously), or reportedly by playing 
> around with the --format option of tar.

Thanks for figuring this out.

I've had some surprises with Apple's tar before, which were partially 
addressed in 8f6046b7f850.  Since I don't see reasons to support a native 
"Apple look-and-feel" for Unix tools, I've now standardized to GNU tar in 
5ff12177a067 -- once and for all within the Isabelle process environment.

The updated tar.gz bundles are again on 
http://www4.in.tum.de/~wenzelm/test/Isabelle_25-Sep-2013/


Note that the Isabelle release is produced on Mac OS X for two reasons:

   * Tobias and Gerwin use special latex fonts that only work smoothly on
     MacTeX.

   * Apple demands Mac OS X to make a .dmg (via hdiutil).

Otherwise I would do the Admin/Release/build on some Linux box, since that 
reduces the potential for surprise.


 	Makarius



More information about the isabelle-dev mailing list