Email Gateway (Aug 18 2026 at 11:33): Email Gateway (Aug 18 2026 at 11:33):From: Dmitriy Traytel <cl-isabelle-users@lists.cam.ac.uk>
Hi all, mostly Makarius,
After trying things around (and consulting with various agents :) ), I cannot get Isabelle2026-RC0.app to work on my machine. First, the standard recipe from https://isabelle.in.tum.de/website-Isabelle2026-RC0/installation.html :
Open Isabelle2026-RC0.app and Cancel the subsequent security dialog.
Open Security & Privacy in system preferences: section "Allow apps ..." at the bottom should list the blocked application (see screenshot).
Click Open Anyway and provide further confirmations as required.
never worked on my managed machine (MacBook Pro, M4 Max)—I am root, but cannot change System Preferences arbitrarily—also not for past Isabelle versions.
However, removing the quarantine from the downloaded tar.gz (xattr -d com.apple.quarantine …) was sufficient so far to make the app work. With Isabelle2026-RC0.app I get a popup saying
“Isabelle2026-RC0” is damaged and can’t be opened. You should move it to the Trash.
This file was downloaded on an unknown date.
The workaround suggested by Claude: drop the .app ending, so that macOS stops treating this as an app bundle—I can then execute the binaries directly. This is workable for me since I mostly start Isabelle from the command line anyway. Claude also suggests the following upon further investigation (ignore if unhelpful; the user-facing symptoms are described above):
Isabelle2026-RC0_macos_arm.tar.gz has Contents/MacOS/Isabelle2026-RC0 signed by "Developer ID Application: Azul Systems, Inc. (TDTHCUPYFR)" with Sealed Resources=none, while bin, src, contrib, ANNOUNCE etc. sit at the bundle root outside Contents/; codesign --verify on the bundle reports "code has no resources but signature indicates they must be present", and re-signing fails with "unsealed contents present in the bundle root”.
Dmitriy
Email Gateway (Aug 18 2026 at 12:54):From: Makarius <makarius@sketis.net>
On 18/08/2026 13:33, Dmitriy Traytel (via cl-isabelle-users Mailing List) wrote:
After trying things around (and consulting with various agents :) ), I cannot
get Isabelle2026-RC0.app to work on my machine. First, the standard recipe
from https://isabelle.in.tum.de/website-Isabelle2026-RC0/installation.htmlnever worked on my managed machine (MacBook Pro, M4 Max)—I am root, but
cannot change System Preferences arbitrarily—also not for past Isabelle versions.
I cannot reproduce any of the mentioned problems, which are not specific
anyway. I have many old and new installations of macOS around, and have tested
the new app bundle everywhere: it looks fine so far.
Maybe you have some odd system settings to start with.
The workaround suggested by Claude: drop the .app ending, so that macOS stops
treating this as an app bundle—I can then execute the binaries directly.
What follows sounds like typical AI-nonsense from 2025. I thought that things
have significantly improved 2026 --- apparently not.
I did experiment with proper codesigning on our side, but this is not shipped
for now: it means spending extra time and money, for relatively little in return.
Makarius
Email Gateway (Aug 18 2026 at 13:41):From: Frédéric Boulanger <frederic.boulanger@centralesupelec.fr>
Hi,
I have just installed Isabelle2026-RC0 on an M3 Mac running MacOS 26.6.1, and it runs fine.
The steps I followed are:
The second step may be important because of the way Gatekeeper handles applications that have not been moved to another folder (not necessarily the /Application one). I found this post about this issue:
https://github.com/potionfactory/LetsMove/issues/56
More details are given on:
https://weblog.rogueamoeba.com/2016/06/29/sierra-and-gatekeeper-path-randomization/
Anyway, it is worth trying to move Isabelle2026-RC0 to another folder to see if it solves your problem.
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 18 août 2026 à 14:54, Makarius <makarius@sketis.net> a écrit :
On 18/08/2026 13:33, Dmitriy Traytel (via cl-isabelle-users Mailing List) wrote:
After trying things around (and consulting with various agents :) ), I cannot get Isabelle2026-RC0.app to work on my machine. First, the standard recipe from https://isabelle.in.tum.de/website-Isabelle2026-RC0/installation.html never worked on my managed machine (MacBook Pro, M4 Max)—I am root, but cannot change System Preferences arbitrarily—also not for past Isabelle versions.
I cannot reproduce any of the mentioned problems, which are not specific anyway. I have many old and new installations of macOS around, and have tested the new app bundle everywhere: it looks fine so far.
Maybe you have some odd system settings to start with.
The workaround suggested by Claude: drop the .app ending, so that macOS stops treating this as an app bundle—I can then execute the binaries directly.
What follows sounds like typical AI-nonsense from 2025. I thought that things have significantly improved 2026 --- apparently not.
I did experiment with proper codesigning on our side, but this is not shipped for now: it means spending extra time and money, for relatively little in return.
Makarius
Email Gateway (Aug 18 2026 at 13:46):From: Dmitriy Traytel <cl-isabelle-users@lists.cam.ac.uk>
On 18 Aug 2026, at 14.54, Makarius <makarius@sketis.net> wrote:
On 18/08/2026 13:33, Dmitriy Traytel (via cl-isabelle-users Mailing List) wrote:
After trying things around (and consulting with various agents :) ), I cannot get Isabelle2026-RC0.app to work on my machine. First, the standard recipe from https://isabelle.in.tum.de/website-Isabelle2026-RC0/installation.html never worked on my managed machine (MacBook Pro, M4 Max)—I am root, but cannot change System Preferences arbitrarily—also not for past Isabelle versions.
I cannot reproduce any of the mentioned problems, which are not specific anyway. I have many old and new installations of macOS around, and have tested the new app bundle everywhere: it looks fine so far.
Maybe you have some odd system settings to start with.
Odd system settings is what I meant by managed machine. The oddness is summarized by this screenshot: I cannot allow arbitrary applications via the UI (the greyed out area saying “App Store & Known Developers"), so I can’t follow the recipe written on the website. This has been the case before.
My workaround for prior versions has been to remove things from Gatekeeper quarantine manually (xattr -d com.apple.quarantine <downloade_isabelle>.tar.gz, then extract and move to /Applications).
After I do this with Isabelle2026-RC0 and run
/Applications/Isabelle2026-RC0.app/bin/isabelle jedit
I get the said error message (“Isabelle2026-RC0” is damaged and can’t be opened. You should move it to the Trash. This file was downloaded on an unknown date.)
However
mv /Applications/Isabelle2026-RC0.app /Applications/Isabelle2026-RC0
/Applications/Isabelle2026-RC0/bin/isabelle jedit
works without problems. Thus my problem is resolved—I just wanted to flag that using the app did not work for me.
Dmitriy
[Screenshot 2026-08-18 at 15.27.47.png]
Screenshot 2026-08-18 at 15.27.47.png
Email Gateway (Aug 18 2026 at 14:57):From: Makarius <makarius@sketis.net>
On 18/08/2026 15:46, Dmitriy Traytel (via cl-isabelle-users Mailing List) >
On 18 Aug 2026, at 14.54, Makarius <makarius@sketis.net> wrote:
Maybe you have some odd system settings to start with.
Odd system settings is what I meant by managed machine. The oddness is
summarized by this screenshot: I cannot allow arbitrary applications via the
UI (the greyed out area saying “App Store & Known Developers"), so I can’t
follow the recipe written on the website. This has been the case before.
OK, so at least we understand the problem. Without codesigning it is
definitely not from "Known Developers", but codesigning alone might not be
sufficient: there is a second stage of "notarization" that is pretty much
involved.
However
mv /Applications/Isabelle2026-RC0.app /Applications/Isabelle2026-RC0
/Applications/Isabelle2026-RC0/bin/isabelle jeditworks without problems. Thus my problem is resolved—I just wanted to flag that
using the app did not work for me.
This means it is not a proper macOS app, just some accidental directory content.
I would not call it a proper solution to the problem, though.
Makarius
Last updated: Sep 02 2026 at 16:10 UTC