Chengsong Tan (Sep 11 2024 at 17:26): Chengsong Tan (Sep 11 2024 at 17:26):Hi,
I got this error when doing some sledgehammer calls on Windows (using Isabelle2023):
Warning: exception Io {cause = SysErr ("Access is denied.", SOME ERROR_ACCESS_DENIED), function = "BinIO.openOut", name =
"prob15193332_1_proof.p"} raised (line 124 of "./basis/BinIO.sml")
has anyone else encountered this?
How do you fix this?
Thanks a lot,
Chengsong
Mathias Fleury (Sep 11 2024 at 17:40):that means that sledgehammer is trying to read a proof file but does not have the rights to do so
Chengsong Tan (Sep 12 2024 at 08:15):Mathias Fleury said:
that means that sledgehammer is trying to read a proof file but does not have the rights to do so
Thank you! But if it created that file itself, what could cause this to happen? Weirdly that after downloading and decompressing Isabelle2023 again to a different folder (Documents instead of Desktop) this issue does not turn up for the same s/h call now......
Mathias Fleury (Sep 12 2024 at 08:24):An antivirus maybe?
Mathias Fleury (Sep 12 2024 at 08:25):the proof files are stored somewhere /tmp or whatever this is called under windows
Mathias Fleury (Sep 12 2024 at 08:25):especially for antivirus, waiting longer can make issues appear and disappear…
Chengsong Tan (Sep 12 2024 at 08:29):Mathias Fleury said:
An antivirus maybe?
I've turned off windows defender and no antivirus other than that installed.
Chengsong Tan (Sep 12 2024 at 08:29):Mathias Fleury said:
especially for antivirus, waiting longer can make issues appear and disappear…
Windows sledgehammer is so buggy.......
Chengsong Tan (Sep 12 2024 at 08:30):Mathias Fleury said:
the proof files are stored somewhere /tmp or whatever this is called under windows
I do lots of s/h calls at the same time. Could it be the case that at some point a certain problem file's name collides with another, such that it cannot be created?
Mathias Fleury (Sep 12 2024 at 08:31):no they cannot collide (unless you use the overlord option)
Mathias Fleury (Sep 12 2024 at 08:32):Chengsong Tan said:
Mathias Fleury said:
especially for antivirus, waiting longer can make issues appear and disappear…
Windows sledgehammer is so buggy.......
No really. Some people encounter a lot of issues, but most are fine (including students)
Chengsong Tan (Sep 12 2024 at 08:32):Mathias Fleury said:
no they cannot collide (unless you use the overlord option)
LOL that's a funny name for an option
Chengsong Tan (Sep 12 2024 at 08:33):(deleted)
Chengsong Tan (Sep 12 2024 at 08:34):Mathias Fleury said:
Chengsong Tan said:
Mathias Fleury said:
especially for antivirus, waiting longer can make issues appear and disappear…
Windows sledgehammer is so buggy.......
No really. Some people encounter a lot of issues, but most are fine (including students)
Not sure if raised in the mailing list/forum, but haven't you noticed that Isabelle 2024 on windows will have e provers hanging around even after sledgehammer has terminated?
Chengsong Tan (Sep 12 2024 at 08:34):which will quickly exhaust system memory after you do a number of s/h calls.
Mathias Fleury (Sep 12 2024 at 08:37):Yeah I saw this one (and my last take is that we still do not know why)
Mathias Fleury (Sep 12 2024 at 08:37):in particular sledgehammer is supposed to kill jobs
Mathias Fleury (Sep 12 2024 at 08:38):so windows for some reason is not killing jobs properly
Mathias Fleury (Sep 12 2024 at 08:38):There are good reasons why most heavy Isabelle users are on linux or mac…
Chengsong Tan (Sep 12 2024 at 08:43):Mathias Fleury said:
so windows for some reason is not killing jobs properly
But could we integrate a stronger killing method into Isabelle2024 on windows? Say taskkill, which does kill properly (which is how I try to kill eprover.exe).
Mathias Fleury (Sep 12 2024 at 08:44):Sure. But for that we need someone who uses windows and bothers enough to try to fix the issue.
Chengsong Tan (Sep 12 2024 at 08:59):Mathias Fleury said:
Sure. But for that we need someone who uses windows and bothers enough to try to fix the issue.
I use Windows. Is this an easy fix? It does sound like one and presumably you can just find the place where the killing API is called in isabelle/ML and do a search+replace?
Mathias Fleury (Sep 12 2024 at 09:16):It will not be as easy as a search and replace.
So:
lemma "(∀(x::nat). P x)"
sledgehammer[e,verbose]
They issue might go down as far as it is a polyml bug (after unpealing the Isabelle_Threads layer and so on). In that case, it might be end up with a Polyml bug if you can reproduce it without isabelle
Chengsong Tan (Sep 13 2024 at 13:48):Mathias Fleury said:
They issue might go down as far as it is a polyml bug (after unpealing the Isabelle_Threads layer and so on). In that case, it might be end up with a Polyml bug if you can reproduce it without isabelle
Have you ever encountered a polyml bug before?
Mathias Fleury (Sep 13 2024 at 13:49):I have not
Mathias Fleury (Sep 13 2024 at 13:49):but I have debugged weird Windows + Sledgehammer problems before
Mathias Fleury (Sep 13 2024 at 13:50):(where that file you have issues with was empty instead of containing the proof)
Chengsong Tan (Sep 13 2024 at 13:51):Mathias Fleury said:
(where that file you have issues with was empty instead of containing the proof)
What tends to be the cause of such problems?
Mathias Fleury (Sep 13 2024 at 13:52):In that case, there was a weird timing problems. In that case if you waited just a tiny bit longer the file had the content (like if the flush was too slow)
Mathias Fleury (Sep 13 2024 at 13:52):Usually the hard part is to identify what is the issue exactly
Mathias Fleury (Sep 13 2024 at 13:53):or at least finding a way to reproduce it consistently (or consistently enough)
irvin (Nov 04 2024 at 00:32):Mathias Fleury said:
It will not be as easy as a search and replace.
So:
- open isabelle with base theory Pure
- open the file Sledgehammer.thy
- Now try to find a lemma where you can trigger the issue. Maybe this does:
lemma "(∀(x::nat). P x)" sledgehammer[e,verbose]
- Then you will have to look at the file timeout.ML and see why the interrupt is not working properly
if your interested @Moritz R you could try to fix this.
irvin (Nov 04 2024 at 00:34):note that there appear to have some changes in sledgehammer so base your work on the latest branch.
Last updated: Dec 21 2024 at 12:33 UTC