Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Building fork releases


view this post on Zulip Email Gateway (May 21 2023 at 10:29):

From: Lex Bailey <cl-isabelle-users@lists.cam.ac.uk>
Hi,
I have a fork of isabelle, and I want to produce releases of it to
distribute to users across macos/ubuntu/windows. How do I generate packages
like the ones available on the isabelle website?

I have come across the program Admin/build_release, and I have tried using
it, but had no luck.
The first hurdle was that it depends on the mercurial history, but I forked
from a git mirror, so mercurial commands don't work. I tried using the -S
option instead which I think is supposed to bypass this by using an archive
file of the repo, and that looked like it was going to work until it
crashed with this error:

*** java.lang.OutOfMemoryError: Requested array size exceeds VM limit

If this error is unexpected then I'm happy to do some deeper debugging if
someone can provide a few pointers about how and where to start. (I don't
have much experience debugging java or scala.) Otherwise: what am I doing
wrong?

Thanks.
Lex.

view this post on Zulip Email Gateway (May 21 2023 at 20:44):

From: Makarius <makarius@sketis.net>
On 20/05/2023 16:19, Lex Bailey (via cl-isabelle-users Mailing List) wrote:

I have come across the program Admin/build_release, and I have tried using it,
but had no luck.

The first hurdle was that it depends on the mercurial history, but I forked
from a git mirror, so mercurial commands don't work.

All git "mirrors" of Isabelle consist mainly of broken glass. The Mercurial
history of Isabelle is very valuable to the project, and there is no proper
way to migrate it to git --- I've investigated that thoroughly a few years ago.

Better forget git for now. You do need "hg" to get it right.

If this error is unexpected then I'm happy to do some deeper debugging if
someone can provide a few pointers about how and where to start. (I don't have
much experience debugging java or scala.) Otherwise: what am I doing wrong?

What is already wrong here is the idea that making Isabelle fork releases is
easy, just because almost everything works most of the time for official releases.

For each release I spend a lot of time. And I had to learn many things in
approx. 20 years doing this. From that background I can only say: Please spare
the world bad Isabelle clones!

You did not even provide any proof why you think you need that. (I do know a
few people who make their own internal releases for their working group, but
that is hardly a proper public release.)

Makarius

view this post on Zulip Email Gateway (May 22 2023 at 18:19):

From: Makarius <makarius@sketis.net>
On 22/05/2023 00:02, Lex Bailey wrote:

Currently our install instructions include: install git to clone and build the
whole thing locally, or boot a prebuilt VM image.

As as user, I would find this very awkward.

I've seen bad things happen when users are asked to work with git, often for
the very first time: e.g. a bad default on Windows to convert LF to CRLF
everywhere. (How do you address Windows users anyway?)

We had to fork Isabelle to add one extra feature that we need.
As far as I'm aware, the changes we needed to make to Isabelle have already
been deemed unsuitable for upstream Isabelle.

Can you open this existential quantifier, and say explicitly what it is about?

Isabelle is a system where end-users can do almost everything, without having
to patch + fork.

Makarius

view this post on Zulip Email Gateway (May 23 2023 at 19:38):

From: Lex Bailey <cl-isabelle-users@lists.cam.ac.uk>
Hi,

See my responses inline below...
I hope these address your concerns.
I look forward to hearing your suggestions about how best to proceed.

Thanks.
Lex.

On Sun, 21 May 2023 at 21:43, Makarius <makarius@sketis.net> wrote:

On 20/05/2023 16:19, Lex Bailey (via cl-isabelle-users Mailing List) wrote:

I have come across the program Admin/build_release, and I have tried
using it,
but had no luck.

The first hurdle was that it depends on the mercurial history, but I
forked
from a git mirror, so mercurial commands don't work.

All git "mirrors" of Isabelle consist mainly of broken glass. The
Mercurial
history of Isabelle is very valuable to the project, and there is no
proper
way to migrate it to git --- I've investigated that thoroughly a few years
ago.

Better forget git for now. You do need "hg" to get it right.

As far as I can tell, the release process only uses hg to determine a
release name and to generate an archive of the tracked files. I can easily
map this onto git for our fork if I need to. Is there anything else that
specifically needs hg?
Furthermore, we have plenty of experience with git, but not so much with
mercurial. All our related projects also use git, and it simplifies our
workflow. We're not going to move away from git, and we don't expect
Isabelle to move away from mercurial.

If this error is unexpected then I'm happy to do some deeper debugging
if
someone can provide a few pointers about how and where to start. (I
don't have
much experience debugging java or scala.) Otherwise: what am I doing
wrong?

What is already wrong here is the idea that making Isabelle fork releases
is
easy, just because almost everything works most of the time for official
releases.

I never expected it to be easy.

For each release I spend a lot of time. And I had to learn many things in
approx. 20 years doing this. From that background I can only say: Please
spare
the world bad Isabelle clones!

I'm trying to make proper releases so that this fork is NOT a bad isabelle
clone. It makes minimal changes to isabelle (just enough to enable one
small extra feature)
Currently our install instructions include: install git to clone and build
the whole thing locally, or boot a prebuilt VM image.
In my mind, this kind of thing is what makes a "bad Isabelle clone". If we
were able to make proper releases using the existing process then we would
have a "good Isabelle clone".
I'm asking how to do this because I deliberately want to avoid our fork
being labeled as a bad fork.
This fork is going to be used by students, including students that are
totally new to Isabelle, so we want their first experience of installing
Isabelle to be an easy one.

You did not even provide any proof why you think you need that. (I do know
a
few people who make their own internal releases for their working group,
but
that is hardly a proper public release.)

I didn't know that I needed to justify making a fork release before asking
for help.
We had to fork Isabelle to add one extra feature that we need.
As far as I'm aware, the changes we needed to make to Isabelle have already
been deemed unsuitable for upstream Isabelle.

Makarius

view this post on Zulip Email Gateway (May 23 2023 at 19:38):

From: Lex Bailey <cl-isabelle-users@lists.cam.ac.uk>
I agree that we shouldn't expect users to install Git to be able to use
Isabelle or any fork of it.

The change that we have adds in an ML command
"Active.run_system_shell_command", which is then used by some ML code in a
theory file to provide clickable text in the output pane which lets the
user run the command in a console pane. Correct me if I'm wrong, but my
understanding is that this change was already rejected as it is "risky".
(it makes it easier for theory files to run arbitrary commands on a users
machine when they might not expect that to be possible)

If there is a way that we can achieve that without forking then that would
be ideal. If that is the case then how do we do that? and what is the best
way to package a vanilla Isabelle distribution with some custom heap images?

Full patch is here:
https://github.com/isabelle-utp/interaction-trees/blob/master/Isabelle2021-1-CyPhyAssure.diff
(there is also a patch for the 2022 release)

Thanks.


Last updated: Mar 29 2024 at 04:18 UTC