Email Gateway (Aug 22 2022 at 20:51): Email Gateway (Aug 22 2022 at 20:51):From: Lawrence Paulson <lp15@cam.ac.uk>
Mac users please note: the latest version of OS X, Catalina, no longer supports 32-bit code. Isabelle is unaffected except for one of its add-ons, namely csdp. It is used by the sos proof method, which uses a sum of squares technique to decide certain problems involving real-valued polynomials. If you want to upgrade to Catalina and use this admittedly obscure sos method, you will need to rebuild csdp from sources.
Download the sources from https://github.com/coin-or/Csdp.
It’s necessary to install gfortran, which can be done in a single line using homebrew (https://brew.sh):
brew cask install gfortran
This also installs a copy of the real gcc compiler. Put a link in a more sensible place:
ln -s /usr/local/gfortran/bin/gcc /usr/local/bin/
Type, at the top level of the Csdp-6.1.1 source directory,
make CC=/usr/local/bin/gcc
Finally, install the binary somewhere and put a line such as the following in your settings file:
ISABELLE_CSDP=/usr/local/bin/csdp
In theory, there could be other 32-bit code somewhere within Isabelle, but I did a scan and couldn’t find any.
Larry Paulson
Email Gateway (Aug 22 2022 at 20:52):From: Makarius <makarius@sketis.net>
Note that following hints by René Thiemann
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2019-October/msg00020.html
there are more fundamental problems to run our unregistered Isabelle
application, even from the command-line.
It only works if the app has been "blessed" by Gatekeeper before. There are
more details and hints on websites like
https://eclecticlight.co/2019/10/04/will-gatekeeper-let-me-run-that-app-in-catalina
We need to find a proper solution eventually, but my general impression is
that macOS users better stay away from Catalina until the dust has settled.
Makarius
Email Gateway (Aug 22 2022 at 20:52):From: Makarius <makarius@sketis.net>
I did some further research on it: Apple seems to require official Developer
Program Membership in order to sign and thus run applications on Catalina. It
costs 99$ per year, with some additional administrative overhead.
Makarius
Email Gateway (Aug 22 2022 at 20:53):From: Lawrence Paulson <lp15@cam.ac.uk>
I don’t think there’s anything new about the need for signed applications in OSX.
There are various ways to override this security check for specific applications/binaries. Users can also switch checking off using the Security & Privacy preference pane.
Larry
Email Gateway (Aug 22 2022 at 20:53):From: Makarius <makarius@sketis.net>
Apple did change something significantly for Catalina. There are already many
websites to tell users how to circumvent it, but it requires rather brutal
measures, e.g.
https://www.imore.com/how-open-apps-anywhere-macos-catalina-and-mojave
Makarius
Email Gateway (Aug 22 2022 at 20:54):From: Makarius <makarius@sketis.net>
Larry, I think you did not see anything because you made an in-place update of
an existing system where Gatekeeper was already configured in a liberal manner.
My own test installation was a fresh one, as usual. This leads to so many
roadblocks that people have already started to make fun websites about it,
comparing macOS Catalina with Windows Vista.
It is almost impossible to do anything we are used to, without disabling many
of the new security defaults (e.g. the directories that a Terminal process may
access).
(I am myself only a part-time macOS user, and not a macOS developer.)
Makarius
Email Gateway (Aug 22 2022 at 20:54):From: Lawrence Paulson <lp15@cam.ac.uk>
I use the default Security & Privacy settings.
To launch an unsigned application for the first time, you right-click on it, select Open and then click through the “are you sure?” dialogue box. Then you are set for life. I tested this just now with the Isabelle nightly release snapshot.
The main new security feature I see with Catalina is that users are asked things like “Do you want to download from Internet address X?” and “Can application X have access to resource R?”. These defend against well-known threats and you are only asked once.
People need to calm down. There’s really nothing to see here.
Larry
Email Gateway (Aug 22 2022 at 21:04):From: Makarius <makarius@sketis.net>
Did you try this on a fresh installation, without any previous settings of yours?
Makarius
Email Gateway (Aug 22 2022 at 21:04):From: Makarius <makarius@sketis.net>
That looks like well-substantiated reading of Apple tea leaves. Some notable
quotes:
"""
Apple could ban any non-notarized software in a future version of macOS.
Based on the direction that it’s heading, the process could be as simple as
“flipping a switch,” so to speak.
[...]
But Apple could simply be using app notarization to add a bit of extra
security (or security theater) to the Mac without forcing all apps to go
through the Mac App Store, as it does for iOS.
In our opinion, and the opinions of many developers, this seems like the most
likely scenario. But, of course, it’s hard to predict what Apple is going to
do so take this forecast with a grain of salt.
"""
The conclusion for now: nothing else to do for Catalina and the Isabelle2020
release (presumably June 2020).
Makarius
Email Gateway (Aug 22 2022 at 21:05):From: Jesper Bengtson <jebe@itu.dk>
I have tried, and I agree with Larry.
Catalina asks you more questions than previous versions of OSX, but once you answered those questions it does not bother you again (for that application). There really is no problem here. It is a minor passing inconvenience for some added security. I actually like being able to tell my apps that they may not access a bunch of stuff that they may want for no good reason.
/Jesper
Email Gateway (Aug 22 2022 at 21:07):From: Stephan Merz <stephan.merz@loria.fr>
You may want to consider "notarizing" the Isabelle app for Catalina [1]. Apple claims that this will become a requirement from January 1, 2020. Since Isabelle is developed in academia, you should be eligible for a membership fee waiver [2].
Stephan
[1] https://developer.apple.com/documentation/xcode/notarizing_macos_software_before_distribution <https://developer.apple.com/documentation/xcode/notarizing_macos_software_before_distribution>
[2] https://developer.apple.com/support/membership-fee-waiver/ <https://developer.apple.com/support/membership-fee-waiver/>
Email Gateway (Aug 22 2022 at 21:08):From: Makarius <makarius@sketis.net>
Thanks, I take it as a second independent source of information -- a minimal
requirement for proper journalism. With that in mind, I made a more careful
web search and came about the following primary source by Apple:
https://support.apple.com/en-us/HT202491
At the bottom of the page is a very informative section about "How to open an
app that hasn’t been notarized or is from an unidentified developer", it
covers Mojave and Catalina.
Then I made a ultra-clean Catalina installation, without referring to any of
my personal profile (no Apple ID login etc.).
Now I can confirm that Isabelle2019.app runs on it as follows:
* Right-click "Open" -- application starts to open but is rejected by Gatekeeper
* Open Security & Privacy preferences: it shows the rejected application
* Click "Open Anyway"
Afterwards everything works as expected, even our embedded executables (for
sledgehammer etc.) -- excluding the obscure CSDP tool (old 32bit application).
So I have learned something new as a part-time macOS user!
It seems that the majority of macOS users out there has been mislead by a
multiplication of hints about the rather brutal "sudo spctl --master-disable".
Probably a case of misinformation due to Google ranking algorithms, but that
is another problem.
I will update https://isabelle.in.tum.de/installation.html shortly to refer to
this documentation by Apple, such we have an easily repeatable solution to
tell new users (few people read it on their own).
Makarius
Email Gateway (Aug 22 2022 at 21:09):From: Makarius <makarius@sketis.net>
New potential problems emerging ... Do you have further sources for that? I've
found the following not on the spot:
https://developer.apple.com/news/?id=09032019a
Reading just that, my understanding (or hope) is that users can still run
unnotarized apps by the "Open Anyway" procedure in Security preferences.
Makarius
Email Gateway (Aug 22 2022 at 21:10):From: Stephan Merz <stephan.merz@loria.fr>
It looks to me that users will still be able to override the notarization requirement, but that Apple appears to want to make it progressively more difficult to do so. Then again, they delayed the implementation of the requirement to January 1 instead of making it mandatory with the release of Catalina, probably due to developer and user backlash, so all of this is speculation at this point. I found [1] to be a reasonably clear description of the current situation. (And I haven't switched to Catalina just yet.)
Best,
Stephan
[1] https://appletoolbox.com/everything-you-need-to-know-about-app-notarization-in-macos-catalina/
Email Gateway (Aug 22 2022 at 21:11):From: Norbert Schirmer via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Dear Isabelle - Team,
Please note the update to the notarization prerequisites for macOS Catalina that will be active starting from February, 03rd, 2020.
https://developer.apple.com/news/?id=12232019a <https://developer.apple.com/news/?id=12232019a>
Regards,
Norbert
Last updated: May 07 2024 at 01:07 UTC