Email Gateway (Jan 26 2021 at 16:19): 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]);
if (dcmd == NULL) fail("Failed to allocate command line");
dname = dirname(dcmd);
cmd_line = malloc(sizeof(char *) * (argc + 1));
if (cmd_line == NULL) fail("Failed to allocate command line");
cmd = cmd_line[0];
cmd = malloc(strlen(dname) + strlen("/lib/scripts/Isabelle_app") + 1);
if (cmd == NULL) fail("Failed to allocate command name");
sprintf(cmd, "%s/lib/scripts/Isabelle_app", dname);
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
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
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
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: Jan 04 2025 at 20:18 UTC