Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle2016-RC0 available for testing


view this post on Zulip Email Gateway (Aug 22 2022 at 12:07):

From: Makarius <makarius@sketis.net>
Dear Isabelle users,

the coming Isabelle2016 release is scheduled for February 2016, after the
next big Java 8 update by Oracle in January and some weeks before the
deadline of ITP 2016.

To get started with systematic testing there is now the relatively early
http://isabelle.in.tum.de/website-Isabelle2016-RC0 (corresponding to
Isabelle/e18444532fce and AFP/c62777f3e932).

The website, NEWS, ANNOUNCE etc. are already mostly up-to-date. Some
documentation is still lagging behind, notably the Isabelle/jEdit manual.
There are further fine points still to be sorted out.

When discussing problems, observations, suggustions, etc. the mail subject
line should be changed to something meaningful (but the release candidate
number still given in the message body).

As usual it is important to keep general laws of causality in mind:
release candidates may still change, but the final release is final.
Although this is tautological, in the past few releases we've often had
complaints right after final lift-off, when it was too late.

So the best time to start testing is now.

Makarius

view this post on Zulip Email Gateway (Aug 22 2022 at 12:25):

From: Lars Hupel <hupel@in.tum.de>
Dear Makarius,

I have two questions about the release candidate:

1) Why has the Linux tarball been renamed from "linux" to "app"? I now
need a switch in libisabelle to find the correct file to download.

2) Could you please provide the Windows and OS X tarballs
(Isabelle2016_windows.tar.gz and Isabelle2016_macos.tar.gz). These are
required for libisabelle.

Cheers
Lars

view this post on Zulip Email Gateway (Aug 22 2022 at 12:26):

From: Makarius <makarius@sketis.net>
On Fri, 1 Jan 2016, Lars Hupel wrote:

1) Why has the Linux tarball been renamed from "linux" to "app"? I now
need a switch in libisabelle to find the correct file to download.

Formally, it is the following change:

changeset: 61002:8c52177fb436
user: wenzelm
date: Fri Aug 21 20:58:23 2015 +0200
files: Admin/Release/build Admin/lib/Tools/makedist_bundle
description:
clarified linux application bundle;

Informally it was just normal garbage collection: historically there were
only odd tar.gz archives, later they emerged into proper application
bundles, and from that perspectives the tar.gz could be seen as obsolete.

2) Could you please provide the Windows and OS X tarballs
(Isabelle2016_windows.tar.gz and Isabelle2016_macos.tar.gz). These
are required for libisabelle.

See this later change after Isabelle2016-RC0:

changeset: 62032:620d3f63ead1
tag: tip
user: wenzelm
date: Fri Jan 01 19:52:00 2016 +0100
files: Admin/lib/Tools/makedist_bundle
description:
keep generic archive for all platforms -- required for Admin/Release/build_library;

I was also thinking of libisabelle, but not sure about its precise
requirements. The general principle behind this to provide "headless"
distribution bundles, not just "apps". So we shall keep that until there
is yet another better idea.

Makarius

view this post on Zulip Email Gateway (Aug 22 2022 at 12:27):

From: Lars Hupel <hupel@in.tum.de>

Informally it was just normal garbage collection: historically there
were only odd tar.gz archives, later they emerged into proper
application bundles, and from that perspectives the tar.gz could be seen
as obsolete.

But if I'm reading this changeset right, it's still a tarball. I don't
have a strong opinion here, but I think there should be at least some
platform "identifier" in the file name (e.g. ".exe", ".dmg",
"_linux.tar.gz").

See this later change after Isabelle2016-RC0:

changeset: 62032:620d3f63ead1
tag: tip
user: wenzelm
date: Fri Jan 01 19:52:00 2016 +0100
files: Admin/lib/Tools/makedist_bundle
description:
keep generic archive for all platforms -- required for
Admin/Release/build_library;

Thanks, that's very helpful. To clarify: With RC1, the usual tarballs
will be back?

I was also thinking of libisabelle, but not sure about its precise
requirements. The general principle behind this to provide "headless"
distribution bundles, not just "apps". So we shall keep that until
there is yet another better idea.

libisabelle is only able to unpack tarballs (not via a Unix-style "tar"
shell invocation, but via some pure JVM code). It is able to re-use an
existing Isabelle installation, too, but automatic download & unpacking
is very useful for non-Isabelle users, e.g. when Leon users want to try
out the Isabelle backend without knowing anything about Isabelle. The
existing code in libisabelle supports that for Isabelle2014 and 2015
under Windows, Mac OS X and Linux.

Cheers
Lars

view this post on Zulip Email Gateway (Aug 22 2022 at 12:29):

From: Makarius <makarius@sketis.net>
On Fri, 1 Jan 2016, Lars Hupel wrote:

Informally it was just normal garbage collection: historically there
were only odd tar.gz archives, later they emerged into proper
application bundles, and from that perspectives the tar.gz could be
seen as obsolete.

But if I'm reading this changeset right, it's still a tarball. I don't
have a strong opinion here, but I think there should be at least some
platform "identifier" in the file name (e.g. ".exe", ".dmg",
"_linux.tar.gz").

With RC1, the usual tarballs will be back?

The tar balls are already back right now:
http://isabelle.in.tum.de/website-Isabelle2016-RC0/dist

This is a manual retrofitting of Isabelle/e1a4d52d3d53 release procedure
on Isabelle2016-RC0.

libisabelle is only able to unpack tarballs (not via a Unix-style "tar"
shell invocation, but via some pure JVM code).

This is a potential source of problems on Windows, also depending on
details of the Java platform. Isabelle2016-RC0 already contains an
updated Cygwin, with its magic init now in isabelle.Isabelle_System.init,
instead of former isabelle.Main (the application entry).

So there is a new chance to make it all work on Windows. Note that there
is now "windows" and "windows64".

BTW, this is now a specific discussion under the subject "Isabelle2016-RC0
available for testing". Last time we've had hundreds of mails like that,
and it got difficult to follow topics.

Makarius

view this post on Zulip Email Gateway (Aug 22 2022 at 12:31):

From: Lars Hupel <hupel@in.tum.de>

The tar balls are already back right now:
http://isabelle.in.tum.de/website-Isabelle2016-RC0/dist

Thanks for that. I can preliminary confirm that libisabelle still works
with RC0 under Linux (with minor changes in theory sources).

Cheers
Lars


Last updated: Apr 25 2024 at 20:15 UTC