[isabelle] Isabelle2025-RC0 available for early experimen... · Mirror: Isabelle Users Mailing List

Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle2025-RC0 available for early experimen...

Email Gateway (Jan 07 2025 at 19:11):

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

the Isabelle2025 release process is about to start soon, see
https://isabelle-dev.sketis.net/phame/post/view/85/release_candidates_for_isabelle2025
for ongoing documentation of its stages.

To warm up, we now have Isabelle2025-RC0 for early experimentation:
https://isabelle.in.tum.de/website-Isabelle2025-RC0

It is important to use the current window of opportunity until 15-Mar-2025 for
testing, and reporting of observations and problems. Quite often, people think
that release quality is achieved by doing nothing and merely waiting for the
final date. For Isabelle releases, "final" means eternal and unchangeable:
remaining problems will not be addressed until a later release (every 8-10
months).

Makarius

Email Gateway (Jan 07 2025 at 20:13):

From: Frédéric Boulanger <frederic.boulanger@centralesupelec.fr>
Dear Makarius,

I cannot launch this version of Isabelle, I constantly get a dialog about the possibility of malware in the bundle (I tried double-clicking the application icon, choosing "Open" from the contextual menu, and launching the Isabelle2025-RC0 binary in a terminal).

I tried to sign the application using "sudo codesign --force --deep --sign - /Applications/Isabelle2025-RC0.app", but I got the following message "/Applications/Isabelle2025-RC0.app: unsealed contents present in the bundle root".

I tried to remove the quarantine attribute using "sudo find Isabelle2025-RC0.app -type f -exec xattr -c {} \;", but this did not change anything.

It seems that the structure of the Isabelle2025-RC0.app bundle does no longer respect what MacOS expects.

This happened on a Macbook Pro with an M3 Max chip under Sequoia 15.2 (last known version of MacOS at this time).

I also checked on an old Intel MacbookPro (2.9Ghz Intel Core i9 from 2018) under the same OS (Sequoia 15.2), and everything worked fine after the "Verifying..." progress bar disappeared.

So there may be an issue that is specific to the ARM version of Isabelle here.

Best regards,

Frédéric

Frédéric Boulanger
CentraleSupélec - Département Informatique Laboratoire Méthodes Formelles (LMF)
3 rue Joliot-Curie, 91192 Gif-sur-Yvette cedex Bât. 650 - 1 rue Raimond Castaing, 91190 Gif-sur-Yvette
+33 [0]1 75 31 78 32‬

Le 7 janv. 2025 à 20:10, Makarius <makarius@sketis.net> a écrit :

Dear Isabelle users,

the Isabelle2025 release process is about to start soon, see https://isabelle-dev.sketis.net/phame/post/view/85/release_candidates_for_isabelle2025 for ongoing documentation of its stages.

To warm up, we now have Isabelle2025-RC0 for early experimentation: https://isabelle.in.tum.de/website-Isabelle2025-RC0

It is important to use the current window of opportunity until 15-Mar-2025 for testing, and reporting of observations and problems. Quite often, people think that release quality is achieved by doing nothing and merely waiting for the final date. For Isabelle releases, "final" means eternal and unchangeable: remaining problems will not be addressed until a later release (every 8-10 months).

Makarius

Email Gateway (Jan 07 2025 at 22:06):

From: Makarius <makarius@sketis.net>
On 07/01/2025 21:06, Frédéric Boulanger wrote:

I cannot launch this version of Isabelle, I constantly get a dialog about the
possibility of malware in the bundle (I tried double-clicking the application
icon, choosing "Open" from the contextual menu, and launching the
Isabelle2025-RC0 binary in a terminal).

So there may be an issue that is specific to the ARM version of Isabelle here.

Do you have Rosetta 2 already installed on the ARM machine? Normally the
system should ask for that, but who knows for sure ...

Makarius

Email Gateway (Jan 08 2025 at 09:14):

From: Frédéric Boulanger <frederic.boulanger@centralesupelec.fr>
Isabelle2024 works fine on the same machine, so I guess Rosetta 2 is installed and working.

Frédéric

Le 7 janv. 2025 à 22:59, Makarius <makarius@sketis.net> a écrit :

On 07/01/2025 21:06, Frédéric Boulanger wrote:

I cannot launch this version of Isabelle, I constantly get a dialog about the possibility of malware in the bundle (I tried double-clicking the application icon, choosing "Open" from the contextual menu, and launching the Isabelle2025-RC0 binary in a terminal).

So there may be an issue that is specific to the ARM version of Isabelle here.

Do you have Rosetta 2 already installed on the ARM machine? Normally the system should ask for that, but who knows for sure ...

Makarius

Email Gateway (Jan 08 2025 at 11:15):

From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
When I start Isabelle2025-RC0 by, e.g.:

/opt/Isabelle2025-RC0/bin/isabelle jedit&

the initial window takes over the entire screen area. I consider this behavior
to be intrusive and Isabelle2024 does not do this. Even if I "restore down"
using the window manager controls at the upper right of the title bar,
exit the program, and restart, it still does the same thing. I scanned all the
options I could find and I don't see anything that would enable me to change this.

System: Linux Mint 22 (Xorg).

On 1/7/25 14:10, Makarius wrote:

Dear Isabelle users,

the Isabelle2025 release process is about to start soon, see https://isabelle-dev.sketis.net/phame/post/view/85/
release_candidates_for_isabelle2025 for ongoing documentation of its stages.

To warm up, we now have Isabelle2025-RC0 for early experimentation: https://isabelle.in.tum.de/website-Isabelle2025-RC0

It is important to use the current window of opportunity until 15-Mar-2025 for testing, and reporting of observations
and problems. Quite often, people think that release quality is achieved by doing nothing and merely waiting for the
final date. For Isabelle releases, "final" means eternal and unchangeable: remaining problems will not be addressed
until a later release (every 8-10 months).

Makarius

Email Gateway (Jan 08 2025 at 11:19):

From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
Correction to my previous message (sorry):

The behavior observed is when running Isabelle on Ubuntu 22.04 under Xorg,
displayed remotely using Reminna -> xrdp on a system running Linux Mint 22,
also with Xorg. I have not tried it without the xrdp, but the behavior of
Isabelle2024 and Isabelle2025-RC0 is different even under this configuration.

On 1/8/25 06:14, Eugene W. Stark wrote:

When I start Isabelle2025-RC0 by, e.g.:

/opt/Isabelle2025-RC0/bin/isabelle jedit&

the initial window takes over the entire screen area. I consider this behavior
to be intrusive and Isabelle2024 does not do this. Even if I "restore down"
using the window manager controls at the upper right of the title bar,
exit the program, and restart, it still does the same thing. I scanned all the
options I could find and I don't see anything that would enable me to change this.

System: Linux Mint 22 (Xorg).

On 1/7/25 14:10, Makarius wrote:

Dear Isabelle users,

the Isabelle2025 release process is about to start soon, see https://isabelle-dev.sketis.net/phame/post/view/85/
release_candidates_for_isabelle2025 for ongoing documentation of its stages.

To warm up, we now have Isabelle2025-RC0 for early experimentation: https://isabelle.in.tum.de/website-Isabelle2025-RC0

It is important to use the current window of opportunity until 15-Mar-2025 for testing, and reporting of observations
and problems. Quite often, people think that release quality is achieved by doing nothing and merely waiting for the
final date. For Isabelle releases, "final" means eternal and unchangeable: remaining problems will not be addressed
until a later release (every 8-10 months).

Makarius

Email Gateway (Jan 08 2025 at 11:29):

From: Lawrence Paulson <lp15@cam.ac.uk>
I was able to open it on an M3 MacBook Pro by going to the privacy & security tab of settings and going to the bottom (under security). There it actually said “application Isabelle2025-RC0 blocked from opening“, with a button labelled “open anyway“.

It then opened, and I tested that it would open without complications a second time. This on a locked-down corporate machine, so it should work for you.

Larry

Begin forwarded message:

From: Frédéric Boulanger <frederic.boulanger@centralesupelec.fr>Subject: Re: [isabelle] Isabelle2025-RC0 available for early experimentationDate: 7 January 2025 at 20:06:55 GMTTo: Makarius <makarius@sketis.net>Cc: cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Dear Makarius,

I tried to remove the quarantine attribute using "sudo find Isabelle2025-RC0.app -type f -exec xattr -c {} \;", but this did not change anything.

It seems that the structure of the Isabelle2025-RC0.app bundle does no longer respect what MacOS expects.

This happened on a Macbook Pro with an M3 Max chip under Sequoia 15.2 (last known version of MacOS at this time).

I also checked on an old Intel MacbookPro (2.9Ghz Intel Core i9 from 2018) under the same OS (Sequoia 15.2), and everything worked fine after the "Verifying..." progress bar disappeared.

So there may be an issue that is specific to the ARM version of Isabelle here.

Best regards,

Frédéric

Email Gateway (Jan 08 2025 at 12:00):

From: Lawrence Paulson <lp15@cam.ac.uk>
I note that the theory Divides is being deprecated in favour of Euclidean_Rings and that there are three separate news items seemingly relating to aspects of this change. Could they be consolidated?

Larry Paulson

On 7 Jan 2025 at 19:10 +0000, Makarius <makarius@sketis.net>, wrote:
Dear Isabelle users,

the Isabelle2025 release process is about to start soon, see

Email Gateway (Jan 08 2025 at 19:55):

From: Frédéric Boulanger <frederic.boulanger@centralesupelec.fr>
Thanks for this tip!
I works fine, but it is a pity to see Apple giving notifications that are hidden in a preference panel.
The behavior in previous versions of MacOS was already strange because you had to try to open the app twice before getting the "Open anyway" button...

Back in the 1990s, Apple wrote a book called "Macintosh Human Interface Guidelines <https://dl.acm.org/doi/pdf/10.5555/573097>", and on page 9, it says:

Feedback and Dialog

Keep users informed about what’s happening with your product. Provide
feedback as they do tasks and make that feedback as immediate as possible.
When a user initiates an action, provide some indicator, visual or auditory
(or both), that your application has received the user’s input and is operating
on it. Provide as much information as possible about how long operations
take. When your application can’t respond to user input because it’s
processing a different task, inform the user of what to expect and describe any
delays, why they occur, and how long they’ll take. Also, tell the user how to
get out of the current situation whenever possible.
Provide direct, simple feedback that people can understand. Most people
would not know what to do if they saw this message “The computer
unexpectedly crashed. ID = 13.” It would be very helpful if the message
spelled out exactly which situation caused the error—for example, not
enough memory was available for the computer to complete the task—so that
the user could understand how to avoid the situation in the future.

It seems they forgot about all this.

Frédéric

Le 8 janv. 2025 à 12:28, Lawrence Paulson <lp15@cam.ac.uk> a écrit :

I was able to open it on an M3 MacBook Pro by going to the privacy & security tab of settings and going to the bottom (under security). There it actually said “application Isabelle2025-RC0 blocked from opening“, with a button labelled “open anyway“.

It then opened, and I tested that it would open without complications a second time. This on a locked-down corporate machine, so it should work for you.

Larry

Begin forwarded message:

From: Frédéric Boulanger <frederic.boulanger@centralesupelec.fr>Subject: Re: [isabelle] Isabelle2025-RC0 available for early experimentationDate: 7 January 2025 at 20:06:55 GMTTo: Makarius <makarius@sketis.net>Cc: cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Dear Makarius,

I cannot launch this version of Isabelle, I constantly get a dialog about the possibility of malware in the bundle (I tried double-clicking the application icon, choosing "Open" from the contextual menu, and launching the Isabelle2025-RC0 binary in a terminal).

I tried to sign the application using "sudo codesign --force --deep --sign - /Applications/Isabelle2025-RC0.app", but I got the following message "/Applications/Isabelle2025-RC0.app: unsealed contents present in the bundle root".

I tried to remove the quarantine attribute using "sudo find Isabelle2025-RC0.app -type f -exec xattr -c {} \;", but this did not change anything.

It seems that the structure of the Isabelle2025-RC0.app bundle does no longer respect what MacOS expects.

This happened on a Macbook Pro with an M3 Max chip under Sequoia 15.2 (last known version of MacOS at this time).

I also checked on an old Intel MacbookPro (2.9Ghz Intel Core i9 from 2018) under the same OS (Sequoia 15.2), and everything worked fine after the "Verifying..." progress bar disappeared.

So there may be an issue that is specific to the ARM version of Isabelle here.

Best regards,

Frédéric

Email Gateway (Jan 08 2025 at 22:08):

From: Makarius <makarius@sketis.net>
On 08/01/2025 19:25, Frédéric Boulanger wrote:

I works fine, but it is a pity to see Apple giving notifications that are
hidden in a preference panel.

We've had that for some years already, starting with Isabelle2020, or so. The
Isabelle "Installation" webpage has some brief text with a screenshot for
that, see https://isabelle.in.tum.de/img/macos_security.png

I used to have very liberal security settings on my macOS test machines for
convenience, but now keep the strict defaults for testing Isabelle downloads.
With current macOS 15 Sequoia --- a fresh install, not an update --- I have to
make many clicks in many dialogs to run the application eventually, but it
usually works.

This challenge actually conforms to the model of "Hooked" by Nir Eyal
https://www.nirandfar.com/hooked to "turn users into fanatic followers". I am
unsure if that is actually a good idea ...

Back in the 1990s, Apple wrote a book called "Macintosh Human Interface
Guidelines <https://dl.acm.org/doi/pdf/10.5555/573097>", and on page 9, it says:

It seems they forgot about all this.

I get the impression that they do this on purpose, to make it difficult or
impossible to run "unofficial" apps.

Makarius

Email Gateway (Jan 09 2025 at 09:12):

From: Florian Haftmann <florian.haftmann@cit.tum.de>
Dear all,

I would appreciate to discuss issues concerning Isabelle2025-RC0 in
separate threads per topics. It is difficult to follow the discussion if
everything is mixed into one thread.

Thanks a lot,
Florian

Am 07.01.25 um 20:10 schrieb Makarius:

Dear Isabelle users,

the Isabelle2025 release process is about to start soon, see https://
isabelle-dev.sketis.net/phame/post/view/85/
release_candidates_for_isabelle2025 for ongoing documentation of its
stages.

To warm up, we now have Isabelle2025-RC0 for early experimentation:
https://isabelle.in.tum.de/website-Isabelle2025-RC0

It is important to use the current window of opportunity until 15-
Mar-2025 for testing, and reporting of observations and problems. Quite
often, people think that release quality is achieved by doing nothing
and merely waiting for the final date. For Isabelle releases, "final"
means eternal and unchangeable: remaining problems will not be addressed
until a later release (every 8-10 months).

Makarius

OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc

Last updated: Jan 30 2025 at 04:21 UTC