Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle C wrapper [was Isabelle2021-RC3: macO...


view this post on Zulip Email Gateway (Jan 26 2021 at 16:19):

From: "Fernandez, Matthew" <matthew.fernandez@intel.com>
A bit OT, but it looks like there's an unchecked allocation and a dead store in this code. HTH.

--- Isabelle.c 2021-01-26 08:06:45.916458951 -0800
+++ Isabelle1.c 2021-01-26 08:07:31.720458189 -0800
@@ -24,12 +24,12 @@ int main(int argc, char *argv[])
int i = 0;

dcmd = strdup(argv[0]);

view this post on Zulip Email Gateway (Jan 26 2021 at 16:39):

From: Makarius <makarius@sketis.net>
Thanks. I will take it into account when reworking it once again.

I actually stopped using C in 1992, after reading the first edition of Larry's
book "ML for the working programmer".

Maybe I should have done it in Go or Rust.

Makarius

view this post on Zulip Email Gateway (Jan 26 2021 at 20:25):

From: Frédéric Boulanger <frederic.boulanger@lri.fr>
I have setup a very simple wrapper that just invokes sh on the original shell script.

https://github.com/Frederic-Boulanger-UPS/FatIsabelleLauncher <https://github.com/Frederic-Boulanger-UPS/FatIsabelleLauncher>

The first time you try to open a file in the "Documents" folder after patching Isabelle2021-RC3 is a bit long, but you are finally asked if you want to allow the access, and the authorization is then remembered between launches.

The patch consists in renaming the Isabelle2021-RC3 script to Isabelle2021-RC3.sh, and replacing the original script with the fat binary.

The C++ program simply finds the application bundle directory from argv[0] and then invokes sh on the Isabelle2021-RC3.sh file in the bundle directory.
I used C++ to avoid the awkwardness of handling memory buffers to copy and join strings the old plain C way...
It is necessary to use c++17 to benefit from std::filesystem::path for finding the bundle directory path.

The C++ source is compiled to both the x86_64 and arm64 targets, and the two executables are combined with lipo into a:

Mach-O universal binary with 2 architectures: [x86_64:Mach-O 64-bit executable x86_64] [arm64:Mach-O 64-bit executable arm64]

as revealed by a call to the file command.
The Makefile takes care of building and combining the executables.

I hope this can make Isabelle more usable on Big Sur with the next release candidate.

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

view this post on Zulip Email Gateway (Jan 26 2021 at 21:03):

From: Makarius <makarius@sketis.net>
Thanks for the example. C++ is even more foreign to me than C.

I am presently experimenting with a brushed-up version of plain Isabelle.c:
https://isabelle.sketis.net/repos/isabelle-release/annotate/02973da6180a/Admin/Linux/Isabelle.c

It turns out that having a native x86_64-darwin program execute a shell script
has the desired effect:

* The security system accepts it as a proper app and asks for permissions to
access "Documents" etc.

* It is still multi-platform capable, due to the intermission of the shell,
and my earlier change to detect the overall platform despite the x86_64
context:
https://isabelle.sketis.net/repos/isabelle-release/annotate/bf573ed376ef/lib/scripts/isabelle-platform

I will finish the exploration and come back with a fully-integrated macOS app
soon --- unless there are further surprises.

Makarius

view this post on Zulip Email Gateway (Jan 26 2021 at 21:08):

From: "Fernandez, Matthew" <matthew.fernandez@intel.com>
FYI std::filesystem is still quite poorly supported on some OSes. Though maybe none of them are supported dev environments for Isabelle.


Last updated: Dec 08 2021 at 08:24 UTC