Email Gateway (Jul 07 2022 at 07:33): Email Gateway (Jul 07 2022 at 07:33):From: Tobias Nipkow <nipkow@in.tum.de>
More problems with my new Mac:
Nitpick says:
Kodkod warning: cannot launch SAT solver, falling back on "DefaultSAT4J"
Sledgehammer says:
Error: Bad executable:
"/Users/nipkow/.isabelle/contrib/vampire-4.6/x86_64-darwin/vampire"
Anything I can or should do?
Tobias
smime.p7s
Email Gateway (Jul 07 2022 at 08:47):From: Frédéric Boulanger <frederic.boulanger@centralesupelec.fr>
Maybe you need to install Rosetta 2 to be able to run x86_64 code.
https://support.apple.com/en-gb/HT211861
This should happen automatically when you launch an x86 application on a
M1 Mac, but you can install it manually in the terminal with the
following command :
|softwareupdate --install-rosetta
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 (Jul 07 2022 at 15:51):From: Tobias Nipkow <nipkow@in.tum.de>
On 07/07/2022 10:47, Frédéric Boulanger wrote:
Maybe you need to install Rosetta 2 to be able to run x86_64 code.
https://support.apple.com/en-gb/HT211861
This should happen automatically when you launch an x86 application on a M1 Mac,
but you can install it manually in the terminal with the following command :
|softwareupdate --install-rosetta
Thanks but, as expected, it made no difference.
Anybody out there using an M1 Mac and (not) having my problems?
Tobias
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 84Le 07/07/2022 à 09:33, Tobias Nipkow a écrit :
More problems with my new Mac:
Nitpick says:
Kodkod warning: cannot launch SAT solver, falling back on "DefaultSAT4J"Sledgehammer says:
Error: Bad executable:
"/Users/nipkow/.isabelle/contrib/vampire-4.6/x86_64-darwin/vampire"Anything I can or should do?
Tobias
On 30/06/2022 16:19, Tobias Nipkow wrote:
On my new MacBook Pro M1, when I start Isabelle a pop-up with
“libsqlitejdbc.jnilib” can’t be opened because Apple cannot check it for
malicious software.appears and I have to click on OK. In the shell window it prints
Failed to load native library:libsqlitejdbc.jnilib. osinfo: Mac/aarch64
java.lang.UnsatisfiedLinkError: Can't load library:
/Users/nipkow/.isabelle/contrib/sqlite-jdbc-3.36.0.3/arm64-darwin/libsqlitejdbc.jnilibIsabelle starts, but having to click OK is annoying. What to do?
Tobias
Email Gateway (Jul 07 2022 at 16:21):From: Fiedler Ben <ben.fiedler@inf.ethz.ch>
Hi Tobias,
I have an M1 Mac and I don’t have those problems. I checked the vampire executable and it is also an x86 executable, which runs using Rosetta without issues.
bfiedler@laptop:/Applications/Isabelle2021-1.app
% ./contrib/vampire-4.6/x86_64-darwin/vampire
Running in auto input_syntax mode. Trying TPTP
^C83743 Aborted by signal SIGINT on
% ------------------------------
% Version: Vampire 4.6.0 (commit )
% Termination reason: Unknown
% Termination phase: Parsing
% Memory used [KB]: 383
% Time elapsed: 0.992 s
% ------------------------------
% ------------------------------
bfiedler@laptop:/Applications/Isabelle2021-1.app
% file ./contrib/vampire-4.6/x86_64-darwin/vampire
./contrib/vampire-4.6/x86_64-darwin/vampire: Mach-O 64-bit executable x86_64
No idea what it could be then, maybe an issue during the Rosetta installation?
Cheers,
Ben
Email Gateway (Jul 07 2022 at 16:36):From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Hi Tobias,
I’m also using a Mac M1 and have the following behaviour:
Vampire: no problem
lemma "x = y ==> P x ==> P y ∨ x ~= y" sledgehammer[provers = vampire]
Sledgehammering...
Proof found...
"vampire": Try this: by force (1 ms)
Nitpick: strange
lemma "P x ==> x = y ==> P z" nitpick
Nitpicking formula...
Kodkod warning: cannot launch SAT solver, falling back on "DefaultSAT4J"
Nitpick found a counterexample for card 'a = 2:
so nitpick complains about SAT solver; however, minisat seems to work:
/Applications/Isabelle2021-1.app/contrib/minisat-2.2.1-1/x86_64-darwin/minisat
Reading from standard input... Use '--help' for help.
============================[ Problem Statistics ]=============================
| |
So, in practise I did not encounter any serious problems, and I am really happy
with the new Isabelle/Mac M1 combination: I can process theories faster than on my current
desktop machine, and even when compiling larger projects the fans stay silent.
I did nothing in .isabelle/Isabelle2021-1/etc/settings.
Best,
René
Email Gateway (Jul 07 2022 at 17:55):From: Makarius <makarius@sketis.net>
I am only a part-time Mac user, occasionally running tests on various machines
that are in my reach.
A few days ago, I updated the macOS Monterey installation on my Mac Mini M1,
which normally runs Big Sur. After the update, Rosetta 2 did not work, or was
silently uninstalled. Doing the above "softwareupdate --install-rosetta"
solved the problem.
Makarius
Email Gateway (Jul 08 2022 at 07:06):From: Tobias Nipkow <nipkow@in.tum.de>
René,
Thanks for the feedback. I was using the development version and I have now
tried the release 21-1 and get exactly the same behaviour as you: vampire works
but nitpick still gives me that Kodkod warning, but minisat executes fine when
called from the command line.
I also ran minisat in .isabelle and it worked:
$.isabelle/contrib/minisat-2.2.1-1/x86_64-darwin/minisat
Reading from standard input... Use '--help' for help.
Maybe Isabelle tries to execute a different executable?
Tobias
smime.p7s
Email Gateway (Jul 08 2022 at 12:31):From: "\"Blanchette, J.C. (Jasmin Christian)\"" <cl-isabelle-users@lists.cam.ac.uk>
Hi Tobias,
Indeed, Nitpick tries to use the JNI (Java Native Interface) version. I'm guessing the JNI stuff is out of date. JNI offers a tighter integration, which can be used e.g. to enumerate models (not just get one), but we don't really need it in Nitpick, so I'll consider getting rid of JNI altogether. Makarius also pointed out to me last year that the JNI stuff is somewhat outdated.
Cheers,
Jasmin
Email Gateway (Jul 08 2022 at 13:24):From: Tobias Nipkow <nipkow@in.tum.de>
On 08/07/2022 14:31, Blanchette, J.C. (Jasmin Christian) wrote:
Hi Tobias,
Indeed, Nitpick tries to use the JNI (Java Native Interface) version. I'm
guessing the JNI stuff is out of date. JNI offers a tighter integration, which
can be used e.g. to enumerate models (not just get one), but we don't really
need it in Nitpick, so I'll consider getting rid of JNI altogether. Makarius
also pointed out to me last year that the JNI stuff is somewhat outdated.
Thanks, that explains nitpick. (although it does not explain why some people
report they don't have a problem).
That leaves the question why, with the development version, Vampire isn't executing.
Tobias
Cheers,
Jasmin
From: cl-isabelle-users-request@lists.cam.ac.uk on behalf of Tobias Nipkow
Sent: Friday, July 8, 2022 9:06
To: Thiemann, René
Cc: Isabelle Users List
Subject: Re: [isabelle] Mac M1 12.4: nitpick and sledgehammer
René,Thanks for the feedback. I was using the development version and I have now
tried the release 21-1 and get exactly the same behaviour as you: vampire works
but nitpick still gives me that Kodkod warning, but minisat executes fine when
called from the command line.I also ran minisat in .isabelle and it worked:
$.isabelle/contrib/minisat-2.2.1-1/x86_64-darwin/minisat
Reading from standard input... Use '--help' for help.Maybe Isabelle tries to execute a different executable?
Tobias
On 07/07/2022 18:36, Thiemann, René wrote:
Hi Tobias,
I’m also using a Mac M1 and have the following behaviour:
Vampire: no problem
lemma "x = y ==> P x ==> P y ∨ x ~= y" sledgehammer[provers = vampire]
Sledgehammering...
Proof found...
"vampire": Try this: by force (1 ms)Nitpick: strange
lemma "P x ==> x = y ==> P z" nitpick
Nitpicking formula...
Kodkod warning: cannot launch SAT solver, falling back on "DefaultSAT4J"
Nitpick found a counterexample for card 'a = 2:so nitpick complains about SAT solver; however, minisat seems to work:
/Applications/Isabelle2021-1.app/contrib/minisat-2.2.1-1/x86_64-darwin/minisat
Reading from standard input... Use '--help' for help.
============================[ Problem Statistics ]=============================
| |So, in practise I did not encounter any serious problems, and I am really happy
with the new Isabelle/Mac M1 combination: I can process theories faster than on my current
desktop machine, and even when compiling larger projects the fans stay silent.I did nothing in .isabelle/Isabelle2021-1/etc/settings.
Best,
RenéAm 07.07.2022 um 17:50 schrieb Tobias Nipkow <nipkow@in.tum.de>:
On 07/07/2022 10:47, Frédéric Boulanger wrote:
Maybe you need to install Rosetta 2 to be able to run x86_64 code.
https://support.apple.com/en-gb/HT211861 <https://support.apple.com/en-gb/HT211861>
This should happen automatically when you launch an x86 application on a M1 Mac, but you can install it manually in the terminal with the following command :
|softwareupdate --install-rosettaThanks but, as expected, it made no difference.
Anybody out there using an M1 Mac and (not) having my problems?
Tobias
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 84Le 07/07/2022 à 09:33, Tobias Nipkow a écrit :
More problems with my new Mac:
Nitpick says:
Kodkod warning: cannot launch SAT solver, falling back on "DefaultSAT4J"Sledgehammer says:
Error: Bad executable: "/Users/nipkow/.isabelle/contrib/vampire-4.6/x86_64-darwin/vampire"Anything I can or should do?
Tobias
On 30/06/2022 16:19, Tobias Nipkow wrote:
On my new MacBook Pro M1, when I start Isabelle a pop-up with
“libsqlitejdbc.jnilib” can’t be opened because Apple cannot check it for malicious software.
appears and I have to click on OK. In the shell window it prints
Failed to load native library:libsqlitejdbc.jnilib. osinfo: Mac/aarch64
java.lang.UnsatisfiedLinkError: Can't load library: /Users/nipkow/.isabelle/contrib/sqlite-jdbc-3.36.0.3/arm64-darwin/libsqlitejdbc.jnilibIsabelle starts, but having to click OK is annoying. What to do?
Tobias
Email Gateway (Jul 11 2022 at 12:14):From: "\"Blanchette, J.C. (Jasmin Christian)\"" <cl-isabelle-users@lists.cam.ac.uk>
That leaves the question why, with the development version, Vampire isn't executing.
I really have no idea. I was hoping Makarius would comment on this -- he's been officially in charge of the ATP packages for the last 1.5 years or so (with modest financial support from VU Amsterdam).
Jasmin
From: Tobias Nipkow
Sent: Friday, July 8, 2022 15:24
To: Blanchette, J.C. (Jasmin Christian)
Cc: Isabelle Users List
Subject: Re: [isabelle] Mac M1 12.4: nitpick and sledgehammer
On 08/07/2022 14:31, Blanchette, J.C. (Jasmin Christian) wrote:
Hi Tobias,
Indeed, Nitpick tries to use the JNI (Java Native Interface) version. I'm
guessing the JNI stuff is out of date. JNI offers a tighter integration, which
can be used e.g. to enumerate models (not just get one), but we don't really
need it in Nitpick, so I'll consider getting rid of JNI altogether. Makarius
also pointed out to me last year that the JNI stuff is somewhat outdated.
Thanks, that explains nitpick. (although it does not explain why some people
report they don't have a problem).
That leaves the question why, with the development version, Vampire isn't executing.
Tobias
Cheers,
Jasmin
From: cl-isabelle-users-request@lists.cam.ac.uk on behalf of Tobias Nipkow
Sent: Friday, July 8, 2022 9:06
To: Thiemann, René
Cc: Isabelle Users List
Subject: Re: [isabelle] Mac M1 12.4: nitpick and sledgehammer
René,Thanks for the feedback. I was using the development version and I have now
tried the release 21-1 and get exactly the same behaviour as you: vampire works
but nitpick still gives me that Kodkod warning, but minisat executes fine when
called from the command line.I also ran minisat in .isabelle and it worked:
$.isabelle/contrib/minisat-2.2.1-1/x86_64-darwin/minisat
Reading from standard input... Use '--help' for help.Maybe Isabelle tries to execute a different executable?
Tobias
On 07/07/2022 18:36, Thiemann, René wrote:
Hi Tobias,
I’m also using a Mac M1 and have the following behaviour:
Vampire: no problem
lemma "x = y ==> P x ==> P y ∨ x ~= y" sledgehammer[provers = vampire]
Sledgehammering...
Proof found...
"vampire": Try this: by force (1 ms)Nitpick: strange
lemma "P x ==> x = y ==> P z" nitpick
Nitpicking formula...
Kodkod warning: cannot launch SAT solver, falling back on "DefaultSAT4J"
Nitpick found a counterexample for card 'a = 2:so nitpick complains about SAT solver; however, minisat seems to work:
/Applications/Isabelle2021-1.app/contrib/minisat-2.2.1-1/x86_64-darwin/minisat
Reading from standard input... Use '--help' for help.
============================[ Problem Statistics ]=============================
| |So, in practise I did not encounter any serious problems, and I am really happy
with the new Isabelle/Mac M1 combination: I can process theories faster than on my current
desktop machine, and even when compiling larger projects the fans stay silent.I did nothing in .isabelle/Isabelle2021-1/etc/settings.
Best,
RenéAm 07.07.2022 um 17:50 schrieb Tobias Nipkow <nipkow@in.tum.de>:
On 07/07/2022 10:47, Frédéric Boulanger wrote:
Maybe you need to install Rosetta 2 to be able to run x86_64 code.
https://support.apple.com/en-gb/HT211861 <https://support.apple.com/en-gb/HT211861>
This should happen automatically when you launch an x86 application on a M1 Mac, but you can install it manually in the terminal with the following command :
|softwareupdate --install-rosettaThanks but, as expected, it made no difference.
Anybody out there using an M1 Mac and (not) having my problems?
Tobias
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 84Le 07/07/2022 à 09:33, Tobias Nipkow a écrit :
More problems with my new Mac:
Nitpick says:
Kodkod warning: cannot launch SAT solver, falling back on "DefaultSAT4J"Sledgehammer says:
Error: Bad executable: "/Users/nipkow/.isabelle/contrib/vampire-4.6/x86_64-darwin/vampire"Anything I can or should do?
Tobias
On 30/06/2022 16:19, Tobias Nipkow wrote:
On my new MacBook Pro M1, when I start Isabelle a pop-up with
“libsqlitejdbc.jnilib” can’t be opened because Apple cannot check it for malicious software.
appears and I have to click on OK. In the shell window it prints
Failed to load native library:libsqlitejdbc.jnilib. osinfo: Mac/aarch64
java.lang.UnsatisfiedLinkError: Can't load library: /Users/nipkow/.isabelle/contrib/sqlite-jdbc-3.36.0.3/arm64-darwin/libsqlitejdbc.jnilibIsabelle starts, but having to click OK is annoying. What to do?
Tobias
Email Gateway (Jul 11 2022 at 12:28):From: Makarius <makarius@sketis.net>
Yes, I will comment on it rather soon, but I am still busy elsewhere.
Makarius
Email Gateway (Jul 22 2022 at 17:38):From: Makarius <makarius@sketis.net>
I have no idea either: it works fine for me with Big Sur and Monterey on Apple
M1 with Rosetta installed. I have tried both Isabelle2021-1 and current
Isabelle/707748d3d186: the vampire-4.6 component is the same anyway.
Maybe some evil Apple security subsystem has marked a particular copy of the
vampire executable as "bad". It could help to purge
$HOME/.isabelle/contrib/vampire-4.6 and use Admin/init again (for repository
versions, not releases).
Makarius
Email Gateway (Jul 22 2022 at 17:42):From: Makarius <makarius@sketis.net>
We can't reproduce any of the original Kodkod JNI libraries now --- at least I
did not find any sources for them after searching carefully > 3 times.
What did work out for Isabelle2021-1 was a fresh build of MiniSat as external
program, see this NEWS entry:
Makarius
Email Gateway (Jul 24 2022 at 15:52):From: Tobias Nipkow <nipkow@in.tum.de>
That did the job, thanks a lot!
Tobias
smime.p7s
Last updated: Jan 04 2025 at 20:18 UTC