Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle2023-RC3: sledgehammer bug?

view this post on Zulip Email Gateway (Aug 22 2023 at 18:11):

From: Christoph Sprenger <sprenger@inf.ethz.ch>
Dear Isabelle developers,

at some point, Isabelle2023-RC3’s sledgehammer started reporting the exception

Warning: exception Io {cause = SysErr ("No such file or directory", SOME ENOENT), function = "BinIO.openOut", name =
"/tmp/isabelle-christoph/process16408342100844058494/prob26598484_1.p"} raised (line 124 of "./basis/BinIO.sml")

for all further invocations without producing any other output.

Restarting Isabelle2023-RC3 fixed the problem. Unfortunately, I have no clue how to reproduce this. I thought I'd still report it, in case you have an idea what could possibly have gone wrong here. As it is a file error, could the problem possibly be located somewhere in the interface with sledgehammer?

Thank you for all your great work!

Best wishes,
Christoph

view this post on Zulip Email Gateway (Aug 22 2023 at 20:04):

From: Makarius <makarius@sketis.net>
This looks very odd to me.

What operating system is this? Which version? Which hardware?

Makarius

view this post on Zulip Email Gateway (Aug 23 2023 at 05:53):

From: Christoph Sprenger <sprenger@inf.ethz.ch>
Hi Makarius,

pretty weird indeed. It happened on macOS 12.6.8 running on a 2018 13” MacBook Pro.

Best,
Christoph

view this post on Zulip Email Gateway (Aug 26 2023 at 09:37):

From: Makarius <makarius@sketis.net>
That is an Intel Mac.

I can't say anything specific about that, but I've recently seen many crashes
on Intel Mac Minis --- reasons unclear.

It could be due to rather old macOS 10.13 High Sierra that we are still using
as baseline, e.g. to build Poly/ML. See also
https://isabelle.sketis.net/repos/isabelle-release/file/Isabelle2023-RC3/Admin/components/PLATFORMS#l26

After the Isabelle2023 release, I am inclined to fast-forward to macOS 11 Big
Sur: thus the version for Intel and ARM64 will be the same.

It means that 10.13 High Sierra, 10.14 Mojave, 10.15 Catalina will be
discontinued.

Makarius

view this post on Zulip Email Gateway (Sep 02 2023 at 10:41):

From: Makarius <makarius@sketis.net>
Did you see this problem on macOS again?

It could be somehow related to the problem seen on Windows 11, when invoking
an external SMT solver (but above it is an ATP for sledgehammer). See also the
thread "smt failures on HOL-Analysis on Windows".

Makarius

view this post on Zulip Email Gateway (Sep 04 2023 at 08:30):

From: Christoph Sprenger <sprenger@inf.ethz.ch>
Hi Makarius,

thank you for your follow-up email. No, the problem did not occur again so far.

Also, in contrast to the problem discussed in the other thread you mention, I could build HOL-Analysis and HOL-Probability in RC3-5 without any problems (under Isabelle’s default settings).

Best,
Christoph

Last updated: Apr 29 2024 at 04:18 UTC