Re: [isabelle] Isabelle2019-RC1 release file names



On 04/05/2019 15:00, Lars Hupel wrote:
>> A fairly stable Isabelle2019-RC1 is now available from
>> https://isabelle.in.tum.de/website-Isabelle2019-RC1 -- it corresponds to
>> AFP/d50417d0ae64 (e.g. see
>> https://isabelle.sketis.net/repos/afp-devel/rev/d50417d0ae64).
> 
> Why did all the file names of the tarballs change? This breaks automatic
> download and extraction of isabellectl. I'm assuming the following files
> exist:
> 
> Isabelle<identifier>_linux.tar.gz
> Isabelle<identifier>_macos.tar.gz
> Isabelle<identifier>_windows.tar.gz
> 
> In RC0 they were still present (like for 2016–2018).

The former tar.gz files used to be an internal "interface" between
various old shell scripts to create the regular application bundles for
end-users. They were publicly available for some time, to make it
possible to access the content by other tools; this now works
differently as shown below.

For Isabelle2019, build_release now happens in Isabelle/Scala without
odd shell scripts and intermediate archives. The app bundles have become
much larger (due to Java 11 and bundled HOL image), so I wanted to avoid
redundant copies of material. I have also started to experiment with xz
instead of gz: infortunately, macOS seems to lack xz by default; in
further testing we might see reasons to switch linux back to gz, too.


In Isabelle2019-RC1 the situation of app bundles is as follows, together
with subsequent tool invocations to get the directory content in batch mode.

  * linux:
https://isabelle.in.tum.de/website-Isabelle2019-RC1/dist/Isabelle2019-RC1_linux.tar.xz

    tar -xJf Isabelle2019-RC1_linux.tar.xz

  * macos:
https://isabelle.in.tum.de/website-Isabelle2019-RC1/dist/Isabelle2019-RC1_macos.tar.gz

    tar -xzf Isabelle2019-RC1_macos.tar.gz

  * windows:
https://isabelle.in.tum.de/website-Isabelle2019-RC1/dist/Isabelle2019-RC1.exe

    7z x Isabelle2019-RC1.exe

Recall that on Windows, the first invocation of Isabelle_System.init()
will update file permissions and symlinks via Cygwin.init(). For a
read-only installation, this needs to be done once after unpacking.


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.