Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle/HOL on MacBook "untrusted"?


view this post on Zulip Email Gateway (Aug 22 2022 at 18:35):

From: Alexander Steen <a.steen@fu-berlin.de>
Hi all,

I'm using Isabelle for a lecture course on deontic logic (and other
topics) at the University of Luxembourg. Today, a student tried to
install Isabelle/HOL 2018 on her MacBook (macOS Sierra, version 10.12.5,
MacBook Air) and, while doing so, it showed an error message saying that
it will not run Isabelle since it's untrusted (or so). See the exact
message as screenshot attached to this e-mail.

I'm sure there are options to disable this check (as a hot fix), so it's
not an urgent problem. But maybe it would be a good idea to look into
this in the future; it would be sad to see people not using Isabelle
just because of this. Of course, I don't know if this can be addressed
by Isabelle developers at all. Does anyone have experience with this?

Thanks in advance!

Best
Alex
Screen Shot 2018-10-03 at 14.53.10.png

view this post on Zulip Email Gateway (Aug 22 2022 at 18:36):

From: Lars-Henrik Eriksson <lhe@it.uu.se>
It's very simple. Right-click on the Isabelle application and choose "Open". You will now get a dialog box asking whether you want to run the application even though it is untrusted. Click that you will. From now on Isabelle can be started the usual way by double-clicking the application.

Lars-Henrik Eriksson, PhD, Senior Lecturer
Computing Science, Dept. of Information Technology, Uppsala University, Sweden

När du har kontakt med oss på Uppsala universitet med e-post så innebär det att vi behandlar dina personuppgifter. För att läsa mer om hur vi gör det kan du läsa här: http://www.uu.se/om-uu/dataskydd-personuppgifter/

E-mailing Uppsala University means that we will process your personal data. For more information on how this is performed, please read here: http://www.uu.se/om-uu/dataskydd-personuppgifter/

view this post on Zulip Email Gateway (Aug 22 2022 at 18:37):

From: Makarius <makarius@sketis.net>
See this note on http://isabelle.in.tum.de/installation.html

"""
The Isabelle application lacks special certificates and signatures, so
Apple tends to reject it by default. Running it for the first time might
require a right-click or control-click on the application icon to open
it explicitly.
"""

Some years ago Apple (and MicroSoft) have made it very difficult to run
arbitrary applications: one needs to pay a subscription fee for
developer status and then submit the application to an "app store".

Makarius


Last updated: Mar 29 2024 at 08:18 UTC