Email Gateway (Aug 22 2022 at 19:46): Email Gateway (Aug 22 2022 at 19:46):From: Lars Hupel <hupel@in.tum.de>
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).
Email Gateway (Aug 22 2022 at 19:47):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 22 2022 at 19:47):From: Lars Hupel <hupel@in.tum.de>
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.
Do we have a space problem on the servers?
In Isabelle2019-RC1 the situation of app bundles is as follows,
together
with subsequent tool invocations to get the directory content in batch
mode.
Just like you I'm trying to stay within Scala as much as possible,
without having to resort to command-line tools, whose presence I cannot
assume. I currently only have to care about Gzip. Newer Apache Commons
Compress versions may also support Xz and that odd Windows EXE format,
but I haven't tried that out yet.
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.
isabellectl takes care of that. So far it worked with very little
problems on Windows, using a uniform extraction mechanism from the
tarball.
Email Gateway (Aug 22 2022 at 19:48):From: Lars Hupel <hupel@in.tum.de>
I've just spoken to a contributor of Commons Compress who told me that
streaming unpacking for 7z is impossible. This is very inconvenient.
Email Gateway (Aug 22 2022 at 19:48):From: Makarius <makarius@sketis.net>
On 07/05/2019 09:37, Makarius wrote:
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.
Linux and macOS are now both back to gz, since xz is too slow and
cumbersome, see https://isabelle.in.tum.de/repos/isabelle/rev/7c55ea37fbf7
* windows:
https://isabelle.in.tum.de/website-Isabelle2019-RC1/dist/Isabelle2019-RC1.exe7z x Isabelle2019-RC1.exe
This still works: you could bundle 7z.exe to make it self-contained.
An alternative is to use the self-extractor with option -ai (and
probably -gm2) as explained in
https://github.com/chrislake/7zsfxmm/wiki/Switches
This requires an updated version of Isabelle.exe according to
https://isabelle.in.tum.de/repos/isabelle/rev/4ce07be8ba17 -- in approx.
2h there should be a new version at
https://isabelle.sketis.net/devel/release_snapshot
One remaining question is how to do it robustly in a headless
environment. With the Cygwin ssh server on Windows, I managed like this:
run -wait ./Isabelle_09-May-2019.exe -ai -gm2
Without that, the Java splash screen could cause problems, but I don't
know how to disable that without creating an alternative executable --
which is definitely beyond the present ambition on such rare
applications of batch-mode installation.
Makarius
Email Gateway (Aug 22 2022 at 19:48):From: Lars Hupel <hupel@in.tum.de>
To quote your latest CICM paper:
The “download–unpack–run” experience of Isabelle/PIDE needs fine-tuning
for first-time users. In particular, AFP needs to be included in this,
to avoid manual intervention with session ROOTS and ROOT files.
isabellectl has been providing just that experience for many years now.
The big advantage is that isabellectl is decidedly not part of the
Isabelle, which means it can bootstrap various Isabelle distributions
(up to 2018, after which you changed the packaging format) assuming any
JRE installation.
Email Gateway (Aug 22 2022 at 19:48):From: Lars Hupel <hupel@in.tum.de>
None of these problems existed with the tarball. I reckon I'll just drop
support for auto installation on Windows; these workarounds are just too
cumbersome.
Email Gateway (Aug 22 2022 at 19:48):From: Makarius <makarius@sketis.net>
This is all a bit alien to Isabelle system integration, and probably the
reason why I don't understand it.
Makarius
Email Gateway (Aug 22 2022 at 19:49):From: Dominique Unruh <unruh@ut.ee>
Hi,
as a user of Lars' libisabelle, I would like to chime in here and "vote"
for reincluding the tarballs on the webpage.
Tar seems to be the only widespread format that can be downloaded and
unpacked without temporary storage which might be useful also for other
applications which try to automatically install Isabelle.
My suggestion be to simply include both the tarballs and the other
compressed formats on the webserver. Unless the webserver has a very
small storage allowance, that should make very little difference to the
server.
That way it should work for everyone.
Best wishes,
Dominique.
Email Gateway (Aug 22 2022 at 19:49):From: Makarius <makarius@sketis.net>
Except for Windows, where self-extracting archives are standard.
I have already explained that this is also a matter of minimality: there
were historic reasons to have redundant tars lying around, and these no
longer exist. I am not going to maintain legacy features.
The concept of isabellectl by Lars appears to be to level-out
differences over various Isabelle distributions: he merely needs to
follow these natural changes.
As for the official Isabelle distribution and release policy: there is
only one latest version, and everything else is historic. (It may still
be discussed informally in this mailing list, but there is no official
support for it.)
This is vital to keep Isabelle going with a fraction of the normal
resource requirements for such a huge project. It is in the best
interest of Isabelle users to stay faithful to the principles behind
Isabelle.
Makarius
Last updated: Apr 24 2024 at 12:33 UTC