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

[Alexander Steen]

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
--
Alexander Steen
Institute of Computer Science
Department of Mathematics and Computer Science
Freie UniversitÀt Berlin
Arnimallee 7, Room 113
14195 Berlin

E-Mail ***@fu-berlin.de
Web inf.fu-berlin.de/~lex
Phone [phone]

[Lars-Henrik Eriksson]

Post by Alexander Steen
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?

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/

[Makarius]

Post by Alexander Steen
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 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