[isabelle] Isabelle2021-RC3: macOS access to Documents fo... · Mirror: Isabelle Users Mailing List

Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle2021-RC3: macOS access to Documents fo...

Email Gateway (Jan 24 2021 at 21:37):

From: Makarius <makarius@sketis.net>
There have been reports about problems accessing folders like "Desktop",
"Documents", "Downloads" etc.

When starting from the Terminal, e.g. as
"Isabelle2021-RC3.app/Isabelle/bin/isabelle jedit" an open operation in the
editor will provoke a system security dialog on behalf of the Terminal.app.
When starting the Isabelle2021-RC3.app directly in the finder, there is no
such dialog, only an empty directory listing (e.g. in the file-open dialog).

It looks like macOS is becoming more an more like a fortress.

Maybe some macOS exports know some ways out of this security nightmare.

Makarius

Email Gateway (Jan 25 2021 at 14:54):

From: Lawrence Paulson <lp15@cam.ac.uk>
For some years now, I believe, MacOS has informed the user when a particular app seeks to access certain critical resources, including the folders you mention. This is to protect the user against malicious code.

It is only necessary to approve the access once for each app.

Larry

Email Gateway (Jan 25 2021 at 15:24):

From: Makarius <makarius@sketis.net>
But this approval does not work: it is a consequence of my change to an older
form of .app with a toplevel shell script, instead of actual executable. See
https://isabelle-dev.sketis.net/rISABELLEa95f5ae5a12 and further changes on
top of it.

The motivation was to make a hybrid app for Java x86_64-darwin and
arm64-darwin (Apple Silicon).

It might have been better to ignore Apple Silicon for now --- I would also
have preferred to ignore macOS Big Sur, but in the last consequence it would
mean to ignore all of Apple (which has become the most powerful HW/SW tech
giant on the planet).

Makarius

Email Gateway (Jan 25 2021 at 15:42):

From: Lawrence Paulson <lp15@cam.ac.uk>
Interesting. What I am finding is different: I can read files on the Desktop and Downloads folders without granting permission. However, even if I use the System Preferences > Security & Privacy > Privacy panel to grant “full disk access”, the app seems unable to see any files in the Documents folder. Weird but not a serious problem, if documented.

Larry

Email Gateway (Jan 25 2021 at 16:39):

From: Frédéric Boulanger <frederic.boulanger@lri.fr>
I am not sure if this could solve the M1/Big Sur issue, but I just tried to use an AppleScript exported as an Application to launch Isabelle, and the first time I try to open a file under "Documents", I am asked if I want to allow that, and the setting is remembered when I quit Isabelle and launch it again through the AppleScript App. The "applet" binary inside the exported Application has both x86_64 and arm64 architectures.

Here is the (simple) code I wrote to launch Isabelle :

on run do
set isabelle to the quoted form of POSIX path of "/Applications/Isabelle2021-RC3.app/Contents/Resources/Isabelle2021-RC3/bin/isabelle"
do shell script isabelle & " jedit"
end run

on open (dropedItems)
set isabelle to the quoted form of POSIX path of "/Applications/Isabelle2021-RC3.app/Contents/Resources/Isabelle2021-RC3/bin/isabelle"
set myFiles to " "
repeat with f in dropedItems
set myFiles to myFiles & " " & the quoted form of POSIX path of f
end repeat
do shell script isabelle & " jedit" & myFiles
end open

The "open" handler is useful for opening files when launching Isabelle, but this is too basic to handle files dropped on the application while Isabelle is already running.

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 69 85 14 84

Email Gateway (Jan 25 2021 at 16:44):

From: Lawrence Paulson <lp15@cam.ac.uk>
Remark: The existing Isabelle Mac App already provides some basic Mac-like functionality, but it would be great to see it upgraded with code such as this. Though maybe not in time for 2021 :-(

Larry

Email Gateway (Jan 25 2021 at 16:54):

From: Makarius <makarius@sketis.net>
The formal task is now https://isabelle-dev.sketis.net/T37 --- I have also
added some links to discussions about this problems for Fontforge, Gimp, Inkscape.

This was first reported almost 1 year ago, so there is an indication that
Apple does not care about Unix-style shell script apps.

Makarius

Email Gateway (Jan 26 2021 at 09:48):

From: Lawrence Paulson <lp15@cam.ac.uk>
Today I tried a different experiment: to access the Documents folder (which I seldom normally use) from Isabelle2020. I got the expected pop-up, clicked okay and finally was able to open a theory file I had put there. With the Isabelle2021 release candidate however, there was no pop-up and the Documents folder was displayed as empty.

This difference is odd given that the application bundles are surely produced from the Isabelle sources in the same way, but I did notice major differences in the respective copies of info.plist and conceivably something like that is where the explanation lies.

Larry

Email Gateway (Jan 26 2021 at 10:15):

From: Frédéric Boulanger <frederic.boulanger@lri.fr>
This difference comes from the fact that what is executed when you launch the RC is a shell script (/Applications/Isabelle2021-RC3.app/Isabelle2021-RC3), while it is a Mach-O executable in the case of Isabelle2020 (/Applications/Isabelle2020.app/Contents/MacOS/JavaAppLauncher). It seems that MacOS does not handle authorizations in the same way for scripts and for binary executables.

If I remember well, when you start Isabelle in the terminal using "isabelle jedit", the authorization to access the "Documents" folder is given to the Terminal application, not to the isabelle shell script.

Frédéric

Email Gateway (Jan 26 2021 at 11:08):

From: Jakub Kądziołka <kuba@kadziolka.net>
On Mon Jan 25, 2021 at 5:38 PM CET, Frédéric Boulanger wrote:

Here is the (simple) code I wrote to launch Isabelle :

on run do
set isabelle to the quoted form of POSIX path of "/Applications/Isabelle2021-RC3.app/Contents/Resources/Isabelle2021-RC3/bin/isabelle"
do shell script isabelle & " jedit"
end run

on open (dropedItems)

Is this typo (droped with a single p) a part of the Apple API, or would
it be possible to correct it?

set isabelle to the quoted form of POSIX path of "/Applications/Isabelle2021-RC3.app/Contents/Resources/Isabelle2021-RC3/bin/isabelle"
set myFiles to " "
repeat with f in dropedItems
set myFiles to myFiles & " " & the quoted form of POSIX path of f
end repeat
do shell script isabelle & " jedit" & myFiles
end open

Regards,
Jakub Kądziołka

Email Gateway (Jan 26 2021 at 12:29):

From: Frédéric Boulanger <frederic.boulanger@lri.fr>
Just a typo. It is just the name of the argument on the "open" handler, you can use any valid identifier.

See https://help.apple.com/applescript/mac/10.9/#apscrpt1131 <https://help.apple.com/applescript/mac/10.9/#apscrpt1131>

Best regards,
Frédéric

Email Gateway (Jan 26 2021 at 16:06):

From: Makarius <makarius@sketis.net>
Yes, the new shell script is an indirect consequence of of supporting both
arm64-darwin and x86_64-darwin while replacing Adopt OpenJDK by Zulu OpenJDK.

Afterwards the old JavaAppLauncher stopped working: it refers to a particular
shared library of Java, which is unlikely to be able to change from x86_64 to
arm64 on the spot.

In contrast, the Rosetta 2 system is able to run x86_64 Java, but it is one
level of extra indirection: JVM-bytecode translation followed by x86_64
machine code translation. I wanted to reduce this insanity a bit by using
native arm64 JDK.

In the space of possibilities there are surely other points of stability ---
like the Apple Script app or maybe just a plain C app wrapper like we have for
Linux:
https://isabelle.sketis.net/repos/isabelle-release/file/Isabelle2021-RC3/Admin/Linux/Isabelle.c

I will continue the experiments.

Makarius

Email Gateway (Jan 26 2021 at 22:19):

From: Makarius <makarius@sketis.net>
The plain C app wrapper works and the solution will be in the next release
candidate (first week of February).

Makarius

Last updated: Jan 04 2025 at 20:18 UTC